Theorem: Ideal.quotDecomposition_right_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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
⊢ Function.RightInverse ⇑(coeLinearMap (quotSubmodule R 𝒜 I)) ⇑(quotDecompose R 𝒜 hI)
Tactic:
rw [rightInverse_iff_comp, ← LinearMap.coe_comp, ← @LinearMap.id_coe R]
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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
⊢ ⇑(quotDecompose R 𝒜 hI ∘ₗ coeLinearMap (quotSubmodule R 𝒜 I)) = ⇑LinearMap.id

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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
⊢ ⇑(quotDecompose R 𝒜 hI ∘ₗ coeLinearMap (quotSubmodule R 𝒜 I)) = ⇑LinearMap.id
Tactic:
apply congr_arg
State after:
case h
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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
⊢ quotDecompose R 𝒜 hI ∘ₗ coeLinearMap (quotSubmodule R 𝒜 I) = LinearMap.id

State before:
case h
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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
⊢ quotDecompose R 𝒜 hI ∘ₗ coeLinearMap (quotSubmodule R 𝒜 I) = LinearMap.id
Tactic:
apply linearMap_ext
State after:
case h.H
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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
⊢ ∀ (i : ι),
    (quotDecompose R 𝒜 hI ∘ₗ coeLinearMap (quotSubmodule R 𝒜 I)) ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i =
      LinearMap.id ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i

State before:
case h.H
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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
⊢ ∀ (i : ι),
    (quotDecompose R 𝒜 hI ∘ₗ coeLinearMap (quotSubmodule R 𝒜 I)) ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i =
      LinearMap.id ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i
Tactic:
intro i
State after:
case h.H
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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
⊢ (quotDecompose R 𝒜 hI ∘ₗ coeLinearMap (quotSubmodule R 𝒜 I)) ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i =
    LinearMap.id ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i

State before:
case h.H
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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
⊢ (quotDecompose R 𝒜 hI ∘ₗ coeLinearMap (quotSubmodule R 𝒜 I)) ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i =
    LinearMap.id ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i
