internlm/Lean-Github huggingface dataset:
Theorem: quotDecompose_injective'
Proof state before:
case intro.refl.intro.refl.h
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
hφ : ∀ (i : ι), Surjective ⇑(quotCompMap R 𝒜 rel i)
a b : ⨁ (i : ι), ↥(𝒜 i)
hxy :
  (RingQuot.mkAlgHom R rel) ((coeLinearMap fun i => 𝒜 i) a) = (RingQuot.mkAlgHom R rel) ((coeLinearMap fun i => 𝒜 i) b)
i : ι
hxy' :
  (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap fun i => 𝒜 i) a)) i) =
    (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap fun i => 𝒜 i) b)) i)
⊢ ((lmap' (quotCompMap R 𝒜 rel)) a) i = ((lmap' (quotCompMap R 𝒜 rel)) b) i
Tactic:
simp only [Decomposition.decompose'_eq] at hxy'
Proof state after:
case intro.refl.intro.refl.h
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
hφ : ∀ (i : ι), Surjective ⇑(quotCompMap R 𝒜 rel i)
a b : ⨁ (i : ι), ↥(𝒜 i)
hxy :
  (RingQuot.mkAlgHom R rel) ((coeLinearMap fun i => 𝒜 i) a) = (RingQuot.mkAlgHom R rel) ((coeLinearMap fun i => 𝒜 i) b)
i : ι
hxy' :
  (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap fun i => 𝒜 i) a)) i) =
    (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap fun i => 𝒜 i) b)) i)
⊢ ((lmap' (quotCompMap R 𝒜 rel)) a) i = ((lmap' (quotCompMap R 𝒜 rel)) b) i
Theorem: quotDecompose_injective'
Proof state before:
case intro.refl.intro.refl.h
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
hφ : ∀ (i : ι), Surjective ⇑(quotCompMap R 𝒜 rel i)
a b : ⨁ (i : ι), ↥(𝒜 i)
hxy :
  (RingQuot.mkAlgHom R rel) ((coeLinearMap fun i => 𝒜 i) a) = (RingQuot.mkAlgHom R rel) ((coeLinearMap fun i => 𝒜 i) b)
i : ι
hxy' :
  (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap fun i => 𝒜 i) a)) i) =
    (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap fun i => 𝒜 i) b)) i)
