noncomputable def HomogeneousSubmonoid.localizationToPotion {ι : 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) : Localization T'.genSubmonoid →+* (S * T).Potion

Equations

• HomogeneousSubmonoid.localizationToPotion T' = IsLocalization.lift ⋯

theorem HomogeneousSubmonoid.localizationToPotion_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 𝒜) (T' : S.PotionGen T) (x : HomogeneousLocalization.NumDenSameDeg 𝒜 S.toSubmonoid) (t : T'.index) (n : ℕ) : (HomogeneousSubmonoid.localizationToPotion T') (Localization.mk (HomogeneousLocalization.mk x) ⟨S.equivBarPotion.symm (HomogeneousLocalization.mk { deg := T'.i t, num := ⟨T'.elem t ^ ↑(T'.n t) * T'.s' t, ⋯⟩, den := ⟨T'.s t, ⋯⟩, den_mem := ⋯ }) ^ n, ⋯⟩) = HomogeneousLocalization.mk { deg := x.deg, num := x.num, den := x.den, den_mem := ⋯ } * (S * T).equivBarPotion.symm (HomogeneousLocalization.mk { deg := T'.i t, num := ⟨T'.s t, ⋯⟩, den := ⟨T'.elem t ^ ↑(T'.n t) * T'.s' t, ⋯⟩, den_mem := ⋯ } ^ n)

theorem HomogeneousSubmonoid.localizationToPotion_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 T : HomogeneousSubmonoid 𝒜} (T' : S.PotionGen T) : Function.Injective ⇑(HomogeneousSubmonoid.localizationToPotion T')

theorem HomogeneousSubmonoid.localizationToPotion_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 T : HomogeneousSubmonoid 𝒜} (T' : S.PotionGen T) : Function.Surjective ⇑(HomogeneousSubmonoid.localizationToPotion T')

noncomputable def HomogeneousSubmonoid.localizationRingEquivPotion {ι : 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) : Localization T'.genSubmonoid ≃+* (S * T).Potion

Equations

• HomogeneousSubmonoid.localizationRingEquivPotion T' = RingEquiv.ofBijective (HomogeneousSubmonoid.localizationToPotion T') ⋯

@[simp]

theorem HomogeneousSubmonoid.localizationRingEquivPotion_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 T : HomogeneousSubmonoid 𝒜} (T' : S.PotionGen T) (x : Localization T'.genSubmonoid) : (HomogeneousSubmonoid.localizationRingEquivPotion T') x = (HomogeneousSubmonoid.localizationToPotion T') x

noncomputable def HomogeneousSubmonoid.localizationAlgEquivPotion {ι : 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) : Localization T'.genSubmonoid ≃ₐ[S.Potion] (S * T).Potion

Equations

• HomogeneousSubmonoid.localizationAlgEquivPotion T' = AlgEquiv.ofRingEquiv ⋯

theorem HomogeneousSubmonoid.localizationAlgEquivPotion_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 T : HomogeneousSubmonoid 𝒜) (T' : S.PotionGen T) (x : Localization T'.genSubmonoid) : (HomogeneousSubmonoid.localizationAlgEquivPotion T') x = (HomogeneousSubmonoid.localizationToPotion T') x

theorem HomogeneousSubmonoid.localizationToPotion_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 𝒜) (T' : S.PotionGen T) (x : HomogeneousLocalization.NumDenSameDeg 𝒜 S.toSubmonoid) {ι✝ : Type u_4} (s : Finset ι✝) (t : ι✝ → T'.index) (n : ι✝ → ℕ) : (HomogeneousSubmonoid.localizationToPotion T') (Localization.mk (HomogeneousLocalization.mk x) (∏ y ∈ s, ⟨S.equivBarPotion.symm (HomogeneousLocalization.mk { deg := T'.i (t y), num := ⟨T'.elem (t y) ^ ↑(T'.n (t y)) * T'.s' (t y), ⋯⟩, den := ⟨T'.s (t y), ⋯⟩, den_mem := ⋯ }) ^ n y, ⋯⟩)) = HomogeneousLocalization.mk { deg := x.deg, num := x.num, den := x.den, den_mem := ⋯ } * (S * T).equivBarPotion.symm (∏ y ∈ s, HomogeneousLocalization.mk { deg := T'.i (t y), num := ⟨T'.s (t y), ⋯⟩, den := ⟨T'.elem (t y) ^ ↑(T'.n (t y)) * T'.s' (t y), ⋯⟩, den_mem := ⋯ } ^ n y)

instance HomogeneousSubmonoid.instIsLocalizationPotionGenSubmonoidHMulSubmodule {ι : 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) : IsLocalization T'.genSubmonoid (S * T).Potion

theorem HomogeneousSubmonoid.IsOpenImmersion.of_isRelevant_FG {ι : 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) : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (S.potionToMul T)))