NYLL
Module

ResidueLift.lean

Nyll.EtaleFundamentalGroups.Completions.FiniteEtale.ResidueLift
18 declarations indexed from sourceView source ↗

Module documentation

Lifting a finite separable residue extension

Let R be a local ring and let l / κ(R) be finite separable. We choose a power-basis generator of l, lift its minimal polynomial coefficientwise to a monic polynomial over R, and adjoin a root. The resulting algebra is local, finite, and étale over R, and its residue extension is l / κ(R).

The local structure is not registered globally. It is produced from the explicit special fibre: quotienting the adjoined-root algebra by the extended maximal ideal gives the adjoined root of the residue minimal polynomial, hence a field.

Imports5
Imported by2

Declarations

def

finiteEtaleResidueLiftPowerBasis

L41 ↗
EtaleFundamentalGroups.finiteEtaleResidueLiftPowerBasis
Documentation

A chosen power basis for a finite separable residue extension.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u
variable (R l : Type u) [CommRing R] [IsLocalRing R]
  [Field l] [Algebra (IsLocalRing.ResidueField R) l]
  [FiniteDimensional (IsLocalRing.ResidueField R) l]
  [Algebra.IsSeparable (IsLocalRing.ResidueField R) l]
Lean source · statement
def finiteEtaleResidueLiftPowerBasis :
    PowerBasis (IsLocalRing.ResidueField R) l
theorem

exists_monic_residue_polynomial_lift

L45 ↗
EtaleFundamentalGroups.exists_monic_residue_polynomial_lift
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u
variable (R l : Type u) [CommRing R] [IsLocalRing R]
  [Field l] [Algebra (IsLocalRing.ResidueField R) l]
  [FiniteDimensional (IsLocalRing.ResidueField R) l]
  [Algebra.IsSeparable (IsLocalRing.ResidueField R) l]
Lean source · statement
theorem exists_monic_residue_polynomial_lift :
    ∃ f : R[X],
      f.map (IsLocalRing.residue R) =
          minpoly (IsLocalRing.ResidueField R)
            (finiteEtaleResidueLiftPowerBasis R l).gen ∧
        f.natDegree =
          (minpoly (IsLocalRing.ResidueField R)
            (finiteEtaleResidueLiftPowerBasis R l).gen).natDegree ∧
        f.Monic
def

finiteEtaleResidueLiftPolynomial

L64 ↗
EtaleFundamentalGroups.finiteEtaleResidueLiftPolynomial
Documentation

A monic lift of the minimal polynomial of a chosen residue generator.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u
variable (R l : Type u) [CommRing R] [IsLocalRing R]
  [Field l] [Algebra (IsLocalRing.ResidueField R) l]
  [FiniteDimensional (IsLocalRing.ResidueField R) l]
  [Algebra.IsSeparable (IsLocalRing.ResidueField R) l]
Lean source · statement
def finiteEtaleResidueLiftPolynomial : R[X]
theorem

finiteEtaleResidueLiftPolynomial_map

L67 ↗
EtaleFundamentalGroups.finiteEtaleResidueLiftPolynomial_map
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u
variable (R l : Type u) [CommRing R] [IsLocalRing R]
  [Field l] [Algebra (IsLocalRing.ResidueField R) l]
  [FiniteDimensional (IsLocalRing.ResidueField R) l]
  [Algebra.IsSeparable (IsLocalRing.ResidueField R) l]
Lean source · statement
theorem finiteEtaleResidueLiftPolynomial_map :
    (finiteEtaleResidueLiftPolynomial R l).map (IsLocalRing.residue R) =
      minpoly (IsLocalRing.ResidueField R)
        (finiteEtaleResidueLiftPowerBasis R l).gen
theorem

finiteEtaleResidueLiftPolynomial_natDegree

L73 ↗
EtaleFundamentalGroups.finiteEtaleResidueLiftPolynomial_natDegree
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u
variable (R l : Type u) [CommRing R] [IsLocalRing R]
  [Field l] [Algebra (IsLocalRing.ResidueField R) l]
  [FiniteDimensional (IsLocalRing.ResidueField R) l]
  [Algebra.IsSeparable (IsLocalRing.ResidueField R) l]
