Project.Potions.Basic

@[reducible, inline]

noncomputable abbrev HomogeneousSubmonoid.Potion {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} (S : HomogeneousSubmonoid 𝒜) :

Type (max u_1 u_3)

Equations

S.Potion = HomogeneousLocalization 𝒜 S.toSubmonoid

Instances For

source

noncomputable def HomogeneousSubmonoid.potionToMap {ι : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] [CommRing B] [Algebra R B] {ℬ : ι → Submodule R B} [GradedAlgebra ℬ] (S : HomogeneousSubmonoid 𝒜) (Φ : GradedRingHom 𝒜 ℬ) :

S.Potion →+* (HomogeneousSubmonoid.map Φ S).Potion

Equations

S.potionToMap Φ = HomogeneousLocalization.map 𝒜 ℬ ↑Φ ⋯ ⋯

Instances For

source

@[simp]

theorem HomogeneousSubmonoid.potionToMap_mk {ι : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] [CommRing B] [Algebra R B] {ℬ : ι → Submodule R B} [GradedAlgebra ℬ] (S : HomogeneousSubmonoid 𝒜) (Φ : GradedRingHom 𝒜 ℬ) (x : HomogeneousLocalization.NumDenSameDeg 𝒜 S.toSubmonoid) :

(S.potionToMap Φ) (HomogeneousLocalization.mk x) = HomogeneousLocalization.mk { deg := x.deg, num := ⟨Φ ↑x.num, ⋯⟩, den := ⟨Φ ↑x.den, ⋯⟩, den_mem := ⋯ }

source

noncomputable def HomogeneousSubmonoid.potionEquiv {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] {S T : HomogeneousSubmonoid 𝒜} (eq : S = T) :

S.Potion ≃+* T.Potion

Equations

HomogeneousSubmonoid.potionEquiv eq = RingEquiv.ofHomInv (HomogeneousLocalization.map 𝒜 𝒜 (RingHom.id A) ⋯ ⋯) (HomogeneousLocalization.map 𝒜 𝒜 (RingHom.id A) ⋯ ⋯) ⋯ ⋯

Instances For

source

@[simp]

theorem HomogeneousSubmonoid.potionEquiv_mk {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] {S T : HomogeneousSubmonoid 𝒜} (eq : S = T) (x : HomogeneousLocalization.NumDenSameDeg 𝒜 S.toSubmonoid) :

(HomogeneousSubmonoid.potionEquiv eq) (HomogeneousLocalization.mk x) = HomogeneousLocalization.mk { deg := x.deg, num := ⟨↑x.num, ⋯⟩, den := ⟨↑x.den, ⋯⟩, den_mem := ⋯ }

source

@[simp]

theorem HomogeneousSubmonoid.potionEquiv_mk' {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] {S T : HomogeneousSubmonoid 𝒜} (eq : S = T) (x : HomogeneousLocalization.NumDenSameDeg 𝒜 S.toSubmonoid) :

(HomogeneousSubmonoid.potionEquiv eq) (Quotient.mk'' x) = HomogeneousLocalization.mk { deg := x.deg, num := ⟨↑x.num, ⋯⟩, den := ⟨↑x.den, ⋯⟩, den_mem := ⋯ }

source

@[simp]

theorem HomogeneousSubmonoid.potionEquiv_refl {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] (S : HomogeneousSubmonoid 𝒜) :

HomogeneousSubmonoid.potionEquiv ⋯ = RingEquiv.refl S.Potion

source

@[simp]

theorem HomogeneousSubmonoid.potionEquiv_refl_apply {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] (S : HomogeneousSubmonoid 𝒜) (x : S.Potion) :

(HomogeneousSubmonoid.potionEquiv ⋯) x = x

source

@[simp]

theorem HomogeneousSubmonoid.potionEquiv_symm {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] {R✝ S : HomogeneousSubmonoid 𝒜} (eq : R✝ = S) :

(HomogeneousSubmonoid.potionEquiv eq).symm = HomogeneousSubmonoid.potionEquiv ⋯

source

@[simp]

theorem HomogeneousSubmonoid.potionEquiv_symm_apply {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] {R✝ S : HomogeneousSubmonoid 𝒜} (eq : R✝ = S) (x : S.Potion) :

