Theorem: Ideal.quotDecomposition_left_inv' (DividedPowers/ForMathlib/GradedRingQuot.lean)

State before:
R : Type u_1
inst✝⁵ : CommRing R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
⊢ LeftInverse ⇑(coeLinearMap (quotSubmodule R 𝒜 I)) ⇑(quotDecompose R 𝒜 hI)
Tactic:
intro x
State after:
R : Type u_1
inst✝⁵ : CommRing R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
x : A ⧸ I
⊢ (coeLinearMap (quotSubmodule R 𝒜 I)) ((quotDecompose R 𝒜 hI) x) = x

State before:
R : Type u_1
inst✝⁵ : CommRing R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
x : A ⧸ I
⊢ (coeLinearMap (quotSubmodule R 𝒜 I)) ((quotDecompose R 𝒜 hI) x) = x
Tactic:
obtain ⟨(a : A), rfl⟩ := Ideal.Quotient.mk_surjective x
State after:
case intro
R : Type u_1
inst✝⁵ : CommRing R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
a : A
⊢ (coeLinearMap (quotSubmodule R 𝒜 I)) ((quotDecompose R 𝒜 hI) ((Quotient.mk I) a)) = (Quotient.mk I) a

State before:
case intro
R : Type u_1
inst✝⁵ : CommRing R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
a : A
⊢ (coeLinearMap (quotSubmodule R 𝒜 I)) ((quotDecompose R 𝒜 hI) ((Quotient.mk I) a)) = (Quotient.mk I) a
Tactic:
conv_lhs =>
  rw [quotDecomposeLaux_apply_mk, quotDecomposeLaux, LinearMap.comp_apply]
  simp only [AlgEquiv.toLinearMap_apply, ← LinearMap.comp_apply]
State after:
case intro
R : Type u_1
inst✝⁵ : CommRing R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
a : A
⊢ (coeLinearMap (quotSubmodule R 𝒜 I) ∘ₗ lmap' (quotCompMap R 𝒜 I)) ((decomposeAlgEquiv 𝒜) a) = (Quotient.mk I) a

State before:
case intro
R : Type u_1
inst✝⁵ : CommRing R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
a : A
⊢ (coeLinearMap (quotSubmodule R 𝒜 I) ∘ₗ lmap' (quotCompMap R 𝒜 I)) ((decomposeAlgEquiv 𝒜) a) = (Quotient.mk I) a
Tactic:
rw [Ideal.quotDecomposition_left_inv'_aux]
State after:
case intro
R : Type u_1
inst✝⁵ : CommRing R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
a : A
⊢ ((Submodule.restrictScalars R I).mkQ ∘ₗ coeLinearMap 𝒜) ((decomposeAlgEquiv 𝒜) a) = (Quotient.mk I) a

State before:
case intro
R : Type u_1
inst✝⁵ : CommRing R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
a : A
⊢ ((Submodule.restrictScalars R I).mkQ ∘ₗ coeLinearMap 𝒜) ((decomposeAlgEquiv 𝒜) a) = (Quotient.mk I) a
Tactic:
conv_rhs =>
  rw [← h𝒜.left_inv a]
  simp only [← LinearMap.comp_apply]
State after:
case intro
R : Type u_1
inst✝⁵ : CommRing R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
a : A
⊢ ((Submodule.restrictScalars R I).mkQ ∘ₗ coeLinearMap 𝒜) ((decomposeAlgEquiv 𝒜) a) =
    (Quotient.mk I) ((DirectSum.coeAddMonoidHom 𝒜) (Decomposition.decompose' a))

State before:
case intro
R : Type u_1
inst✝⁵ : CommRing R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommRing A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
I : Ideal A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
a : A
⊢ ((Submodule.restrictScalars R I).mkQ ∘ₗ coeLinearMap 𝒜) ((decomposeAlgEquiv 𝒜) a) =
    (Quotient.mk I) ((DirectSum.coeAddMonoidHom 𝒜) (Decomposition.decompose' a))
Tactic:
rfl
State after:
no goals