Lean source · statement
theorem finiteEtaleResidueLiftPolynomial_natDegree :
    (finiteEtaleResidueLiftPolynomial R l).natDegree =
      (minpoly (IsLocalRing.ResidueField R)
        (finiteEtaleResidueLiftPowerBasis R l).gen).natDegree
theorem

finiteEtaleResidueLiftPolynomial_monic

L79 ↗
EtaleFundamentalGroups.finiteEtaleResidueLiftPolynomial_monic
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u
variable (R l : Type u) [CommRing R] [IsLocalRing R]
  [Field l] [Algebra (IsLocalRing.ResidueField R) l]
  [FiniteDimensional (IsLocalRing.ResidueField R) l]
  [Algebra.IsSeparable (IsLocalRing.ResidueField R) l]
Lean source · statement
theorem finiteEtaleResidueLiftPolynomial_monic :
    (finiteEtaleResidueLiftPolynomial R l).Monic
abbrev

FiniteEtaleResidueLift

L84 ↗
EtaleFundamentalGroups.FiniteEtaleResidueLift
Documentation

The explicit local lift of a finite separable residue extension.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u
variable (R l : Type u) [CommRing R] [IsLocalRing R]
  [Field l] [Algebra (IsLocalRing.ResidueField R) l]
  [FiniteDimensional (IsLocalRing.ResidueField R) l]
  [Algebra.IsSeparable (IsLocalRing.ResidueField R) l]
Lean source · statement
abbrev FiniteEtaleResidueLift
def

finiteEtaleResidueLiftClosedIdeal

L88 ↗
EtaleFundamentalGroups.finiteEtaleResidueLiftClosedIdeal
Documentation

The extended closed-point ideal in the explicit residue lift.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u
variable (R l : Type u) [CommRing R] [IsLocalRing R]
  [Field l] [Algebra (IsLocalRing.ResidueField R) l]
  [FiniteDimensional (IsLocalRing.ResidueField R) l]
  [Algebra.IsSeparable (IsLocalRing.ResidueField R) l]
Lean source · statement
def finiteEtaleResidueLiftClosedIdeal :
    Ideal (FiniteEtaleResidueLift R l)
def

finiteEtaleResidueLiftSpecialFiberRingEquiv

L95 ↗
EtaleFundamentalGroups.finiteEtaleResidueLiftSpecialFiberRingEquiv
Documentation

The special fibre of the explicit lift is the adjoined-root presentation of the given residue extension.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u
variable (R l : Type u) [CommRing R] [IsLocalRing R]
  [Field l] [Algebra (IsLocalRing.ResidueField R) l]
  [FiniteDimensional (IsLocalRing.ResidueField R) l]
  [Algebra.IsSeparable (IsLocalRing.ResidueField R) l]
Lean source · statement
def finiteEtaleResidueLiftSpecialFiberRingEquiv :
    FiniteEtaleResidueLift R l ⧸ finiteEtaleResidueLiftClosedIdeal R l ≃+*
      AdjoinRoot
        ((finiteEtaleResidueLiftPolynomial R l).map
          (IsLocalRing.residue R))
theorem

finiteEtaleResidueLiftSpecialFiberRingEquiv_mk

L105 ↗
EtaleFundamentalGroups.finiteEtaleResidueLiftSpecialFiberRingEquiv_mk
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u
variable (R l : Type u) [CommRing R] [IsLocalRing R]
  [Field l] [Algebra (IsLocalRing.ResidueField R) l]
  [FiniteDimensional (IsLocalRing.ResidueField R) l]
  [Algebra.IsSeparable (IsLocalRing.ResidueField R) l]
