Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AlgebraicGeometry_HomogeneousIdealQuotientGradingInfra.lean

definition module

Induced grading on a quotient by a homogeneous ideal

The module transports a graded-ring structure along the quotient map \pi \colon A \to A/I. In the general ('engine') setting, A is a commutative ring with a family \mathcal{A} \colon \iota \to \sigma of additive submonoids, I \subseteq A an ideal, and \mathcal{B} \colon \iota \to \tau a family of additive submonoids of A/I subject to two hypotheses: hmem, that \pi(\mathcal{A}_i) \subseteq \mathcal{B}_i for all i, and hsurj, that every b \in \mathcal{B}_i is \pi(a) for some a \in \mathcal{A}_i. From hmem one gets pieceHom, the additive map \mathcal{A}_i \to \mathcal{B}_i induced by \pi, surjective under hsurj; gradedMonoidOfImages deduces 1 \in \mathcal{B}_0 and \mathcal{B}_i \mathcal{B}_j \subseteq \mathcal{B}_{i+j} from the corresponding facts for \mathcal{A}. Assuming moreover GradedRing π’œ, the map preDecompose sends a \in A to the degreewise image of its decomposition, \bigoplus_i \pi(a_i); it is compatible with the coercion \bigoplus_i \mathcal{B}_i \to A/I and vanishes on I when I is homogeneous, so it descends to quotDecompose on A/I. decompositionOfImages and gradedRingOfImages package this as DirectSum.Decomposition ℬ and GradedRing ℬ, and decompose_mk, decompose_mk_apply record that the i-th component of \pi(a) is \pi(a_i).

Two concrete instantiations follow. For \mathcal{A} a family of additive subgroups, quotGrading π’œ I i is the image subgroup \pi(\mathcal{A}_i) \subseteq A/I, with its membership criterion, a graded-monoid instance, and, for a homogeneous ideal, quotGradingGradedRing together with the componentwise formula decompose_quotGrading_mk_apply. For \mathcal{A} a family of R-submodules of an R-algebra A, quotGradingSubmodule π’œ I i is the image submodule under the quotient algebra map, yielding quotGradingSubmoduleGradedAlgebra and the analogous component formula. A final worked example takes A = \mathbb{Z}[X_0, X_1] with its standard grading and I = (X_0 X_1): the ideal is homogeneous and nonzero, X_0 \notin I (seen by evaluating at (1,0)), the quotient carries the induced graded ring and graded algebra structures, and \pi(X_0) is a nonzero element of degree 1 equal to its own degree-1 component.

Relation to Mathlib

The grading classes used (SetLike.GradedMonoid, DirectSum.Decomposition, GradedRing, GradedAlgebra), the notions Ideal.IsHomogeneous and HomogeneousIdeal, and the standard grading of a multivariate polynomial ring via MvPolynomial.homogeneousSubmodule and MvPolynomial.gradedAlgebra are Mathlib's; what is added here is the transport of such a structure to a quotient ring along degreewise surjections, and the two resulting families quotGrading (additive subgroups) and quotGradingSubmodule (submodules).

Where it is used

The constructions serve the algebraic-geometry layer, where projective models are presented as \mathrm{Proj} of a quotient of a polynomial ring by a homogeneous ideal and therefore need that quotient's inherited grading, in the \mathbb{N}-indexed submodule form required by GradedAlgebra.

References

  1. D. Eisenbud, Commutative Algebra with a View Toward Algebraic Geometry, Graduate Texts in Mathematics 150, Springer, 1995
  2. R. Hartshorne, Algebraic Geometry, Graduate Texts in Mathematics 52, Springer, 1977, Chapter II.2

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_AlgebraicGeometry_HomogeneousIdealQuotientGradingInfra.lean

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib

namespace HomogeneousIdealQuotientGrading

open DirectSum

section Engine

variable {ΞΉ A Οƒ Ο„ : Type*}
variable [CommRing A] [SetLike Οƒ A] [AddSubmonoidClass Οƒ A] (π’œ : ΞΉ β†’ Οƒ)
variable (I : Ideal A)
variable [SetLike Ο„ (A β§Έ I)] [AddSubmonoidClass Ο„ (A β§Έ I)] (ℬ : ΞΉ β†’ Ο„)

