[GOAL]
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
⊢ Projective R P ↔ ∃ s, comp (Finsupp.total P P R id) s = LinearMap.id
[PROOFSTEP]
simp_rw [projective_def, FunLike.ext_iff, Function.LeftInverse, comp_apply, id_apply]
[GOAL]
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
[PROOFSTEP]
let φ : (P →₀ R) →ₗ[R] M :=
  Finsupp.total _ _ _ fun p =>
    Function.surjInv hf
      (g p)
        -- By projectivity we have a map `P →ₗ (P →₀ R)`;
[GOAL]
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
[PROOFSTEP]
cases' h.out with s hs
[GOAL]
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
[PROOFSTEP]
use φ.comp s
[GOAL]
case 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
⊢ comp f (comp φ s) = g
[PROOFSTEP]
ext p
[GOAL]
case h.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
[PROOFSTEP]
conv_rhs => rw [← hs p]
[GOAL]
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
| ↑g p
[PROOFSTEP]
rw [← hs p]
[GOAL]
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
| ↑g p
[PROOFSTEP]
rw [← hs p]
[GOAL]
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
| ↑g p
[PROOFSTEP]
rw [← hs p]
[GOAL]
case h.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))
[PROOFSTEP]
simp [Finsupp.total_apply, Function.surjInv_eq hf]
[GOAL]
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
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Projective R P
inst✝ : Projective R Q
⊢ Projective R (P × Q)
[PROOFSTEP]
refine .of_lifting_property'' fun f hf ↦ ?_
[GOAL]
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
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Projective R P
inst✝ : Projective R Q
f : (P × Q →₀ R) →ₗ[R] P × Q
hf : Function.Surjective ↑f
⊢ ∃ h, comp f h = LinearMap.id
[PROOFSTEP]
rcases projective_lifting_property f (.inl _ _ _) hf with ⟨g₁, hg₁⟩
[GOAL]
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
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Projective R P
inst✝ : Projective R Q
f : (P × Q →₀ R) →ₗ[R] P × Q
hf : Function.Surjective ↑f
g₁ : P →ₗ[R] P × Q →₀ R
hg₁ : comp f g₁ = inl R P Q
⊢ ∃ h, comp f h = LinearMap.id
[PROOFSTEP]
rcases projective_lifting_property f (.inr _ _ _) hf with ⟨g₂, hg₂⟩
[GOAL]
case intro.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
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Projective R P
inst✝ : Projective R Q
f : (P × Q →₀ R) →ₗ[R] P × Q
hf : Function.Surjective ↑f
g₁ : P →ₗ[R] P × Q →₀ R
hg₁ : comp f g₁ = inl R P Q
g₂ : Q →ₗ[R] P × Q →₀ R
hg₂ : comp f g₂ = inr R P Q
⊢ ∃ h, comp f h = LinearMap.id
[PROOFSTEP]
refine ⟨coprod g₁ g₂, ?_⟩
[GOAL]
case intro.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
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Projective R P
inst✝ : Projective R Q
f : (P × Q →₀ R) →ₗ[R] P × Q
hf : Function.Surjective ↑f
g₁ : P →ₗ[R] P × Q →₀ R
hg₁ : comp f g₁ = inl R P Q
g₂ : Q →ₗ[R] P × Q →₀ R
hg₂ : comp f g₂ = inr R P Q
⊢ comp f (coprod g₁ g₂) = LinearMap.id
[PROOFSTEP]
rw [LinearMap.comp_coprod, hg₁, hg₂, LinearMap.coprod_inl_inr]
[GOAL]
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
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
ι : Type u_6
A : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : (i : ι) → Module R (A i)
h : ∀ (i : ι), Projective R (A i)
f : ((Π₀ (i : ι), A i) →₀ R) →ₗ[R] Π₀ (i : ι), A i
hf : Function.Surjective ↑f
⊢ ∃ h, comp f h = LinearMap.id
[PROOFSTEP]
classical
choose g hg using fun i ↦ projective_lifting_property f (DFinsupp.lsingle i) hf
replace hg : ∀ i x, f (g i x) = DFinsupp.single i x := fun i ↦ FunLike.congr_fun (hg i)
refine ⟨DFinsupp.coprodMap g, ?_⟩
ext i x j
simp only [comp_apply, id_apply, DFinsupp.lsingle_apply, DFinsupp.coprodMap_apply_single, hg]
[GOAL]
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
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
ι : Type u_6
A : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : (i : ι) → Module R (A i)
h : ∀ (i : ι), Projective R (A i)
f : ((Π₀ (i : ι), A i) →₀ R) →ₗ[R] Π₀ (i : ι), A i
hf : Function.Surjective ↑f
⊢ ∃ h, comp f h = LinearMap.id
[PROOFSTEP]
choose g hg using fun i ↦ projective_lifting_property f (DFinsupp.lsingle i) hf
[GOAL]
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
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
ι : Type u_6
A : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : (i : ι) → Module R (A i)
h : ∀ (i : ι), Projective R (A i)
f : ((Π₀ (i : ι), A i) →₀ R) →ₗ[R] Π₀ (i : ι), A i
hf : Function.Surjective ↑f
g : (i : ι) → A i →ₗ[R] (Π₀ (i : ι), A i) →₀ R
hg : ∀ (i : ι), comp f (g i) = DFinsupp.lsingle i
⊢ ∃ h, comp f h = LinearMap.id
[PROOFSTEP]
replace hg : ∀ i x, f (g i x) = DFinsupp.single i x := fun i ↦ FunLike.congr_fun (hg i)
[GOAL]
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
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
ι : Type u_6
A : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : (i : ι) → Module R (A i)
h : ∀ (i : ι), Projective R (A i)
f : ((Π₀ (i : ι), A i) →₀ R) →ₗ[R] Π₀ (i : ι), A i
hf : Function.Surjective ↑f
g : (i : ι) → A i →ₗ[R] (Π₀ (i : ι), A i) →₀ R
hg : ∀ (i : ι) (x : A i), ↑f (↑(g i) x) = DFinsupp.single i x
⊢ ∃ h, comp f h = LinearMap.id
[PROOFSTEP]
refine ⟨DFinsupp.coprodMap g, ?_⟩
[GOAL]
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
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
ι : Type u_6
A : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : (i : ι) → Module R (A i)
h : ∀ (i : ι), Projective R (A i)
f : ((Π₀ (i : ι), A i) →₀ R) →ₗ[R] Π₀ (i : ι), A i
hf : Function.Surjective ↑f
g : (i : ι) → A i →ₗ[R] (Π₀ (i : ι), A i) →₀ R
hg : ∀ (i : ι) (x : A i), ↑f (↑(g i) x) = DFinsupp.single i x
⊢ comp f (DFinsupp.coprodMap g) = LinearMap.id
[PROOFSTEP]
ext i x j
[GOAL]
case h.h.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
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
ι : Type u_6
A : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : (i : ι) → Module R (A i)
h : ∀ (i : ι), Projective R (A i)
f : ((Π₀ (i : ι), A i) →₀ R) →ₗ[R] Π₀ (i : ι), A i
hf : Function.Surjective ↑f
g : (i : ι) → A i →ₗ[R] (Π₀ (i : ι), A i) →₀ R
hg : ∀ (i : ι) (x : A i), ↑f (↑(g i) x) = DFinsupp.single i x
i : ι
x : A i
j : ι
⊢ ↑(↑(comp (comp f (DFinsupp.coprodMap g)) (DFinsupp.lsingle i)) x) j = ↑(↑(comp LinearMap.id (DFinsupp.lsingle i)) x) j
[PROOFSTEP]
simp only [comp_apply, id_apply, DFinsupp.lsingle_apply, DFinsupp.coprodMap_apply_single, hg]
[GOAL]
R : Type u_1
inst✝² : Ring R
P : Type u_2
inst✝¹ : AddCommGroup P
inst✝ : Module R P
ι : Type u_3
b : Basis ι R P
⊢ Projective R P
[PROOFSTEP]
use b.constr ℕ fun i => Finsupp.single (b i) (1 : R)
[GOAL]
case h
R : Type u_1
inst✝² : Ring R
P : Type u_2
inst✝¹ : AddCommGroup P
inst✝ : Module R P
ι : Type u_3
b : Basis ι R P
⊢ Function.LeftInverse ↑(Finsupp.total P P R id) ↑(↑(Basis.constr b ℕ) fun i => Finsupp.single (↑b i) 1)
[PROOFSTEP]
intro m
[GOAL]
case h
R : Type u_1
inst✝² : Ring R
P : Type u_2
inst✝¹ : AddCommGroup P
inst✝ : Module R P
ι : Type u_3
b : Basis ι R P
m : P
⊢ ↑(Finsupp.total P P R id) (↑(↑(Basis.constr b ℕ) fun i => Finsupp.single (↑b i) 1) m) = m
[PROOFSTEP]
simp only [b.constr_apply, mul_one, id.def, Finsupp.smul_single', Finsupp.total_single, LinearMap.map_finsupp_sum]
[GOAL]
case h
R : Type u_1
inst✝² : Ring R
P : Type u_2
inst✝¹ : AddCommGroup P
inst✝ : Module R P
ι : Type u_3
b : Basis ι R P
m : P
⊢ (sum (↑b.repr m) fun i d => d • ↑b i) = m
[PROOFSTEP]
exact b.total_repr m
