structure HomogeneousSubmonoid.PreLocalizationGrading {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) (i : ι) : Type (max u_1 u_2)

• num : A
• den : ↥S.toSubmonoid
• degNum : ι
• degDen : ι
• num_mem : self.num ∈ 𝒜 self.degNum
• den_mem : ↑self.den ∈ 𝒜 self.degDen
• deg_frac_eq : self.degNum - self.degDen = i

theorem HomogeneousSubmonoid.PreLocalizationGrading.ext {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) {i : ι} (x y : S.PreLocalizationGrading i) (num_eq : x.num = y.num) (den_eq : x.den = y.den) (degNum_eq : x.degNum = y.degNum) (degDen_eq : x.degDen = y.degDen) : x = y

instance HomogeneousSubmonoid.PreLocalizationGrading.instNeg {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] (i : ι) : Neg (S.PreLocalizationGrading i)

Equations

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

@[simp]

theorem HomogeneousSubmonoid.PreLocalizationGrading.neg_num {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] {i : ι} (x : S.PreLocalizationGrading i) : (-x).num = -x.num

@[simp]

theorem HomogeneousSubmonoid.PreLocalizationGrading.neg_den {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] {i : ι} (x : S.PreLocalizationGrading i) : (-x).den = x.den

@[simp]

theorem HomogeneousSubmonoid.PreLocalizationGrading.neg_degNum {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] {i : ι} (x : S.PreLocalizationGrading i) : (-x).degNum = x.degNum

@[simp]

theorem HomogeneousSubmonoid.PreLocalizationGrading.neg_degDen {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] {i : ι} (x : S.PreLocalizationGrading i) : (-x).degDen = x.degDen

instance HomogeneousSubmonoid.PreLocalizationGrading.instAdd {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] (i : ι) : Add (S.PreLocalizationGrading i)

Equations

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

@[simp]

theorem HomogeneousSubmonoid.PreLocalizationGrading.add_num {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] {i : ι} (x y : S.PreLocalizationGrading i) : (x + y).num = ↑x.den * y.num + ↑y.den * x.num

@[simp]

theorem HomogeneousSubmonoid.PreLocalizationGrading.add_den {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] {i : ι} (x y : S.PreLocalizationGrading i) : (x + y).den = x.den * y.den

@[simp]

theorem HomogeneousSubmonoid.PreLocalizationGrading.add_degNum {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] {i : ι} (x y : S.PreLocalizationGrading i) : (x + y).degNum = x.degDen + y.degNum

@[simp]

theorem HomogeneousSubmonoid.PreLocalizationGrading.add_degDen {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] {i : ι} (x y : S.PreLocalizationGrading i) : (x + y).degDen = x.degDen + y.degDen

instance HomogeneousSubmonoid.PreLocalizationGrading.instOneOfNat {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] : One (S.PreLocalizationGrading 0)

Equations

• HomogeneousSubmonoid.PreLocalizationGrading.instOneOfNat S = { one := { num := 1, den := 1, degNum := 0, degDen := 0, num_mem := ⋯, den_mem := ⋯, deg_frac_eq := ⋯ } }

@[simp]

theorem HomogeneousSubmonoid.PreLocalizationGrading.one_num {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] : HomogeneousSubmonoid.PreLocalizationGrading.num 1 = 1

@[simp]

theorem HomogeneousSubmonoid.PreLocalizationGrading.one_den {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] : HomogeneousSubmonoid.PreLocalizationGrading.den 1 = 1

@[simp]

theorem HomogeneousSubmonoid.PreLocalizationGrading.one_degNum {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] : HomogeneousSubmonoid.PreLocalizationGrading.degNum 1 = 0

@[simp]

theorem HomogeneousSubmonoid.PreLocalizationGrading.one_degDen {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] : HomogeneousSubmonoid.PreLocalizationGrading.degDen 1 = 0

instance HomogeneousSubmonoid.PreLocalizationGrading.instZero {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] (i : ι) : Zero (S.PreLocalizationGrading i)

Equations

• HomogeneousSubmonoid.PreLocalizationGrading.instZero S i = { zero := { num := 0, den := 1, degNum := i, degDen := 0, num_mem := ⋯, den_mem := ⋯, deg_frac_eq := ⋯ } }

@[simp]

theorem HomogeneousSubmonoid.PreLocalizationGrading.zero_num {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] {i : ι} : HomogeneousSubmonoid.PreLocalizationGrading.num 0 = 0

@[simp]

theorem HomogeneousSubmonoid.PreLocalizationGrading.zero_den {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] {i : ι} : HomogeneousSubmonoid.PreLocalizationGrading.den 0 = 1

@[simp]

theorem HomogeneousSubmonoid.PreLocalizationGrading.zero_degNum {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] {i : ι} : HomogeneousSubmonoid.PreLocalizationGrading.degNum 0 = i

@[simp]

theorem HomogeneousSubmonoid.PreLocalizationGrading.zero_degDen {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] {i : ι} : HomogeneousSubmonoid.PreLocalizationGrading.degDen 0 = 0

@[simp]

theorem HomogeneousSubmonoid.PreLocalizationGrading.neg_zero {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] {i : ι} : -0 = 0

instance HomogeneousSubmonoid.PreLocalizationGrading.instAddZeroClass {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] (i : ι) : AddZeroClass (S.PreLocalizationGrading i)

Equations

• HomogeneousSubmonoid.PreLocalizationGrading.instAddZeroClass S i = AddZeroClass.mk ⋯ ⋯

instance HomogeneousSubmonoid.PreLocalizationGrading.instAddSemigroup {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] (i : ι) : AddSemigroup (S.PreLocalizationGrading i)

Equations

• HomogeneousSubmonoid.PreLocalizationGrading.instAddSemigroup S i = AddSemigroup.mk ⋯