def pieceHom (hmem : βˆ€ (i : ΞΉ) (a : A), a ∈ π’œ i β†’ Ideal.Quotient.mk I a ∈ ℬ i) (i : ΞΉ) :
    π’œ i β†’+ ℬ i :=
  AddMonoidHom.codRestrict
    ((Ideal.Quotient.mk I).toAddMonoidHom.comp (AddSubmonoidClass.subtype (π’œ i))) (ℬ i)
    (fun a => hmem i a a.2)

@[simp] lemma pieceHom_coe (hmem : βˆ€ (i : ΞΉ) (a : A), a ∈ π’œ i β†’ Ideal.Quotient.mk I a ∈ ℬ i)
    (i : ΞΉ) (a : π’œ i) :
    (pieceHom π’œ I ℬ hmem i a : A β§Έ I) = Ideal.Quotient.mk I (a : A) := rfl

lemma pieceHom_surjective (hmem : βˆ€ (i : ΞΉ) (a : A), a ∈ π’œ i β†’ Ideal.Quotient.mk I a ∈ ℬ i)
    (hsurj : βˆ€ (i : ΞΉ), βˆ€ b ∈ ℬ i, βˆƒ a ∈ π’œ i, Ideal.Quotient.mk I a = b) (i : ΞΉ) :
    Function.Surjective (pieceHom π’œ I ℬ hmem i) := by
  rintro ⟨b, hb⟩
  obtain ⟨a, ha, rfl⟩ := hsurj i b hb
  exact ⟨⟨a, ha⟩, rfl⟩

omit [AddSubmonoidClass Οƒ A] [AddSubmonoidClass Ο„ (A β§Έ I)] in

theorem gradedMonoidOfImages [AddMonoid ΞΉ] [SetLike.GradedMonoid π’œ]
    (hmem : βˆ€ (i : ΞΉ) (a : A), a ∈ π’œ i β†’ Ideal.Quotient.mk I a ∈ ℬ i)
    (hsurj : βˆ€ (i : ΞΉ), βˆ€ b ∈ ℬ i, βˆƒ a ∈ π’œ i, Ideal.Quotient.mk I a = b) :
    SetLike.GradedMonoid ℬ where
  one_mem := by
    have h1 : (1 : A β§Έ I) = Ideal.Quotient.mk I 1 := (map_one _).symm
    rw [h1]
    exact hmem 0 1 (SetLike.one_mem_graded π’œ)
  mul_mem := by
    intro i j x y hx hy
    obtain ⟨a, ha, rfl⟩ := hsurj i x hx
    obtain ⟨b, hb, rfl⟩ := hsurj j y hy
    rw [← map_mul]
    exact hmem _ _ (SetLike.mul_mem_graded ha hb)

variable [DecidableEq ΞΉ]

lemma coeAddMonoidHom_map_pieceHom
    (hmem : βˆ€ (i : ΞΉ) (a : A), a ∈ π’œ i β†’ Ideal.Quotient.mk I a ∈ ℬ i) (y : ⨁ i, π’œ i) :
    DirectSum.coeAddMonoidHom ℬ (DirectSum.map (pieceHom π’œ I ℬ hmem) y)
      = Ideal.Quotient.mk I (DirectSum.coeAddMonoidHom π’œ y) := by
  refine DirectSum.induction_on y ?_ ?_ ?_
  Β· simp
  Β· intro i x
    rw [DirectSum.map_of, DirectSum.coeAddMonoidHom_of, DirectSum.coeAddMonoidHom_of,
      pieceHom_coe]
  Β· intro x y hx hy
    rw [map_add, map_add, map_add, map_add, hx, hy]

variable [AddMonoid ΞΉ] [GradedRing π’œ]

def preDecompose (hmem : βˆ€ (i : ΞΉ) (a : A), a ∈ π’œ i β†’ Ideal.Quotient.mk I a ∈ ℬ i) :
    A β†’+ ⨁ i, ℬ i :=
  (DirectSum.map (pieceHom π’œ I ℬ hmem)).comp (decomposeAddEquiv π’œ).toAddMonoidHom

