Documentation

TauCeti.RingTheory.Huber.LocalizationTopology.Laurent.Identification

Remark 7.55: the Laurent quotient is A⟨T'/s⟩ #

TauCeti.RingTheory.Huber.LocalizationTopology.Laurent.Presentation constructs the two maps between the Laurent quotient A⟨T/s⟩⟨X⟩ ⧸ (t/s - X) and the enlarged rational localisation A⟨T'/s⟩. This file proves them mutually inverse, so that Wedhorn's Remark 7.55 is available as an isomorphism of topological rings.

The identification holds under the same hsplit the second map needs — T' adjoins no numerator beyond t — together with closedness of the relation ideal. For a general enlargement no identification is expected, since T' may adjoin other numerators.

A consumer transports a statement about one side to the other: Proposition 8.30 uses it to carry flatness of the Laurent quotient over A⟨T/s⟩ across to A⟨T'/s⟩.

Main definitions #

Main results #

References #

source
@[simp]
theorem TauCeti.Huber.PairOfDefinition.laurentQuotientRestrictionRingHom_comp_laurentQuotientRingHom {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s t : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s S'] (hden' : P.HasDenominatorPower T' s S') (hTT' : ∀ u ∈ T, u ∈ T') (ht : t ∈ T') (hsplit : ∀ u ∈ T', u ∈ T ∨ u = t) (hcl : IsClosed ↑(P.laurentRelationIdeal T s t S hden)) :
(P.laurentQuotientRestrictionRingHom T s t S hden T' S' hden' hTT' ht).comp (P.laurentQuotientRingHom T s t S hden T' S' hden' hsplit hcl) = RingHom.id (UniformSpace.Completion S')

The two maps of Remark 7.55 compose to the identity of A⟨T'/s⟩: going into the Laurent quotient and back out again is the identity of the enlarged rational localisation.