Lean source · statement
theorem finiteEtaleResidueLiftSpecialFiberRingEquiv_mk (g : R[X]) :
    finiteEtaleResidueLiftSpecialFiberRingEquiv R l
        (Ideal.Quotient.mk (finiteEtaleResidueLiftClosedIdeal R l)
          (AdjoinRoot.mk (finiteEtaleResidueLiftPolynomial R l) g)) =
      AdjoinRoot.mk
        ((finiteEtaleResidueLiftPolynomial R l).map
          (IsLocalRing.residue R))
        (g.map (IsLocalRing.residue R))
theorem

finiteEtaleResidueLiftClosedIdeal_isMaximal

L118 ↗
EtaleFundamentalGroups.finiteEtaleResidueLiftClosedIdeal_isMaximal
Documentation

The extended closed point in the explicit lift is maximal.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u
variable (R l : Type u) [CommRing R] [IsLocalRing R]
  [Field l] [Algebra (IsLocalRing.ResidueField R) l]
  [FiniteDimensional (IsLocalRing.ResidueField R) l]
  [Algebra.IsSeparable (IsLocalRing.ResidueField R) l]
Lean source · statement
theorem finiteEtaleResidueLiftClosedIdeal_isMaximal :
    (finiteEtaleResidueLiftClosedIdeal R l).IsMaximal
theorem

isLocalRing_finiteEtaleResidueLift

L135 ↗
EtaleFundamentalGroups.isLocalRing_finiteEtaleResidueLift
Documentation

The explicit lift of a finite separable residue extension is local.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u
variable (R l : Type u) [CommRing R] [IsLocalRing R]
  [Field l] [Algebra (IsLocalRing.ResidueField R) l]
  [FiniteDimensional (IsLocalRing.ResidueField R) l]
  [Algebra.IsSeparable (IsLocalRing.ResidueField R) l]
Lean source · statement
theorem isLocalRing_finiteEtaleResidueLift :
    IsLocalRing (FiniteEtaleResidueLift R l)
theorem

maximalIdeal_finiteEtaleResidueLift

L162 ↗
EtaleFundamentalGroups.maximalIdeal_finiteEtaleResidueLift
Documentation

The maximal ideal of the explicit lift is the extended base maximal ideal.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u
variable (R l : Type u) [CommRing R] [IsLocalRing R]
  [Field l] [Algebra (IsLocalRing.ResidueField R) l]
  [FiniteDimensional (IsLocalRing.ResidueField R) l]
  [Algebra.IsSeparable (IsLocalRing.ResidueField R) l]
Lean source · statement
theorem maximalIdeal_finiteEtaleResidueLift
    [IsLocalRing (FiniteEtaleResidueLift R l)] :
    IsLocalRing.maximalIdeal (FiniteEtaleResidueLift R l) =
      finiteEtaleResidueLiftClosedIdeal R l
theorem

isUnit_aeval_derivative_finiteEtaleResidueLift

L171 ↗
EtaleFundamentalGroups.isUnit_aeval_derivative_finiteEtaleResidueLift
Documentation

The reduction of the lifted derivative is nonzero, so the derivative at the adjoined root is a unit.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u
variable (R l : Type u) [CommRing R] [IsLocalRing R]
  [Field l] [Algebra (IsLocalRing.ResidueField R) l]
  [FiniteDimensional (IsLocalRing.ResidueField R) l]
  [Algebra.IsSeparable (IsLocalRing.ResidueField R) l]