(HomogeneousSubmonoid.potionEquiv eq).symm x = (HomogeneousSubmonoid.potionEquiv ⋯) x

source

@[simp]

theorem HomogeneousSubmonoid.potionEquiv_trans {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] {R✝ S T : HomogeneousSubmonoid 𝒜} (eq1 : R✝ = S) (eq2 : S = T) :

(HomogeneousSubmonoid.potionEquiv eq1).trans (HomogeneousSubmonoid.potionEquiv eq2) = HomogeneousSubmonoid.potionEquiv ⋯

source

@[simp]

theorem HomogeneousSubmonoid.potionEquiv_comp {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] {R✝ S T : HomogeneousSubmonoid 𝒜} (eq1 : R✝ = S) (eq2 : S = T) :

(HomogeneousSubmonoid.potionEquiv eq2).toRingHom.comp (HomogeneousSubmonoid.potionEquiv eq1).toRingHom = (HomogeneousSubmonoid.potionEquiv ⋯).toRingHom

source

@[simp]

theorem HomogeneousSubmonoid.potionEquiv_trans_apply {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] {R✝ S T : HomogeneousSubmonoid 𝒜} (eq1 : R✝ = S) (eq2 : S = T) (x : R✝.Potion) :

(HomogeneousSubmonoid.potionEquiv eq2) ((HomogeneousSubmonoid.potionEquiv eq1) x) = (HomogeneousSubmonoid.potionEquiv ⋯) x

source

theorem HomogeneousSubmonoid.potionToMap_comp_potionEquiv {ι : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] [CommRing B] [Algebra R B] {ℬ : ι → Submodule R B} [GradedAlgebra ℬ] (S T : HomogeneousSubmonoid 𝒜) (Φ : GradedRingHom 𝒜 ℬ) (eq : S = T) :

(S.potionToMap Φ).comp (HomogeneousSubmonoid.potionEquiv ⋯).toRingHom = (HomogeneousSubmonoid.potionEquiv ⋯).toRingHom.comp (T.potionToMap Φ)

source

noncomputable def HomogeneousSubmonoid.potionToMul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] (S T : HomogeneousSubmonoid 𝒜) :

S.Potion →+* (S * T).Potion

Equations

S.potionToMul T = HomogeneousLocalization.map 𝒜 𝒜 (RingHom.id A) ⋯ ⋯

Instances For

source

noncomputable def HomogeneousSubmonoid.potionToMulSelf {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] (S : HomogeneousSubmonoid 𝒜) :

S.Potion ≃+* (S * S).Potion

Equations

S.potionToMulSelf = HomogeneousSubmonoid.potionEquiv ⋯

Instances For

source

@[simp]

theorem HomogeneousSubmonoid.potionToMul_mk {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] (S T : HomogeneousSubmonoid 𝒜) (x : HomogeneousLocalization.NumDenSameDeg 𝒜 S.toSubmonoid) :

(S.potionToMul T) (HomogeneousLocalization.mk x) = HomogeneousLocalization.mk { deg := x.deg, num := x.num, den := x.den, den_mem := ⋯ }

source

@[simp]

theorem HomogeneousSubmonoid.potionToMul_mk' {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] (S T : HomogeneousSubmonoid 𝒜) (x : HomogeneousLocalization.NumDenSameDeg 𝒜 S.toSubmonoid) :

(S.potionToMul T) (Quotient.mk'' x) = HomogeneousLocalization.mk { deg := x.deg, num := x.num, den := x.den, den_mem := ⋯ }

source

theorem HomogeneousSubmonoid.potionToMul_comp_potionToMap {ι : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] [CommRing B] [Algebra R B] {ℬ : ι → Submodule R B} [GradedAlgebra ℬ] (S T : HomogeneousSubmonoid 𝒜) (Φ : GradedRingHom 𝒜 ℬ) :

((HomogeneousSubmonoid.map Φ S).potionToMul (HomogeneousSubmonoid.map Φ T)).comp (S.potionToMap Φ) = ((HomogeneousSubmonoid.potionEquiv ⋯).toRingHom.comp ((S * T).potionToMap Φ)).comp (S.potionToMul T)

