NYLL
Module

ChosenFactor.lean

Nyll.EtaleFundamentalGroups.Completions.FiniteEtale.ChosenFactor
8 declarations indexed from sourceView source ↗

Module documentation

Trivializing a chosen finite étale local factor after a finite residue lift

Suppose R → B is a local map inducing an isomorphism on residue fields and D / B is finite étale local. Lift the actual finite separable residue field κ(D) / κ(R) to the explicit finite étale local R-algebra constructed in CompleteFiniteEtaleResidueLift. After base change to B, that lift is isomorphic to D.

The proof is concrete. Hensel's lemma lifts the distinguished residue generator to a root in D; residue generation and Nakayama make the resulting tensor-product map surjective, and equality of the finite free ranks makes it an isomorphism.

Imports3
Imported by4

Declarations

theorem

isLocalRing_of_unique_prime_over_maximal

L37 ↗
EtaleFundamentalGroups.isLocalRing_of_unique_prime_over_maximal
Documentation

A finite integral algebra with a unique prime over the closed point of a local base is local. No separable-closedness hypothesis is involved.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
open scoped TensorProduct
universe u
Lean source · statement
theorem isLocalRing_of_unique_prime_over_maximal
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    [IsLocalRing R] [Module.Finite R S]
    (q : Ideal S) [q.IsPrime]
    [q.LiesOver (IsLocalRing.maximalIdeal R)]
    (hunique : ∀ Q : Ideal S, Q.IsPrime →
      Q.LiesOver (IsLocalRing.maximalIdeal R) → Q = q) :
    IsLocalRing S
theorem

isLocalHom_of_unique_prime_over_maximal

L61 ↗
EtaleFundamentalGroups.isLocalHom_of_unique_prime_over_maximal
Documentation

The algebra map to the unique chosen factor is local.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
open scoped TensorProduct
universe u
Lean source · full declaration
theorem isLocalHom_of_unique_prime_over_maximal
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    [IsLocalRing R] [Module.Finite R S]
    (q : Ideal S) [q.IsPrime]
    [q.LiesOver (IsLocalRing.maximalIdeal R)]
    (hunique : ∀ Q : Ideal S, Q.IsPrime →
      Q.LiesOver (IsLocalRing.maximalIdeal R) → Q = q) :
    letI : IsLocalRing S :=
      isLocalRing_of_unique_prime_over_maximal q hunique
    IsLocalHom (algebraMap R S) := by
  let : IsLocalRing S :=
    isLocalRing_of_unique_prime_over_maximal q hunique
  let : Algebra.IsIntegral R S := Algebra.IsIntegral.of_finite R S
  have hq_maximal : q.IsMaximal :=
    Ideal.isMaximal_of_isIntegral_of_isMaximal_under (R := R) q <| by
      rw [← q.over_def (IsLocalRing.maximalIdeal R)]
      exact IsLocalRing.maximalIdeal.isMaximal R
  have hq_eq : q = IsLocalRing.maximalIdeal S :=
    IsLocalRing.eq_maximalIdeal hq_maximal
  have hcomap :
      (IsLocalRing.maximalIdeal S).comap (algebraMap R S) =
        IsLocalRing.maximalIdeal R := by
    rw [← hq_eq]
    exact (q.over_def (IsLocalRing.maximalIdeal R)).symm
  exact ((IsLocalRing.local_hom_TFAE (algebraMap R S)).out 5 1).mp hcomap
theorem

faithfullyFlat_of_unique_prime_over_maximal

L89 ↗
EtaleFundamentalGroups.faithfullyFlat_of_unique_prime_over_maximal
Documentation

