NYLL
Module

HenselianQuotientLift.lean

Nyll.SchemeTheory.FiniteEtale.Algebra.HenselianQuotientLift
1 declaration indexed from sourceView source ↗

Module documentation

Lifting finite étale algebras over Henselian pairs

First lift the étale presentation. Its finite special fiber selects a factor of the integral closure on a principal neighborhood. Lift the corresponding idempotent using the Henselian pair, and transport its factor through that localization. The resulting factor of the étale lift is integral, hence finite, and still has the prescribed special fiber.

Imports13
Imported by2

Declarations

theorem

exists_lift_of_quotient_of_henselian

L44 ↗
Algebra.FiniteEtale.exists_lift_of_quotient_of_henselian
Documentation

Every finite étale algebra over the quotient of a Henselian pair is the reduction of a finite étale algebra over the original ring.

Source context 5 commands

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

@[expose] public section
open AlgebraicGeometry
open scoped TensorProduct
universe u
namespace Algebra.FiniteEtale
Lean source · statement
theorem exists_lift_of_quotient_of_henselian
    {R A : Type u} [CommRing R] [CommRing A] (I : Ideal R) [HenselianRing R I]
    [Algebra (R ⧸ I) A] [Module.Finite (R ⧸ I) A] [Algebra.Etale (R ⧸ I) A] :
    ∃ B : CommAlgCat.{u} R, Module.Finite R B ∧ Algebra.Etale R B ∧
      Nonempty ((R ⧸ I) ⊗[R] B ≃ₐ[R ⧸ I] A)

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