instance HomogeneousSubmonoid.PreLocalizationGrading.instSubNegMonoid {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] (i : ι) : SubNegMonoid (S.PreLocalizationGrading i)

Equations

• HomogeneousSubmonoid.PreLocalizationGrading.instSubNegMonoid S i = SubNegMonoid.mk ⋯ zsmulRec ⋯ ⋯ ⋯

def HomogeneousSubmonoid.PreLocalizationGrading.val {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] (i : ι) : S.PreLocalizationGrading i →+ Localization S.toSubmonoid

Equations

• HomogeneousSubmonoid.PreLocalizationGrading.val S i = { toFun := fun (x : S.PreLocalizationGrading i) => Localization.mk x.num x.den, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem HomogeneousSubmonoid.PreLocalizationGrading.val_apply {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] (i : ι) (x : S.PreLocalizationGrading i) : (HomogeneousSubmonoid.PreLocalizationGrading.val S i) x = Localization.mk x.num x.den

def HomogeneousSubmonoid.PreLocalizationGrading.addCon {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] (i : ι) : AddCon (S.PreLocalizationGrading i)

Equations

• HomogeneousSubmonoid.PreLocalizationGrading.addCon S i = AddCon.ker (HomogeneousSubmonoid.PreLocalizationGrading.val S i)

instance HomogeneousSubmonoid.PreLocalizationGrading.instNegQuotientAddCon {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] (i : ι) : Neg (HomogeneousSubmonoid.PreLocalizationGrading.addCon S i).Quotient

Equations

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

instance HomogeneousSubmonoid.PreLocalizationGrading.instAddCommGroupQuotientAddCon {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] (i : ι) : AddCommGroup (HomogeneousSubmonoid.PreLocalizationGrading.addCon S i).Quotient

Equations

• HomogeneousSubmonoid.PreLocalizationGrading.instAddCommGroupQuotientAddCon S i = AddCommGroup.mk ⋯

def HomogeneousSubmonoid.PreLocalizationGrading.emb {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] (i : ι) : (HomogeneousSubmonoid.PreLocalizationGrading.addCon S i).Quotient →+ Localization S.toSubmonoid

Equations

• HomogeneousSubmonoid.PreLocalizationGrading.emb S i = (HomogeneousSubmonoid.PreLocalizationGrading.addCon S i).lift (HomogeneousSubmonoid.PreLocalizationGrading.val S i) ⋯

@[simp]

theorem HomogeneousSubmonoid.PreLocalizationGrading.emb_apply {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] (i : ι) (x : (HomogeneousSubmonoid.PreLocalizationGrading.addCon S i).Quotient) : (HomogeneousSubmonoid.PreLocalizationGrading.emb S i) x = AddCon.liftOn x ⇑(HomogeneousSubmonoid.PreLocalizationGrading.val S i) ⋯

def HomogeneousSubmonoid.LocalizationGrading {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] (i : ι) : AddSubgroup (Localization S.toSubmonoid)

Equations

• S.LocalizationGrading i = (HomogeneousSubmonoid.PreLocalizationGrading.emb S i).range

theorem HomogeneousSubmonoid.LocalizationGrading.one_mem {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] : 1 ∈ S.LocalizationGrading 0

instance HomogeneousSubmonoid.LocalizationGrading.instGradedMonoidLocalizationAddSubgroup {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] : SetLike.GradedMonoid S.LocalizationGrading

noncomputable def HomogeneousSubmonoid.LocalizationGrading.decomposition {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] : Localization S.toSubmonoid →+* DirectSum ι fun (i : ι) => ↥(S.LocalizationGrading i)

Equations

• HomogeneousSubmonoid.LocalizationGrading.decomposition S = IsLocalization.lift ⋯

theorem HomogeneousSubmonoid.LocalizationGrading.decomposition_homogeneous_mk {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] {i j : ι} (a : A) (ha : a ∈ 𝒜 i) (b : ↥S.toSubmonoid) (hb : ↑b ∈ 𝒜 j) : (HomogeneousSubmonoid.LocalizationGrading.decomposition S) (Localization.mk a b) = (DirectSum.of (fun (i : ι) => ↥(S.LocalizationGrading i)) (i - j)) ⟨Localization.mk a b, ⋯⟩

noncomputable instance HomogeneousSubmonoid.LocalizationGrading.instDecompositionLocalizationAddSubgroup {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] : DirectSum.Decomposition S.LocalizationGrading

Equations

• HomogeneousSubmonoid.LocalizationGrading.instDecompositionLocalizationAddSubgroup S = { decompose' := ⇑(HomogeneousSubmonoid.LocalizationGrading.decomposition S), left_inv := ⋯, right_inv := ⋯ }

noncomputable instance HomogeneousSubmonoid.LocalizationGrading.instGradedRingLocalizationAddSubgroup {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] : GradedRing S.LocalizationGrading

Equations

• HomogeneousSubmonoid.LocalizationGrading.instGradedRingLocalizationAddSubgroup S = GradedRing.mk

theorem HomogeneousSubmonoid.mem_localizationGrading_iff {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [AddCommGroup ι] [CommRing A] [SetLike σ A] {𝒜 : ι → σ} (S : HomogeneousSubmonoid 𝒜) [AddSubgroupClass σ A] [DecidableEq ι] [GradedRing 𝒜] (x : Localization S.toSubmonoid) (i : ι) : x ∈ S.LocalizationGrading i ↔ ∃ (m : ι) (n : ι) (_ : m - n = i) (a : ↥(𝒜 m)) (b : ↥(𝒜 n)) (hb : ↑b ∈ S.toSubmonoid), x = Localization.mk ↑a ⟨↑b, hb⟩