NYLL
Module

ComponentTargetAction.lean

Nyll.EtaleFundamentalGroups.Kummer.Completions.Conditional.ChosenFactor.ComponentTargetAction
5 declarations indexed from sourceView source ↗

Module documentation

Conditional completed root actions in the selected generic component

The completed conditional root cover has a chosen local normalization factor inside an already selected finite generic component M. Completeness and finite etaleness make that localization a genuine finite chosen factor, so the completed chosen-factor theorem supplies all root coordinates in its literal fraction ring. The canonical normalization-localization comparison then transports those coordinates to the same M.

No action on an unrelated global field, universal embedding, or right-coordinate bijectivity is used.

Imports3
Imported by1

Declarations

def

completedChosenFactorComponentResidueLift_of_mem_or_eq_one

L37 ↗
EtaleFundamentalGroups.Kummer.completedChosenFactorComponentResidueLift_of_mem_or_eq_one
Documentation

The canonical residue lift of the localization selected inside a fixed generic component. Henselian localization and the unique closed prime are constructed here once, instead of being repeated in every theorem type and proof that names this lift.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
universe u
Lean source · full declaration
def completedChosenFactorComponentResidueLift_of_mem_or_eq_one
    {A : Type u} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (hn : ∀ i, 0 < n i)
    (hstage : ∀ i,
      a i ∈ IsLocalRing.maximalIdeal A ∨ n i = 1) :
    let Ahat := AdicCompletion (IsLocalRing.maximalIdeal A) A
    let aHat : Fin r → Ahat := fun i ↦ algebraMap A Ahat (a i)
    let Bhat := iteratedRadical Ahat r n aHat
    let hstageHat : ∀ i,
        aHat i ∈ IsLocalRing.maximalIdeal Ahat ∨ n i = 1 := fun i ↦ by
      rcases hstage i with ha | hOne
      · left
        rw [AdicCompletion.maximalIdeal_eq_map]
        exact Ideal.mem_map_of_mem (algebraMap A Ahat) ha
      · exact Or.inr hOne
    letI : IsLocalRing Bhat :=
      isLocalRing_iteratedRadical_of_mem_or_eq_one n aHat hn hstageHat
    ∀ {M : Type u} [Field M] [Algebra Bhat M],
      ∀ (q : Ideal (integralClosure Bhat M)) [q.IsPrime]
        [q.LiesOver (IsLocalRing.maximalIdeal Bhat)],
        Algebra.Etale Bhat (integralClosure Bhat M) → CommAlgCat Ahat := by
  dsimp only
  intro M _ _ q _ _ hEtale
  let Ahat := AdicCompletion (IsLocalRing.maximalIdeal A) A
  let aHat : Fin r → Ahat := fun i ↦ algebraMap A Ahat (a i)
  let Bhat := iteratedRadical Ahat r n aHat
  have hstageHat : ∀ i,
      aHat i ∈ IsLocalRing.maximalIdeal Ahat ∨ n i = 1 := fun i ↦ by
    rcases hstage i with ha | hOne
    · left
      rw [AdicCompletion.maximalIdeal_eq_map]
      exact Ideal.mem_map_of_mem (algebraMap A Ahat) ha
    · exact Or.inr hOne
  letI : IsLocalRing Bhat :=
    isLocalRing_iteratedRadical_of_mem_or_eq_one n aHat hn hstageHat
  have hmaxFG : (IsLocalRing.maximalIdeal Ahat).FG := by
    rw [AdicCompletion.maximalIdeal_eq_map]
    exact Ideal.FG.map
      (IsLocalRing.maximalIdeal A).fg_of_isNoetherianRing
      (algebraMap A Ahat)
  letI : HenselianLocalRing Bhat :=
    henselianLocalRing_iteratedRadical_of_isAdicComplete_of_fg_of_mem_or_eq_one
      hmaxFG n aHat hn hstageHat
  letI : Module.FaithfullyFlat Ahat Bhat :=
    faithfullyFlat_iteratedRadical n aHat hn
  letI : IsLocalHom (algebraMap Ahat Bhat) := by
    let : Module.Finite Ahat Bhat := finite_iteratedRadical n aHat hn
    let : Algebra.IsIntegral Ahat Bhat :=
      Algebra.IsIntegral.of_finite Ahat Bhat
    exact Algebra.IsIntegral.isLocalHom Ahat Bhat
  let C := integralClosure Bhat M
  letI : Algebra.Etale Bhat C := hEtale
  let D := Localization.AtPrime q
  letI : Module.Finite Bhat D :=
    moduleFinite_localizationAtPrime_of_henselian_of_etale q
  letI : Algebra.Etale Bhat D :=
    etale_localizationAtPrime_of_henselian_of_etale q
  letI : IsLocalHom (algebraMap Bhat D) :=
    isLocalHom_algebraMap_localizationAtPrime_of_liesOver_maximalIdeal q
  let aDAlgebra : Algebra Ahat D :=
    ((algebraMap Bhat D).comp (algebraMap Ahat Bhat)).toAlgebra
  letI : Algebra Ahat D := aDAlgebra
  letI : IsScalarTower Ahat Bhat D :=
    IsScalarTower.of_algebraMap_eq' rfl
  letI : IsLocalHom (algebraMap Ahat D) := by
    rw [IsScalarTower.algebraMap_eq Ahat Bhat D]
    exact
      RingHom.isLocalHom_comp
        (algebraMap Bhat D) (algebraMap Ahat Bhat)
  let k := IsLocalRing.ResidueField Ahat
  let kB := IsLocalRing.ResidueField Bhat
  let l := IsLocalRing.ResidueField D
  let eResidue : k ≃ₐ[k] kB :=
    AlgEquiv.ofBijective (Algebra.ofId k kB)
      (residueFieldMap_bijective_iteratedRadical_of_mem_or_eq_one
        n aHat hn hstageHat)
  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
  exact CommAlgCat.of Ahat (FiniteEtaleResidueLift Ahat l)