⊢ ((lmap' (quotCompMap R 𝒜 rel)) a) i = ((lmap' (quotCompMap R 𝒜 rel)) b) i
Tactic:
simpa only [lmap'_quotCompMap_apply, SetLike.coe_eq_coe] using hxy'
Proof state after:
no goals
Theorem: quotDecompose_injective'
Proof state before:
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
⊢ ∀ (i : ι), Surjective ⇑(quotCompMap R 𝒜 rel i)
Tactic:
rintro i ⟨x, ⟨a, ha, rfl⟩ ⟩
Proof state after:
case mk.intro.intro
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
i : ι
a : A
ha : a ∈ ↑(𝒜 i)
⊢ ∃ a_1, (quotCompMap R 𝒜 rel i) a_1 = ⟨(RingQuot.mkAlgHom R rel) a, ⋯⟩
Theorem: quotDecompose_injective'
Proof state before:
case mk.intro.intro
R : Type u_1
inst✝⁵ : CommSemiring R
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid ι
A : Type u_3
inst✝² : CommSemiring A
inst✝¹ : DecidableEq A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
rel : A → A → Prop
h𝒜 : GradedAlgebra 𝒜
hrel : Rel.IsHomogeneous 𝒜 rel
i : ι
a : A
ha : a ∈ ↑(𝒜 i)
⊢ ∃ a_1, (quotCompMap R 𝒜 rel i) a_1 = ⟨(RingQuot.mkAlgHom R rel) a, ⋯⟩
Tactic:
exact ⟨⟨a, ha⟩, rfl⟩
Proof state after:
no goals
Theorem: Ideal.quotDecomposeLaux_of_mem_eq_zero
Proof 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
x : A
hx : x ∈ I
i : ι
⊢ ((quotDecomposeLaux R 𝒜 I) x) i = 0
Tactic:
rw [Ideal.quotDecomposeLaux, LinearMap.comp_apply, lmap'_apply, quotCompMap]
Proof 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
x : A
hx : x ∈ I
i : ι
⊢ { toFun := fun u => ⟨(Quotient.mkₐ R I) ↑u, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }
      (((decomposeAlgEquiv 𝒜).toLinearMap x) i) =
    0
Theorem: Ideal.quotDecomposeLaux_of_mem_eq_zero
Proof 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
x : A
hx : x ∈ I
i : ι
⊢ { toFun := fun u => ⟨(Quotient.mkₐ R I) ↑u, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }
      (((decomposeAlgEquiv 𝒜).toLinearMap x) i) =
    0
Tactic:
simp only [Ideal.Quotient.mkₐ_eq_mk, AlgEquiv.toLinearMap_apply, decomposeAlgEquiv_apply,
  LinearMap.coe_mk, AddHom.coe_mk, Submodule.mk_eq_zero]
Proof 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
x : A
hx : x ∈ I
i : ι
⊢ (Quotient.mk I) ↑(((decompose 𝒜) x) i) = 0
Theorem: Ideal.quotDecomposeLaux_of_mem_eq_zero
Proof 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
x : A
hx : x ∈ I
i : ι
⊢ (Quotient.mk I) ↑(((decompose 𝒜) x) i) = 0
Tactic:
rw [Ideal.Quotient.eq_zero_iff_mem]
Proof 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
x : A
hx : x ∈ I
i : ι
⊢ ↑(((decompose 𝒜) x) i) ∈ I
Theorem: Ideal.quotDecomposeLaux_of_mem_eq_zero
Proof 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
x : A
hx : x ∈ I
i : ι
⊢ ↑(((decompose 𝒜) x) i) ∈ I
Tactic:
exact hI i hx
Proof state after:
no goals
Theorem: Ideal.quotDecomposition_left_inv'_aux
Proof 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 𝒜
⊢ coeLinearMap (quotSubmodule R 𝒜 I) ∘ₗ lmap' (quotCompMap R 𝒜 I) =
    (Submodule.restrictScalars R I).mkQ ∘ₗ coeLinearMap 𝒜
Tactic:
apply linearMap_ext
Proof 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 𝒜
⊢ ∀ (i : ι),
    (coeLinearMap (quotSubmodule R 𝒜 I) ∘ₗ lmap' (quotCompMap R 𝒜 I)) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i =
      ((Submodule.restrictScalars R I).mkQ ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i
Theorem: Ideal.quotDecomposition_left_inv'_aux
Proof 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 𝒜
⊢ ∀ (i : ι),
    (coeLinearMap (quotSubmodule R 𝒜 I) ∘ₗ lmap' (quotCompMap R 𝒜 I)) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i =
      ((Submodule.restrictScalars R I).mkQ ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i
Tactic:
intro i
Proof 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 𝒜
i : ι
⊢ (coeLinearMap (quotSubmodule R 𝒜 I) ∘ₗ lmap' (quotCompMap R 𝒜 I)) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i =
    ((Submodule.restrictScalars R I).mkQ ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i
Theorem: Ideal.quotDecomposition_left_inv'_aux
Proof 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 𝒜
i : ι
⊢ (coeLinearMap (quotSubmodule R 𝒜 I) ∘ₗ lmap' (quotCompMap R 𝒜 I)) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i =
    ((Submodule.restrictScalars R I).mkQ ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i
Tactic:
ext x
Proof 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 𝒜
i : ι
x : ↥(𝒜 i)
⊢ ((coeLinearMap (quotSubmodule R 𝒜 I) ∘ₗ lmap' (quotCompMap R 𝒜 I)) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i) x =
    (((Submodule.restrictScalars R I).mkQ ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i) x
Theorem: Ideal.quotDecomposition_left_inv'_aux
Proof 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 𝒜
i : ι
x : ↥(𝒜 i)
⊢ ((coeLinearMap (quotSubmodule R 𝒜 I) ∘ₗ lmap' (quotCompMap R 𝒜 I)) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i) x =
    (((Submodule.restrictScalars R I).mkQ ∘ₗ coeLinearMap 𝒜) ∘ₗ lof R ι (fun i => ↥(𝒜 i)) i) x
Tactic:
dsimp only [LinearMap.coe_comp, comp_apply]
Proof 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 𝒜
i : ι
x : ↥(𝒜 i)
⊢ (coeLinearMap (quotSubmodule R 𝒜 I)) ((lmap' (quotCompMap R 𝒜 I)) ((lof R ι (fun i => ↥(𝒜 i)) i) x)) =
    ((Submodule.restrictScalars R I).mkQ ∘ₗ coeLinearMap 𝒜) ((lof R ι (fun i => ↥(𝒜 i)) i) x)
Theorem: Ideal.quotDecomposition_left_inv'_aux
Proof 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 𝒜
i : ι
x : ↥(𝒜 i)
⊢ (coeLinearMap (quotSubmodule R 𝒜 I)) ((lmap' (quotCompMap R 𝒜 I)) ((lof R ι (fun i => ↥(𝒜 i)) i) x)) =
    ((Submodule.restrictScalars R I).mkQ ∘ₗ coeLinearMap 𝒜) ((lof R ι (fun i => ↥(𝒜 i)) i) x)
Tactic:
change _ = (Submodule.mkQ (Submodule.restrictScalars R I)) (_)
Proof 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 𝒜
i : ι
x : ↥(𝒜 i)
⊢ (coeLinearMap (quotSubmodule R 𝒜 I)) ((lmap' (quotCompMap R 𝒜 I)) ((lof R ι (fun i => ↥(𝒜 i)) i) x)) =
    (Submodule.restrictScalars R I).mkQ ((coeLinearMap 𝒜) ((lof R ι (fun i => ↥(𝒜 i)) i) x))
Theorem: Ideal.quotDecomposition_left_inv'_aux
Proof 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 𝒜
i : ι
x : ↥(𝒜 i)
⊢ (coeLinearMap (quotSubmodule R 𝒜 I)) ((lmap' (quotCompMap R 𝒜 I)) ((lof R ι (fun i => ↥(𝒜 i)) i) x)) =
    (Submodule.restrictScalars R I).mkQ ((coeLinearMap 𝒜) ((lof R ι (fun i => ↥(𝒜 i)) i) x))
Tactic:
rw [lmap'_lof]
Proof 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 𝒜
i : ι
x : ↥(𝒜 i)
⊢ (coeLinearMap (quotSubmodule R 𝒜 I)) ((lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i) ((quotCompMap R 𝒜 I i) x)) =
    (Submodule.restrictScalars R I).mkQ ((coeLinearMap 𝒜) ((lof R ι (fun i => ↥(𝒜 i)) i) x))
Theorem: Ideal.quotDecomposition_left_inv'_aux
Proof 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 𝒜
i : ι
x : ↥(𝒜 i)
⊢ (coeLinearMap (quotSubmodule R 𝒜 I)) ((lof R ι (fun i => ↥(quotSubmodule R 𝒜 I i)) i) ((quotCompMap R 𝒜 I i) x)) =
    (Submodule.restrictScalars R I).mkQ ((coeLinearMap 𝒜) ((lof R ι (fun i => ↥(𝒜 i)) i) x))
Tactic:
simp only [lof_eq_of, coeLinearMap_of, Submodule.mkQ_apply]
Proof 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 𝒜
i : ι
x : ↥(𝒜 i)
⊢ ↑((quotCompMap R 𝒜 I i) x) = Submodule.Quotient.mk ↑x
Theorem: Ideal.quotDecomposition_left_inv'_aux
Proof 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 𝒜
i : ι
x : ↥(𝒜 i)
⊢ ↑((quotCompMap R 𝒜 I i) x) = Submodule.Quotient.mk ↑x
Tactic:
rfl
Proof state after:
no goals
Theorem: Ideal.quotDecomposition_left_inv'
Proof 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
Proof 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
Theorem: Ideal.quotDecomposition_left_inv'
Proof 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
Proof 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
Theorem: Ideal.quotDecomposition_left_inv'
Proof 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]
Proof 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
Theorem: Ideal.quotDecomposition_left_inv'
Proof 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]
Proof 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
Theorem: Ideal.quotDecomposition_left_inv'
Proof 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]
Proof 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))
Theorem: Ideal.quotDecomposition_left_inv'
Proof 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
Proof state after:
no goals
Theorem: Ideal.quotDecomposition_right_inv'
Proof 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]
Proof 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
Theorem: Ideal.quotDecomposition_right_inv'
Proof 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
Proof 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
Theorem: Ideal.quotDecomposition_right_inv'
Proof 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
Proof 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
Theorem: Ideal.quotDecomposition_right_inv'
Proof 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
Proof 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