A rational localisation as a quotient of A⟨X₁, …, Xₖ⟩

Wedhorn's Example 6.38 presents the coordinate ring of a rational subset as a quotient of a restricted power series ring. For a presentation (T, s) whose numerators other than s are listed by t : Fin k → A, this file constructs the identification

A⟨X₁, …, Xₖ⟩ ⧸ (t₁ - s X₁, …, tₖ - s Xₖ)  ≃  A⟨T/s⟩,      Xᵢ ↦ tᵢ/s,

as an isomorphism of topological rings compatible with the structure maps from A. It asks A to be a complete Huber ring, the relation ideal to be closed, every tᵢ to lie in T, every element of T to be s or some tᵢ, and T together with s to generate the unit ideal.

The denominator need not be listed even when it is a numerator: ({f, 1}, 1) with t = (f), ({1}, f) with t = (1), and ({f², f, 1}, f) with t = (f², 1) all satisfy the hypotheses.

Main definitions

• TauCeti.Huber.rationalRelationIdeal: the ideal (t₁ - s X₁, …, tₖ - s Xₖ) of A⟨X₁, …, Xₖ⟩.
• TauCeti.Huber.PairOfDefinition.rationalQuotientRingEquiv: the identification of the quotient with A⟨T/s⟩.
• TauCeti.Huber.PairOfDefinition.rationalQuotientHom: the identification precomposed with the quotient map, presenting A⟨T/s⟩ directly as a quotient of A⟨X₁, …, Xₖ⟩.

Main results

• TauCeti.Huber.rationalRelationIdeal_quotientMk_weightedC_mul_weightedX: in the quotient the classes of s and Xᵢ multiply to the class of tᵢ.
• TauCeti.Huber.isUnit_rationalRelationIdeal_quotientMk_weightedC: the class of s is a unit when s and the tᵢ generate the unit ideal.
• TauCeti.Huber.PairOfDefinition.rationalQuotientRingEquiv_quotientMk_weightedC, TauCeti.Huber.PairOfDefinition.rationalQuotientRingEquiv_quotientMk_weightedX, TauCeti.Huber.PairOfDefinition.rationalQuotientRingEquiv_symm_toCompletionLoc and TauCeti.Huber.PairOfDefinition.rationalQuotientRingEquiv_symm_coe_divBy: the identification and its inverse on constants and on the variables.
• TauCeti.Huber.PairOfDefinition.rationalQuotientRingEquiv_algebraMap: the identification is compatible with the structure maps from A.
• TauCeti.Huber.PairOfDefinition.continuous_rationalQuotientRingEquiv and its symm form: the identification is one of topological rings.
• TauCeti.Huber.PairOfDefinition.rationalQuotientHom_surjective, TauCeti.Huber.PairOfDefinition.continuous_rationalQuotientHom, TauCeti.Huber.PairOfDefinition.rationalQuotientHom_weightedC, TauCeti.Huber.PairOfDefinition.rationalQuotientHom_weightedX and TauCeti.Huber.PairOfDefinition.rationalQuotientHom_weightedC_mul_weightedX: the presentation map is a continuous surjection, and its values on constants and on the relations.
• TauCeti.Huber.PairOfDefinition.rationalQuotientHom_eq_zero_iff_mem: the kernel of the presentation map is the relation ideal, as an iff usable in both directions. Together with the bullet above these characterise a map out of A⟨T/s⟩ without mentioning the quotient.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Example 6.38.

Provenance

AINTLIB (github.com/CBirkbeck/AINTLIB, branch dev/adic-spaces, commit 37bbdaeb9, Apache-2.0), projects/AdicSpaces/Adic spaces/Example638.lean, proves the two one-variable cases as example638Plus_equiv, B⟨X⟩ ⧸ (b - X) ≃+* presheafValue (trivialPlusDatum P b), and example638Minus_equiv, B⟨X⟩ ⧸ (1 - b X) ≃+* presheafValue (trivialMinusDatum P b), over its own TateAlgebra and presheafValue. This file states the identification for k variables and an arbitrary presentation, against this repository's weightedRestrictedSubring and toCompletionLoc; no AINTLIB code is copied.

