Documentation

TauCeti.AlgebraicGeometry.AdicSpace.Spa.Localization.FaithfullyFlat

Faithful flatness of a rational cover #

Wedhorn's Corollary 8.32: let A be a complete Hausdorff strongly noetherian Tate ring and let the rational subsets R(Tᵢ/sᵢ) of a finite family cover Spa(A, A⁺). Then the map A → ∏ᵢ A⟨Tᵢ/sᵢ⟩ into the product of the rational localisations is faithfully flat, and in particular injective.

Each factor is flat by TauCeti.Huber.PairOfDefinition.flat_toCompletionLoc. For faithfulness, a maximal ideal of A is the support of a point of Spa(A, A⁺) (TauCeti.ValuationSpectrum.exists_mem_spa_supp_eq_of_isMaximal). That point lies in some R(Tᵢ/sᵢ), and its support stays proper in A⟨Tᵢ/sᵢ⟩ by TauCeti.ValuationSpectrum.map_supp_toCompletionLoc_ne_top. These are the two hypotheses of RingHom.FaithfullyFlat.pi_of_exists_map_ne_top, the faithful-flatness criterion for a finite product of flat ring homomorphisms.

Main results #

References #

Provenance #

AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0), branch dev/adic-spaces at commit 37bbdaeb9ad9e3bc9f0d660feadc2779e455a91c, was consulted. Its file projects/AdicSpaces/Adic spaces/Cor832.lean proves the maximal-ideal criterion for a finite product of flat algebras (faithfullyFlat_pi_of_maximal_ne_top) and states the corollary with chart flatness and prime lifting as hypotheses. AuditCleanWrappers.lean (cor_8_32_clean_proof) discharges these for its presheaf values by lifting primes to points of Spa, through lemmas that are still sorried there. The argument here has the same shape, but its inputs are Tau Ceti's own flatness and support lemmas, and no code is ported.

source
theorem TauCeti.ValuationSpectrum.faithfullyFlat_pi_toCompletionLoc {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [CompleteSpace A] [T0Space A] [Huber.IsTateRing A] [Huber.IsStronglyNoetherian A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hplus : Huber.IsRingOfIntegralElements Aplus) (hP : P.ringOfDefinition ≤ Aplus) {ι : Type u_2} [Finite ι] (T : ι → Finset A) (s : ι → A) (S : ι → Type u_3) [(i : ι) → CommRing (S i)] [(i : ι) → Algebra A (S i)] [∀ (i : ι), IsLocalization.Away (s i) (S i)] (hden : ∀ (i : ι), P.HasDenominatorPower (T i) (s i) (S i)) (hcov : spa Aplus ⊆ ⋃ (i : ι), rationalSubset Aplus (T i) (s i)) :
(RingHom.pi fun (i : ι) => P.toCompletionLoc (T i) (s i) (S i) ⋯).FaithfullyFlat

Wedhorn's Corollary 8.32, faithful flatness. If the rational subsets R(Tᵢ/sᵢ) of a finite family cover Spa(A, A⁺), then the map A → ∏ᵢ A⟨Tᵢ/sᵢ⟩ into the product of the rational localisations is faithfully flat. Here A is a complete Hausdorff strongly noetherian Tate ring, and A⁺ is a ring of integral elements containing the chosen ring of definition. For the standard rational cover of a set generating the unit ideal, where no A⁺ has to be chosen, see faithfullyFlat_rationalLocalizationPiHom_of_span_eq_top.

source
theorem TauCeti.ValuationSpectrum.pi_toCompletionLoc_injective {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [CompleteSpace A] [T0Space A] [Huber.IsTateRing A] [Huber.IsStronglyNoetherian A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (hplus : Huber.IsRingOfIntegralElements Aplus) (hP : P.ringOfDefinition ≤ Aplus) {ι : Type u_2} [Finite ι] (T : ι → Finset A) (s : ι → A) (S : ι → Type u_3) [(i : ι) → CommRing (S i)] [(i : ι) → Algebra A (S i)] [∀ (i : ι), IsLocalization.Away (s i) (S i)] (hden : ∀ (i : ι), P.HasDenominatorPower (T i) (s i) (S i)) (hcov : spa Aplus ⊆ ⋃ (i : ι), rationalSubset Aplus (T i) (s i)) :
Function.Injective ⇑(RingHom.pi fun (i : ι) => P.toCompletionLoc (T i) (s i) (S i) ⋯)

Wedhorn's Corollary 8.32, injectivity. If the rational subsets R(Tᵢ/sᵢ) of a finite family cover Spa(A, A⁺), then the map A → ∏ᵢ A⟨Tᵢ/sᵢ⟩ is injective. It is even faithfully flat (faithfullyFlat_pi_toCompletionLoc); for the standard rational cover of a set generating the unit ideal, see rationalLocalizationPiHom_injective_of_span_eq_top.

source
theorem TauCeti.ValuationSpectrum.faithfullyFlat_rationalLocalizationPiHom_of_span_eq_top {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [CompleteSpace A] [T0Space A] [Huber.IsTateRing A] [Huber.IsStronglyNoetherian A] (P : Huber.PairOfDefinition A) {T : Finset A} (hT : Ideal.span ↑T = ⊤) (S : ↥T → Type u_2) [(t : ↥T) → CommRing (S t)] [(t : ↥T) → Algebra A (S t)] [∀ (t : ↥T), IsLocalization.Away (↑t) (S t)] (hden : ∀ (t : ↥T), P.HasDenominatorPower T (↑t) (S t)) :
(P.rationalLocalizationPiHom T S hden).FaithfullyFlat

Corollary 8.32 for a standard rational cover. When T generates the unit ideal, the structure map A → ∏_{t ∈ T} A⟨T/t⟩ into the family of rational localisations is faithfully flat. This is faithfullyFlat_pi_toCompletionLoc for the family (R(T/t))_{t ∈ T}; the unit-ideal condition on T takes the place of its ring of integral elements A⁺ and covering hypothesis.

source
theorem TauCeti.ValuationSpectrum.rationalLocalizationPiHom_injective_of_span_eq_top {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [CompleteSpace A] [T0Space A] [Huber.IsTateRing A] [Huber.IsStronglyNoetherian A] (P : Huber.PairOfDefinition A) {T : Finset A} (hT : Ideal.span ↑T = ⊤) (S : ↥T → Type u_2) [(t : ↥T) → CommRing (S t)] [(t : ↥T) → Algebra A (S t)] [∀ (t : ↥T), IsLocalization.Away (↑t) (S t)] (hden : ∀ (t : ↥T), P.HasDenominatorPower T (↑t) (S t)) :
Function.Injective ⇑(P.rationalLocalizationPiHom T S hden)

Corollary 8.32 for a standard rational cover, injectivity. When T generates the unit ideal, the structure map A → ∏_{t ∈ T} A⟨T/t⟩ is injective. It is even faithfully flat (faithfullyFlat_rationalLocalizationPiHom_of_span_eq_top); for an arbitrary finite rational cover of Spa(A, A⁺), see pi_toCompletionLoc_injective.