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
a b : ⨁ (i : ι), ↥(𝒜 i)
hxy : (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) b)
i : ι
hxy' :
  (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap 𝒜) a)) i) =
    (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap 𝒜) 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
a b : ⨁ (i : ι), ↥(𝒜 i)
hxy : (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) b)
i : ι
hxy' :
  (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap 𝒜) a)) i) =
    (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap 𝒜) 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
a b : ⨁ (i : ι), ↥(𝒜 i)
hxy : (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) b)
i : ι
hxy' :
  (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap 𝒜) a)) i) =
    (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap 𝒜) b)) i)
⊢ ((lmap' (quotCompMap R 𝒜 rel)) a) i = ((lmap' (quotCompMap R 𝒜 rel)) b) i
Tactic:
suffices ∀ a, RingQuot.mkAlgHom R rel ↑(((decompose fun i => 𝒜 i)
    ((coeLinearMap fun i => 𝒜 i) a)) i) = ((lmap' (quotCompMap R 𝒜 rel)) a) i by
  simpa only [this, SetLike.coe_eq_coe] using 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
a b : ⨁ (i : ι), ↥(𝒜 i)
hxy : (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) b)
i : ι
hxy' :
  (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap 𝒜) a)) i) =
    (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap 𝒜) b)) i)
⊢ ∀ (a : ⨁ (i : ι), ↥(𝒜 i)),
    (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap fun i => 𝒜 i) a)) i) =
      ↑(((lmap' (quotCompMap R 𝒜 rel)) a) 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
a b : ⨁ (i : ι), ↥(𝒜 i)
hxy : (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) b)
i : ι
hxy' :
  (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap 𝒜) a)) i) =
    (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap 𝒜) b)) i)
⊢ ∀ (a : ⨁ (i : ι), ↥(𝒜 i)),
    (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap fun i => 𝒜 i) a)) i) =
      ↑(((lmap' (quotCompMap R 𝒜 rel)) a) i)
Tactic:
intro a
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
a✝ b : ⨁ (i : ι), ↥(𝒜 i)
hxy : (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a✝) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) b)
i : ι
hxy' :
  (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap 𝒜) a✝)) i) =
    (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap 𝒜) b)) i)
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap fun i => 𝒜 i) a)) i) =
    ↑(((lmap' (quotCompMap R 𝒜 rel)) a) 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
a✝ b : ⨁ (i : ι), ↥(𝒜 i)
hxy : (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a✝) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) b)
i : ι
hxy' :
  (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap 𝒜) a✝)) i) =
    (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap 𝒜) b)) i)
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap fun i => 𝒜 i) a)) i) =
    ↑(((lmap' (quotCompMap R 𝒜 rel)) a) i)
Tactic:
simp only [lmap'_apply]
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
a✝ b : ⨁ (i : ι), ↥(𝒜 i)
hxy : (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a✝) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) b)
i : ι
hxy' :
  (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap 𝒜) a✝)) i) =
    (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap 𝒜) b)) i)
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap fun i => 𝒜 i) a)) i) =
    ↑((quotCompMap R 𝒜 rel i) (a 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
a✝ b : ⨁ (i : ι), ↥(𝒜 i)
hxy : (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a✝) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) b)
i : ι
hxy' :
  (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap 𝒜) a✝)) i) =
    (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap 𝒜) b)) i)
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap fun i => 𝒜 i) a)) i) =
    ↑((quotCompMap R 𝒜 rel i) (a i))
Tactic:
congr
Proof state after:
case intro.refl.intro.refl.h.h.e_6.h.e_self.e_a
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
a✝ b : ⨁ (i : ι), ↥(𝒜 i)
hxy : (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a✝) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) b)
i : ι
hxy' :
  (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap 𝒜) a✝)) i) =
    (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap 𝒜) b)) i)
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ (decompose fun i => 𝒜 i) ((coeLinearMap fun i => 𝒜 i) a) = a
Theorem: quotDecompose'_injective
Proof state before:
case intro.refl.intro.refl.h.h.e_6.h.e_self.e_a
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
a✝ b : ⨁ (i : ι), ↥(𝒜 i)
hxy : (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a✝) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) b)
i : ι
hxy' :
  (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap 𝒜) a✝)) i) =
    (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap 𝒜) b)) i)
a : ⨁ (i : ι), ↥(𝒜 i)
⊢ (decompose fun i => 𝒜 i) ((coeLinearMap fun i => 𝒜 i) a) = a
Tactic:
exact h𝒜.right_inv a
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
a b : ⨁ (i : ι), ↥(𝒜 i)
hxy : (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) a) = (RingQuot.mkAlgHom R rel) ((coeLinearMap 𝒜) b)
i : ι
hxy' :
  (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap 𝒜) a)) i) =
    (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap 𝒜) b)) i)
this :
  ∀ (a : ⨁ (i : ι), ↥(𝒜 i)),
    (RingQuot.mkAlgHom R rel) ↑(((decompose fun i => 𝒜 i) ((coeLinearMap fun i => 𝒜 i) a)) i) =
      ↑(((lmap' (quotCompMap R 𝒜 rel)) a) i)
⊢ ((lmap' (quotCompMap R 𝒜 rel)) a) i = ((lmap' (quotCompMap R 𝒜 rel)) b) i
Tactic:
simpa only [this, 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
⊢ Injective ⇑(coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i))
Tactic:
have hφ : ∀ i, Surjective (quotCompMap R 𝒜 rel i) := by
  rintro i ⟨x, ⟨a, ha, rfl⟩ ⟩
  exact ⟨⟨a, ha⟩, rfl⟩
Proof state after:
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)
⊢ Injective ⇑(coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i))
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
hφ : ∀ (i : ι), Surjective ⇑(quotCompMap R 𝒜 rel i)
⊢ Injective ⇑(coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i))
Tactic:
intro x y hxy
Proof state after:
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)
x y : ⨁ (i : ι), ↥(Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i))
hxy :
  (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) x =
    (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) y
