Standard syntomic algebras and localization

Standard syntomic algebras of relative dimension n are stable under composition with localizations away from an element, on either side:

• if S is standard syntomic of relative dimension n over R and g ∈ S, then so is S[1/g];
• if r ∈ R and T is standard syntomic of relative dimension n over R[1/r], then T is standard syntomic of relative dimension n over R.

In both cases a presentation is obtained by composing with the presentation of a localization by one generator x and one relation rx - 1, which adds one generator and one relation. The content is the fibre dimension. In the first case the fibre of S[1/g] over a prime p is the localization of the fibre κ(p) ⊗[R] S at 1 ⊗ g. This fibre is a global complete intersection over κ(p), so each of its nonzero localizations still has dimension n (Algebra.Presentation.ringKrullDim_eq_of_isLocalization_away). In the second case a nonempty fibre lies over a prime p not containing r, and κ(p) ⊗[R] T is then the fibre κ(p) ⊗[R[1/r]] T of T over R[1/r].

These two stability properties, together with stability under base change, are what make "locally standard syntomic of relative dimension n" a property of ring maps that is local on the source and the target, and hence define syntomic morphisms of schemes of relative dimension n.

Main results

• TauCeti.Algebra.IsStandardSyntomicOfRelativeDimension.trans_localization_away: if S is standard syntomic of relative dimension n over R, so is every localization S[1/g].
• TauCeti.Algebra.IsStandardSyntomicOfRelativeDimension.localization_away_trans: an algebra that is standard syntomic of relative dimension n over R[1/r] is standard syntomic of relative dimension n over R.

References

• The Stacks Project, Commutative Algebra, Section Syntomic morphisms: the stability of relative global complete intersections under localization S → S_g, and the locality of syntomic ring maps.

theorem TauCeti.Algebra.IsStandardSyntomicOfRelativeDimension.trans_localization_away {n : ℕ} {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T] [h : IsStandardSyntomicOfRelativeDimension n R S] (g : S) [IsLocalization.Away g T] : IsStandardSyntomicOfRelativeDimension n R T

If S is standard syntomic of relative dimension n over R, then so is its localization S[1/g] away from any g ∈ S.

theorem TauCeti.Algebra.IsStandardSyntomicOfRelativeDimension.localization_away_trans {n : ℕ} {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T] (r : R) [IsLocalization.Away r S] [h : IsStandardSyntomicOfRelativeDimension n S T] : IsStandardSyntomicOfRelativeDimension n R T

If T is standard syntomic of relative dimension n over the localization S = R[1/r] of R away from r, then T is standard syntomic of relative dimension n over R.