theorem

algEquiv_apply_algebraMap

L124 ↗
EtaleFundamentalGroups.Kummer.algEquiv_apply_algebraMap
Documentation

Evaluation of an algebra equivalence on a base-ring coordinate, isolated from the larger completed-factor instance environment.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
universe u
Lean source · statement
theorem algEquiv_apply_algebraMap
    {D F M : Type u} [CommRing D] [CommRing F] [CommRing M]
    [Algebra D F] [Algebra D M]
    (e : F ≃ₐ[D] M) (x : D) :
    e (algebraMap D F x) = algebraMap D M x
theorem

transport_iteratedRadicalTargetAction

L135 ↗
EtaleFundamentalGroups.Kummer.transport_iteratedRadicalTargetAction
Documentation

Transport an already constructed radical action across compatible fraction-field equivalences. The source and target algebra structures are explicit inputs, so this proof performs no reconstruction of the completed chosen-factor instance tower.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
universe u
Lean source · statement
theorem transport_iteratedRadicalTargetAction
    {Ahat D F M : Type u}
    [CommRing Ahat] [CommRing D] [Field F] [Field M]
    {r : ℕ} (n : Fin r → ℕ) (aHat : Fin r → Ahat)
    [Algebra Ahat F] [Algebra Ahat M]
    [Algebra D F] [Algebra D M]
    [Algebra (iteratedRadical Ahat r n aHat) D]
    [Algebra (iteratedRadical Ahat r n aHat) M]
    [IsScalarTower (iteratedRadical Ahat r n aHat) D M]
    [IsScalarTower Ahat (iteratedRadical Ahat r n aHat) M]
    (eDM : F ≃ₐ[D] M) (eAhat : F ≃ₐ[Ahat] M)
    (hcompat : ∀ y, eAhat y = eDM y)
    (xF : Fin r → F)
    (hxF : ∀ i, xF i ^ n i = algebraMap Ahat F (aHat i))
    (hinjectiveF : Function.Injective
      (iteratedRadicalTargetAlgHom n aHat xF hxF))
    (hcoordinatesF : ∀ i, xF i =
      algebraMap D F
        (algebraMap (iteratedRadical Ahat r n aHat) D
          (iteratedRadicalRoot Ahat n aHat i))) :
    ∃ (xM : Fin r → M)
        (hxM : ∀ i, xM i ^ n i = algebraMap Ahat M (aHat i)),
      Function.Injective
          (iteratedRadicalTargetAlgHom n aHat xM hxM) ∧
        iteratedRadicalTargetAlgHom n aHat xM hxM =
          (Algebra.ofId (iteratedRadical Ahat r n aHat) M).restrictScalars Ahat ∧
        ∀ i, xM i =
          algebraMap D M
            (algebraMap (iteratedRadical Ahat r n aHat) D
              (iteratedRadicalRoot Ahat n aHat i))
def

HasCompletedChosenFactorComponentTargetAction

L217 ↗
EtaleFundamentalGroups.Kummer.HasCompletedChosenFactorComponentTargetAction
Documentation

The complete dependent result carried by a selected conditional component. Keeping it opaque prevents callers from repeatedly normalizing the canonical residue-lift and algebra setup merely to state the result.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
universe u
Lean source · statement
def HasCompletedChosenFactorComponentTargetAction
    {A : Type u} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (hn : ∀ i, 0 < n i)
    (hstage : ∀ i,
      a i ∈ IsLocalRing.maximalIdeal A ∨ n i = 1) : Prop
theorem

exists_completedChosenFactorComponentTargetAction_of_mem_or_eq_one

L284 ↗
EtaleFundamentalGroups.Kummer.exists_completedChosenFactorComponentTargetAction_of_mem_or_eq_one
Documentation

A finite-etale normalization of the completed conditional root cover, localized at a specified closed prime, produces an injective simultaneous root action in the same selected generic component M.

The finite local factor, its residue-lift tensor presentation, and its fraction-field comparison with M are all constructed internally. The returned action is explicitly identified with the existing map Bhat → M. Its coordinate formula records that each target root is the image of the distinguished root through the canonical localization map D → M.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
universe u
Lean source · statement
theorem
    exists_completedChosenFactorComponentTargetAction_of_mem_or_eq_one
    {A : Type u} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (hn : ∀ i, 0 < n i)
    (hstage : ∀ i,
      a i ∈ IsLocalRing.maximalIdeal A ∨ n i = 1) :
    HasCompletedChosenFactorComponentTargetAction n a hn hstage

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