noncomputable def
HomogeneousSubmonoid.localizationToLocalizationBar
{ι : Type u_1}
{A : Type u_2}
{σ : Type u_3}
[AddCommGroup ι]
[CommRing A]
[SetLike σ A]
{𝒜 : ι → σ}
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
(S : HomogeneousSubmonoid 𝒜)
:
Localization S.toSubmonoid →+* Localization S.bar.toSubmonoid
Equations
- S.localizationToLocalizationBar = IsLocalization.lift ⋯
Instances For
@[simp]
theorem
HomogeneousSubmonoid.localizationToLocalizationBar_mk
{ι : Type u_1}
{A : Type u_2}
{σ : Type u_3}
[AddCommGroup ι]
[CommRing A]
[SetLike σ A]
{𝒜 : ι → σ}
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
(S : HomogeneousSubmonoid 𝒜)
(a : A)
(s : ↥S.toSubmonoid)
:
S.localizationToLocalizationBar (Localization.mk a s) = Localization.mk a ⟨↑s, ⋯⟩
noncomputable def
HomogeneousSubmonoid.localizationBarToLocalization
{ι : Type u_1}
{A : Type u_2}
{σ : Type u_3}
[AddCommGroup ι]
[CommRing A]
[SetLike σ A]
{𝒜 : ι → σ}
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
(S : HomogeneousSubmonoid 𝒜)
:
Localization S.bar.toSubmonoid →+* Localization S.toSubmonoid
Equations
- S.localizationBarToLocalization = IsLocalization.lift ⋯
Instances For
theorem
HomogeneousSubmonoid.localizationBarToLocalization_mk
{ι : Type u_1}
{A : Type u_2}
{σ : Type u_3}
[AddCommGroup ι]
[CommRing A]
[SetLike σ A]
{𝒜 : ι → σ}
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
(S : HomogeneousSubmonoid 𝒜)
(a z : A)
(s : ↥S.bar.toSubmonoid)
(hz : ↑s * z ∈ S.toSubmonoid)
:
S.localizationBarToLocalization (Localization.mk a s) = Localization.mk (a * z) ⟨↑s * z, hz⟩
@[simp]
theorem
HomogeneousSubmonoid.localizationBarToLocalization_mk'
{ι : Type u_1}
{A : Type u_2}
{σ : Type u_3}
[AddCommGroup ι]
[CommRing A]
[SetLike σ A]
{𝒜 : ι → σ}
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
(S : HomogeneousSubmonoid 𝒜)
(a : A)
(s : ↥S.toSubmonoid)
:
S.localizationBarToLocalization (Localization.mk a ⟨↑s, ⋯⟩) = Localization.mk a s
noncomputable def
HomogeneousSubmonoid.localizationEquivLocalizationBar
{ι : Type u_1}
{A : Type u_2}
{σ : Type u_3}
[AddCommGroup ι]
[CommRing A]
[SetLike σ A]
{𝒜 : ι → σ}
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
(S : HomogeneousSubmonoid 𝒜)
:
GradedRingEquiv S.LocalizationGrading S.bar.LocalizationGrading
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
HomogeneousSubmonoid.localizationEquivLocalizationBar_apply
{ι : Type u_1}
{A : Type u_2}
{σ : Type u_3}
[AddCommGroup ι]
[CommRing A]
[SetLike σ A]
{𝒜 : ι → σ}
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
(S : HomogeneousSubmonoid 𝒜)
(x : Localization S.toSubmonoid)
:
S.localizationEquivLocalizationBar x = S.localizationToLocalizationBar x
@[simp]
theorem
HomogeneousSubmonoid.localizationEquivLocalizationBar_symm_apply
{ι : Type u_1}
{A : Type u_2}
{σ : Type u_3}
[AddCommGroup ι]
[CommRing A]
[SetLike σ A]
{𝒜 : ι → σ}
[DecidableEq ι]
[AddSubgroupClass σ A]
[GradedRing 𝒜]
(S : HomogeneousSubmonoid 𝒜)
(x : Localization S.bar.toSubmonoid)
:
S.localizationEquivLocalizationBar.symm x = S.localizationBarToLocalization x