Lean source · full declaration
theorem isUnit_aeval_derivative_finiteEtaleResidueLift :
    let C := FiniteEtaleResidueLift R l
    letI : IsLocalRing C := isLocalRing_finiteEtaleResidueLift R l
    IsUnit (aeval
      (AdjoinRoot.root (finiteEtaleResidueLiftPolynomial R l))
      (finiteEtaleResidueLiftPolynomial R l).derivative) := by
  dsimp only
  let f := finiteEtaleResidueLiftPolynomial R l
  let p := minpoly (IsLocalRing.ResidueField R)
    (finiteEtaleResidueLiftPowerBasis R l).gen
  let : IsLocalRing (FiniteEtaleResidueLift R l) :=
    isLocalRing_finiteEtaleResidueLift R l
  have hp_irreducible : Irreducible p :=
    minpoly.irreducible
      (finiteEtaleResidueLiftPowerBasis R l).isIntegral_gen
  have hp_separable : p.Separable :=
    Algebra.IsSeparable.isSeparable _
      (finiteEtaleResidueLiftPowerBasis R l).gen
  have hp_derivative_ne : p.derivative ≠ 0 :=
    (Polynomial.separable_iff_derivative_ne_zero hp_irreducible).1
      hp_separable
  let q := f.map (IsLocalRing.residue R)
  have hq_monic : q.Monic :=
    (finiteEtaleResidueLiftPolynomial_monic R l).map _
  have hq_derivative_ne : q.derivative ≠ 0 := by
    have hqp : q = p := by
      simpa [q, p, f] using finiteEtaleResidueLiftPolynomial_map R l
    rw [hqp]
    exact hp_derivative_ne
  have hqmk_ne : AdjoinRoot.mk q q.derivative ≠ 0 :=
    AdjoinRoot.mk_ne_zero_of_degree_lt hq_monic hq_derivative_ne
      (Polynomial.degree_derivative_lt hq_monic.ne_zero)
  apply (IsLocalRing.residue_ne_zero_iff_isUnit _).1
  intro hzero
  have hxmax :
      aeval (AdjoinRoot.root f) f.derivative ∈
        IsLocalRing.maximalIdeal (FiniteEtaleResidueLift R l) :=
    (IsLocalRing.residue_eq_zero_iff _).1 hzero
  have hxclosed :
      aeval (AdjoinRoot.root f) f.derivative ∈
        finiteEtaleResidueLiftClosedIdeal R l := by
    rw [← maximalIdeal_finiteEtaleResidueLift R l]
    exact hxmax
  have hquot :
      Ideal.Quotient.mk (finiteEtaleResidueLiftClosedIdeal R l)
          (aeval (AdjoinRoot.root f) f.derivative) = 0 :=
    Ideal.Quotient.eq_zero_iff_mem.2 hxclosed
  have hmap := congrArg
    (finiteEtaleResidueLiftSpecialFiberRingEquiv R l) hquot
  apply hqmk_ne
  dsimp only [f] at hmap
  simp only [AdjoinRoot.aeval_eq,
    finiteEtaleResidueLiftSpecialFiberRingEquiv_mk, map_zero] at hmap
  dsimp only [q, f]
  rw [Polynomial.derivative_map]
  exact hmap
theorem

moduleFinite_finiteEtaleResidueLift

L229 ↗
EtaleFundamentalGroups.moduleFinite_finiteEtaleResidueLift
Documentation

The explicit residue lift is finite as a module.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u
variable (R l : Type u) [CommRing R] [IsLocalRing R]
  [Field l] [Algebra (IsLocalRing.ResidueField R) l]
  [FiniteDimensional (IsLocalRing.ResidueField R) l]
  [Algebra.IsSeparable (IsLocalRing.ResidueField R) l]
Lean source · statement
theorem moduleFinite_finiteEtaleResidueLift :
    Module.Finite R (FiniteEtaleResidueLift R l)
theorem

faithfulSMul_finiteEtaleResidueLift

L234 ↗
EtaleFundamentalGroups.faithfulSMul_finiteEtaleResidueLift
Documentation

The explicit residue lift is faithfully acted on by the base.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u
variable (R l : Type u) [CommRing R] [IsLocalRing R]
  [Field l] [Algebra (IsLocalRing.ResidueField R) l]
  [FiniteDimensional (IsLocalRing.ResidueField R) l]
  [Algebra.IsSeparable (IsLocalRing.ResidueField R) l]
Lean source · statement
theorem faithfulSMul_finiteEtaleResidueLift :
    FaithfulSMul R (FiniteEtaleResidueLift R l)
theorem

etale_finiteEtaleResidueLift

L243 ↗
EtaleFundamentalGroups.etale_finiteEtaleResidueLift
Documentation

