Theorem: DividedPowerAlgebra.deg_one_right_inv (DividedPowers/DPAlgebra/Graded/GradeOne.lean)

State before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ Function.RightInverse (⇑(sndHom R M) ∘ ⇑(toTrivSqZeroExt R M).toLinearMap ∘ ⇑(grade R M 1).subtype)
    (⇑(proj' R M 1) ∘ ⇑(ι R M))
Tactic:
simp only [Function.rightInverse_iff_comp, ← LinearMap.coe_comp, ← @LinearMap.id_coe R]
State after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ ⇑((proj' R M 1 ∘ₗ ι R M) ∘ₗ sndHom R M ∘ₗ (toTrivSqZeroExt R M).toLinearMap ∘ₗ (grade R M 1).subtype) = ⇑LinearMap.id

State before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ ⇑((proj' R M 1 ∘ₗ ι R M) ∘ₗ sndHom R M ∘ₗ (toTrivSqZeroExt R M).toLinearMap ∘ₗ (grade R M 1).subtype) = ⇑LinearMap.id
Tactic:
rw [DFunLike.coe_injective.eq_iff]
State after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ (proj' R M 1 ∘ₗ ι R M) ∘ₗ sndHom R M ∘ₗ (toTrivSqZeroExt R M).toLinearMap ∘ₗ (grade R M 1).subtype = LinearMap.id

State before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ (proj' R M 1 ∘ₗ ι R M) ∘ₗ sndHom R M ∘ₗ (toTrivSqZeroExt R M).toLinearMap ∘ₗ (grade R M 1).subtype = LinearMap.id
Tactic:
apply LinearMap.ext_on_range (grade_one_eq_span' R M).symm
State after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ ∀ (i : M),
    ((proj' R M 1 ∘ₗ ι R M) ∘ₗ sndHom R M ∘ₗ (toTrivSqZeroExt R M).toLinearMap ∘ₗ (grade R M 1).subtype) ⟨dp R 1 i, ⋯⟩ =
      LinearMap.id ⟨dp R 1 i, ⋯⟩

State before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ ∀ (i : M),
    ((proj' R M 1 ∘ₗ ι R M) ∘ₗ sndHom R M ∘ₗ (toTrivSqZeroExt R M).toLinearMap ∘ₗ (grade R M 1).subtype) ⟨dp R 1 i, ⋯⟩ =
      LinearMap.id ⟨dp R 1 i, ⋯⟩
Tactic:
intro m
State after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ ((proj' R M 1 ∘ₗ ι R M) ∘ₗ sndHom R M ∘ₗ (toTrivSqZeroExt R M).toLinearMap ∘ₗ (grade R M 1).subtype) ⟨dp R 1 m, ⋯⟩ =
    LinearMap.id ⟨dp R 1 m, ⋯⟩

State before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ ((proj' R M 1 ∘ₗ ι R M) ∘ₗ sndHom R M ∘ₗ (toTrivSqZeroExt R M).toLinearMap ∘ₗ (grade R M 1).subtype) ⟨dp R 1 m, ⋯⟩ =
    LinearMap.id ⟨dp R 1 m, ⋯⟩
Tactic:
simp only [proj', proj, ι, LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk,
  Submodule.coeSubtype, comp_apply, AlgHom.toLinearMap_apply, sndHom_apply,
  LinearMap.id_coe, id_eq]
State after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ ((DirectSum.decompose (grade R M)) (dp R 1 ((toTrivSqZeroExt R M) (dp R 1 m)).snd)) 1 = ⟨dp R 1 m, ⋯⟩

State before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ ((DirectSum.decompose (grade R M)) (dp R 1 ((toTrivSqZeroExt R M) (dp R 1 m)).snd)) 1 = ⟨dp R 1 m, ⋯⟩
Tactic:
ext
State after:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ ↑(((DirectSum.decompose (grade R M)) (dp R 1 ((toTrivSqZeroExt R M) (dp R 1 m)).snd)) 1) = ↑⟨dp R 1 m, ⋯⟩

State before:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ ↑(((DirectSum.decompose (grade R M)) (dp R 1 ((toTrivSqZeroExt R M) (dp R 1 m)).snd)) 1) = ↑⟨dp R 1 m, ⋯⟩
Tactic:
dsimp only
State after:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ ↑(((DirectSum.decompose (grade R M)) (dp R 1 ((toTrivSqZeroExt R M) (dp R 1 m)).snd)) 1) = dp R 1 m

State before:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ ↑(((DirectSum.decompose (grade R M)) (dp R 1 ((toTrivSqZeroExt R M) (dp R 1 m)).snd)) 1) = dp R 1 m
Tactic:
rw [← ι_def R M m, toTrivSqZeroExt_ι, ← ι_def, snd_inr, decompose_of_mem_same]
State after:
case a.hx
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ (ι R M) m ∈ grade R M 1

State before:
case a.hx
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ (ι R M) m ∈ grade R M 1
Tactic:
apply ι_mem_grade_one
State after:
no goals