lemma preDecompose_apply (hmem : βˆ€ (i : ΞΉ) (a : A), a ∈ π’œ i β†’ Ideal.Quotient.mk I a ∈ ℬ i)
    (a : A) :
    preDecompose π’œ I ℬ hmem a = DirectSum.map (pieceHom π’œ I ℬ hmem) (decompose π’œ a) := rfl

lemma preDecompose_apply_apply
    (hmem : βˆ€ (i : ΞΉ) (a : A), a ∈ π’œ i β†’ Ideal.Quotient.mk I a ∈ ℬ i) (a : A) (i : ΞΉ) :
    preDecompose π’œ I ℬ hmem a i = pieceHom π’œ I ℬ hmem i (decompose π’œ a i) := by
  rw [preDecompose_apply, DirectSum.map_apply]

lemma preDecompose_of_mem (hmem : βˆ€ (i : ΞΉ) (a : A), a ∈ π’œ i β†’ Ideal.Quotient.mk I a ∈ ℬ i)
    {i : ΞΉ} {a : A} (ha : a ∈ π’œ i) :
    preDecompose π’œ I ℬ hmem a
      = DirectSum.of (fun j => ℬ j) i ⟨Ideal.Quotient.mk I a, hmem i a ha⟩ := by
  rw [preDecompose_apply, decompose_of_mem π’œ ha, DirectSum.map_of]
  rfl

lemma coeAddMonoidHom_preDecompose
    (hmem : βˆ€ (i : ΞΉ) (a : A), a ∈ π’œ i β†’ Ideal.Quotient.mk I a ∈ ℬ i) (a : A) :
    DirectSum.coeAddMonoidHom ℬ (preDecompose π’œ I ℬ hmem a) = Ideal.Quotient.mk I a := by
  rw [preDecompose_apply, coeAddMonoidHom_map_pieceHom]
  congr 1
  exact (DirectSum.decompose π’œ).symm_apply_apply a

lemma preDecompose_eq_zero_of_mem
    (hmem : βˆ€ (i : ΞΉ) (a : A), a ∈ π’œ i β†’ Ideal.Quotient.mk I a ∈ ℬ i)
    (hI : I.IsHomogeneous π’œ) {a : A} (ha : a ∈ I) :
    preDecompose π’œ I ℬ hmem a = 0 := by
  ext i
  rw [preDecompose_apply_apply, DirectSum.zero_apply, pieceHom_coe, ZeroMemClass.coe_zero,
    Ideal.Quotient.eq_zero_iff_mem]
  exact hI i ha

def quotDecompose (hmem : βˆ€ (i : ΞΉ) (a : A), a ∈ π’œ i β†’ Ideal.Quotient.mk I a ∈ ℬ i)
    (hI : I.IsHomogeneous π’œ) : A β§Έ I β†’+ ⨁ i, ℬ i :=
  QuotientAddGroup.lift I.toAddSubgroup (preDecompose π’œ I ℬ hmem)
    (fun _ ha => preDecompose_eq_zero_of_mem π’œ I ℬ hmem hI ha)

@[simp] lemma quotDecompose_mk
    (hmem : βˆ€ (i : ΞΉ) (a : A), a ∈ π’œ i β†’ Ideal.Quotient.mk I a ∈ ℬ i)
    (hI : I.IsHomogeneous π’œ) (a : A) :
    quotDecompose π’œ I ℬ hmem hI (Ideal.Quotient.mk I a) = preDecompose π’œ I ℬ hmem a := rfl