noncomputable def TauCeti.Huber.rationalRelationIdeal {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {k : ℕ} (t : Fin k → A) (s : A) : Ideal ↥(weightedRestrictedSubring (fun (x : Fin k) => {1}) ⋯)

The relation ideal (t₁ - s X₁, …, tₖ - s Xₖ) of A⟨X₁, …, Xₖ⟩, the ring of restricted power series in k variables (the weighted restricted series with weight {1}). In the quotient the class of s times the class of Xᵢ is the class of tᵢ (rationalRelationIdeal_quotientMk_weightedC_mul_weightedX). PairOfDefinition.rationalQuotientRingEquiv identifies the quotient with A⟨T/s⟩.

Compare TauCeti.Huber.PairOfDefinition.laurentRelationIdeal, the ideal (t/s - X) of A⟨T/s⟩⟨X⟩: its quotient adjoins one more fraction to A⟨T/s⟩, whereas the quotient by this ideal builds A⟨T/s⟩ from A.

Equations

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

theorem TauCeti.Huber.rationalRelationIdeal_def {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {k : ℕ} (t : Fin k → A) (s : A) : rationalRelationIdeal t s = Ideal.span (Set.range fun (i : Fin k) => (weightedC (fun (x : Fin k) => {1}) ⋯) (t i) - (weightedC (fun (x : Fin k) => {1}) ⋯) s * weightedX (fun (x : Fin k) => {1}) ⋯ i)

rationalRelationIdeal t s is the span of the tᵢ - s Xᵢ. The definition's body is not exposed across module boundaries, so rewrite with this lemma to reach the generators; for computing in the quotient, rationalRelationIdeal_quotientMk_weightedC_mul_weightedX is usually more direct.

@[simp]

theorem TauCeti.Huber.rationalRelationIdeal_quotientMk_weightedC_mul_weightedX {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {k : ℕ} (t : Fin k → A) (s : A) (i : Fin k) : (Ideal.Quotient.mk (rationalRelationIdeal t s)) ((weightedC (fun (x : Fin k) => {1}) ⋯) s) * (Ideal.Quotient.mk (rationalRelationIdeal t s)) (weightedX (fun (x : Fin k) => {1}) ⋯ i) = (Ideal.Quotient.mk (rationalRelationIdeal t s)) ((weightedC (fun (x : Fin k) => {1}) ⋯) (t i))

The relations the ideal imposes: in A⟨X₁, …, Xₖ⟩ ⧸ (tᵢ - s Xᵢ) the class of the constant s times the class of the variable Xᵢ is the class of the constant tᵢ. simp rewrites this product only with the class of s on the left; for the other order, rewrite with mul_comm first. When the class of s is a unit (isUnit_rationalRelationIdeal_quotientMk_weightedC), this identifies the class of Xᵢ with the class of tᵢ times the inverse of the class of s.

theorem TauCeti.Huber.isUnit_rationalRelationIdeal_quotientMk_weightedC {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {k : ℕ} {t : Fin k → A} {s : A} (hspan : Ideal.span (insert s (Set.range t)) = ⊤) : IsUnit ((Ideal.Quotient.mk (rationalRelationIdeal t s)) ((weightedC (fun (x : Fin k) => {1}) ⋯) s))

s becomes a unit in A⟨X₁, …, Xₖ⟩ ⧸ (tᵢ - s Xᵢ) when s and the numerators tᵢ generate the unit ideal of A.

noncomputable def TauCeti.Huber.PairOfDefinition.rationalQuotientRingEquiv {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] [CompleteSpace A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) {k : ℕ} (t : Fin k → A) (ht : ∀ (i : Fin k), t i ∈ T) (hsplit : ∀ u ∈ T, u = s ∨ u ∈ Set.range t) (hspan : Ideal.span (insert s ↑T) = ⊤) (hcl : IsClosed ↑(rationalRelationIdeal t s)) : ↥(weightedRestrictedSubring (fun (x : Fin k) => {1}) ⋯) ⧸ rationalRelationIdeal t s ≃+* UniformSpace.Completion S

Wedhorn's Example 6.38: over a complete Huber ring A, for a presentation (T, s) and a listing t : Fin k → A of numerators, the ring isomorphism

A⟨X₁, …, Xₖ⟩ ⧸ (t₁ - s X₁, …, tₖ - s Xₖ)  ≃  A⟨T/s⟩

that is the structure map from A on constants and sends Xᵢ to tᵢ/s. The hypotheses: every tᵢ lies in T (ht), every element of T is s or some tᵢ (hsplit), T and s generate the unit ideal (hspan), and the relation ideal is closed (hcl). For instance, hcl holds when A is a separated strongly noetherian Tate ring, by TauCeti.Huber.isClosed_of_isNoetherian.

Equations

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

@[simp]

theorem TauCeti.Huber.PairOfDefinition.rationalQuotientRingEquiv_quotientMk_weightedC {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] [CompleteSpace A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) {k : ℕ} (t : Fin k → A) (ht : ∀ (i : Fin k), t i ∈ T) (hsplit : ∀ u ∈ T, u = s ∨ u ∈ Set.range t) (hspan : Ideal.span (insert s ↑T) = ⊤) (hcl : IsClosed ↑(rationalRelationIdeal t s)) (a : A) : (P.rationalQuotientRingEquiv T s S hden t ht hsplit hspan hcl) ((Ideal.Quotient.mk (rationalRelationIdeal t s)) ((weightedC (fun (x : Fin k) => {1}) ⋯) a)) = (P.toCompletionLoc T s S hden) a

On constants the identification is the structure map A → A⟨T/s⟩. The values on the variables are given by rationalQuotientRingEquiv_quotientMk_weightedX, and rationalQuotientRingEquiv_symm_toCompletionLoc is the same fact read through the inverse.

@[simp]

theorem TauCeti.Huber.PairOfDefinition.rationalQuotientRingEquiv_algebraMap {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] [CompleteSpace A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) {k : ℕ} (t : Fin k → A) (ht : ∀ (i : Fin k), t i ∈ T) (hsplit : ∀ u ∈ T, u = s ∨ u ∈ Set.range t) (hspan : Ideal.span (insert s ↑T) = ⊤) (hcl : IsClosed ↑(rationalRelationIdeal t s)) (a : A) : (P.rationalQuotientRingEquiv T s S hden t ht hsplit hspan hcl) ((algebraMap A (↥(weightedRestrictedSubring (fun (x : Fin k) => {1}) ⋯) ⧸ rationalRelationIdeal t s)) a) = (P.toCompletionLoc T s S hden) a

The identification is compatible with the structure maps from A: it sends the image of a under algebraMap A (A⟨X₁, …, Xₖ⟩ ⧸ (tᵢ - s Xᵢ)) to the image of a in A⟨T/s⟩. This is rationalQuotientRingEquiv_quotientMk_weightedC stated through the A-algebra structure of the quotient, which is the form that composes with algebraMap, for instance under RingHom.ext.

@[simp]

theorem TauCeti.Huber.PairOfDefinition.rationalQuotientRingEquiv_quotientMk_weightedX {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] [CompleteSpace A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) {k : ℕ} (t : Fin k → A) (ht : ∀ (i : Fin k), t i ∈ T) (hsplit : ∀ u ∈ T, u = s ∨ u ∈ Set.range t) (hspan : Ideal.span (insert s ↑T) = ⊤) (hcl : IsClosed ↑(rationalRelationIdeal t s)) (i : Fin k) : (P.rationalQuotientRingEquiv T s S hden t ht hsplit hspan hcl) ((Ideal.Quotient.mk (rationalRelationIdeal t s)) (weightedX (fun (x : Fin k) => {1}) ⋯ i)) = ↑(Localization.divBy (t i) s)

The identification sends Xᵢ to tᵢ/s: the class of the variable goes to the image in A⟨T/s⟩ of the fraction divBy (t i) s. The inverse form is rationalQuotientRingEquiv_symm_coe_divBy.

theorem TauCeti.Huber.PairOfDefinition.rationalQuotientRingEquiv_symm_toCompletionLoc {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] [CompleteSpace A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) {k : ℕ} (t : Fin k → A) (ht : ∀ (i : Fin k), t i ∈ T) (hsplit : ∀ u ∈ T, u = s ∨ u ∈ Set.range t) (hspan : Ideal.span (insert s ↑T) = ⊤) (hcl : IsClosed ↑(rationalRelationIdeal t s)) (a : A) : (P.rationalQuotientRingEquiv T s S hden t ht hsplit hspan hcl).symm ((P.toCompletionLoc T s S hden) a) = (Ideal.Quotient.mk (rationalRelationIdeal t s)) ((weightedC (fun (x : Fin k) => {1}) ⋯) a)

The inverse identification on A: it sends the image of a in A⟨T/s⟩ to the class of the constant a. Use it with rw: simp first rewrites toCompletionLoc by toCompletionLoc_apply, so the left-hand side is not in simp normal form.

@[simp]

theorem TauCeti.Huber.PairOfDefinition.rationalQuotientRingEquiv_symm_coe_divBy {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] [CompleteSpace A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) {k : ℕ} (t : Fin k → A) (ht : ∀ (i : Fin k), t i ∈ T) (hsplit : ∀ u ∈ T, u = s ∨ u ∈ Set.range t) (hspan : Ideal.span (insert s ↑T) = ⊤) (hcl : IsClosed ↑(rationalRelationIdeal t s)) (i : Fin k) : (P.rationalQuotientRingEquiv T s S hden t ht hsplit hspan hcl).symm ↑(Localization.divBy (t i) s) = (Ideal.Quotient.mk (rationalRelationIdeal t s)) (weightedX (fun (x : Fin k) => {1}) ⋯ i)

The inverse identification sends tᵢ/s to Xᵢ: the image in A⟨T/s⟩ of the fraction divBy (t i) s goes to the class of the variable. simp and rw find it only while the numerator is still of the form t i; for a concrete listing such as ![f, g], whose entries simp evaluates first, simp [RingEquiv.symm_apply_eq] reaches the class of the variable through rationalQuotientRingEquiv_quotientMk_weightedX instead.

theorem TauCeti.Huber.PairOfDefinition.continuous_rationalQuotientRingEquiv {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] [CompleteSpace A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) {k : ℕ} (t : Fin k → A) (ht : ∀ (i : Fin k), t i ∈ T) (hsplit : ∀ u ∈ T, u = s ∨ u ∈ Set.range t) (hspan : Ideal.span (insert s ↑T) = ⊤) (hcl : IsClosed ↑(rationalRelationIdeal t s)) : Continuous ⇑(P.rationalQuotientRingEquiv T s S hden t ht hsplit hspan hcl)

The identification A⟨X₁, …, Xₖ⟩ ⧸ (tᵢ - s Xᵢ) ≃+* A⟨T/s⟩ is continuous. With continuous_rationalQuotientRingEquiv_symm this makes it an isomorphism of topological rings.

theorem TauCeti.Huber.PairOfDefinition.continuous_rationalQuotientRingEquiv_symm {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] [CompleteSpace A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) {k : ℕ} (t : Fin k → A) (ht : ∀ (i : Fin k), t i ∈ T) (hsplit : ∀ u ∈ T, u = s ∨ u ∈ Set.range t) (hspan : Ideal.span (insert s ↑T) = ⊤) (hcl : IsClosed ↑(rationalRelationIdeal t s)) : Continuous ⇑(P.rationalQuotientRingEquiv T s S hden t ht hsplit hspan hcl).symm

The inverse of the identification A⟨X₁, …, Xₖ⟩ ⧸ (tᵢ - s Xᵢ) ≃+* A⟨T/s⟩ is continuous. With continuous_rationalQuotientRingEquiv this makes it an isomorphism of topological rings.

noncomputable def TauCeti.Huber.PairOfDefinition.rationalQuotientHom {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] [CompleteSpace A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) {k : ℕ} (t : Fin k → A) (ht : ∀ (i : Fin k), t i ∈ T) (hsplit : ∀ u ∈ T, u = s ∨ u ∈ Set.range t) (hspan : Ideal.span (insert s ↑T) = ⊤) (hcl : IsClosed ↑(rationalRelationIdeal t s)) : ↥(weightedRestrictedSubring (fun (x : Fin k) => {1}) ⋯) →+* UniformSpace.Completion S

The presentation map A⟨X₁, …, Xₖ⟩ → A⟨T/s⟩: the quotient map by the relation ideal (tᵢ - s Xᵢ) followed by rationalQuotientRingEquiv. It exhibits the completed rational localisation as a quotient of a restricted power-series ring in one stroke, which is what a caller wanting generators and relations for A⟨T/s⟩ needs: it is surjective (rationalQuotientHom_surjective) and continuous (continuous_rationalQuotientHom), sends a constant to its image under the structure map (rationalQuotientHom_weightedC), takes the relations to zero (rationalQuotientHom_weightedC_mul_weightedX), and has the relation ideal for its kernel (rationalQuotientHom_eq_zero_iff_mem). Its hypotheses are those of rationalQuotientRingEquiv.

Equations

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

theorem TauCeti.Huber.PairOfDefinition.rationalQuotientHom_surjective {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] [CompleteSpace A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) {k : ℕ} (t : Fin k → A) (ht : ∀ (i : Fin k), t i ∈ T) (hsplit : ∀ u ∈ T, u = s ∨ u ∈ Set.range t) (hspan : Ideal.span (insert s ↑T) = ⊤) (hcl : IsClosed ↑(rationalRelationIdeal t s)) : Function.Surjective ⇑(P.rationalQuotientHom T s S hden t ht hsplit hspan hcl)

The presentation map is surjective: every element of A⟨T/s⟩ is the image of a restricted power series. This is what lets a statement about A⟨T/s⟩ be checked on restricted power series, as the Laurent-cover chase does.

theorem TauCeti.Huber.PairOfDefinition.continuous_rationalQuotientHom {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] [CompleteSpace A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) {k : ℕ} (t : Fin k → A) (ht : ∀ (i : Fin k), t i ∈ T) (hsplit : ∀ u ∈ T, u = s ∨ u ∈ Set.range t) (hspan : Ideal.span (insert s ↑T) = ⊤) (hcl : IsClosed ↑(rationalRelationIdeal t s)) : Continuous ⇑(P.rationalQuotientHom T s S hden t ht hsplit hspan hcl)

The presentation map is continuous. With rationalQuotientHom_surjective this is what makes it usable as a presentation of the topological ring A⟨T/s⟩: a continuous map out of A⟨T/s⟩ may be tested after composing with it, by TauCeti.Huber.weightedRestrictedSubring_ringHom_ext_of_continuous.

@[simp]

theorem TauCeti.Huber.PairOfDefinition.rationalQuotientHom_weightedC {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] [CompleteSpace A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) {k : ℕ} (t : Fin k → A) (ht : ∀ (i : Fin k), t i ∈ T) (hsplit : ∀ u ∈ T, u = s ∨ u ∈ Set.range t) (hspan : Ideal.span (insert s ↑T) = ⊤) (hcl : IsClosed ↑(rationalRelationIdeal t s)) (a : A) : (P.rationalQuotientHom T s S hden t ht hsplit hspan hcl) ((weightedC (fun (x : Fin k) => {1}) ⋯) a) = (P.toCompletionLoc T s S hden) a

The presentation map on constants is the structure map A → A⟨T/s⟩.

@[simp]

theorem TauCeti.Huber.PairOfDefinition.rationalQuotientHom_weightedX {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] [CompleteSpace A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) {k : ℕ} (t : Fin k → A) (ht : ∀ (i : Fin k), t i ∈ T) (hsplit : ∀ u ∈ T, u = s ∨ u ∈ Set.range t) (hspan : Ideal.span (insert s ↑T) = ⊤) (hcl : IsClosed ↑(rationalRelationIdeal t s)) (i : Fin k) : (P.rationalQuotientHom T s S hden t ht hsplit hspan hcl) (weightedX (fun (x : Fin k) => {1}) ⋯ i) = ↑(Localization.divBy (t i) s)

The presentation map sends Xᵢ to tᵢ/s.

theorem TauCeti.Huber.PairOfDefinition.rationalQuotientHom_weightedC_mul_weightedX {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] [CompleteSpace A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) {k : ℕ} (t : Fin k → A) (ht : ∀ (i : Fin k), t i ∈ T) (hsplit : ∀ u ∈ T, u = s ∨ u ∈ Set.range t) (hspan : Ideal.span (insert s ↑T) = ⊤) (hcl : IsClosed ↑(rationalRelationIdeal t s)) (i : Fin k) : (P.rationalQuotientHom T s S hden t ht hsplit hspan hcl) ((weightedC (fun (x : Fin k) => {1}) ⋯) s) * (P.rationalQuotientHom T s S hden t ht hsplit hspan hcl) (weightedX (fun (x : Fin k) => {1}) ⋯ i) = (P.rationalQuotientHom T s S hden t ht hsplit hspan hcl) ((weightedC (fun (x : Fin k) => {1}) ⋯) (t i))

The presentation map takes the relations to zero: the images of the constant s and of the variable Xᵢ multiply to the image of the constant tᵢ. This is the relation tᵢ - s Xᵢ read in A⟨T/s⟩, and it is stated this way rather than as Xᵢ ↦ tᵢ/s so that it can be used without naming the fraction; where s is invertible in A⟨T/s⟩ it determines the image of Xᵢ. Unlike the neighbouring normal-form rules this one is not @[simp], and cannot be: simp rewrites the left factor by rationalQuotientHom_weightedC and then by toCompletionLoc_apply, so this left-hand side is not in simp normal form. Use it with rw, or state the goal with the left factor already rewritten.

@[simp]

theorem TauCeti.Huber.PairOfDefinition.rationalQuotientHom_eq_zero_iff_mem {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] [CompleteSpace A] (P : PairOfDefinition A) (T : Finset A) (s : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) {k : ℕ} (t : Fin k → A) (ht : ∀ (i : Fin k), t i ∈ T) (hsplit : ∀ u ∈ T, u = s ∨ u ∈ Set.range t) (hspan : Ideal.span (insert s ↑T) = ⊤) (hcl : IsClosed ↑(rationalRelationIdeal t s)) {u : ↥(weightedRestrictedSubring (fun (x : Fin k) => {1}) ⋯)} : (P.rationalQuotientHom T s S hden t ht hsplit hspan hcl) u = 0 ↔ u ∈ rationalRelationIdeal t s

The kernel of the presentation map is the relation ideal: a restricted power series is taken to zero exactly when it lies in (t₁ - s X₁, …, tₖ - s Xₖ). Read left to right this turns a vanishing statement in A⟨T/s⟩ back into a membership in A⟨X₁, …, Xₖ⟩; read right to left it is rationalRelationIdeal's defining property carried through the quotient map, so a caller can also use it to show that a value of the presentation map vanishes. Together with rationalQuotientHom_surjective, rationalQuotientHom_weightedC and rationalQuotientHom_weightedC_mul_weightedX it presents A⟨T/s⟩ by generators and relations without mentioning the quotient.