A finite étale unique chosen factor is faithfully flat over the local base.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
open scoped TensorProduct
universe u
Lean source · full declaration
theorem faithfullyFlat_of_unique_prime_over_maximal
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    [IsLocalRing R] [Module.Finite R S] [Algebra.Etale R S]
    (q : Ideal S) [q.IsPrime]
    [q.LiesOver (IsLocalRing.maximalIdeal R)]
    (hunique : ∀ Q : Ideal S, Q.IsPrime →
      Q.LiesOver (IsLocalRing.maximalIdeal R) → Q = q) :
    letI : IsLocalRing S :=
      isLocalRing_of_unique_prime_over_maximal q hunique
    Module.FaithfullyFlat R S := by
  let : IsLocalRing S :=
    isLocalRing_of_unique_prime_over_maximal q hunique
  let : IsLocalHom (algebraMap R S) :=
    isLocalHom_of_unique_prime_over_maximal q hunique
  exact Module.FaithfullyFlat.of_flat_of_isLocalHom
theorem

exists_baseChange_finiteEtaleResidueLift_algEquiv_of_residue_bijective

L111 ↗
EtaleFundamentalGroups.exists_baseChange_finiteEtaleResidueLift_algEquiv_of_residue_bijective
Documentation

A finite étale local factor over a complete local algebra with unchanged residue field becomes the base change of the explicit finite residue lift.

The finite-dimensionality and separability hypotheses are facts about the actual residue extension. The iterated-root-cover consumer below produces them from finite étaleness and residue preservation.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
open scoped TensorProduct
universe u
Lean source · statement
theorem exists_baseChange_finiteEtaleResidueLift_algEquiv_of_residue_bijective
    {R B D : Type u} [CommRing R] [CommRing B] [CommRing D]
    [Algebra R B] [Algebra B D] [Algebra R D] [IsScalarTower R B D]
    [IsLocalRing R] [IsLocalRing B] [IsLocalRing D]
    [IsLocalHom (algebraMap R B)] [IsLocalHom (algebraMap B D)]
    [IsLocalHom (algebraMap R D)]
    [IsAdicComplete (IsLocalRing.maximalIdeal B) B]
    [Module.Finite B D] [Algebra.Etale B D]
    [FiniteDimensional (IsLocalRing.ResidueField R)
      (IsLocalRing.ResidueField D)]
    [Algebra.IsSeparable (IsLocalRing.ResidueField R)
      (IsLocalRing.ResidueField D)]
    (hresidue : Function.Bijective
      (IsLocalRing.ResidueField.map (algebraMap R B))) :
    Nonempty ((B ⊗[R]
      FiniteEtaleResidueLift R (IsLocalRing.ResidueField D)) ≃ₐ[B] D)
theorem

exists_finiteEtaleResidueLift_of_residue_bijective

L262 ↗
EtaleFundamentalGroups.exists_finiteEtaleResidueLift_of_residue_bijective
Documentation

A finite étale local algebra over a complete local algebra with unchanged residue field is obtained by base change from a finite étale algebra over the original local ring.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
open scoped TensorProduct
universe u
Lean source · statement
theorem exists_finiteEtaleResidueLift_of_residue_bijective
    {R B D : Type u} [CommRing R] [CommRing B] [CommRing D]
    [Algebra R B] [Algebra B D] [Algebra R D] [IsScalarTower R B D]
    [IsLocalRing R] [IsLocalRing B] [IsLocalRing D]
    [IsLocalHom (algebraMap R B)] [IsLocalHom (algebraMap B D)]
    [IsLocalHom (algebraMap R D)]
    [IsAdicComplete (IsLocalRing.maximalIdeal B) B]
    [Module.Finite B D] [Algebra.Etale B D]
    (hresidue : Function.Bijective
      (IsLocalRing.ResidueField.map (algebraMap R B))) :
    ∃ (C : Type u) (_ : CommRing C) (_ : Algebra R C)
      (_ : Module.Finite R C) (_ : Algebra.Etale R C),
      Nonempty ((B ⊗[R] C) ≃ₐ[B] D)
theorem

exists_baseChange_finiteEtaleResidueLift_algEquiv

L298 ↗
EtaleFundamentalGroups.exists_baseChange_finiteEtaleResidueLift_algEquiv
Documentation

