Étale algebras, norms and differentials

Algebras over commutative rings: étale algebras and the trace form, norm and trace maps, Kähler differentials and derivations.

• Algebra homomorphisms into an algebraically closed field
• Iterated derivations and the Leibniz rule
• Kähler differentials
• Localizations of smooth and étale algebras
• Norm and trace of algebras
• Point derivations
• Tensor products of reduced algebras and domains
• Étale algebras and the trace form

TheoremUniversal-property criterion for a pushout square of algebras#✓fully proved

A square of algebras is a pushout when it satisfies the universal property for algebra homomorphisms: for every R'-algebra T and every g : S →+* T compatible with the maps from R, there is a unique R'-algebra map S' →ₐ[R'] T extending g. The rings may lie in independent universes; it suffices to quantify T in the maximum of the universes of S, R', and S'.

This is the hands-on criterion for recognizing pushouts (tensor products) without computing the tensor product: it is used to identify fiber products of schemes, base changes, and tensor-product decompositions from their mapping properties.

theorem isPushout_of_forall_existsUnique_algHom_comp_eq
    {R : Type u} {S : Type v} {R' : Type w} {S' : Type x}
    [CommRing R] [CommRing S] [CommRing R'] [CommRing S']
    [Algebra R S] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S']
    [IsScalarTower R S S'] [IsScalarTower R R' S']
    (h : ∀ (T : Type max v w x) [CommRing T] [Algebra R' T] (g : S →+* T),
      g.comp (algebraMap R S) = (algebraMap R' T).comp (algebraMap R R') →
        ∃! k : S' →ₐ[R'] T, k.toRingHom.comp (algebraMap S S') = g) :
    Algebra.IsPushout R S R' S'

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.