structure
HomogeneousSubmonoid.PreLocalizedModuleGrading
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
(i : ι)
:
Type (max (max u_1 u_2) u_3)
- num : Q
- den : ↥S.toSubmonoid
- degNum : ι
- degDen : ι
- num_mem : self.num ∈ 𝒬 self.degNum
- den_mem : ↑self.den ∈ 𝒜 self.degDen
Instances For
theorem
HomogeneousSubmonoid.PreLocalizedModuleGrading.ext
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
{i : ι}
(x y : HomogeneousSubmonoid.PreLocalizedModuleGrading 𝒬 S 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.PreLocalizedModuleGrading.instNeg
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
(i : ι)
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
HomogeneousSubmonoid.PreLocalizedModuleGrading.neg_num
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
{i : ι}
(x : HomogeneousSubmonoid.PreLocalizedModuleGrading 𝒬 S i)
:
@[simp]
theorem
HomogeneousSubmonoid.PreLocalizedModuleGrading.neg_den
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
{i : ι}
(x : HomogeneousSubmonoid.PreLocalizedModuleGrading 𝒬 S i)
:
@[simp]
theorem
HomogeneousSubmonoid.PreLocalizedModuleGrading.neg_degNum
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
{i : ι}
(x : HomogeneousSubmonoid.PreLocalizedModuleGrading 𝒬 S i)
:
@[simp]
theorem
HomogeneousSubmonoid.PreLocalizedModuleGrading.neg_degDen
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
{i : ι}
(x : HomogeneousSubmonoid.PreLocalizedModuleGrading 𝒬 S i)
:
instance
HomogeneousSubmonoid.PreLocalizedModuleGrading.instAdd
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
[Module A Q]
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
[SetLike.GradedSMul 𝒜 𝒬]
(i : ι)
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
HomogeneousSubmonoid.PreLocalizedModuleGrading.add_num
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
[Module A Q]
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
[SetLike.GradedSMul 𝒜 𝒬]
{i : ι}
(x y : HomogeneousSubmonoid.PreLocalizedModuleGrading 𝒬 S i)
:
@[simp]
theorem
HomogeneousSubmonoid.PreLocalizedModuleGrading.add_den
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
[Module A Q]
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
[SetLike.GradedSMul 𝒜 𝒬]
{i : ι}
(x y : HomogeneousSubmonoid.PreLocalizedModuleGrading 𝒬 S i)
:
@[simp]
theorem
HomogeneousSubmonoid.PreLocalizedModuleGrading.add_degNum
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
[Module A Q]
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
[SetLike.GradedSMul 𝒜 𝒬]
{i : ι}
(x y : HomogeneousSubmonoid.PreLocalizedModuleGrading 𝒬 S i)
:
@[simp]
theorem
HomogeneousSubmonoid.PreLocalizedModuleGrading.add_degDen
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
[Module A Q]
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
[SetLike.GradedSMul 𝒜 𝒬]
{i : ι}
(x y : HomogeneousSubmonoid.PreLocalizedModuleGrading 𝒬 S i)
:
instance
HomogeneousSubmonoid.PreLocalizedModuleGrading.instZero
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
(i : ι)
:
Equations
- HomogeneousSubmonoid.PreLocalizedModuleGrading.instZero 𝒬 S i = { zero := { num := 0, den := 1, degNum := i, degDen := 0, num_mem := ⋯, den_mem := ⋯, deg_frac_eq := ⋯ } }
@[simp]
theorem
HomogeneousSubmonoid.PreLocalizedModuleGrading.zero_num
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
{i : ι}
:
@[simp]
theorem
HomogeneousSubmonoid.PreLocalizedModuleGrading.zero_den
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
{i : ι}
:
@[simp]
theorem
HomogeneousSubmonoid.PreLocalizedModuleGrading.zero_degNum
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
{i : ι}
:
@[simp]
theorem
HomogeneousSubmonoid.PreLocalizedModuleGrading.zero_degDen
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
{i : ι}
:
@[simp]
theorem
HomogeneousSubmonoid.PreLocalizedModuleGrading.neg_zero
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
{i : ι}
:
-0 = 0
instance
HomogeneousSubmonoid.PreLocalizedModuleGrading.instAddZeroClass
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
[Module A Q]
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
[SetLike.GradedSMul 𝒜 𝒬]
(i : ι)
:
Equations
instance
HomogeneousSubmonoid.PreLocalizedModuleGrading.instAddSemigroup
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
[Module A Q]
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
[SetLike.GradedSMul 𝒜 𝒬]
(i : ι)
:
instance
HomogeneousSubmonoid.PreLocalizedModuleGrading.instSubNegMonoid
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
[Module A Q]
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
[SetLike.GradedSMul 𝒜 𝒬]
(i : ι)
:
Equations
def
HomogeneousSubmonoid.PreLocalizedModuleGrading.val
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
[Module A Q]
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
[SetLike.GradedSMul 𝒜 𝒬]
(i : ι)
:
HomogeneousSubmonoid.PreLocalizedModuleGrading 𝒬 S i →+ LocalizedModule S.toSubmonoid Q
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
HomogeneousSubmonoid.PreLocalizedModuleGrading.val_apply
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
[Module A Q]
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
[SetLike.GradedSMul 𝒜 𝒬]
(i : ι)
(x : HomogeneousSubmonoid.PreLocalizedModuleGrading 𝒬 S i)
:
(HomogeneousSubmonoid.PreLocalizedModuleGrading.val 𝒬 S i) x = LocalizedModule.mk x.num x.den
def
HomogeneousSubmonoid.PreLocalizedModuleGrading.addCon
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
[Module A Q]
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
[SetLike.GradedSMul 𝒜 𝒬]
(i : ι)
:
Equations
Instances For
instance
HomogeneousSubmonoid.PreLocalizedModuleGrading.instNegQuotientAddCon
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
[Module A Q]
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
[SetLike.GradedSMul 𝒜 𝒬]
(i : ι)
:
Neg (HomogeneousSubmonoid.PreLocalizedModuleGrading.addCon 𝒬 S i).Quotient
Equations
- One or more equations did not get rendered due to their size.
instance
HomogeneousSubmonoid.PreLocalizedModuleGrading.instAddCommGroupQuotientAddCon
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
[Module A Q]
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
[SetLike.GradedSMul 𝒜 𝒬]
(i : ι)
:
AddCommGroup (HomogeneousSubmonoid.PreLocalizedModuleGrading.addCon 𝒬 S i).Quotient
def
HomogeneousSubmonoid.PreLocalizedModuleGrading.emb
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
[Module A Q]
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
[SetLike.GradedSMul 𝒜 𝒬]
(i : ι)
:
(HomogeneousSubmonoid.PreLocalizedModuleGrading.addCon 𝒬 S i).Quotient →+ LocalizedModule S.toSubmonoid Q
Equations
Instances For
@[simp]
theorem
HomogeneousSubmonoid.PreLocalizedModuleGrading.emb_apply
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
[Module A Q]
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
[SetLike.GradedSMul 𝒜 𝒬]
(i : ι)
(x : (HomogeneousSubmonoid.PreLocalizedModuleGrading.addCon 𝒬 S i).Quotient)
:
instance
HomogeneousSubmonoid.PreLocalizedModuleGrading.instAddGroupQuotientAddCon
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[AddSubgroupClass τ Q]
[Module A Q]
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
[SetLike.GradedSMul 𝒜 𝒬]
(i : ι)
:
AddGroup (HomogeneousSubmonoid.PreLocalizedModuleGrading.addCon 𝒬 S i).Quotient
def
HomogeneousSubmonoid.LocalizedModuleGrading
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[Module A Q]
[AddSubgroupClass σ A]
[AddSubgroupClass τ Q]
[DecidableEq ι]
[GradedRing 𝒜]
[SetLike.GradedSMul 𝒜 𝒬]
(i : ι)
:
AddSubgroup (LocalizedModule S.toSubmonoid Q)
Equations
Instances For
instance
HomogeneousSubmonoid.LocalizedModuleGrading.instGradedSMulAddSubgroupLocalizationLocalizedModuleLocalizationGrading
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[Module A Q]
[AddSubgroupClass σ A]
[AddSubgroupClass τ Q]
[DecidableEq ι]
[GradedRing 𝒜]
[SetLike.GradedSMul 𝒜 𝒬]
:
SetLike.GradedSMul S.LocalizationGrading (HomogeneousSubmonoid.LocalizedModuleGrading 𝒬 S)
noncomputable instance
HomogeneousSubmonoid.LocalizedModuleGrading.instGmoduleSubtypeLocalizationMemAddSubgroupLocalizationGradingLocalizedModule
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[Module A Q]
[AddSubgroupClass σ A]
[AddSubgroupClass τ Q]
[DecidableEq ι]
[GradedRing 𝒜]
[SetLike.GradedSMul 𝒜 𝒬]
:
DirectSum.Gmodule (fun (i : ι) => ↥(S.LocalizationGrading i)) fun (i : ι) =>
↥(HomogeneousSubmonoid.LocalizedModuleGrading 𝒬 S i)
noncomputable instance
HomogeneousSubmonoid.LocalizedModuleGrading.instModuleDirectSumSubtypeLocalizationMemAddSubgroupLocalizationGradingLocalizedModule
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[Module A Q]
[AddSubgroupClass σ A]
[AddSubgroupClass τ Q]
[DecidableEq ι]
[GradedRing 𝒜]
[SetLike.GradedSMul 𝒜 𝒬]
:
Module (DirectSum ι fun (i : ι) => ↥(S.LocalizationGrading i))
(DirectSum ι fun (i : ι) => ↥(HomogeneousSubmonoid.LocalizedModuleGrading 𝒬 S i))
noncomputable instance
HomogeneousSubmonoid.LocalizedModuleGrading.instModuleLocalizationDirectSumSubtypeLocalizedModuleMemAddSubgroup
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[Module A Q]
[AddSubgroupClass σ A]
[AddSubgroupClass τ Q]
[DecidableEq ι]
[GradedRing 𝒜]
[SetLike.GradedSMul 𝒜 𝒬]
:
Module (Localization S.toSubmonoid) (DirectSum ι fun (i : ι) => ↥(HomogeneousSubmonoid.LocalizedModuleGrading 𝒬 S i))
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
HomogeneousSubmonoid.LocalizedModuleGrading.localization_smul_directSum_def
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[Module A Q]
[AddSubgroupClass σ A]
[AddSubgroupClass τ Q]
[DecidableEq ι]
[GradedRing 𝒜]
[SetLike.GradedSMul 𝒜 𝒬]
(x : Localization S.toSubmonoid)
(y : DirectSum ι fun (i : ι) => ↥(HomogeneousSubmonoid.LocalizedModuleGrading 𝒬 S i))
:
x • y = (DirectSum.decompose S.LocalizationGrading) x • y
noncomputable instance
HomogeneousSubmonoid.LocalizedModuleGrading.instModuleDirectSumSubtypeLocalizedModuleMemAddSubgroup
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[Module A Q]
[AddSubgroupClass σ A]
[AddSubgroupClass τ Q]
[DecidableEq ι]
[GradedRing 𝒜]
[SetLike.GradedSMul 𝒜 𝒬]
:
Module A (DirectSum ι fun (i : ι) => ↥(HomogeneousSubmonoid.LocalizedModuleGrading 𝒬 S i))
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
HomogeneousSubmonoid.LocalizedModuleGrading.smul_directSum_def
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[Module A Q]
[AddSubgroupClass σ A]
[AddSubgroupClass τ Q]
[DecidableEq ι]
[GradedRing 𝒜]
[SetLike.GradedSMul 𝒜 𝒬]
(a : A)
(x : DirectSum ι fun (i : ι) => ↥(HomogeneousSubmonoid.LocalizedModuleGrading 𝒬 S i))
:
a • x = (algebraMap A (Localization S.toSubmonoid)) a • x
instance
HomogeneousSubmonoid.LocalizedModuleGrading.instIsScalarTowerLocalizationDirectSumSubtypeLocalizedModuleMemAddSubgroup
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{σ : Type u_4}
{τ : Type u_5}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[SetLike σ A]
[SetLike τ Q]
{𝒜 : ι → σ}
(𝒬 : ι → τ)
(S : HomogeneousSubmonoid 𝒜)
[Module A Q]
[AddSubgroupClass σ A]
[AddSubgroupClass τ Q]
[DecidableEq ι]
[GradedRing 𝒜]
[SetLike.GradedSMul 𝒜 𝒬]
:
IsScalarTower A (Localization S.toSubmonoid)
(DirectSum ι fun (i : ι) => ↥(HomogeneousSubmonoid.LocalizedModuleGrading 𝒬 S i))
noncomputable def
HomogeneousSubmonoid.LocalizedModuleGrading.decompositionAux1
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[Module A Q]
[DecidableEq ι]
{𝓐 : ι → AddSubgroup A}
[GradedRing 𝓐]
(𝓠 : ι → AddSubgroup Q)
[SetLike.GradedSMul 𝓐 𝓠]
(S : HomogeneousSubmonoid 𝓐)
:
(DirectSum ι fun (i : ι) => ↥(𝓠 i)) →+ DirectSum ι fun (i : ι) => ↥(HomogeneousSubmonoid.LocalizedModuleGrading 𝓠 S i)
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
HomogeneousSubmonoid.LocalizedModuleGrading.decompositionAux2
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[Module A Q]
[DecidableEq ι]
{𝓐 : ι → AddSubgroup A}
[GradedRing 𝓐]
(𝓠 : ι → AddSubgroup Q)
[DirectSum.Decomposition 𝓠]
[SetLike.GradedSMul 𝓐 𝓠]
(S : HomogeneousSubmonoid 𝓐)
:
Q →+ DirectSum ι fun (i : ι) => ↥(HomogeneousSubmonoid.LocalizedModuleGrading 𝓠 S i)
Equations
Instances For
noncomputable def
HomogeneousSubmonoid.LocalizedModuleGrading.decompositionAux3
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[Module A Q]
[DecidableEq ι]
{𝓐 : ι → AddSubgroup A}
[GradedRing 𝓐]
(𝓠 : ι → AddSubgroup Q)
[DirectSum.Decomposition 𝓠]
[SetLike.GradedSMul 𝓐 𝓠]
(S : HomogeneousSubmonoid 𝓐)
:
Q →ₗ[A] DirectSum ι fun (i : ι) => ↥(HomogeneousSubmonoid.LocalizedModuleGrading 𝓠 S i)
Equations
- HomogeneousSubmonoid.LocalizedModuleGrading.decompositionAux3 𝓠 S = { toFun := ⇑(HomogeneousSubmonoid.LocalizedModuleGrading.decompositionAux2 𝓠 S), map_add' := ⋯, map_smul' := ⋯ }
Instances For
@[simp]
theorem
HomogeneousSubmonoid.LocalizedModuleGrading.decompositionAux3_apply
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[Module A Q]
[DecidableEq ι]
{𝓐 : ι → AddSubgroup A}
[GradedRing 𝓐]
(𝓠 : ι → AddSubgroup Q)
[DirectSum.Decomposition 𝓠]
[SetLike.GradedSMul 𝓐 𝓠]
(S : HomogeneousSubmonoid 𝓐)
(a : Q)
:
theorem
HomogeneousSubmonoid.LocalizedModuleGrading.decompositionAux3_apply_mem_mem
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[Module A Q]
[DecidableEq ι]
{𝓐 : ι → AddSubgroup A}
[GradedRing 𝓐]
(𝓠 : ι → AddSubgroup Q)
[DirectSum.Decomposition 𝓠]
[SetLike.GradedSMul 𝓐 𝓠]
(S : HomogeneousSubmonoid 𝓐)
{i j : ι}
(a : A)
(ha : a ∈ 𝓐 i)
(q : Q)
(hq : q ∈ 𝓠 j)
:
(HomogeneousSubmonoid.LocalizedModuleGrading.decompositionAux3 𝓠 S) (a • q) = (DirectSum.of (fun (i : ι) => ↥(HomogeneousSubmonoid.LocalizedModuleGrading 𝓠 S i)) (i + j))
⟨LocalizedModule.mk (a • q) 1, ⋯⟩
theorem
HomogeneousSubmonoid.LocalizedModuleGrading.inv_of
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[Module A Q]
[DecidableEq ι]
{𝓐 : ι → AddSubgroup A}
[GradedRing 𝓐]
(𝓠 : ι → AddSubgroup Q)
[SetLike.GradedSMul 𝓐 𝓠]
(S : HomogeneousSubmonoid 𝓐)
(x y : A)
(hx1 : x ∈ S.toSubmonoid)
(i j k jsk jki : ι)
(hx2 : x ∈ 𝓐 i)
(q : Q)
(hq : q ∈ 𝓠 j)
(hy1 : y ∈ 𝓐 k)
(hy2 : y ∈ S.toSubmonoid)
(hjsk : jsk = j - k)
(hjki : jki = j - (k + i))
:
(HomogeneousSubmonoid.LocalizedModuleGrading.inv✝ 𝓠 S x hx1 i hx2)
((DirectSum.of (fun (i : ι) => ↥(HomogeneousSubmonoid.LocalizedModuleGrading 𝓠 S i)) jsk)
⟨LocalizedModule.mk q ⟨y, hy2⟩, ⋯⟩) = (DirectSum.of (fun (i : ι) => ↥(HomogeneousSubmonoid.LocalizedModuleGrading 𝓠 S i)) jki)
⟨LocalizedModule.mk q ⟨x * y, ⋯⟩, ⋯⟩
noncomputable def
HomogeneousSubmonoid.LocalizedModuleGrading.decomposition
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[Module A Q]
[DecidableEq ι]
{𝓐 : ι → AddSubgroup A}
[GradedRing 𝓐]
(𝓠 : ι → AddSubgroup Q)
[DirectSum.Decomposition 𝓠]
[SetLike.GradedSMul 𝓐 𝓠]
(S : HomogeneousSubmonoid 𝓐)
:
LocalizedModule S.toSubmonoid Q →ₗ[A] DirectSum ι fun (i : ι) => ↥(HomogeneousSubmonoid.LocalizedModuleGrading 𝓠 S i)
Equations
Instances For
theorem
HomogeneousSubmonoid.LocalizedModuleGrading.decomposition_homogeneous_mk
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[Module A Q]
[DecidableEq ι]
{𝓐 : ι → AddSubgroup A}
[GradedRing 𝓐]
(𝓠 : ι → AddSubgroup Q)
[DirectSum.Decomposition 𝓠]
[SetLike.GradedSMul 𝓐 𝓠]
(S : HomogeneousSubmonoid 𝓐)
{i j : ι}
(a : Q)
(ha : a ∈ 𝓠 i)
(b : ↥S.toSubmonoid)
(hb : ↑b ∈ 𝓐 j)
:
(HomogeneousSubmonoid.LocalizedModuleGrading.decomposition 𝓠 S) (LocalizedModule.mk a b) = (DirectSum.of (fun (i : ι) => ↥(HomogeneousSubmonoid.LocalizedModuleGrading 𝓠 S i)) (i - j))
⟨LocalizedModule.mk a b, ⋯⟩
theorem
HomogeneousSubmonoid.LocalizedModuleGrading.decomposition_left_inv
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[Module A Q]
[DecidableEq ι]
{𝓐 : ι → AddSubgroup A}
[GradedRing 𝓐]
(𝓠 : ι → AddSubgroup Q)
[DirectSum.Decomposition 𝓠]
[SetLike.GradedSMul 𝓐 𝓠]
(S : HomogeneousSubmonoid 𝓐)
(x : LocalizedModule S.toSubmonoid Q)
:
theorem
HomogeneousSubmonoid.LocalizedModuleGrading.decomposition_right_inv
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[Module A Q]
[DecidableEq ι]
{𝓐 : ι → AddSubgroup A}
[GradedRing 𝓐]
(𝓠 : ι → AddSubgroup Q)
[DirectSum.Decomposition 𝓠]
[SetLike.GradedSMul 𝓐 𝓠]
(S : HomogeneousSubmonoid 𝓐)
(x : DirectSum ι fun (i : ι) => ↥(HomogeneousSubmonoid.LocalizedModuleGrading 𝓠 S i))
:
noncomputable instance
HomogeneousSubmonoid.LocalizedModuleGrading.instDecompositionLocalizedModuleAddSubgroup
{ι : Type u_1}
{A : Type u_2}
{Q : Type u_3}
[AddCommGroup ι]
[CommRing A]
[AddCommGroup Q]
[Module A Q]
[DecidableEq ι]
{𝓐 : ι → AddSubgroup A}
[GradedRing 𝓐]
(𝓠 : ι → AddSubgroup Q)
[DirectSum.Decomposition 𝓠]
[SetLike.GradedSMul 𝓐 𝓠]
(S : HomogeneousSubmonoid 𝓐)
:
Equations
- One or more equations did not get rendered due to their size.