NYLL
Module

StrictHenselianLocalization.lean

Nyll.EtaleFundamentalGroups.Kummer.HigherRadical.UnitFactor.StrictHenselianLocalization
4 declarations indexed from sourceView source ↗

Module documentation

The strict-Henselian localization of the retained unit factor

A finite etale algebra over a strictly Henselian local ring need not be the base ring before a connected factor is selected. Nevertheless, every chosen closed localization has separable residue field over the separably closed base residue field, and hence is canonically the base ring by the pointed Henselian theorem.

The specialization below applies this source-producing statement to the literal lower factor retained by HigherRadicalUnitFactorData. It does not assume that this factor has a unique closed prime, and it does not compare its generic field with a later full-root component.

Imports4
Imported by3

Declarations

theorem

isSepClosed_of_ringEquiv

L35 ↗
EtaleFundamentalGroups.isSepClosed_of_ringEquiv
Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u v w x
Lean source · statement
theorem isSepClosed_of_ringEquiv
    {k : Type u} {l : Type v} [Field k] [Field l] [IsSepClosed k]
    (e : k ≃+* l) : IsSepClosed l
theorem

exists_strictHenselian_finiteEtale_localizationAlgEquiv

L55 ↗
EtaleFundamentalGroups.exists_strictHenselian_finiteEtale_localizationAlgEquiv
Documentation

A finite etale algebra over a strictly Henselian local ring has a closed local factor canonically isomorphic to the base.

The prime and the residue-field bijection are both produced internally: integrality gives a prime over the closed point, while unramifiedness makes its finite residue extension separable, hence trivial over the separably closed residue field. No uniqueness assumption on primes of S is used.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u v w x
Lean source · statement
theorem exists_strictHenselian_finiteEtale_localizationAlgEquiv
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    [Algebra R S] [HenselianLocalRing R]
    [IsSepClosed (IsLocalRing.ResidueField R)]
    [Module.Finite R S] [Algebra.Etale R S] [Nontrivial S] :
    ∃ q : (IsLocalRing.maximalIdeal R).primesOver S,
      Nonempty (R ≃ₐ[R] Localization.AtPrime q.1)
theorem

higherRadicalUnitFactorData_isDomain

L96 ↗
EtaleFundamentalGroups.Kummer.higherRadicalUnitFactorData_isDomain
Documentation

The literal unit factor retained in HigherRadicalUnitFactorData is a domain. This is the integral counterpart of the irreducible generic factor already used by lowerUnitFactorGenericFiberAlgEquiv.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u v w x
namespace Kummer
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
theorem higherRadicalUnitFactorData_isDomain
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (base : DVF.{u, w} K) (target : DVF.{v, x} L)
    [base.valuation.HasExtension target.valuation]
    (varpi : base.valuationSubring)
    (pi : target.valuationSubring) (N : ℕ)
    (beta : AlgebraicClosure L)
    (factor : HigherRadicalUnitFactorData base target varpi pi N beta) :
    IsDomain (AdjoinRoot factor.q)
theorem

higherRadicalUnitFactorData_exists_strictHenselian_localizationAlgEquiv

L125 ↗
EtaleFundamentalGroups.Kummer.higherRadicalUnitFactorData_exists_strictHenselian_localizationAlgEquiv
Documentation

Over a strict-Henselian actual-root base, the retained lower unit factor has a chosen closed localization canonically isomorphic to that base.

The returned prime is produced from the literal map factor.radicalToUnitFactor; no prime comparison, connectedness, or unique-prime hypothesis is exposed. Since Cq is a domain, localizing at the returned prime preserves its retained generic field and root coordinate, but this theorem deliberately makes no comparison with a later full-root tensor component.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u v w x
namespace Kummer
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · full declaration
theorem higherRadicalUnitFactorData_exists_strictHenselian_localizationAlgEquiv
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (base : DVF.{u, w} K) (target : DVF.{v, x} L)
    [base.valuation.HasExtension target.valuation]
    [Module.Finite base.valuationSubring target.valuationSubring]
    (varpi : base.valuationSubring)
    (pi : target.valuationSubring) (N : ℕ)
    (beta : AlgebraicClosure L)
    (factor : HigherRadicalUnitFactorData base target varpi pi N beta)
    [HenselianLocalRing
      (AdjoinRoot
        (X ^ ramificationIndex base target - C varpi))]
    [IsSepClosed
      (IsLocalRing.ResidueField
        (AdjoinRoot
          (X ^ ramificationIndex base target - C varpi)))] :
    let e := ramificationIndex base target
    let Rₑ := AdjoinRoot (X ^ e - C varpi)
    let Cq := AdjoinRoot factor.q
    letI : Algebra Rₑ Cq :=
      factor.radicalToUnitFactor.toRingHom.toAlgebra
    ∃ q : (IsLocalRing.maximalIdeal Rₑ).primesOver Cq,
      Nonempty (Rₑ ≃ₐ[Rₑ] Localization.AtPrime q.1) := by
  dsimp only
  let e := ramificationIndex base target
  let Rₑ := AdjoinRoot (X ^ e - C varpi)
  let Cq := AdjoinRoot factor.q
  let : IsDomain Cq :=
    higherRadicalUnitFactorData_isDomain
      base target varpi pi N beta factor
  let : Algebra Rₑ Cq :=
    factor.radicalToUnitFactor.toRingHom.toAlgebra
  let : Module.Finite Rₑ Cq :=
    higherRadicalUnitFactorData_radical_finite
      base target varpi pi N beta factor
  let : Algebra.Etale Rₑ Cq := factor.radical_etale
  exact exists_strictHenselian_finiteEtale_localizationAlgEquiv
    (R := Rₑ) (S := Cq)

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