Module

FiniteEtaleQuotientLift.lean

Nyll.EtaleFundamentalGroups.Purity.Local.FiniteEtaleQuotientLift

3 declarations indexed from sourceView source ↗

Module documentation

Finite étale local algebras over complete local quotients

A finite étale local algebra over a quotient of a complete Noetherian local ring is the base change of a finite étale algebra over the original ring. The lift is the explicit monogenic lift of the residue-field extension.

Imports2

Imported by2

theorem

residueField_map_bijective_of_surjective

L28 ↗

EtaleFundamentalGroups.residueField_map_bijective_of_surjective

Documentation

A surjective local homomorphism induces an isomorphism on residue fields.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u

Lean source · statement

theorem residueField_map_bijective_of_surjective
    {R S : Type u} [CommRing R] [CommRing S]
    [IsLocalRing R] [IsLocalRing S]
    (f : R →+* S) [IsLocalHom f] (hf : Function.Surjective f) :
    Function.Bijective (ResidueField.map f)

theorem

isLocalHom_algebraMap_of_moduleFinite_of_isLocalRing

L40 ↗

EtaleFundamentalGroups.isLocalHom_algebraMap_of_moduleFinite_of_isLocalRing

Documentation

The algebra map of a finite extension between local rings is local.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u

Lean source · statement

theorem isLocalHom_algebraMap_of_moduleFinite_of_isLocalRing
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    [IsLocalRing R] [IsLocalRing S] [Module.Finite R S] :
    IsLocalHom (algebraMap R S)

theorem

exists_finiteEtaleLocal_lift_of_quotient

L57 ↗

EtaleFundamentalGroups.exists_finiteEtaleLocal_lift_of_quotient

Documentation

Every finite étale local algebra over a proper quotient of a complete Noetherian local ring is obtained by base change from an explicit finite étale algebra over the original ring.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u

Lean source · statement

theorem exists_finiteEtaleLocal_lift_of_quotient
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    [IsAdicComplete (maximalIdeal R) R]
    (I : Ideal R) (hI : I ≤ maximalIdeal R)
    {D : Type u} [CommRing D] [Algebra (R ⧸ I) D]
    [IsLocalRing D] [Module.Finite (R ⧸ I) D]
    [Algebra.Etale (R ⧸ I) D] :
    ∃ (C : Type u) (_ : CommRing C) (_ : Algebra R C)
      (_ : Module.Finite R C) (_ : Algebra.Etale R C),
      Nonempty (((R ⧸ I) ⊗[R] C) ≃ₐ[R ⧸ I] D)

Module documentation

Finite étale local algebras over complete local quotients

Declarations

residueField_map_bijective_of_surjective

isLocalHom_algebraMap_of_moduleFinite_of_isLocalRing

exists_finiteEtaleLocal_lift_of_quotient