@[reducible] def decompositionOfImages
    (hmem : βˆ€ (i : ΞΉ) (a : A), a ∈ π’œ i β†’ Ideal.Quotient.mk I a ∈ ℬ i)
    (hsurj : βˆ€ (i : ΞΉ), βˆ€ b ∈ ℬ i, βˆƒ a ∈ π’œ i, Ideal.Quotient.mk I a = b)
    (hI : I.IsHomogeneous π’œ) : DirectSum.Decomposition ℬ :=
  DirectSum.Decomposition.ofAddHom ℬ (quotDecompose π’œ I ℬ hmem hI)
    (by
      refine AddMonoidHom.ext fun x => ?_
      obtain ⟨a, rfl⟩ := Ideal.Quotient.mk_surjective x
      rw [AddMonoidHom.comp_apply, AddMonoidHom.id_apply, quotDecompose_mk,
        coeAddMonoidHom_preDecompose])
    (by
      refine DirectSum.addHom_ext fun i b => ?_
      rw [AddMonoidHom.comp_apply, AddMonoidHom.id_apply, DirectSum.coeAddMonoidHom_of]
      obtain ⟨a, ha, hab⟩ := hsurj i (b : A ⧸ I) b.2
      rw [← hab, quotDecompose_mk, preDecompose_of_mem π’œ I ℬ hmem ha]
      exact congrArg _ (Subtype.ext hab))

@[reducible] def gradedRingOfImages
    (hmem : βˆ€ (i : ΞΉ) (a : A), a ∈ π’œ i β†’ Ideal.Quotient.mk I a ∈ ℬ i)
    (hsurj : βˆ€ (i : ΞΉ), βˆ€ b ∈ ℬ i, βˆƒ a ∈ π’œ i, Ideal.Quotient.mk I a = b)
    (hI : I.IsHomogeneous π’œ) : GradedRing ℬ where
  toGradedMonoid := gradedMonoidOfImages π’œ I ℬ hmem hsurj
  toDecomposition := decompositionOfImages π’œ I ℬ hmem hsurj hI

theorem decompose_mk (hmem : βˆ€ (i : ΞΉ) (a : A), a ∈ π’œ i β†’ Ideal.Quotient.mk I a ∈ ℬ i)
    [DirectSum.Decomposition ℬ] (a : A) :
    DirectSum.decompose ℬ (Ideal.Quotient.mk I a)
      = DirectSum.map (pieceHom π’œ I ℬ hmem) (DirectSum.decompose π’œ a) := by
  apply (DirectSum.decompose ℬ).symm.injective
  rw [Equiv.symm_apply_apply]
  rw [show ⇑(DirectSum.decompose ℬ).symm = ⇑(DirectSum.coeAddMonoidHom ℬ) from rfl]
  rw [coeAddMonoidHom_map_pieceHom]
  congr 1
  exact ((DirectSum.decompose π’œ).symm_apply_apply a).symm

theorem decompose_mk_apply (hmem : βˆ€ (i : ΞΉ) (a : A), a ∈ π’œ i β†’ Ideal.Quotient.mk I a ∈ ℬ i)
    [DirectSum.Decomposition ℬ] (a : A) (i : ΞΉ) :
    (DirectSum.decompose ℬ (Ideal.Quotient.mk I a) i : A β§Έ I)
      = Ideal.Quotient.mk I (DirectSum.decompose π’œ a i) := by
  rw [decompose_mk π’œ I ℬ hmem, DirectSum.map_apply, pieceHom_coe]

end Engine

section QuotGradingDef

variable {ΞΉ A Οƒ : Type*}
variable [CommRing A] [SetLike Οƒ A] [AddSubgroupClass Οƒ A] (π’œ : ΞΉ β†’ Οƒ)
variable (I : Ideal A)

def quotGrading (i : ΞΉ) : AddSubgroup (A β§Έ I) :=
  (AddSubgroup.ofClass (π’œ i)).map (Ideal.Quotient.mk I).toAddMonoidHom

lemma mem_quotGrading_iff {i : ΞΉ} {x : A β§Έ I} :
    x ∈ quotGrading π’œ I i ↔ βˆƒ a ∈ π’œ i, Ideal.Quotient.mk I a = x := by
  constructor
  · rintro ⟨a, ha, rfl⟩
    exact ⟨a, ha, rfl⟩
  · rintro ⟨a, ha, rfl⟩
    exact ⟨a, ha, rfl⟩

lemma mk_mem_quotGrading {i : ΞΉ} {a : A} (ha : a ∈ π’œ i) :
    Ideal.Quotient.mk I a ∈ quotGrading π’œ I i :=
  (mem_quotGrading_iff π’œ I).mpr ⟨a, ha, rfl⟩

