Theorem: LinearMap.ker_lTensor_of_linearProjOfIsCompl (DividedPowers/ForMathlib/RingTheory/AugmentationIdeal.lean)

State before:
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
⊢ ker (lTensor Q (M₁.linearProjOfIsCompl M₂ hM)) = range (lTensor Q M₂.subtype)
Tactic:
rw [← exact_iff]
State after:
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
⊢ Function.Exact ⇑(lTensor Q M₂.subtype) ⇑(lTensor Q (M₁.linearProjOfIsCompl M₂ hM))

State before:
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
⊢ Function.Exact ⇑(lTensor Q M₂.subtype) ⇑(lTensor Q (M₁.linearProjOfIsCompl M₂ hM))
Tactic:
apply lTensor_exact
State after:
case hfg
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
⊢ Function.Exact ⇑M₂.subtype ⇑(M₁.linearProjOfIsCompl M₂ hM)

case hg
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
⊢ Function.Surjective ⇑(M₁.linearProjOfIsCompl M₂ hM)

State before:
case hfg
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
⊢ Function.Exact ⇑M₂.subtype ⇑(M₁.linearProjOfIsCompl M₂ hM)

case hg
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
⊢ Function.Surjective ⇑(M₁.linearProjOfIsCompl M₂ hM)
Tactic:
simp only [exact_iff, range_subtype, linearProjOfIsCompl_ker]
State after:
case hg
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
⊢ Function.Surjective ⇑(M₁.linearProjOfIsCompl M₂ hM)

State before:
case hg
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
J : Ideal A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module A M
M₁ M₂ : Submodule A M
hM : IsCompl M₁ M₂
Q : Type u_4
inst✝¹ : AddCommGroup Q
inst✝ : Module A Q
⊢ Function.Surjective ⇑(M₁.linearProjOfIsCompl M₂ hM)
Tactic:
simp only [← range_eq_top, linearProjOfIsCompl_range]
State after:
no goals