source
@[simp]
theorem TauCeti.Huber.PairOfDefinition.laurentQuotientRingHom_comp_laurentQuotientRestrictionRingHom {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s t : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s S'] (hden' : P.HasDenominatorPower T' s S') (hTT' : ∀ u ∈ T, u ∈ T') (ht : t ∈ T') (hsplit : ∀ u ∈ T', u ∈ T ∨ u = t) (hcl : IsClosed ↑(P.laurentRelationIdeal T s t S hden)) :
(P.laurentQuotientRingHom T s t S hden T' S' hden' hsplit hcl).comp (P.laurentQuotientRestrictionRingHom T s t S hden T' S' hden' hTT' ht) = RingHom.id (↥(weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯) ⧸ P.laurentRelationIdeal T s t S hden)

The two maps of Remark 7.55 compose to the identity of the Laurent quotient: going out of A⟨T/s⟩⟨X⟩ ⧸ (t/s - X) and back in again is its identity.

source
noncomputable def TauCeti.Huber.PairOfDefinition.laurentQuotientRingEquiv {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s t : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s S'] (hden' : P.HasDenominatorPower T' s S') (hTT' : ∀ u ∈ T, u ∈ T') (ht : t ∈ T') (hsplit : ∀ u ∈ T', u ∈ T ∨ u = t) (hcl : IsClosed ↑(P.laurentRelationIdeal T s t S hden)) :
↥(weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯) ⧸ P.laurentRelationIdeal T s t S hden ≃+* UniformSpace.Completion S'

Wedhorn's Remark 7.55: when the numerators of T' are those of T together with t, the Laurent quotient is A⟨T'/s⟩,

A⟨T/s⟩⟨X⟩ ⧸ (t/s - X)  ≃  A⟨T'/s⟩

the two maps already constructed being mutually inverse. This is the identification Proposition 8.30 consumes: it turns a statement about the Laurent quotient, such as its flatness over A⟨T/s⟩, into the same statement about A⟨T'/s⟩.

Use TauCeti.Huber.PairOfDefinition.continuous_laurentQuotientRingEquiv and its symm form for continuity, and the @[simp] lemmas below to compute: the equivalence is TauCeti.Huber.PairOfDefinition.laurentQuotientRestrictionRingHom and its inverse is TauCeti.Huber.PairOfDefinition.laurentQuotientRingHom.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.Huber.PairOfDefinition.laurentQuotientRingEquiv_coe {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s t : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s S'] (hden' : P.HasDenominatorPower T' s S') (hTT' : ∀ u ∈ T, u ∈ T') (ht : t ∈ T') (hsplit : ∀ u ∈ T', u ∈ T ∨ u = t) (hcl : IsClosed ↑(P.laurentRelationIdeal T s t S hden)) :
    ↑(P.laurentQuotientRingEquiv T s t S hden T' S' hden' hTT' ht hsplit hcl) = P.laurentQuotientRestrictionRingHom T s t S hden T' S' hden' hTT' ht

    The identification is laurentQuotientRestrictionRingHom, as a ring homomorphism: it packages that map together with the inverse supplied by TauCeti.Huber.PairOfDefinition.laurentQuotientRingHom, rather than introducing a new one.

    source
    @[simp]
    theorem TauCeti.Huber.PairOfDefinition.laurentQuotientRingEquiv_apply {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s t : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s S'] (hden' : P.HasDenominatorPower T' s S') (hTT' : ∀ u ∈ T, u ∈ T') (ht : t ∈ T') (hsplit : ∀ u ∈ T', u ∈ T ∨ u = t) (hcl : IsClosed ↑(P.laurentRelationIdeal T s t S hden)) (x : ↥(weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯) ⧸ P.laurentRelationIdeal T s t S hden) :
    (P.laurentQuotientRingEquiv T s t S hden T' S' hden' hTT' ht hsplit hcl) x = (P.laurentQuotientRestrictionRingHom T s t S hden T' S' hden' hTT' ht) x

    The pointwise form of TauCeti.Huber.PairOfDefinition.laurentQuotientRingEquiv_coe.

    source
    @[simp]
    theorem TauCeti.Huber.PairOfDefinition.laurentQuotientRingEquiv_symm_coe {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s t : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s S'] (hden' : P.HasDenominatorPower T' s S') (hTT' : ∀ u ∈ T, u ∈ T') (ht : t ∈ T') (hsplit : ∀ u ∈ T', u ∈ T ∨ u = t) (hcl : IsClosed ↑(P.laurentRelationIdeal T s t S hden)) :
    ↑(P.laurentQuotientRingEquiv T s t S hden T' S' hden' hTT' ht hsplit hcl).symm = P.laurentQuotientRingHom T s t S hden T' S' hden' hsplit hcl

    The inverse of the identification is laurentQuotientRingHom, as a ring homomorphism.

    source
    @[simp]
    theorem TauCeti.Huber.PairOfDefinition.laurentQuotientRingEquiv_symm_apply {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s t : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s S'] (hden' : P.HasDenominatorPower T' s S') (hTT' : ∀ u ∈ T, u ∈ T') (ht : t ∈ T') (hsplit : ∀ u ∈ T', u ∈ T ∨ u = t) (hcl : IsClosed ↑(P.laurentRelationIdeal T s t S hden)) (x : UniformSpace.Completion S') :
    (P.laurentQuotientRingEquiv T s t S hden T' S' hden' hTT' ht hsplit hcl).symm x = (P.laurentQuotientRingHom T s t S hden T' S' hden' hsplit hcl) x

    The pointwise form of TauCeti.Huber.PairOfDefinition.laurentQuotientRingEquiv_symm_coe.

    source
    theorem TauCeti.Huber.PairOfDefinition.continuous_laurentQuotientRingEquiv {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s t : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s S'] (hden' : P.HasDenominatorPower T' s S') (hTT' : ∀ u ∈ T, u ∈ T') (ht : t ∈ T') (hsplit : ∀ u ∈ T', u ∈ T ∨ u = t) (hcl : IsClosed ↑(P.laurentRelationIdeal T s t S hden)) :
    Continuous ⇑(P.laurentQuotientRingEquiv T s t S hden T' S' hden' hTT' ht hsplit hcl)

    The identification is continuous.

    source
    theorem TauCeti.Huber.PairOfDefinition.continuous_laurentQuotientRingEquiv_symm {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) (T : Finset A) (s t : A) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (T' : Finset A) (S' : Type u_3) [CommRing S'] [Algebra A S'] [IsLocalization.Away s S'] (hden' : P.HasDenominatorPower T' s S') (hTT' : ∀ u ∈ T, u ∈ T') (ht : t ∈ T') (hsplit : ∀ u ∈ T', u ∈ T ∨ u = t) (hcl : IsClosed ↑(P.laurentRelationIdeal T s t S hden)) :
    Continuous ⇑(P.laurentQuotientRingEquiv T s t S hden T' S' hden' hTT' ht hsplit hcl).symm

    The inverse of the identification is continuous, so it is a homeomorphism.