def quotGradingPieceHom (i : ΞΉ) : π’œ i β†’+ quotGrading π’œ I i :=
  pieceHom π’œ I (quotGrading π’œ I) (fun _ _ ha => mk_mem_quotGrading π’œ I ha) i

@[simp] lemma quotGradingPieceHom_coe (i : ΞΉ) (a : π’œ i) :
    (quotGradingPieceHom π’œ I i a : A β§Έ I) = Ideal.Quotient.mk I (a : A) := rfl

lemma quotGradingPieceHom_surjective (i : ΞΉ) :
    Function.Surjective (quotGradingPieceHom π’œ I i) :=
  pieceHom_surjective π’œ I (quotGrading π’œ I) (fun _ _ ha => mk_mem_quotGrading π’œ I ha)
    (fun _ _ hb => (mem_quotGrading_iff π’œ I).mp hb) i

instance quotGradingGradedMonoid [AddMonoid ΞΉ] [SetLike.GradedMonoid π’œ] :
    SetLike.GradedMonoid (quotGrading π’œ I) :=
  gradedMonoidOfImages π’œ I (quotGrading π’œ I)
    (fun _ _ ha => mk_mem_quotGrading π’œ I ha)
    (fun _ _ hb => (mem_quotGrading_iff π’œ I).mp hb)

end QuotGradingDef

section QuotGradingGraded

variable {ΞΉ A Οƒ : Type*}
variable [DecidableEq ΞΉ] [AddMonoid ΞΉ] [CommRing A]
variable [SetLike Οƒ A] [AddSubgroupClass Οƒ A] (π’œ : ΞΉ β†’ Οƒ) [GradedRing π’œ]
variable (I : Ideal A)

@[reducible] def quotGradingGradedRing (hI : I.IsHomogeneous π’œ) :
    GradedRing (quotGrading π’œ I) :=
  gradedRingOfImages π’œ I (quotGrading π’œ I)
    (fun _ _ ha => mk_mem_quotGrading π’œ I ha)
    (fun _ _ hb => (mem_quotGrading_iff π’œ I).mp hb)
    hI

instance quotGradingGradedRingOfHomogeneous (J : HomogeneousIdeal π’œ) :
    GradedRing (quotGrading π’œ J.toIdeal) :=
  quotGradingGradedRing π’œ J.toIdeal J.isHomogeneous

theorem decompose_quotGrading_mk_apply (J : HomogeneousIdeal π’œ) (a : A) (i : ΞΉ) :
    (DirectSum.decompose (quotGrading π’œ J.toIdeal) (Ideal.Quotient.mk J.toIdeal a) i
        : A β§Έ J.toIdeal)
      = Ideal.Quotient.mk J.toIdeal (DirectSum.decompose π’œ a i) :=
  decompose_mk_apply π’œ J.toIdeal (quotGrading π’œ J.toIdeal)
    (fun _ _ ha => mk_mem_quotGrading π’œ J.toIdeal ha) a i

end QuotGradingGraded

section SubmoduleVersion

variable {ΞΉ R A : Type*}
variable [CommRing R] [CommRing A] [Algebra R A]
variable (π’œ : ΞΉ β†’ Submodule R A)
variable (I : Ideal A)

def quotGradingSubmodule (i : ΞΉ) : Submodule R (A β§Έ I) :=
  (π’œ i).map (Ideal.Quotient.mkₐ R I).toLinearMap

lemma mem_quotGradingSubmodule_iff {i : ΞΉ} {x : A β§Έ I} :
    x ∈ quotGradingSubmodule π’œ I i ↔ βˆƒ a ∈ π’œ i, Ideal.Quotient.mk I a = x := by
  constructor
  · rintro ⟨a, ha, rfl⟩
    exact ⟨a, ha, rfl⟩
  · rintro ⟨a, ha, rfl⟩
    exact ⟨a, ha, rfl⟩

lemma mk_mem_quotGradingSubmodule {i : ΞΉ} {a : A} (ha : a ∈ π’œ i) :
    Ideal.Quotient.mk I a ∈ quotGradingSubmodule π’œ I i :=
  (mem_quotGradingSubmodule_iff π’œ I).mpr ⟨a, ha, rfl⟩

