NYLL
Module

FiniteEtaleQuotientLift.lean

Nyll.EtaleFundamentalGroups.Purity.FiniteEtaleQuotientLift
2 declarations indexed from sourceView source ↗

Module documentation

Finite étale algebras over quotients of complete local rings

A finite étale algebra over a quotient of a complete Noetherian local ring splits into finitely many local factors. Lifting those factors separately and taking their product gives a finite étale algebra over the original ring whose base change is the given algebra.

Imports6
Imported by2

Declarations

theorem

exists_finiteEtale_product_lift

L34 ↗
EtaleFundamentalGroups.exists_finiteEtale_product_lift
Documentation

A finite family of finite étale lifts can be assembled into a single lift by taking the product of the lifted algebras.

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_finiteEtale_product_lift
    {R B J : Type u} [CommRing R] [CommRing B] [Algebra R B]
    [Finite J]
    (D : J → Type u) [∀ j, CommRing (D j)] [∀ j, Algebra B (D j)]
    (hlift : ∀ j, ∃ (C : Type u) (_ : CommRing C) (_ : Algebra R C)
      (_ : Module.Finite R C) (_ : Algebra.Etale R C),
      Nonempty (B ⊗[R] C ≃ₐ[B] D j)) :
    ∃ (C : Type u) (_ : CommRing C) (_ : Algebra R C)
      (_ : Module.Finite R C) (_ : Algebra.Etale R C),
      Nonempty (B ⊗[R] C ≃ₐ[B] ∀ j, D j)
theorem

exists_finiteEtale_lift_of_quotient

L59 ↗
EtaleFundamentalGroups.exists_finiteEtale_lift_of_quotient
Documentation

Every finite étale algebra over a quotient of a complete Noetherian local ring is obtained by base change from a 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_finiteEtale_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]
    [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)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.