Compatibility wrapper for the finite faithfully acted-on base changes used by the chosen-factor constructions.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
open scoped TensorProduct
universe u
Lean source · statement
theorem exists_baseChange_finiteEtaleResidueLift_algEquiv
    {R B D : Type u} [CommRing R] [CommRing B] [CommRing D]
    [Algebra R B] [Algebra B D] [Algebra R D] [IsScalarTower R B D]
    [IsLocalRing R] [IsLocalRing B] [IsLocalRing D]
    [IsLocalHom (algebraMap R B)] [IsLocalHom (algebraMap B D)]
    [IsLocalHom (algebraMap R D)]
    [IsAdicComplete (IsLocalRing.maximalIdeal B) B]
    [Module.Finite R B] [FaithfulSMul R B]
    [Module.Finite B D] [FaithfulSMul B D] [Algebra.Etale B D]
    [FiniteDimensional (IsLocalRing.ResidueField R)
      (IsLocalRing.ResidueField D)]
    [Algebra.IsSeparable (IsLocalRing.ResidueField R)
      (IsLocalRing.ResidueField D)]
    (hresidue : Function.Bijective
      (IsLocalRing.ResidueField.map (algebraMap R B))) :
    Nonempty ((B ⊗[R]
      FiniteEtaleResidueLift R (IsLocalRing.ResidueField D)) ≃ₐ[B] D)
theorem

exists_baseChange_chosenFactorAlgEquiv_iteratedRadical_of_fg

L325 ↗
EtaleFundamentalGroups.Kummer.exists_baseChange_chosenFactorAlgEquiv_iteratedRadical_of_fg
Documentation