instance quotGradingSubmoduleGradedMonoid [AddMonoid ΞΉ] [SetLike.GradedMonoid π’œ] :
    SetLike.GradedMonoid (quotGradingSubmodule π’œ I) :=
  gradedMonoidOfImages π’œ I (quotGradingSubmodule π’œ I)
    (fun _ _ ha => mk_mem_quotGradingSubmodule π’œ I ha)
    (fun _ _ hb => (mem_quotGradingSubmodule_iff π’œ I).mp hb)

variable [DecidableEq ΞΉ] [AddMonoid ΞΉ] [GradedAlgebra π’œ]

@[reducible] def quotGradingSubmoduleGradedAlgebra (hI : I.IsHomogeneous π’œ) :
    GradedAlgebra (quotGradingSubmodule π’œ I) :=
  gradedRingOfImages π’œ I (quotGradingSubmodule π’œ I)
    (fun _ _ ha => mk_mem_quotGradingSubmodule π’œ I ha)
    (fun _ _ hb => (mem_quotGradingSubmodule_iff π’œ I).mp hb)
    hI

instance quotGradingSubmoduleGradedAlgebraOfHomogeneous (J : HomogeneousIdeal π’œ) :
    GradedAlgebra (quotGradingSubmodule π’œ J.toIdeal) :=
  quotGradingSubmoduleGradedAlgebra π’œ J.toIdeal J.isHomogeneous

theorem decompose_quotGradingSubmodule_mk_apply (J : HomogeneousIdeal π’œ) (a : A) (i : ΞΉ) :
    (DirectSum.decompose (quotGradingSubmodule π’œ J.toIdeal) (Ideal.Quotient.mk J.toIdeal a) i
        : A β§Έ J.toIdeal)
      = Ideal.Quotient.mk J.toIdeal (DirectSum.decompose π’œ a i) :=
  decompose_mk_apply π’œ J.toIdeal (quotGradingSubmodule π’œ J.toIdeal)
    (fun _ _ ha => mk_mem_quotGradingSubmodule π’œ J.toIdeal ha) a i

end SubmoduleVersion

section Gate

open MvPolynomial

attribute [local instance] MvPolynomial.gradedAlgebra

noncomputable def gateIdeal : Ideal (MvPolynomial (Fin 2) β„€) :=
  Ideal.span {(X 0 * X 1 : MvPolynomial (Fin 2) β„€)}

lemma gateIdeal_isHomogeneous :
    (gateIdeal).IsHomogeneous (homogeneousSubmodule (Fin 2) β„€) := by
  refine Ideal.homogeneous_span _ _ ?_
  rintro x hx
  rcases Set.mem_singleton_iff.mp hx with rfl
  exact ⟨2, (mem_homogeneousSubmodule _ _).mpr ((isHomogeneous_X _ _).mul (isHomogeneous_X _ _))⟩

noncomputable def gateHomogeneousIdeal :
    HomogeneousIdeal (homogeneousSubmodule (Fin 2) β„€) :=
  ⟨gateIdeal, gateIdeal_isHomogeneous⟩

lemma gate_gateIdeal_ne_bot : gateIdeal β‰  βŠ₯ := by
  intro h
  have hmem : (X 0 * X 1 : MvPolynomial (Fin 2) β„€) ∈ gateIdeal :=
    Ideal.mem_span_singleton_self _
  rw [h, Ideal.mem_bot] at hmem
  exact mul_ne_zero (MvPolynomial.X_ne_zero _) (MvPolynomial.X_ne_zero _) hmem

lemma gate_mk_X0X1_eq_zero :
    Ideal.Quotient.mk gateIdeal (X 0 * X 1 : MvPolynomial (Fin 2) β„€) = 0 :=
  Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.mem_span_singleton_self _)

lemma gate_X0_not_mem : (X 0 : MvPolynomial (Fin 2) β„€) βˆ‰ gateIdeal := by
  intro h
  rw [gateIdeal, Ideal.mem_span_singleton] at h
  obtain ⟨c, hc⟩ := h
  have := congrArg (MvPolynomial.eval (fun j : Fin 2 => if j = 0 then (1 : β„€) else 0)) hc
  simp [MvPolynomial.eval_X, MvPolynomial.eval_mul] at this