source

@[simp]

theorem HomogeneousSubmonoid.potionEquiv_potionToMul_assoc {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] {R✝ S T : HomogeneousSubmonoid 𝒜} (x : R✝.Potion) :

((R✝ * S).potionToMul T) ((R✝.potionToMul S) x) = (HomogeneousSubmonoid.potionEquiv ⋯) ((R✝.potionToMul (S * T)) x)

source

noncomputable instance HomogeneousSubmonoid.instAlgebraPotionHMulSubmodule {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] (S T : HomogeneousSubmonoid 𝒜) :

Algebra S.Potion (S * T).Potion

Equations

S.instAlgebraPotionHMulSubmodule T = (S.potionToMul T).toAlgebra

source

@[simp]

theorem HomogeneousSubmonoid.mul_potion_algebraMap_eq {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] (S T : HomogeneousSubmonoid 𝒜) :

algebraMap S.Potion (S * T).Potion = S.potionToMul T

source

noncomputable def HomogeneousSubmonoid.toBarPotion {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] (S : HomogeneousSubmonoid 𝒜) :

S.Potion →+* S.bar.Potion

Equations

S.toBarPotion = HomogeneousLocalization.map 𝒜 𝒜 (RingHom.id A) ⋯ ⋯

Instances For

source

@[simp]

theorem HomogeneousSubmonoid.toBarPotion_mk {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] (S : HomogeneousSubmonoid 𝒜) (x : HomogeneousLocalization.NumDenSameDeg 𝒜 S.toSubmonoid) :

S.toBarPotion (HomogeneousLocalization.mk x) = HomogeneousLocalization.mk { deg := x.deg, num := x.num, den := x.den, den_mem := ⋯ }

source

@[simp]

theorem HomogeneousSubmonoid.toBarPotion_mk' {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] (S : HomogeneousSubmonoid 𝒜) (x : HomogeneousLocalization.NumDenSameDeg 𝒜 S.toSubmonoid) :

S.toBarPotion (Quotient.mk'' x) = HomogeneousLocalization.mk { deg := x.deg, num := x.num, den := x.den, den_mem := ⋯ }

source

theorem HomogeneousSubmonoid.toBarPotion_surjective {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] (S : HomogeneousSubmonoid 𝒜) :

Function.Surjective ⇑S.toBarPotion

source

theorem HomogeneousSubmonoid.toBarPotion_injective {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] (S : HomogeneousSubmonoid 𝒜) :

Function.Injective ⇑S.toBarPotion

source

noncomputable def HomogeneousSubmonoid.equivBarPotion {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] (S : HomogeneousSubmonoid 𝒜) :

S.Potion ≃+* S.bar.Potion

Equations

S.equivBarPotion = RingEquiv.ofBijective S.toBarPotion ⋯

Instances For

source

theorem HomogeneousSubmonoid.equivBarPotion_apply {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] (S : HomogeneousSubmonoid 𝒜) (x : S.Potion) :

S.equivBarPotion x = S.toBarPotion x

source

theorem HomogeneousSubmonoid.equivBarPotion_symm_apply {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] (S : HomogeneousSubmonoid 𝒜) (i j : ι) (m n : A) (m_mem : m ∈ 𝒜 i) (n_mem : n ∈ 𝒜 i) (z : A) (z_mem : z ∈ 𝒜 j) (hz : n * z ∈ S) :

S.equivBarPotion.symm (HomogeneousLocalization.mk { deg := i, num := ⟨m, m_mem⟩, den := ⟨n, n_mem⟩, den_mem := ⋯ }) = HomogeneousLocalization.mk { deg := i + j, num := ⟨m * z, ⋯⟩, den := ⟨n * z, ⋯⟩, den_mem := hz }

source

theorem HomogeneousSubmonoid.toMul_equivBarPotion_symm {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] (S T : HomogeneousSubmonoid 𝒜) (x : HomogeneousLocalization.NumDenSameDeg 𝒜 S.bar.toSubmonoid) :

(S.potionToMul T) (S.equivBarPotion.symm (HomogeneousLocalization.mk x)) = (S * T).equivBarPotion.symm (HomogeneousLocalization.mk { deg := x.deg, num := x.num, den := x.den, den_mem := ⋯ })