For a complete iterated positive root cover whose base maximal ideal is finitely generated, a uniquely chosen finite étale factor is trivialized after lifting only its actual finite residue extension to the original complete base. No Noetherian-ring or separably-closed-residue instance is required.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
open scoped TensorProduct
universe u
namespace Kummer
Lean source · full declaration
theorem exists_baseChange_chosenFactorAlgEquiv_iteratedRadical_of_fg
    {A : Type u} [CommRing A] [IsLocalRing A]
    [IsAdicComplete (IsLocalRing.maximalIdeal A) A]
    (hmax : (IsLocalRing.maximalIdeal A).FG)
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (hn : ∀ i, 0 < n i)
    (ha : ∀ i, a i ∈ IsLocalRing.maximalIdeal A) :
    let B := iteratedRadical A r n a
    letI : IsLocalRing B := isLocalRing_iteratedRadical n a hn ha
    ∀ {D : Type u} [CommRing D] [Algebra B D]
      [Algebra A D] [IsScalarTower A B D]
      [Module.Finite B D] [Algebra.Etale B D],
      ∀ (q : Ideal D) [q.IsPrime]
        [q.LiesOver (IsLocalRing.maximalIdeal B)],
        ∀ (hunique : ∀ Q : Ideal D, Q.IsPrime →
          Q.LiesOver (IsLocalRing.maximalIdeal B) → Q = q),
          letI : Module.Finite A B := finite_iteratedRadical n a hn
          letI : Module.FaithfullyFlat A B :=
            faithfullyFlat_iteratedRadical n a hn
          letI : Algebra.IsIntegral A B := Algebra.IsIntegral.of_finite A B
          letI : IsLocalHom (algebraMap A B) :=
            Algebra.IsIntegral.isLocalHom A B
          letI : IsAdicComplete (IsLocalRing.maximalIdeal B) B :=
            isAdicComplete_maximalIdeal_iteratedRadical_of_fg
              hmax n a hn ha
          letI : IsLocalRing D :=
            isLocalRing_of_unique_prime_over_maximal q hunique
          letI : IsLocalHom (algebraMap B D) :=
            isLocalHom_of_unique_prime_over_maximal q hunique
          letI : Module.FaithfullyFlat B D :=
            faithfullyFlat_of_unique_prime_over_maximal q hunique
          letI : IsLocalHom (algebraMap A D) := by
            rw [IsScalarTower.algebraMap_eq A B D]
            infer_instance
          let k := IsLocalRing.ResidueField A
          let kB := IsLocalRing.ResidueField B
          let l := IsLocalRing.ResidueField D
          let eResidue : k ≃ₐ[k] kB :=
            AlgEquiv.ofBijective (Algebra.ofId k kB)
              (residueFieldMap_bijective_iteratedRadical n a hn ha)
          letI : Module.Finite k kB :=
            Module.Finite.of_surjective eResidue.toLinearMap eResidue.surjective
          letI : Module.Finite k l := Module.Finite.trans kB l
          letI : Algebra.IsSeparable k kB :=
            AlgEquiv.Algebra.isSeparable eResidue
          letI : Algebra.IsSeparable k l :=
            Algebra.IsSeparable.trans k kB l
          Nonempty ((B ⊗[A] FiniteEtaleResidueLift A l) ≃ₐ[B] D) := by
  dsimp only
  intro D _ _ _ _ _ _ q _ _ hunique
  let B := iteratedRadical A r n a
  let : IsLocalRing B := isLocalRing_iteratedRadical n a hn ha
  let : Module.Finite A B := finite_iteratedRadical n a hn
  let : Module.FaithfullyFlat A B :=
    faithfullyFlat_iteratedRadical n a hn
  let : Algebra.IsIntegral A B := Algebra.IsIntegral.of_finite A B
  let : IsLocalHom (algebraMap A B) :=
    Algebra.IsIntegral.isLocalHom A B
  let : IsAdicComplete (IsLocalRing.maximalIdeal B) B :=
    isAdicComplete_maximalIdeal_iteratedRadical_of_fg hmax n a hn ha
  let : IsLocalRing D :=
    isLocalRing_of_unique_prime_over_maximal q hunique
  let : IsLocalHom (algebraMap B D) :=
    isLocalHom_of_unique_prime_over_maximal q hunique
  let : Module.FaithfullyFlat B D :=
    faithfullyFlat_of_unique_prime_over_maximal q hunique
  let : IsLocalHom (algebraMap A D) := by
    rw [IsScalarTower.algebraMap_eq A B D]
    infer_instance
  let k := IsLocalRing.ResidueField A
  let kB := IsLocalRing.ResidueField B
  let l := IsLocalRing.ResidueField D
  let eResidue : k ≃ₐ[k] kB :=
    AlgEquiv.ofBijective (Algebra.ofId k kB)
      (residueFieldMap_bijective_iteratedRadical n a hn ha)
  let : Module.Finite k kB :=
    Module.Finite.of_surjective eResidue.toLinearMap eResidue.surjective
  let : Module.Finite k l := Module.Finite.trans kB l
  let : Algebra.IsSeparable k kB :=
    AlgEquiv.Algebra.isSeparable eResidue
  let : Algebra.IsSeparable k l := Algebra.IsSeparable.trans k kB l
  exact exists_baseChange_finiteEtaleResidueLift_algEquiv
    (R := A) (B := B) (D := D)
    (residueFieldMap_bijective_iteratedRadical n a hn ha)
abbrev

exists_baseChange_chosenFactorAlgEquiv_iteratedRadical

L412 ↗
EtaleFundamentalGroups.Kummer.exists_baseChange_chosenFactorAlgEquiv_iteratedRadical
Documentation

Noetherian specialization of exists_baseChange_chosenFactorAlgEquiv_iteratedRadical_of_fg.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
open scoped TensorProduct
universe u
namespace Kummer
Lean source · statement
abbrev exists_baseChange_chosenFactorAlgEquiv_iteratedRadical
    {A : Type u} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    [IsAdicComplete (IsLocalRing.maximalIdeal A) A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (hn : ∀ i, 0 < n i)
    (ha : ∀ i, a i ∈ IsLocalRing.maximalIdeal A)

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