lemma gate_mk_X0_ne_zero :
    Ideal.Quotient.mk gateIdeal (X 0 : MvPolynomial (Fin 2) β„€) β‰  0 := by
  rw [Ne, Ideal.Quotient.eq_zero_iff_mem]
  exact gate_X0_not_mem

lemma gate_mk_X0_mem :
    Ideal.Quotient.mk gateIdeal (X 0 : MvPolynomial (Fin 2) β„€)
      ∈ quotGrading (homogeneousSubmodule (Fin 2) β„€) gateIdeal 1 :=
  mk_mem_quotGrading _ _ ((mem_homogeneousSubmodule _ _).mpr (isHomogeneous_X _ _))

@[reducible] noncomputable def gateGradedRing :
    GradedRing (quotGrading (homogeneousSubmodule (Fin 2) β„€) gateIdeal) :=
  quotGradingGradedRing _ _ gateIdeal_isHomogeneous

@[reducible] noncomputable def gateGradedAlgebra :
    GradedAlgebra (quotGradingSubmodule (homogeneousSubmodule (Fin 2) β„€) gateIdeal) :=
  quotGradingSubmoduleGradedAlgebra _ _ gateIdeal_isHomogeneous

lemma gate_decompose_mk_X0 :
    (DirectSum.decompose (quotGrading (homogeneousSubmodule (Fin 2) β„€) gateHomogeneousIdeal.toIdeal)
        (Ideal.Quotient.mk gateHomogeneousIdeal.toIdeal (X 0 : MvPolynomial (Fin 2) β„€)) 1
      : MvPolynomial (Fin 2) β„€ β§Έ gateHomogeneousIdeal.toIdeal)
      = Ideal.Quotient.mk gateHomogeneousIdeal.toIdeal (X 0 : MvPolynomial (Fin 2) β„€) := by
  rw [decompose_quotGrading_mk_apply]
  congr 1
  have hX : (X 0 : MvPolynomial (Fin 2) β„€) ∈ homogeneousSubmodule (Fin 2) β„€ 1 :=
    (mem_homogeneousSubmodule _ _).mpr (isHomogeneous_X _ _)
  exact DirectSum.decompose_of_mem_same _ hX

end Gate

end HomogeneousIdealQuotientGrading

/--
info: 'HomogeneousIdealQuotientGrading.pieceHom' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.pieceHom

/--
info: 'HomogeneousIdealQuotientGrading.pieceHom_coe' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.pieceHom_coe

/--
info: 'HomogeneousIdealQuotientGrading.pieceHom_surjective' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.pieceHom_surjective

/--
info: 'HomogeneousIdealQuotientGrading.gradedMonoidOfImages' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.gradedMonoidOfImages

/--
info: 'HomogeneousIdealQuotientGrading.coeAddMonoidHom_map_pieceHom' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.coeAddMonoidHom_map_pieceHom

/--
info: 'HomogeneousIdealQuotientGrading.preDecompose' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.preDecompose

/--
info: 'HomogeneousIdealQuotientGrading.preDecompose_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.preDecompose_apply

/--
info: 'HomogeneousIdealQuotientGrading.preDecompose_apply_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.preDecompose_apply_apply

/--
info: 'HomogeneousIdealQuotientGrading.preDecompose_of_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.preDecompose_of_mem

/--
info: 'HomogeneousIdealQuotientGrading.coeAddMonoidHom_preDecompose' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.coeAddMonoidHom_preDecompose

/--
info: 'HomogeneousIdealQuotientGrading.preDecompose_eq_zero_of_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.preDecompose_eq_zero_of_mem

/--
info: 'HomogeneousIdealQuotientGrading.quotDecompose' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.quotDecompose

/--
info: 'HomogeneousIdealQuotientGrading.quotDecompose_mk' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.quotDecompose_mk

/--
info: 'HomogeneousIdealQuotientGrading.decompositionOfImages' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.decompositionOfImages

/--
info: 'HomogeneousIdealQuotientGrading.gradedRingOfImages' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.gradedRingOfImages