⊢ x = y
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
hφ : ∀ (i : ι), Surjective ⇑(quotCompMap R 𝒜 rel i)
x y : ⨁ (i : ι), ↥(Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i))
hxy :
  (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) x =
    (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) y
⊢ x = y
Tactic:
obtain ⟨a, ha, rfl⟩ := lmap'_surjective (quotCompMap R 𝒜 rel) hφ x
Proof state after:
case intro.refl
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)
y : ⨁ (i : ι), ↥(Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i))
a : ⨁ (i : ι), ↥(𝒜 i)
hxy :
  (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ((lmap' (quotCompMap R 𝒜 rel)) a) =
    (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) y
⊢ (lmap' (quotCompMap R 𝒜 rel)) a = y
Theorem: quotDecompose_injective'
Proof state before:
case intro.refl
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)
y : ⨁ (i : ι), ↥(Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i))
a : ⨁ (i : ι), ↥(𝒜 i)
hxy :
  (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ((lmap' (quotCompMap R 𝒜 rel)) a) =
    (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) y
⊢ (lmap' (quotCompMap R 𝒜 rel)) a = y
Tactic:
obtain ⟨b, hb, rfl⟩ := lmap'_surjective (quotCompMap R 𝒜 rel) hφ y
Proof state after:
case intro.refl.intro.refl
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 :
  (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ((lmap' (quotCompMap R 𝒜 rel)) a) =
    (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ((lmap' (quotCompMap R 𝒜 rel)) b)
⊢ (lmap' (quotCompMap R 𝒜 rel)) a = (lmap' (quotCompMap R 𝒜 rel)) b
Theorem: quotDecompose_injective'
Proof state before:
case intro.refl.intro.refl
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 :
  (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ((lmap' (quotCompMap R 𝒜 rel)) a) =
    (coeLinearMap fun i => Submodule.map (RingQuot.mkAlgHom R rel) (𝒜 i)) ((lmap' (quotCompMap R 𝒜 rel)) b)
⊢ (lmap' (quotCompMap R 𝒜 rel)) a = (lmap' (quotCompMap R 𝒜 rel)) b
Tactic:
simp only [quotDecompose_left_inv'_aux_apply] at hxy
Proof state after:
case intro.refl.intro.refl
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)
⊢ (lmap' (quotCompMap R 𝒜 rel)) a = (lmap' (quotCompMap R 𝒜 rel)) b
Theorem: quotDecompose_injective'
Proof state before:
case intro.refl.intro.refl
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)
⊢ (lmap' (quotCompMap R 𝒜 rel)) a = (lmap' (quotCompMap R 𝒜 rel)) b
Tactic:
let hxy' := quotDecompose_injective R 𝒜 rel hrel hxy
Proof state after:
case intro.refl.intro.refl
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)
hxy' : ∀ (i : ι),
  (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap fun i => 𝒜 i) a)) i) =
    (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap fun i => 𝒜 i) b)) i) :=
  quotDecompose_injective R 𝒜 rel (fun {a b} => hrel) hxy
⊢ (lmap' (quotCompMap R 𝒜 rel)) a = (lmap' (quotCompMap R 𝒜 rel)) b
Theorem: quotDecompose_injective'
Proof state before:
case intro.refl.intro.refl
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)
hxy' : ∀ (i : ι),
  (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap fun i => 𝒜 i) a)) i) =
    (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap fun i => 𝒜 i) b)) i) :=
  quotDecompose_injective R 𝒜 rel (fun {a b} => hrel) hxy
⊢ (lmap' (quotCompMap R 𝒜 rel)) a = (lmap' (quotCompMap R 𝒜 rel)) b
Tactic:
apply DFinsupp.ext
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)
hxy' : ∀ (i : ι),
  (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap fun i => 𝒜 i) a)) i) =
    (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap fun i => 𝒜 i) b)) i) :=
  quotDecompose_injective R 𝒜 rel (fun {a b} => hrel) hxy
⊢ ∀ (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)
hxy' : ∀ (i : ι),
  (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap fun i => 𝒜 i) a)) i) =
    (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap fun i => 𝒜 i) b)) i) :=
  quotDecompose_injective R 𝒜 rel (fun {a b} => hrel) hxy
⊢ ∀ (i : ι), ((lmap' (quotCompMap R 𝒜 rel)) a) i = ((lmap' (quotCompMap R 𝒜 rel)) b) i
Tactic:
intro i
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)
hxy' : ∀ (i : ι),
  (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap fun i => 𝒜 i) a)) i) =
    (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap fun i => 𝒜 i) b)) i) :=
  quotDecompose_injective R 𝒜 rel (fun {a b} => hrel) hxy
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)
hxy' : ∀ (i : ι),
  (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap fun i => 𝒜 i) a)) i) =
    (RingQuot.mkAlgHom R rel) ↑((Decomposition.decompose' ((coeLinearMap fun i => 𝒜 i) b)) i) :=
  quotDecompose_injective R 𝒜 rel (fun {a b} => hrel) hxy
i : ι
⊢ ((lmap' (quotCompMap R 𝒜 rel)) a) i = ((lmap' (quotCompMap R 𝒜 rel)) b) i
Tactic:
specialize hxy' i
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) ↑((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