R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ↑f
φ : (P →₀ R) →ₗ[R] M := Finsupp.total P M R fun p => Function.surjInv hf (↑g p)
⊢ ∃ h, comp f h = g
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ↑f
⊢ ∃ h, comp f h = g
let φ : (P →₀ R) →ₗ[R] M := Finsupp.total _ _ _ fun p => Function.surjInv hf (g p)
case intro
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ↑f
φ : (P →₀ R) →ₗ[R] M := Finsupp.total P M R fun p => Function.surjInv hf (↑g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ↑(Finsupp.total P P R id) ↑s
⊢ ∃ h, comp f h = g
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ↑f
φ : (P →₀ R) →ₗ[R] M := Finsupp.total P M R fun p => Function.surjInv hf (↑g p)
⊢ ∃ h, comp f h = g
cases' h.out with s hs
case intro
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ↑f
φ : (P →₀ R) →ₗ[R] M := Finsupp.total P M R fun p => Function.surjInv hf (↑g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ↑(Finsupp.total P P R id) ↑s
⊢ comp f (comp φ s) = g
case intro
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ↑f
φ : (P →₀ R) →ₗ[R] M := Finsupp.total P M R fun p => Function.surjInv hf (↑g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ↑(Finsupp.total P P R id) ↑s
⊢ ∃ h, comp f h = g
use φ.comp s
case intro.h
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ↑f
φ : (P →₀ R) →ₗ[R] M := Finsupp.total P M R fun p => Function.surjInv hf (↑g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ↑(Finsupp.total P P R id) ↑s
p : P
⊢ ↑(comp f (comp φ s)) p = ↑g p
case intro
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ↑f
φ : (P →₀ R) →ₗ[R] M := Finsupp.total P M R fun p => Function.surjInv hf (↑g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ↑(Finsupp.total P P R id) ↑s
⊢ comp f (comp φ s) = g
ext p
case intro.h
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ↑f
φ : (P →₀ R) →ₗ[R] M := Finsupp.total P M R fun p => Function.surjInv hf (↑g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ↑(Finsupp.total P P R id) ↑s
p : P
⊢ ↑(comp f (comp φ s)) p = ↑g (↑(Finsupp.total P P R id) (↑s p))
case intro.h
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ↑f
φ : (P →₀ R) →ₗ[R] M := Finsupp.total P M R fun p => Function.surjInv hf (↑g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ↑(Finsupp.total P P R id) ↑s
p : P
⊢ ↑(comp f (comp φ s)) p = ↑g p
conv_rhs => rw [← hs p]
no goals
case intro.h
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ↑f
φ : (P →₀ R) →ₗ[R] M := Finsupp.total P M R fun p => Function.surjInv hf (↑g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ↑(Finsupp.total P P R id) ↑s
p : P
⊢ ↑(comp f (comp φ s)) p = ↑g (↑(Finsupp.total P P R id) (↑s p))
simp [Finsupp.total_apply, Function.surjInv_eq hf]