source

noncomputable instance HomogeneousSubmonoid.instAlgebraPotionBarSubmodule {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] (S : HomogeneousSubmonoid 𝒜) :

Algebra S.Potion S.bar.Potion

Equations

S.instAlgebraPotionBarSubmodule = (↑S.equivBarPotion).toAlgebra

source

@[simp]

theorem HomogeneousSubmonoid.bar_potion_algebraMap_eq {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] (S : HomogeneousSubmonoid 𝒜) :

algebraMap S.Potion S.bar.Potion = ↑S.equivBarPotion

source

structure HomogeneousSubmonoid.PotionGen {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] (S T : HomogeneousSubmonoid 𝒜) :

Type (max (max u_1 u_3) (u_5 + 1))

index : Type u_5
elem : self.index → A
elem_mem (t : self.index) : self.elem t ∈ T
gen : Submonoid.closure (Set.range self.elem) = T.toSubmonoid
n : self.index → ℕ+
s : self.index → A
s' : self.index → A
s_mem_bar (t : self.index) : self.s t ∈ S.bar
s'_mem_bar (t : self.index) : self.s' t ∈ S.bar
i : self.index → ι
i' : self.index → ι
t_deg (t : self.index) : self.elem t ^ ↑(self.n t) ∈ 𝒜 (self.i t - self.i' t)
s_deg (t : self.index) : self.s t ∈ 𝒜 (self.i t)
s'_deg (t : self.index) : self.s' t ∈ 𝒜 (self.i' t)

Instances For

source

noncomputable def HomogeneousSubmonoid.PotionGen.genSubmonoid {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] {S T : HomogeneousSubmonoid 𝒜} (T' : S.PotionGen T) :

Submonoid S.Potion

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem HomogeneousSubmonoid.finite_potionGen_exists_aux₁ {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] {S : HomogeneousSubmonoid 𝒜} (S_rel : S.IsRelevant) (t : A) (m : ι) (ht : t ∈ 𝒜 m) :

∃ (n : ℕ+) (s : A) (s' : A) (i : ι) (i' : ι), t ^ ↑n ∈ 𝒜 (i - i') ∧ s ∈ 𝒜 i ∧ s' ∈ 𝒜 i' ∧ s ∈ S.bar ∧ s' ∈ S.bar

source

theorem HomogeneousSubmonoid.finite_potionGen_exists_aux₂ {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] {S : HomogeneousSubmonoid 𝒜} (S_rel : S.IsRelevant) (t : A) (ht : SetLike.Homogeneous 𝒜 t) :

∃ (n : ℕ+) (s : A) (s' : A) (i : ι) (i' : ι), t ^ ↑n ∈ 𝒜 (i - i') ∧ s ∈ 𝒜 i ∧ s' ∈ 𝒜 i' ∧ s ∈ S.bar ∧ s' ∈ S.bar

source

noncomputable def HomogeneousSubmonoid.finitePotionGen {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] {S T : HomogeneousSubmonoid 𝒜} (S_rel : S.IsRelevant) (T_fg : T.FG) :

S.PotionGen T

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem HomogeneousSubmonoid.finitePotionGen_finite {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] {S T : HomogeneousSubmonoid 𝒜} (S_rel : S.IsRelevant) (T_fg : T.FG) :

Finite (HomogeneousSubmonoid.finitePotionGen S_rel T_fg).index

source

noncomputable def HomogeneousSubmonoid.PotionGen.disjUnion {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] {R✝ S T : HomogeneousSubmonoid 𝒜} (R' : S.PotionGen R✝) (T' : S.PotionGen T) :

S.PotionGen (R✝ * T)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem HomogeneousSubmonoid.PotionGen.disjUnion_genSubmonoid {ι : Type u_1} {R : Type u_2} {A : Type u_3} [AddCommGroup ι] [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ι → Submodule R A} [DecidableEq ι] [GradedAlgebra 𝒜] {R✝ S T : HomogeneousSubmonoid 𝒜} (R' : S.PotionGen R✝) (T' : S.PotionGen T) :

(R'.disjUnion T').genSubmonoid = R'.genSubmonoid * T'.genSubmonoid