The explicit lift of a finite separable residue extension is finite étale.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u
variable (R l : Type u) [CommRing R] [IsLocalRing R]
  [Field l] [Algebra (IsLocalRing.ResidueField R) l]
  [FiniteDimensional (IsLocalRing.ResidueField R) l]
  [Algebra.IsSeparable (IsLocalRing.ResidueField R) l]
Lean source · statement
theorem etale_finiteEtaleResidueLift :
    Algebra.Etale R (FiniteEtaleResidueLift R l)
def

finiteEtaleResidueLiftResidueAlgEquiv

L255 ↗
EtaleFundamentalGroups.finiteEtaleResidueLiftResidueAlgEquiv
Documentation

The residue extension of the explicit finite étale lift is the prescribed finite separable extension.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u
variable (R l : Type u) [CommRing R] [IsLocalRing R]
  [Field l] [Algebra (IsLocalRing.ResidueField R) l]
  [FiniteDimensional (IsLocalRing.ResidueField R) l]
  [Algebra.IsSeparable (IsLocalRing.ResidueField R) l]
Lean source · full declaration
def finiteEtaleResidueLiftResidueAlgEquiv :
    let C := FiniteEtaleResidueLift R l
    letI : IsLocalRing C := isLocalRing_finiteEtaleResidueLift R l
    letI : Module.Finite R C := moduleFinite_finiteEtaleResidueLift R l
    letI : FaithfulSMul R C := faithfulSMul_finiteEtaleResidueLift R l
    letI : Algebra.IsIntegral R C := Algebra.IsIntegral.of_finite R C
    letI : IsLocalHom (algebraMap R C) :=
      Algebra.IsIntegral.isLocalHom R C
    IsLocalRing.ResidueField C ≃ₐ[IsLocalRing.ResidueField R] l := by
  dsimp only
  letI : IsLocalRing (FiniteEtaleResidueLift R l) :=
    isLocalRing_finiteEtaleResidueLift R l
  letI : Module.Finite R (FiniteEtaleResidueLift R l) :=
    moduleFinite_finiteEtaleResidueLift R l
  letI : FaithfulSMul R (FiniteEtaleResidueLift R l) :=
    faithfulSMul_finiteEtaleResidueLift R l
  letI : Algebra.IsIntegral R (FiniteEtaleResidueLift R l) :=
    Algebra.IsIntegral.of_finite R (FiniteEtaleResidueLift R l)
  letI : IsLocalHom (algebraMap R (FiniteEtaleResidueLift R l)) :=
    Algebra.IsIntegral.isLocalHom R (FiniteEtaleResidueLift R l)
  let f := finiteEtaleResidueLiftPolynomial R l
  let q := f.map (IsLocalRing.residue R)
  let p := minpoly (IsLocalRing.ResidueField R)
    (finiteEtaleResidueLiftPowerBasis R l).gen
  let hL : IsAdjoinRootMonic l p :=
    IsAdjoinRootMonic.mkOfAdjoinEqTop'
      (finiteEtaleResidueLiftPowerBasis R l).adjoin_gen_eq_top
  letI : Algebra R l :=
    ((algebraMap (IsLocalRing.ResidueField R) l).comp
      (IsLocalRing.residue R)).toAlgebra
  letI : IsScalarTower R (IsLocalRing.ResidueField R) l :=
    IsScalarTower.of_algebraMap_eq fun _ => rfl
  let eR : IsLocalRing.ResidueField (FiniteEtaleResidueLift R l) ≃ₐ[R] l :=
    (Ideal.quotientEquivAlgOfEq R
      (maximalIdeal_finiteEtaleResidueLift R l)).trans <|
      (AdjoinRoot.quotEquivQuotMap f
        (IsLocalRing.maximalIdeal R)).trans <|
        (((AdjoinRoot.algEquivOfEq (IsLocalRing.ResidueField R) q p <| by
            simpa [q, p, f] using finiteEtaleResidueLiftPolynomial_map R l).trans
          hL.adjoinRootAlgEquiv).restrictScalars R)
  exact eR.extendScalarsOfSurjective IsLocalRing.residue_surjective

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