Documentation

TauCeti.AlgebraicGeometry.AdicSpace.FarguesFontaine.QuotientChart

Images of windows in 𝒳 are the affinoid spectra Spa(B^I, B^{I,+}) #

Let O be the ring of integers of a valuation v : Valuation K ℝβ‰₯0 on a field K, perfect of characteristic p, with a pseudouniformiser Ο–, 0 < v(Ο–) < 1; for O = π’ͺ_F this makes π•Ž O = A_inf. Give π•Ž O its (p, [Ο–])-adic topology and suppose that the structure presheaf π’ͺ_𝒴 of 𝒴 = D(p) ∩ D([Ο–]) βŠ† Spa(π•Ž O, π•Ž O) is a sheaf, so that the Frobenius orbit space 𝒳 = 𝒴 / Ο†^β„€ is a pre-adic space (TauCeti.FarguesFontaine.spaXPreAdicSpace). This file shows that the image in 𝒳 of a window

W = {v ∈ 𝒴 : q ≀ ΞΊ(v) ≀ q'},        0 < q ≀ q',

meeting none of its nontrivial Frobenius translates, such as the windows U_n and V_n, is an open affinoid subspace of 𝒳, isomorphic in 𝒱^pre to Spa(B^I, B^{I,+}) for the interval ring B^I of the radii ρ₁ = v(Ο–) ^ (1 / q) and ρ₂ = v(Ο–) ^ (1 / q').

Two identifications already describe the pieces. TauCeti.FarguesFontaine.windowPreAdicSpaceIso identifies the window, as a restriction of Spa(π•Ž O, π•Ž O), with Spa(B^I, B^{I,+}), and TauCeti.FarguesFontaine.isOpenImmersion_ofRestrict_comp_quotientPreAdicHom makes V β†’ 𝒳 an open immersion for every wandering open V βŠ† 𝒴. The window restriction of Spa(π•Ž O, π•Ž O) and the restriction of 𝒴 to W are open subspaces of Spa(π•Ž O, π•Ž O) with the same image, hence isomorphic, and composing gives the chart Spa(B^I, B^{I,+}) ⟢ 𝒳 with image q(W).

Since the images of U_0 and V_0 cover 𝒳 (TauCeti.FarguesFontaine.image_windowU_zero_union_image_windowV_zero), 𝒳 is covered by two open affinoid subspaces, each isomorphic to the adic spectrum of an interval ring.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.FarguesFontaine.spaXWindowChart {p : β„•} [Fact (Nat.Prime p)] {O : Type u} [CommRing O] {Ο– : O} {q q' : β„šβ‰₯0} {K : Type u_1} [Field K] [Algebra O K] {v : Valuation K NNReal} (hv : v.Integers O) (hΟ– : Ο– β‰  0) (hΟ–' : v ((algebraMap O K) Ο–) < 1) {ρ₁ ρ₂ : NNReal} (hρ₁ : ρ₁ ∈ Set.Ioo 0 1) (hρ₂ : ρ₂ ∈ Set.Ioo 0 1) [TopologicalSpace (WittVector p O)] [IsTopologicalRing (WittVector p O)] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (P : Huber.PairOfDefinition (WittVector p O)) [IsLocalization.Away (WittVector.windowDenominator p Ο– q q') (WittVector.IntervalLocalization p hv hΟ– hΟ–' hρ₁ hρ₂)] (hden : P.HasDenominatorPower (↑(WittVector.windowNumerators p Ο– q q')) (WittVector.windowDenominator p Ο– q q') (WittVector.IntervalLocalization p hv hΟ– hΟ–' hρ₁ hρ₂)) [CharP O p] [PerfectRing O p] (hY : (spaYPresheaf P Ο–).IsSheaf) (h₁ : ρ₁ ^ q.num = v ((algebraMap O K) Ο–) ^ q.den) (hβ‚‚ : ρ₂ ^ q'.num = v ((algebraMap O K) Ο–) ^ q'.den) (h₁₂ : ρ₁ ≀ ρ₂) (P' : Huber.PairOfDefinition (WittVector.IntervalRing p hv hΟ– hΟ–' hρ₁ hρ₂)) :
ValuationSpectrum.presentationLimitPreAdicSpace P' (Huber.powerBoundedSubring (WittVector.IntervalRing p hv hΟ– hΟ–' hρ₁ hρ₂)) β‹― β‹― ⟢ spaXPreAdicSpace P hI hY

The chart of 𝒳 on a window. For the window W = {v ∈ 𝒴 : q ≀ ΞΊ(v) ≀ q'} and radii ρ₁ ^ a = v(Ο–) ^ b, ρ₂ ^ a' = v(Ο–) ^ b' with ρ₁ ≀ ρ₂, where q = a / b and q' = a' / b' in lowest terms, this is the morphism of pre-adic spaces Spa(B^I, B^{I,+}) ⟢ 𝒳 obtained by identifying Spa(B^I, B^{I,+}) with W (windowPreAdicSpaceIso) and composing the inclusion W β†’ 𝒴 with the projection q : 𝒴 β†’ 𝒳. It needs π’ͺ_𝒴 to be a sheaf, as 𝒳 does. When W wanders it is an open immersion (isOpenImmersion_spaXWindowChart) with image q(W) (range_spaXWindowChart_base). Here P' is any pair of definition of B^I.

Instances For
    source
    theorem TauCeti.FarguesFontaine.isOpenImmersion_spaXWindowChart {p : β„•} [Fact (Nat.Prime p)] {O : Type u} [CommRing O] {Ο– : O} {q q' : β„šβ‰₯0} {K : Type u_1} [Field K] [Algebra O K] {v : Valuation K NNReal} (hv : v.Integers O) (hΟ– : Ο– β‰  0) (hΟ–' : v ((algebraMap O K) Ο–) < 1) {ρ₁ ρ₂ : NNReal} (hρ₁ : ρ₁ ∈ Set.Ioo 0 1) (hρ₂ : ρ₂ ∈ Set.Ioo 0 1) [TopologicalSpace (WittVector p O)] [IsTopologicalRing (WittVector p O)] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (P : Huber.PairOfDefinition (WittVector p O)) [IsLocalization.Away (WittVector.windowDenominator p Ο– q q') (WittVector.IntervalLocalization p hv hΟ– hΟ–' hρ₁ hρ₂)] (hden : P.HasDenominatorPower (↑(WittVector.windowNumerators p Ο– q q')) (WittVector.windowDenominator p Ο– q q') (WittVector.IntervalLocalization p hv hΟ– hΟ–' hρ₁ hρ₂)) [CharP O p] [PerfectRing O p] (hY : (spaYPresheaf P Ο–).IsSheaf) (h₁ : ρ₁ ^ q.num = v ((algebraMap O K) Ο–) ^ q.den) (hβ‚‚ : ρ₂ ^ q'.num = v ((algebraMap O K) Ο–) ^ q'.den) (h₁₂ : ρ₁ ≀ ρ₂) (P' : Huber.PairOfDefinition (WittVector.IntervalRing p hv hΟ– hΟ–' hρ₁ hρ₂)) (hW : βˆ€ (k : β„€), k β‰  0 β†’ Disjoint (⇑(frobeniusHomeomorph hI ^ k) ⁻¹' Subtype.val ⁻¹' {v : ValuationSpectrum (WittVector p O) | v ∈ spaY p Ο– ∧ IsRadiusLowerBound p Ο– q v ∧ IsRadiusUpperBound p Ο– q' v}) (Subtype.val ⁻¹' {v : ValuationSpectrum (WittVector p O) | v ∈ spaY p Ο– ∧ IsRadiusLowerBound p Ο– q v ∧ IsRadiusUpperBound p Ο– q' v})) :
    PreAdicSpace.IsOpenImmersion (spaXWindowChart hv hΟ– hΟ–' hρ₁ hρ₂ hI P hden hY h₁ hβ‚‚ h₁₂ P')

    The window chart of 𝒳 is an open immersion when the window W = {q ≀ ΞΊ ≀ q'} wanders, that is, meets none of its nontrivial integer Frobenius translates, as the Frobenius windows U_n and V_n do. It is then an isomorphism of Spa(B^I, B^{I,+}) onto the restriction of 𝒳 to the open image q(W) (PreAdicSpace.IsOpenImmersion.isoRestrict).

    source
    theorem TauCeti.FarguesFontaine.range_spaXWindowChart_base {p : β„•} [Fact (Nat.Prime p)] {O : Type u} [CommRing O] {Ο– : O} {q q' : β„šβ‰₯0} {K : Type u_1} [Field K] [Algebra O K] {v : Valuation K NNReal} (hv : v.Integers O) (hΟ– : Ο– β‰  0) (hΟ–' : v ((algebraMap O K) Ο–) < 1) {ρ₁ ρ₂ : NNReal} (hρ₁ : ρ₁ ∈ Set.Ioo 0 1) (hρ₂ : ρ₂ ∈ Set.Ioo 0 1) [TopologicalSpace (WittVector p O)] [IsTopologicalRing (WittVector p O)] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (P : Huber.PairOfDefinition (WittVector p O)) [IsLocalization.Away (WittVector.windowDenominator p Ο– q q') (WittVector.IntervalLocalization p hv hΟ– hΟ–' hρ₁ hρ₂)] (hden : P.HasDenominatorPower (↑(WittVector.windowNumerators p Ο– q q')) (WittVector.windowDenominator p Ο– q q') (WittVector.IntervalLocalization p hv hΟ– hΟ–' hρ₁ hρ₂)) [CharP O p] [PerfectRing O p] (hY : (spaYPresheaf P Ο–).IsSheaf) (h₁ : ρ₁ ^ q.num = v ((algebraMap O K) Ο–) ^ q.den) (hβ‚‚ : ρ₂ ^ q'.num = v ((algebraMap O K) Ο–) ^ q'.den) (h₁₂ : ρ₁ ≀ ρ₂) (P' : Huber.PairOfDefinition (WittVector.IntervalRing p hv hΟ– hΟ–' hρ₁ hρ₂)) :
    Set.range ⇑(CategoryTheory.ConcreteCategory.hom (spaXWindowChart hv hΟ– hΟ–' hρ₁ hρ₂ hI P hden hY h₁ hβ‚‚ h₁₂ P').base) = quotientMap hI '' Subtype.val ⁻¹' {v : ValuationSpectrum (WittVector p O) | v ∈ spaY p Ο– ∧ IsRadiusLowerBound p Ο– q v ∧ IsRadiusUpperBound p Ο– q' v}

    The image of the window chart is the image q(W) of the window W = {q ≀ ΞΊ ≀ q'} under the projection q : 𝒴 β†’ 𝒳.

    source
    theorem TauCeti.FarguesFontaine.comap_presentationLimitPlusSubring_spaXWindowChart {p : β„•} [Fact (Nat.Prime p)] {O : Type u} [CommRing O] {Ο– : O} {q q' : β„šβ‰₯0} {K : Type u_1} [Field K] [Algebra O K] {v : Valuation K NNReal} (hv : v.Integers O) (hΟ– : Ο– β‰  0) (hΟ–' : v ((algebraMap O K) Ο–) < 1) {ρ₁ ρ₂ : NNReal} (hρ₁ : ρ₁ ∈ Set.Ioo 0 1) (hρ₂ : ρ₂ ∈ Set.Ioo 0 1) [TopologicalSpace (WittVector p O)] [IsTopologicalRing (WittVector p O)] (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})) (P : Huber.PairOfDefinition (WittVector p O)) [IsLocalization.Away (WittVector.windowDenominator p Ο– q q') (WittVector.IntervalLocalization p hv hΟ– hΟ–' hρ₁ hρ₂)] (hden : P.HasDenominatorPower (↑(WittVector.windowNumerators p Ο– q q')) (WittVector.windowDenominator p Ο– q q') (WittVector.IntervalLocalization p hv hΟ– hΟ–' hρ₁ hρ₂)) [CharP O p] [PerfectRing O p] (hY : (spaYPresheaf P Ο–).IsSheaf) (h₁ : ρ₁ ^ q.num = v ((algebraMap O K) Ο–) ^ q.den) (hβ‚‚ : ρ₂ ^ q'.num = v ((algebraMap O K) Ο–) ^ q'.den) (h₁₂ : ρ₁ ≀ ρ₂) (P' : Huber.PairOfDefinition (WittVector.IntervalRing p hv hΟ– hΟ–' hρ₁ hρ₂)) {V : TopologicalSpace.Opens ↑(spaXPreAdicSpace P hI hY).toTopCat} (hV : ↑V βŠ† quotientMap hI '' Subtype.val ⁻¹' {v : ValuationSpectrum (WittVector p O) | v ∈ spaY p Ο– ∧ IsRadiusLowerBound p Ο– q v ∧ IsRadiusUpperBound p Ο– q' v}) :
    Subring.comap (CommRingCat.Hom.hom ((PreAdicSpace.toRingPresheafedSpaceHom (spaXWindowChart hv hΟ– hΟ–' hρ₁ hρ₂ hI P hden hY h₁ hβ‚‚ h₁₂ P').toHom).c.app (Opposite.op V))) (ValuationSpectrum.presentationLimitPlusSubring β‹― β‹― ((TopologicalSpace.Opens.map (spaXWindowChart hv hΟ– hΟ–' hρ₁ hρ₂ hI P hden hY h₁ hβ‚‚ h₁₂ P').base).obj V)) = (spaXPreAdicSpace P hI hY).plusSubring V

    The window chart identifies integral sections. Over an open V βŠ† q(W) of 𝒳, a section of π’ͺ_𝒳 over V lies in π’ͺ_𝒳⁺(V) exactly when its pullback along the chart lies in the plus subring π’ͺ⁺(V') of Spa(B^I, B^{I,+}) over the preimage V' of V. On a rational open V' this plus subring is the plus ring of the rational localisation of (B^I, B^{I,+}), by Wedhorn's Proposition 8.16 (map_completedPlusSubring_eq_presentationLimitPlusSubring).

    source
    theorem TauCeti.FarguesFontaine.quotientMap_image_window_mem_affinoidOpens {p : β„•} [Fact (Nat.Prime p)] {O : Type u} [CommRing O] {Ο– : O} {q q' : β„šβ‰₯0} {K : Type u_1} [Field K] [Algebra O K] {v : Valuation K NNReal} [CharP O p] [PerfectRing O p] (hv : v.Integers O) (hΟ– : Ο– β‰  0) (hΟ–' : v ((algebraMap O K) Ο–) < 1) [TopologicalSpace (WittVector p O)] [IsTopologicalRing (WittVector p O)] {hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})} {P : Huber.PairOfDefinition (WittVector p O)} (hY : (spaYPresheaf P Ο–).IsSheaf) (hq : q β‰  0) (hqq' : q ≀ q') (hW : βˆ€ (k : β„€), k β‰  0 β†’ Disjoint (⇑(frobeniusHomeomorph hI ^ k) ⁻¹' Subtype.val ⁻¹' {v : ValuationSpectrum (WittVector p O) | v ∈ spaY p Ο– ∧ IsRadiusLowerBound p Ο– q v ∧ IsRadiusUpperBound p Ο– q' v}) (Subtype.val ⁻¹' {v : ValuationSpectrum (WittVector p O) | v ∈ spaY p Ο– ∧ IsRadiusLowerBound p Ο– q v ∧ IsRadiusUpperBound p Ο– q' v})) :
    { carrier := quotientMap hI '' Subtype.val ⁻¹' {v : ValuationSpectrum (WittVector p O) | v ∈ spaY p Ο– ∧ IsRadiusLowerBound p Ο– q v ∧ IsRadiusUpperBound p Ο– q' v}, is_open' := β‹― } ∈ (spaXPreAdicSpace P hI hY).affinoidOpens

    The image in 𝒳 of a wandering window is an open affinoid subspace. Let O be the ring of integers of v, perfect of characteristic p, with pseudouniformiser Ο–, and suppose π’ͺ_𝒴 is a sheaf. If 0 < q ≀ q' and the window W = {v ∈ 𝒴 : q ≀ ΞΊ(v) ≀ q'} meets none of its nontrivial integer Frobenius translates, then 𝒳 restricted to q(W) is affinoid: it is isomorphic to Spa(B^I, B^{I,+}) for the interval I = [v(Ο–) ^ (1 / q), v(Ο–) ^ (1 / q')], through the window chart spaXWindowChart.

    source
    theorem TauCeti.FarguesFontaine.quotientMap_image_windowU_mem_affinoidOpens {p : β„•} [Fact (Nat.Prime p)] {O : Type u} [CommRing O] {Ο– : O} {K : Type u_1} [Field K] [Algebra O K] {v : Valuation K NNReal} [CharP O p] [PerfectRing O p] (hv : v.Integers O) (hΟ– : Ο– β‰  0) (hΟ–' : v ((algebraMap O K) Ο–) < 1) [TopologicalSpace (WittVector p O)] [IsTopologicalRing (WittVector p O)] {hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})} {P : Huber.PairOfDefinition (WittVector p O)} (hY : (spaYPresheaf P Ο–).IsSheaf) (n : β„€) :
    { carrier := quotientMap hI '' Subtype.val ⁻¹' windowU p Ο– n, is_open' := β‹― } ∈ (spaXPreAdicSpace P hI hY).affinoidOpens

    The image of the window U_n = {p ^ n ≀ ΞΊ ≀ c p ^ n} in 𝒳 is an open affinoid subspace, isomorphic to Spa(B^I, B^{I,+}) for the matching interval I, when π’ͺ_𝒴 is a sheaf.

    source
    theorem TauCeti.FarguesFontaine.quotientMap_image_windowV_mem_affinoidOpens {p : β„•} [Fact (Nat.Prime p)] {O : Type u} [CommRing O] {Ο– : O} {K : Type u_1} [Field K] [Algebra O K] {v : Valuation K NNReal} [CharP O p] [PerfectRing O p] (hv : v.Integers O) (hΟ– : Ο– β‰  0) (hΟ–' : v ((algebraMap O K) Ο–) < 1) [TopologicalSpace (WittVector p O)] [IsTopologicalRing (WittVector p O)] {hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) Ο–})} {P : Huber.PairOfDefinition (WittVector p O)} (hY : (spaYPresheaf P Ο–).IsSheaf) (n : β„€) :
    { carrier := quotientMap hI '' Subtype.val ⁻¹' windowV p Ο– n, is_open' := β‹― } ∈ (spaXPreAdicSpace P hI hY).affinoidOpens

    The image of the window V_n = {c p ^ n ≀ ΞΊ ≀ p ^ (n + 1)} in 𝒳 is an open affinoid subspace, isomorphic to Spa(B^I, B^{I,+}) for the matching interval I, when π’ͺ_𝒴 is a sheaf.