Module

FormallyUnramifiedDescent.lean

Nyll.EtaleFundamentalGroups.Kummer.Descent.FormallyUnramifiedDescent

1 declaration indexed from sourceView source ↗

Module documentation

Faithfully flat descent of formal unramifiedness

Formal unramifiedness of a composite descends across a formally etale, faithfully flat final map. The proof identifies the base change of the Kaehler differentials with the differentials of the composite and then uses faithful flatness to reflect triviality.

Imports2

Mathlib.RingTheory.Etale.Kaehler
Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Imported by4

theorem

formallyUnramified_of_formallyEtale_faithfullyFlat

L29 ↗

EtaleFundamentalGroups.Kummer.formallyUnramified_of_formallyEtale_faithfullyFlat

Documentation

If T is formally unramified over R, and T/S is both formally etale and faithfully flat, then S is formally unramified over R.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace EtaleFundamentalGroups.Kummer
open scoped TensorProduct
universe uR uS uT

Lean source · statement

theorem formallyUnramified_of_formallyEtale_faithfullyFlat
    {R : Type uR} {S : Type uS} {T : Type uT}
    [CommRing R] [CommRing S] [CommRing T]
    [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T]
    [Algebra.FormallyUnramified R T] [Algebra.FormallyEtale S T]
    [Module.FaithfullyFlat S T] :
    Algebra.FormallyUnramified R S

Module documentation

Faithfully flat descent of formal unramifiedness

Declarations

formallyUnramified_of_formallyEtale_faithfullyFlat