Project.HomogeneousSubmonoid.Basic

source

structure HomogeneousSubmonoid {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [CommRing A] [SetLike σ A] (𝒜 : ι → σ) extends Submonoid A :

Type u_2

carrier : Set A
mul_mem' {a b : A} : a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
one_mem' : 1 ∈ self.carrier
homogeneous_gen : ∃ (s : Set A), self.toSubmonoid = Submonoid.closure s ∧ ∀ x ∈ s, SetLike.Homogeneous 𝒜 x

Instances For

source

theorem HomogeneousSubmonoid.ext {ι : Type u_1} {A : Type u_2} {σ : Type u_4} {inst✝ : CommRing A} {inst✝¹ : SetLike σ A} {𝒜 : ι → σ} {x y : HomogeneousSubmonoid 𝒜} (carrier : x.carrier = y.carrier) :

x = y

source

theorem HomogeneousSubmonoid.toSubmonoid_injective {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [CommRing A] [SetLike σ A] (𝒜 : ι → σ) :

Function.Injective HomogeneousSubmonoid.toSubmonoid

source

instance HomogeneousSubmonoid.instSetLike {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [CommRing A] [SetLike σ A] {𝒜 : ι → σ} :

SetLike (HomogeneousSubmonoid 𝒜) A

Equations

HomogeneousSubmonoid.instSetLike = { coe := fun (S : HomogeneousSubmonoid 𝒜) => ↑S.toSubmonoid, coe_injective' := ⋯ }

source

theorem HomogeneousSubmonoid.mem_iff {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) (x : A) :

x ∈ S ↔ x ∈ S.toSubmonoid

source

@[simp]

theorem HomogeneousSubmonoid.mem_toSubmonoid_iff {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) (x : A) :

x ∈ S.toSubmonoid ↔ x ∈ S

source

instance HomogeneousSubmonoid.instSubmonoidClass {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [CommRing A] [SetLike σ A] {𝒜 : ι → σ} :

SubmonoidClass (HomogeneousSubmonoid 𝒜) A

source

theorem HomogeneousSubmonoid.homogeneous {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S : HomogeneousSubmonoid 𝒜) {x : A} :

x ∈ S → SetLike.Homogeneous 𝒜 x

source

def HomogeneousSubmonoid.map {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {σ' : Type u_5} [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [CommRing B] [SetLike σ' B] {ℬ : ι → σ'} (Φ : GradedRingHom 𝒜 ℬ) (S : HomogeneousSubmonoid 𝒜) :

HomogeneousSubmonoid ℬ

Equations

HomogeneousSubmonoid.map Φ S = { toSubmonoid := Submonoid.map Φ S.toSubmonoid, homogeneous_gen := ⋯ }

Instances For

source

theorem HomogeneousSubmonoid.map_toSubmonoid {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {σ' : Type u_5} [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [CommRing B] [SetLike σ' B] {ℬ : ι → σ'} (Φ : GradedRingHom 𝒜 ℬ) (S : HomogeneousSubmonoid 𝒜) :

(HomogeneousSubmonoid.map Φ S).toSubmonoid = Submonoid.map Φ S.toSubmonoid

source

theorem HomogeneousSubmonoid.mem_map_of_mem {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {σ' : Type u_5} [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [CommRing B] [SetLike σ' B] {ℬ : ι → σ'} (Φ : GradedRingHom 𝒜 ℬ) {S : HomogeneousSubmonoid 𝒜} {x : A} :

x ∈ S → Φ x ∈ HomogeneousSubmonoid.map Φ S

source

def HomogeneousSubmonoid.closure {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (s : Set A) (hs : ∀ x ∈ s, SetLike.Homogeneous 𝒜 x) :

HomogeneousSubmonoid 𝒜

Equations

HomogeneousSubmonoid.closure s hs = { toSubmonoid := Submonoid.closure s, homogeneous_gen := ⋯ }

Instances For

source

theorem HomogeneousSubmonoid.mem_closure_singleton {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (a : A) (ha : SetLike.Homogeneous 𝒜 a) (x : A) :

x ∈ HomogeneousSubmonoid.closure {a} ⋯ ↔ ∃ (n : ℕ), x = a ^ n

source

def HomogeneousSubmonoid.bot {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] :

HomogeneousSubmonoid 𝒜

Equations

HomogeneousSubmonoid.bot = { carrier := {1}, mul_mem' := ⋯, one_mem' := ⋯, homogeneous_gen := ⋯ }

Instances For

source

@[simp]

theorem HomogeneousSubmonoid.bot_carrier {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] :

↑HomogeneousSubmonoid.bot = {1}

source

@[simp]

theorem HomogeneousSubmonoid.mem_bot {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (x : A) :

x ∈ HomogeneousSubmonoid.bot ↔ x = 1

source

instance HomogeneousSubmonoid.instOne {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] :

One (HomogeneousSubmonoid 𝒜)

Equations

HomogeneousSubmonoid.instOne = { one := HomogeneousSubmonoid.bot }

source

@[simp]

theorem HomogeneousSubmonoid.mem_one {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (x : A) :

x ∈ 1 ↔ x = 1

source

instance HomogeneousSubmonoid.instMul {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] :

Mul (HomogeneousSubmonoid 𝒜)

Equations

HomogeneousSubmonoid.instMul = { mul := fun (S T : HomogeneousSubmonoid 𝒜) => { toSubmonoid := S.toSubmonoid * T.toSubmonoid, homogeneous_gen := ⋯ } }

source

@[simp]

theorem HomogeneousSubmonoid.mul_toSubmonoid {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S T : HomogeneousSubmonoid 𝒜) :

(S * T).toSubmonoid = S.toSubmonoid * T.toSubmonoid

source

theorem HomogeneousSubmonoid.mem_mul_iff {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] {S T : HomogeneousSubmonoid 𝒜} (x : A) :

x ∈ S * T ↔ ∃ s ∈ S, ∃ t ∈ T, x = s * t

source

@[simp]

theorem HomogeneousSubmonoid.mul_self {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S : HomogeneousSubmonoid 𝒜) :

S * S = S

source

instance HomogeneousSubmonoid.instCommMonoid {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] :

CommMonoid (HomogeneousSubmonoid 𝒜)

Equations

HomogeneousSubmonoid.instCommMonoid = CommMonoid.mk ⋯

source

theorem HomogeneousSubmonoid.map_mul {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {σ' : Type u_5} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] [CommRing B] [SetLike σ' B] {ℬ : ι → σ'} [AddSubgroupClass σ' B] [GradedRing ℬ] (Φ : GradedRingHom 𝒜 ℬ) (S T : HomogeneousSubmonoid 𝒜) :

HomogeneousSubmonoid.map Φ (S * T) = HomogeneousSubmonoid.map Φ S * HomogeneousSubmonoid.map Φ T

source

def HomogeneousSubmonoid.bar {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S : HomogeneousSubmonoid 𝒜) :

HomogeneousSubmonoid 𝒜

Equations

S.bar = { carrier := {x : A | SetLike.Homogeneous 𝒜 x ∧ ∃ y ∈ S, x ∣ y}, mul_mem' := ⋯, one_mem' := ⋯, homogeneous_gen := ⋯ }

Instances For

source

@[simp]

theorem HomogeneousSubmonoid.mem_bar {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S : HomogeneousSubmonoid 𝒜) (x : A) :

x ∈ S.bar ↔ SetLike.Homogeneous 𝒜 x ∧ ∃ y ∈ S, x ∣ y

source

instance HomogeneousSubmonoid.instPartialOrder {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [CommRing A] [SetLike σ A] {𝒜 : ι → σ} :

PartialOrder (HomogeneousSubmonoid 𝒜)

Equations

HomogeneousSubmonoid.instPartialOrder = PartialOrder.lift (fun (S : HomogeneousSubmonoid 𝒜) => S.toSubmonoid) ⋯

source

theorem HomogeneousSubmonoid.bar_mono {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S T : HomogeneousSubmonoid 𝒜) :

S ≤ T → S.bar ≤ T.bar

source

theorem HomogeneousSubmonoid.le_iff {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S T : HomogeneousSubmonoid 𝒜) :

S ≤ T ↔ S.toSubmonoid ≤ T.toSubmonoid

source

theorem HomogeneousSubmonoid.left_le_mul {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S T : HomogeneousSubmonoid 𝒜) :

S ≤ S * T

source

theorem HomogeneousSubmonoid.right_le_mul {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S T : HomogeneousSubmonoid 𝒜) :

T ≤ S * T

source

instance HomogeneousSubmonoid.instCommMonoid_1 {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] :

CommMonoid (HomogeneousSubmonoid 𝒜)

Equations

HomogeneousSubmonoid.instCommMonoid_1 = CommMonoid.mk ⋯

source

theorem HomogeneousSubmonoid.le_bar {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S : HomogeneousSubmonoid 𝒜) :

S ≤ S.bar

source

theorem HomogeneousSubmonoid.mem_bot_bar {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (x : A) :

x ∈ HomogeneousSubmonoid.bot.bar ↔ SetLike.Homogeneous 𝒜 x ∧ ∃ (y : A), x * y = 1

source

def HomogeneousSubmonoid.deg {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S : HomogeneousSubmonoid 𝒜) :

AddSubmonoid ι

Equations

S.deg = { carrier := {i : ι | ∃ x ∈ S, x ∈ 𝒜 i}, add_mem' := ⋯, zero_mem' := ⋯ }

Instances For

source

@[simp]

theorem HomogeneousSubmonoid.coe_deg {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S : HomogeneousSubmonoid 𝒜) :

↑S.deg = {i : ι | ∃ x ∈ S, x ∈ 𝒜 i}

source

@[simp]

theorem HomogeneousSubmonoid.mem_deg_iff {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S : HomogeneousSubmonoid 𝒜) (i : ι) :

i ∈ S.deg ↔ ∃ x ∈ S, x ∈ 𝒜 i

source

theorem HomogeneousSubmonoid.deg_mono {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S T : HomogeneousSubmonoid 𝒜) :

S ≤ T → S.deg ≤ T.deg

source

@[simp]

theorem HomogeneousSubmonoid.closure_one {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] :

HomogeneousSubmonoid.closure {1} ⋯ = HomogeneousSubmonoid.bot

source

theorem HomogeneousSubmonoid.mem_deg_singleton {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (a : A) (ha : SetLike.Homogeneous 𝒜 a) (x : ι) :

x ∈ (HomogeneousSubmonoid.closure {a} ⋯).deg ↔ ∃ (n : ℕ), a ^ n ∈ 𝒜 x

source

theorem HomogeneousSubmonoid.mem_deg {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S : HomogeneousSubmonoid 𝒜) {i : ι} :

i ∈ S.deg ↔ ∃ x ∈ S, x ∈ 𝒜 i

source

theorem HomogeneousSubmonoid.zero_mem_deg {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S : HomogeneousSubmonoid 𝒜) [Nontrivial A] :

0 ∈ S.deg

source

def HomogeneousSubmonoid.monDeg {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S : HomogeneousSubmonoid 𝒜) :

AddSubmonoid ι

Equations

S.monDeg = AddSubmonoid.closure ↑S.deg

Instances For

source

def HomogeneousSubmonoid.«term_[_⟩» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

def HomogeneousSubmonoid.agrDeg {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S : HomogeneousSubmonoid 𝒜) :

AddSubgroup ι

Equations

S.agrDeg = AddSubgroup.closure ↑S.deg

Instances For

source

def HomogeneousSubmonoid.«term_[_]» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

noncomputable def HomogeneousSubmonoid.agrDegEquiv {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S : HomogeneousSubmonoid 𝒜) :

AddGR ↥S.monDeg ≃+ ↥S.agrDeg

Equations

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

Instances For

source

noncomputable def HomogeneousSubmonoid.convMonDegEmbedding {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S : HomogeneousSubmonoid 𝒜) :

TensorProduct ℕ NNReal ↥S.monDeg →ₗ[NNReal ] TensorProduct ℤ ℝ ι

Equations

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

Instances For

source

@[simp]

theorem HomogeneousSubmonoid.convMonDegEmbedding_apply_tmul {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S : HomogeneousSubmonoid 𝒜) (r : NNReal) (i : ↥S.monDeg) :

S.convMonDegEmbedding (r ⊗ₜ[ℕ ] i) = ↑r ⊗ₜ[ℤ ] ↑i

source

noncomputable def HomogeneousSubmonoid.convMonDeg {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S : HomogeneousSubmonoid 𝒜) :

Submodule NNReal (TensorProduct ℤ ℝ ι)

Equations

S.convMonDeg = LinearMap.range S.convMonDegEmbedding

Instances For

source

noncomputable def HomogeneousSubmonoid.convMonDeg' {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S : HomogeneousSubmonoid 𝒜) :

Submodule NNReal (TensorProduct ℤ ℝ ι)

Equations

S.convMonDeg' = Submodule.span NNReal {x : TensorProduct ℤ ℝ ι | ∃ (a : NNReal) (i : ι) (_ : i ∈ S.deg), x = ↑a ⊗ₜ[ℤ ] i}

Instances For

source

def HomogeneousSubmonoid.«term_[_⟩ℝ≥0» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

theorem HomogeneousSubmonoid.mem_convMonDeg {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S : HomogeneousSubmonoid 𝒜) [Nontrivial A] (x : TensorProduct ℤ ℝ ι) :

x ∈ S.convMonDeg ↔ ∃ (s : ι →₀ NNReal), (∀ i ∈ s.support, i ∈ S.deg) ∧ x = ∑ i ∈ s.support, ↑(s i) ⊗ₜ[ℤ ] i

source

def HomogeneousSubmonoid.IsRelevant {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S : HomogeneousSubmonoid 𝒜) :

Prop

Equations

S.IsRelevant = ∀ (i : ι), ∃ (n : ℕ), 0 < n ∧ n • i ∈ S.bar.agrDeg

Instances For

source

theorem HomogeneousSubmonoid.IsRelevant.mul {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] {S T : HomogeneousSubmonoid 𝒜} (S_rel : S.IsRelevant) (T_rel : T.IsRelevant) :

(S * T).IsRelevant

source

theorem HomogeneousSubmonoid.IsRelevant.map {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {σ' : Type u_5} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] [CommRing B] [SetLike σ' B] {ℬ : ι → σ'} [AddSubgroupClass σ' B] [GradedRing ℬ] {S : HomogeneousSubmonoid 𝒜} (S_rel : S.IsRelevant) (Φ : GradedRingHom 𝒜 ℬ) :

(HomogeneousSubmonoid.map Φ S).IsRelevant

source

theorem HomogeneousSubmonoid.isRelevant_iff_isTorsion_quotient {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S : HomogeneousSubmonoid 𝒜) :

S.IsRelevant ↔ AddMonoid.IsTorsion (ι ⧸ S.bar.agrDeg)

source

theorem HomogeneousSubmonoid.isRelevant_iff_finite_quotient_of_FG {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S : HomogeneousSubmonoid 𝒜) [AddGroup.FG ι] :

S.IsRelevant ↔ Finite (ι ⧸ S.bar.agrDeg)

source

theorem HomogeneousSubmonoid.isRelevant_iff_finiteIndex_of_FG {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (S : HomogeneousSubmonoid 𝒜) [AddGroup.FG ι] :

S.IsRelevant ↔ S.bar.agrDeg.FiniteIndex

source

@[reducible, inline]

abbrev HomogeneousSubmonoid.SetIsRelevant {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (s : Set A) (hs : ∀ i ∈ s, SetLike.Homogeneous 𝒜 i) :

Prop

Equations

HomogeneousSubmonoid.SetIsRelevant s hs = (HomogeneousSubmonoid.closure s hs).IsRelevant

Instances For

source

@[reducible, inline]

abbrev HomogeneousSubmonoid.ElemIsRelevant {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] (a : A) (ha : SetLike.Homogeneous 𝒜 a) :

Prop

Equations

HomogeneousSubmonoid.ElemIsRelevant a ha = (HomogeneousSubmonoid.closure {a} ⋯).IsRelevant

Instances For

source

theorem AddSubgroup.closure_add_image_add_eq_top {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {R S : Set G} (hR : AddSubgroup.IsComplement (↑H) R) (hR1 : 0 ∈ R) (hS : AddSubgroup.closure S = ⊤) :

↑(AddSubgroup.closure ((fun (g : G) => g + -↑(hR.toRightFun g)) '' (R + S))) + R = ⊤

source

theorem AddSubgroup.closure_add_image_eq {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {R S : Set G} (hR : AddSubgroup.IsComplement (↑H) R) (hR1 : 0 ∈ R) (hS : AddSubgroup.closure S = ⊤) :

AddSubgroup.closure ((fun (g : G) => g + -↑(hR.toRightFun g)) '' (R + S)) = H

source

theorem AddSubgroup.closure_add_image_eq_top {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {R S : Set G} (hR : AddSubgroup.IsComplement (↑H) R) (hR1 : 0 ∈ R) (hS : AddSubgroup.closure S = ⊤) :

AddSubgroup.closure ((fun (g : G) => ⟨g + -↑(hR.toRightFun g), ⋯⟩) '' (R + S)) = ⊤

source

theorem AddSubgroup.closure_add_image_eq_top' {G : Type u_1} [AddGroup G] {H : AddSubgroup G} [DecidableEq G] {R S : Finset G} (hR : AddSubgroup.IsComplement ↑H ↑R) (hR1 : 0 ∈ R) (hS : AddSubgroup.closure ↑S = ⊤) :

AddSubgroup.closure ↑(Finset.image (fun (g : G) => ⟨g + -↑(hR.toRightFun g), ⋯⟩) (R + S)) = ⊤

source

theorem AddSubgroup.exists_finset_card_le_add {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [H.FiniteIndex] {S : Finset G} (hS : AddSubgroup.closure ↑S = ⊤) :

∃ (T : Finset ↥H), T.card ≤ H.index * S.card ∧ AddSubgroup.closure ↑T = ⊤

source

instance AddSubgroup.fg_of_index_ne_zero {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [hG : AddGroup.FG G] [H.FiniteIndex] :

AddGroup.FG ↥H

source

theorem HomogeneousSubmonoid.exists_factorisation_of_elemIsRelevant {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] [AddGroup.FG ι] (a : A) (ha : SetLike.Homogeneous 𝒜 a) (a_rel : HomogeneousSubmonoid.ElemIsRelevant a ha) :

∃ (n : ℕ) (x : Fin n → A) (d : Fin n → ι) (_ : ∀ (i : Fin n), x i ∈ 𝒜 (d i)), (AddSubgroup.closure (Set.range d)).FiniteIndex ∧ ∃ (k : ℕ), ∏ i : Fin n, x i = a ^ k

source

theorem HomogeneousSubmonoid.elemIsRelevant_of_homogeneous_of_factorisation {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] [AddGroup.FG ι] (a : A) (ha : SetLike.Homogeneous 𝒜 a) (n : ℕ) (x : Fin n → A) (d : Fin n → ι) (mem : ∀ (i : Fin n), x i ∈ 𝒜 (d i)) (finiteIndex : (AddSubgroup.closure (Set.range d)).FiniteIndex) (k : ℕ) (eq : ∏ i : Fin n, x i = a ^ k) :

HomogeneousSubmonoid.ElemIsRelevant a ha

source

theorem HomogeneousSubmonoid.elemIsRelevant_iff {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] [AddGroup.FG ι] (a : A) (ha : SetLike.Homogeneous 𝒜 a) :

HomogeneousSubmonoid.ElemIsRelevant a ha ↔ ∃ (n : ℕ) (x : Fin n → A) (d : Fin n → ι) (_ : ∀ (i : Fin n), x i ∈ 𝒜 (d i)), (AddSubgroup.closure (Set.range d)).FiniteIndex ∧ ∃ (k : ℕ), ∏ i : Fin n, x i = a ^ k

source

def HomogeneousSubmonoid.dagger {ι : Type u_1} {A : Type u_2} {σ : Type u_4} [AddCommGroup ι] [CommRing A] [SetLike σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddSubgroupClass σ A] [GradedRing 𝒜] :

HomogeneousIdeal 𝒜

Equations

HomogeneousSubmonoid.dagger 𝒜 = { toSubmodule := Ideal.span {x : A | ∃ (h : SetLike.Homogeneous 𝒜 x), HomogeneousSubmonoid.ElemIsRelevant x h}, is_homogeneous' := ⋯ }

Instances For

source

def HomogeneousSubmonoid.«term_†» :

Lean.TrailingParserDescr

Equations

HomogeneousSubmonoid.«term_†» = Lean.ParserDescr.trailingNode `HomogeneousSubmonoid.«term_†» 1024 1024 (Lean.ParserDescr.symbol "†")

Instances For