Documentation

TauCeti.RingTheory.RingHom.StandardSyntomic

Standard syntomic ring homomorphisms #

This file expresses standard syntomic algebras as a property of ring homomorphisms. Localization on either side and arbitrary base change preserve the relative dimension. Consequently the property of being locally standard syntomic is local on both source and base, giving the affine input for syntomic morphisms of schemes. Standard smooth ring maps are standard syntomic with the same relative dimension.

Use TauCeti.IsStandardSyntomicOfRelativeDimension n f for the ring-map predicate; given a proof hf, its consequences are available as hf.flat and hf.finitePresentation. The theorem TauCeti.isStandardSyntomicOfRelativeDimension_iff n f relates an arbitrary ring map to its induced algebra structure. With hf as above, both conversions use the public bridge:

have hAlg := (TauCeti.isStandardSyntomicOfRelativeDimension_iff n f).mp hf
have hRing := (TauCeti.isStandardSyntomicOfRelativeDimension_iff n f).mpr hAlg

The relative dimension is the first explicit argument, as in RingHom.IsStandardSmoothOfRelativeDimension.

For example, the proof methods supply both ring-map consequences:

example (n : ℕ) {R S : Type*} [CommRing R] [CommRing S]
    (f : R →+* S) (hf : TauCeti.IsStandardSyntomicOfRelativeDimension n f) :
    f.Flat ∧ f.FinitePresentation := by
  exact ⟨hf.flat, hf.finitePresentation⟩

The ring-homomorphism bridge follows Mathlib's RingHom.IsStandardSmoothOfRelativeDimension in Mathlib/RingTheory/RingHom/StandardSmooth.lean, by Christian Merten. The underlying complete-intersection definition follows the Stacks Project, Syntomic morphisms.

source
def TauCeti.IsStandardSyntomicOfRelativeDimension (n : ℕ) {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) :
Prop

A ring homomorphism is standard syntomic of relative dimension n if its target, with the algebra structure induced by the homomorphism, is such an algebra.

Equations
Instances For
    source
    theorem TauCeti.isStandardSyntomicOfRelativeDimension_iff {R : Type u} {S : Type v} [CommRing R] [CommRing S] (n : ℕ) (f : R →+* S) :
    IsStandardSyntomicOfRelativeDimension n f ↔ Algebra.IsStandardSyntomicOfRelativeDimension n R S

    A ring map is standard syntomic of relative dimension n exactly when its target is standard syntomic for the induced algebra structure.

    source
    @[simp]
    theorem TauCeti.isStandardSyntomicOfRelativeDimension_algebraMap {n : ℕ} {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] :
    IsStandardSyntomicOfRelativeDimension n (algebraMap R S) ↔ Algebra.IsStandardSyntomicOfRelativeDimension n R S

    The ring-homomorphism and algebra formulations agree on an algebra map.

    source
    theorem RingHom.IsStandardSmoothOfRelativeDimension.isStandardSyntomicOfRelativeDimension {n : ℕ} {R : Type u} {S : Type v} [CommRing R] [CommRing S] {f : R →+* S} (hf : IsStandardSmoothOfRelativeDimension n f) :
    TauCeti.IsStandardSyntomicOfRelativeDimension n f

    A standard smooth ring map is standard syntomic of the same relative dimension.

    source
    theorem TauCeti.IsStandardSyntomicOfRelativeDimension.id (R : Type u) [CommRing R] :
    IsStandardSyntomicOfRelativeDimension 0 (RingHom.id R)

    The identity ring map is standard syntomic of relative dimension zero.

    source
    theorem TauCeti.IsStandardSyntomicOfRelativeDimension.flat {n : ℕ} {R : Type u} {S : Type v} [CommRing R] [CommRing S] {f : R →+* S} (hf : IsStandardSyntomicOfRelativeDimension n f) :
    f.Flat

    Standard syntomic ring maps are flat.

    source
    theorem TauCeti.IsStandardSyntomicOfRelativeDimension.finitePresentation {n : ℕ} {R : Type u} {S : Type v} [CommRing R] [CommRing S] {f : R →+* S} (hf : IsStandardSyntomicOfRelativeDimension n f) :
    f.FinitePresentation

    Standard syntomic ring maps are finitely presented.

    source
    theorem TauCeti.isStandardSyntomicOfRelativeDimension_stableUnderCompositionWithLocalizationAway (n : ℕ) :
    RingHom.StableUnderCompositionWithLocalizationAway (@IsStandardSyntomicOfRelativeDimension n)

    Localizing either side of a standard syntomic map preserves its relative dimension.

    source
    theorem TauCeti.isStandardSyntomicOfRelativeDimension_respectsIso (n : ℕ) :
    RingHom.RespectsIso (@IsStandardSyntomicOfRelativeDimension n)

    Standard syntomic ring maps are invariant under isomorphisms on either side.

    source
    theorem TauCeti.isStandardSyntomicOfRelativeDimension_isStableUnderBaseChange (n : ℕ) :
    RingHom.IsStableUnderBaseChange (@IsStandardSyntomicOfRelativeDimension n)

    Arbitrary base change preserves standard syntomic ring maps and their relative dimension.

    source
    theorem TauCeti.locally_isStandardSyntomicOfRelativeDimension_propertyIsLocal (n : ℕ) :
    RingHom.PropertyIsLocal fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.Locally (@IsStandardSyntomicOfRelativeDimension n)

    Being locally standard syntomic of fixed relative dimension is local on source and base.