[GOAL]
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
⊢ Module.Projective R P ↔ Projective (of R P)
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Module.Projective R P
⊢ Projective (of R P)
[PROOFSTEP]
letI : Module.Projective R (ModuleCat.of R P) := h
[GOAL]
case refine'_1
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Module.Projective R P
this : Module.Projective R ↑(of R P) := h
⊢ Projective (of R P)
[PROOFSTEP]
exact ⟨fun E X epi => Module.projective_lifting_property _ _ ((ModuleCat.epi_iff_surjective _).mp epi)⟩
[GOAL]
case refine'_2
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Projective (of R P)
⊢ Module.Projective R P
[PROOFSTEP]
refine' Module.Projective.of_lifting_property.{u, v} _
[GOAL]
case refine'_2
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Projective (of R P)
⊢ ∀ {M : Type (max v u)} {N : Type (max u v)} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : Module R M]
    [inst_3 : Module R N] (f : M →ₗ[R] N) (g : P →ₗ[R] N), Function.Surjective ↑f → ∃ h, comp f h = g
[PROOFSTEP]
intro E X mE mX sE sX f g s
[GOAL]
case refine'_2
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Projective (of R P)
E : Type (max v u)
X : Type (max u v)
mE : AddCommGroup E
mX : AddCommGroup X
sE : Module R E
sX : Module R X
f : E →ₗ[R] X
g : P →ₗ[R] X
s : Function.Surjective ↑f
⊢ ∃ h, comp f h = g
[PROOFSTEP]
haveI : Epi (↟f) := (ModuleCat.epi_iff_surjective (↟f)).mpr s
[GOAL]
case refine'_2
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Projective (of R P)
E : Type (max v u)
X : Type (max u v)
mE : AddCommGroup E
mX : AddCommGroup X
sE : Module R E
sX : Module R X
f : E →ₗ[R] X
g : P →ₗ[R] X
s : Function.Surjective ↑f
this : Epi (↟f)
⊢ ∃ h, comp f h = g
[PROOFSTEP]
letI : Projective (ModuleCat.of R P) := h
[GOAL]
case refine'_2
R : Type u
inst✝² : Ring R
P : Type (max u v)
inst✝¹ : AddCommGroup P
inst✝ : Module R P
h : Projective (of R P)
E : Type (max v u)
X : Type (max u v)
mE : AddCommGroup E
mX : AddCommGroup X
sE : Module R E
sX : Module R X
f : E →ₗ[R] X
g : P →ₗ[R] X
s : Function.Surjective ↑f
this✝ : Epi (↟f)
this : Projective (of R P) := h
⊢ ∃ h, comp f h = g
[PROOFSTEP]
exact ⟨Projective.factorThru (↟g) (↟f), Projective.factorThru_comp (↟g) (↟f)⟩
[GOAL]
R : Type u
inst✝ : Ring R
M✝ M : ModuleCat R
m : ↑M
⊢ ↑(↑(Basis.constr Finsupp.basisSingleOne ℕ) _root_.id) (Finsupp.single m 1) = m
[PROOFSTEP]
dsimp [Basis.constr]
[GOAL]
R : Type u
inst✝ : Ring R
M✝ M : ModuleCat R
m : ↑M
⊢ ↑(comp (Finsupp.total (↑M) (↑M) R _root_.id) (comp (Finsupp.lmapDomain R R _root_.id) LinearMap.id))
      (Finsupp.single m 1) =
    m
[PROOFSTEP]
simp only [Finsupp.lmapDomain_id, comp_id]
[GOAL]
R : Type u
inst✝ : Ring R
M✝ M : ModuleCat R
m : ↑M
⊢ ↑(Finsupp.total (↑M) (↑M) R _root_.id) (Finsupp.single m 1) = m
[PROOFSTEP]
rw [Finsupp.total_single, one_smul]
[GOAL]
R : Type u
inst✝ : Ring R
M✝ M : ModuleCat R
m : ↑M
⊢ _root_.id m = m
[PROOFSTEP]
rfl
