The fibrewise criterion for syntomic ring maps

A flat, finitely presented R-algebra A whose fibres κ(p) ⊗[R] A are all locally standard syntomic of relative dimension n over the residue fields κ(p) is itself locally standard syntomic of relative dimension n over R (TauCeti.locally_isStandardSyntomicOfRelativeDimension_of_fiber). This is the affine form of the statement that a flat, locally finitely presented morphism with syntomic fibres of relative dimension n is syntomic of relative dimension n.

Let q be a prime of A over p. A standard syntomic chart (κ(p) ⊗[R] A)[1/t] of the fibre around q lifts, up to a unit of κ(p), to an element a ∉ q of A whose fibre κ(p) ⊗[R] A[1/a] is that chart. Its complete-intersection presentation then lifts to a presentation of some localization A[1/a][1/g] with n + c generators and c relations (Algebra.Presentation.exists_presentation_localizationAway_of_fiber). The fibres of this localization have Krull dimension at least n by Krull's height theorem applied to the base changed presentation, and at most n because they are again locally standard syntomic of relative dimension n over a field (TauCeti.ringKrullDim_le_of_locally_isStandardSyntomicOfRelativeDimension).

Main results

• TauCeti.ringKrullDim_le_of_locally_isStandardSyntomicOfRelativeDimension: an algebra over a field which is locally standard syntomic of relative dimension n has Krull dimension at most n.
• TauCeti.exists_notMem_isStandardSyntomicOfRelativeDimension_localization_away: under the fibrewise hypothesis, every prime q of A has a standard syntomic neighbourhood A[1/g] of relative dimension n with g ∉ q.
• TauCeti.locally_isStandardSyntomicOfRelativeDimension_of_fiber: the fibrewise criterion.

References

• The Stacks Project, Commutative Algebra, Section Syntomic morphisms: a flat finitely presented ring map whose fibre is a local complete intersection at a prime is a relative global complete intersection near that prime.

theorem TauCeti.ringKrullDim_le_of_locally_isStandardSyntomicOfRelativeDimension {n : ℕ} {k A : Type u} [Field k] [CommRing A] [Algebra k A] (h : RingHom.Locally (fun {R S : Type u} [CommRing R] [CommRing S] => IsStandardSyntomicOfRelativeDimension n) (algebraMap k A)) : ringKrullDim A ≤ ↑n

An algebra over a field which is locally standard syntomic of relative dimension n has Krull dimension at most n.

theorem TauCeti.exists_notMem_isStandardSyntomicOfRelativeDimension_localization_away {n : ℕ} {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] [Module.Flat R A] [Algebra.FinitePresentation R A] (h : ∀ (p : Ideal R) [inst : p.IsPrime], RingHom.Locally (fun {R S : Type u} [CommRing R] [CommRing S] => IsStandardSyntomicOfRelativeDimension n) (algebraMap p.ResidueField (p.Fiber A))) (q : Ideal A) [q.IsPrime] : ∃ g ∉ q, Algebra.IsStandardSyntomicOfRelativeDimension n R (Localization.Away g)

Let A be a flat, finitely presented R-algebra all of whose fibres κ(p) ⊗[R] A are locally standard syntomic of relative dimension n over κ(p). Then every prime q of A has a neighbourhood A[1/g], g ∉ q, which is standard syntomic of relative dimension n over R.

theorem TauCeti.locally_isStandardSyntomicOfRelativeDimension_of_fiber {n : ℕ} {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] [Module.Flat R A] [Algebra.FinitePresentation R A] (h : ∀ (p : Ideal R) [inst : p.IsPrime], RingHom.Locally (fun {R S : Type u} [CommRing R] [CommRing S] => IsStandardSyntomicOfRelativeDimension n) (algebraMap p.ResidueField (p.Fiber A))) : RingHom.Locally (fun {R S : Type u} [CommRing R] [CommRing S] => IsStandardSyntomicOfRelativeDimension n) (algebraMap R A)

The fibrewise criterion for syntomic ring maps. A flat, finitely presented R-algebra A whose fibres κ(p) ⊗[R] A are all locally standard syntomic of relative dimension n over κ(p) is locally standard syntomic of relative dimension n over R.