/--
info: 'HomogeneousIdealQuotientGrading.decompose_mk' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.decompose_mk

/--
info: 'HomogeneousIdealQuotientGrading.decompose_mk_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.decompose_mk_apply

/--
info: 'HomogeneousIdealQuotientGrading.quotGrading' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.quotGrading

/--
info: 'HomogeneousIdealQuotientGrading.mem_quotGrading_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.mem_quotGrading_iff

/--
info: 'HomogeneousIdealQuotientGrading.mk_mem_quotGrading' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.mk_mem_quotGrading

/--
info: 'HomogeneousIdealQuotientGrading.quotGradingPieceHom' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.quotGradingPieceHom

/--
info: 'HomogeneousIdealQuotientGrading.quotGradingPieceHom_coe' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.quotGradingPieceHom_coe

/--
info: 'HomogeneousIdealQuotientGrading.quotGradingPieceHom_surjective' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.quotGradingPieceHom_surjective

/--
info: 'HomogeneousIdealQuotientGrading.quotGradingGradedMonoid' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.quotGradingGradedMonoid

/--
info: 'HomogeneousIdealQuotientGrading.quotGradingGradedRing' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.quotGradingGradedRing

/--
info: 'HomogeneousIdealQuotientGrading.quotGradingGradedRingOfHomogeneous' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.quotGradingGradedRingOfHomogeneous

/--
info: 'HomogeneousIdealQuotientGrading.decompose_quotGrading_mk_apply' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.decompose_quotGrading_mk_apply

/--
info: 'HomogeneousIdealQuotientGrading.quotGradingSubmodule' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.quotGradingSubmodule

/--
info: 'HomogeneousIdealQuotientGrading.mem_quotGradingSubmodule_iff' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.mem_quotGradingSubmodule_iff

/--
info: 'HomogeneousIdealQuotientGrading.mk_mem_quotGradingSubmodule' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.mk_mem_quotGradingSubmodule

/--
info: 'HomogeneousIdealQuotientGrading.quotGradingSubmoduleGradedMonoid' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.quotGradingSubmoduleGradedMonoid

/--
info: 'HomogeneousIdealQuotientGrading.quotGradingSubmoduleGradedAlgebra' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.quotGradingSubmoduleGradedAlgebra

/--
info: 'HomogeneousIdealQuotientGrading.quotGradingSubmoduleGradedAlgebraOfHomogeneous' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.quotGradingSubmoduleGradedAlgebraOfHomogeneous

/--
info: 'HomogeneousIdealQuotientGrading.decompose_quotGradingSubmodule_mk_apply' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.decompose_quotGradingSubmodule_mk_apply

/--
info: 'HomogeneousIdealQuotientGrading.gateIdeal' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.gateIdeal

/--
info: 'HomogeneousIdealQuotientGrading.gateIdeal_isHomogeneous' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.gateIdeal_isHomogeneous

/--
info: 'HomogeneousIdealQuotientGrading.gateHomogeneousIdeal' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.gateHomogeneousIdeal

/--
info: 'HomogeneousIdealQuotientGrading.gate_gateIdeal_ne_bot' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.gate_gateIdeal_ne_bot

/--
info: 'HomogeneousIdealQuotientGrading.gate_mk_X0X1_eq_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.gate_mk_X0X1_eq_zero

/--
info: 'HomogeneousIdealQuotientGrading.gate_X0_not_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.gate_X0_not_mem

/--
info: 'HomogeneousIdealQuotientGrading.gate_mk_X0_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.gate_mk_X0_ne_zero

/--
info: 'HomogeneousIdealQuotientGrading.gate_mk_X0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.gate_mk_X0_mem

/--
info: 'HomogeneousIdealQuotientGrading.gateGradedRing' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.gateGradedRing

/--
info: 'HomogeneousIdealQuotientGrading.gateGradedAlgebra' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.gateGradedAlgebra

/--
info: 'HomogeneousIdealQuotientGrading.gate_decompose_mk_X0' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms HomogeneousIdealQuotientGrading.gate_decompose_mk_X0

Statements phrased using this module (0)

No statement module imports it directly (it is used through other definition modules or by proofs).