Tactic:
ext y
State after:
case h.H.h
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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
⊢ ((quotDecompose R 𝒜 hI ∘ₗ coeLinearMap (quotSubmodule R 𝒜 I)) ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y =
    (LinearMap.id ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y

State before:
case h.H.h
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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
⊢ ((quotDecompose R 𝒜 hI ∘ₗ coeLinearMap (quotSubmodule R 𝒜 I)) ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y =
    (LinearMap.id ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y
Tactic:
obtain ⟨x, hx, hxy⟩ := y.prop
State after:
case h.H.h.intro.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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ ((quotDecompose R 𝒜 hI ∘ₗ coeLinearMap (quotSubmodule R 𝒜 I)) ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y =
    (LinearMap.id ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y

State before:
case h.H.h.intro.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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ ((quotDecompose R 𝒜 hI ∘ₗ coeLinearMap (quotSubmodule R 𝒜 I)) ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y =
    (LinearMap.id ∘ₗ lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y
Tactic:
simp only [LinearMap.coe_comp, comp_apply, LinearMap.id_comp, lof_eq_of, coeLinearMap_of]
State after:
case h.H.h.intro.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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ (quotDecompose R 𝒜 hI) ↑y = (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y

State before:
case h.H.h.intro.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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ (quotDecompose R 𝒜 hI) ↑y = (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y
Tactic:
rw [← hxy, Ideal.Quotient.mkₐ_eq_mk, Ideal.quotDecomposeLaux_apply_mk, Ideal.quotDecomposeLaux]
State after:
case h.H.h.intro.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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ (lmap' (quotCompMap R 𝒜 I) ∘ₗ (decomposeAlgEquiv 𝒜).toLinearMap) x = (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y

State before:
case h.H.h.intro.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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ (lmap' (quotCompMap R 𝒜 I) ∘ₗ (decomposeAlgEquiv 𝒜).toLinearMap) x = (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y
Tactic:
simp only [LinearMap.coe_comp, comp_apply]
State after:
case h.H.h.intro.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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ (lmap' (quotCompMap R 𝒜 I)) ((decomposeAlgEquiv 𝒜).toLinearMap x) = (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y

State before:
case h.H.h.intro.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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ (lmap' (quotCompMap R 𝒜 I)) ((decomposeAlgEquiv 𝒜).toLinearMap x) = (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y
Tactic:
change lmap' _ (decompose 𝒜 x) = _
State after:
case h.H.h.intro.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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ (lmap' (quotCompMap R 𝒜 I)) ((decompose 𝒜) x) = (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y

State before:
case h.H.h.intro.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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ (lmap' (quotCompMap R 𝒜 I)) ((decompose 𝒜) x) = (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y
Tactic:
suffices decompose 𝒜 x = lof R ι (fun i => 𝒜 i) i (⟨x, hx⟩ : 𝒜 i) by
  rw [this, lmap'_lof, lof_eq_of]
  apply congr_arg₂ _ rfl
  rw [quotCompMap]
  simp only [Ideal.Quotient.mkₐ_eq_mk, Submodule.coe_mk, LinearMap.coe_mk]
  rw [← Subtype.coe_inj, Subtype.coe_mk, ← hxy]
  simp only [Ideal.Quotient.mkₐ_eq_mk]
  rfl
State after:
case h.H.h.intro.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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩

State before:
case h.H.h.intro.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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
Tactic:
conv_lhs => rw [← Subtype.coe_mk x hx]
State after:
case h.H.h.intro.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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ (decompose 𝒜) ↑⟨x, hx⟩ = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩

State before:
case h.H.h.intro.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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
⊢ (decompose 𝒜) ↑⟨x, hx⟩ = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
Tactic:
rw [decompose_coe, lof_eq_of]
State after:
no goals

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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ (lmap' (quotCompMap R 𝒜 I)) ((decompose 𝒜) x) = (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y
Tactic:
rw [this, lmap'_lof, lof_eq_of]
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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) ((quotCompMap R 𝒜 I i) ⟨x, hx⟩) =
    (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y

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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) ((quotCompMap R 𝒜 I i) ⟨x, hx⟩) =
    (of (fun i => ↥(quotSubmodule R 𝒜 I i)) i) y
Tactic:
apply congr_arg₂ _ rfl
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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ (quotCompMap R 𝒜 I i) ⟨x, hx⟩ = y

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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ (quotCompMap R 𝒜 I i) ⟨x, hx⟩ = y
Tactic:
rw [quotCompMap]
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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ { toFun := fun u => ⟨(Quotient.mkₐ R I) ↑u, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } ⟨x, hx⟩ = y

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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ { toFun := fun u => ⟨(Quotient.mkₐ R I) ↑u, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } ⟨x, hx⟩ = y
Tactic:
simp only [Ideal.Quotient.mkₐ_eq_mk, Submodule.coe_mk, LinearMap.coe_mk]
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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ { toFun := fun u => ⟨(Quotient.mk I) ↑u, ⋯⟩, map_add' := ⋯ } ⟨x, hx⟩ = y

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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ { toFun := fun u => ⟨(Quotient.mk I) ↑u, ⋯⟩, map_add' := ⋯ } ⟨x, hx⟩ = y
Tactic:
rw [← Subtype.coe_inj, Subtype.coe_mk, ← hxy]
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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ ↑({ toFun := fun u => ⟨(Quotient.mk I) ↑u, ⋯⟩, map_add' := ⋯ } ⟨x, hx⟩) = (Quotient.mkₐ R I) 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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ ↑({ toFun := fun u => ⟨(Quotient.mk I) ↑u, ⋯⟩, map_add' := ⋯ } ⟨x, hx⟩) = (Quotient.mkₐ R I) x
Tactic:
simp only [Ideal.Quotient.mkₐ_eq_mk]
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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ ↑({ toFun := fun u => ⟨(Quotient.mk I) ↑u, ⋯⟩, map_add' := ⋯ } ⟨x, hx⟩) = (Quotient.mk I) 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
inst✝ : GradedAlgebra 𝒜
hI : IsHomogeneous 𝒜 I
i : ι
y : ↥(quotSubmodule R 𝒜 I i)
x : A
hx : x ∈ ↑(𝒜 i)
hxy : (Quotient.mkₐ R I) x = ↑y
this : (decompose 𝒜) x = (lof R ι (fun i => ↥(𝒜 i)) i) ⟨x, hx⟩
⊢ ↑({ toFun := fun u => ⟨(Quotient.mk I) ↑u, ⋯⟩, map_add' := ⋯ } ⟨x, hx⟩) = (Quotient.mk I) x
Tactic:
rfl
State after:
no goals