NYLL
Module

Residue.lean

Nyll.EtaleFundamentalGroups.Kummer.RootCovers.Local.Residue
5 declarations indexed from sourceView source ↗

Module documentation

Residue fields of local Kummer root covers

A positive root cover R[X] / (X ^ n - a) of an element in the closed point is local, and its closed point is generated by the image of the base closed point and the adjoined root. Hence the canonical map on residue fields is an isomorphism: modulo the closed point, every polynomial is represented by its constant coefficient.

The algebra and local-hom instances are installed only inside proofs. In particular this file does not register root-cover local structures globally.

Imports2
Imported by6

Declarations

theorem

isSepClosed_of_ringEquiv

L30 ↗
EtaleFundamentalGroups.Kummer.isSepClosed_of_ringEquiv
Source context 4 commands

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

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

residueFieldMap_bijective_adjoinRoot_X_pow_sub_C

L43 ↗
EtaleFundamentalGroups.Kummer.residueFieldMap_bijective_adjoinRoot_X_pow_sub_C
Documentation

The canonical residue-field map of a positive local Kummer root cover is bijective.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u
Lean source · full declaration
theorem residueFieldMap_bijective_adjoinRoot_X_pow_sub_C
    {R : Type u} [CommRing R] [IsLocalRing R]
    {n : ℕ} (hn : 0 < n) {a : R} (ha : a ∈ IsLocalRing.maximalIdeal R) :
    let B := AdjoinRoot (X ^ n - C a)
    letI : IsLocalRing B := isLocalRing_adjoinRoot_X_pow_sub_C hn ha
    letI : Module.FaithfullyFlat R B :=
      faithfullyFlat_adjoinRoot_X_pow_sub_C hn a
    Function.Bijective
      (IsLocalRing.ResidueField.map (algebraMap R B)) := by
  dsimp only
  let f : R[X] := X ^ n - C a
  let B := AdjoinRoot f
  let : IsLocalRing B := isLocalRing_adjoinRoot_X_pow_sub_C hn ha
  let : Module.FaithfullyFlat R B :=
    faithfullyFlat_adjoinRoot_X_pow_sub_C hn a
  constructor
  · exact (IsLocalRing.ResidueField.map (algebraMap R B)).injective
  · intro y
    obtain ⟨b, rfl⟩ := IsLocalRing.residue_surjective y
    induction b using AdjoinRoot.induction_on with
    | _ p =>
        refine ⟨IsLocalRing.residue R (p.coeff 0), ?_⟩
        rw [IsLocalRing.ResidueField.map_residue]
        have hroot :
            AdjoinRoot.root f ∈ IsLocalRing.maximalIdeal B := by
          rw [maximalIdeal_adjoinRoot_X_pow_sub_C hn ha]
          exact
            (show Ideal.span {AdjoinRoot.root f} ≤
                localRootCoverClosedIdeal R n a from le_sup_right)
              (Ideal.mem_span_singleton_self (AdjoinRoot.root f))
        have hroot_residue :
            IsLocalRing.residue B (AdjoinRoot.root f) = 0 :=
          (IsLocalRing.residue_eq_zero_iff _).2 hroot
        change IsLocalRing.residue B (AdjoinRoot.of f (p.coeff 0)) =
          IsLocalRing.residue B (AdjoinRoot.mk f p)
        symm
        calc
          IsLocalRing.residue B (AdjoinRoot.mk f p) =
              IsLocalRing.residue B
                (AdjoinRoot.mk f
                  (X * p.divX + C (p.coeff 0))) := by
            rw [Polynomial.X_mul_divX_add]
          _ = IsLocalRing.residue B
              (AdjoinRoot.of f (p.coeff 0)) := by
            rw [map_add, map_mul, AdjoinRoot.mk_X, AdjoinRoot.mk_C,
              map_add, map_mul, hroot_residue, zero_mul, zero_add]
theorem

residueFieldMap_bijective_iteratedRadical

L91 ↗
EtaleFundamentalGroups.Kummer.residueFieldMap_bijective_iteratedRadical
Documentation

A finite positive iterated local Kummer root cover preserves the residue field.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u
Lean source · full declaration
theorem residueFieldMap_bijective_iteratedRadical
    {A : Type u} [CommRing A] [hA : IsLocalRing A]
    {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
    letI : Module.FaithfullyFlat A B :=
      faithfullyFlat_iteratedRadical n a hn
    Function.Bijective
      (IsLocalRing.ResidueField.map (algebraMap A B)) := by
  dsimp only
  induction r with
  | zero =>
      simp only [iteratedRadical]
      constructor
      · exact (IsLocalRing.ResidueField.map (algebraMap A A)).injective
      · intro y
        obtain ⟨x, rfl⟩ := @IsLocalRing.residue_surjective A _ hA y
        refine ⟨@IsLocalRing.residue A _ hA x, ?_⟩
        rfl
  | succ r ih =>
      let T : CommAlgCat.{u} A :=
        iteratedRadical A r (Fin.init n) (Fin.init a)
      let : IsLocalRing T :=
        isLocalRing_iteratedRadical
          (Fin.init n) (Fin.init a)
          (fun i ↦ hn i.castSucc) (fun i ↦ ha i.castSucc)
      let : Module.FaithfullyFlat A T :=
        faithfullyFlat_iteratedRadical
          (Fin.init n) (Fin.init a) (fun i ↦ hn i.castSucc)
      have haLast :
          algebraMap A T (a (Fin.last r)) ∈ IsLocalRing.maximalIdeal T :=
        algebraMap_mem_maximalIdeal_iteratedRadical
          (Fin.init n) (Fin.init a)
          (fun i ↦ hn i.castSucc) (fun i ↦ ha i.castSucc)
          (ha (Fin.last r))
      let f : T[X] :=
        X ^ n (Fin.last r) - C (algebraMap A T (a (Fin.last r)))
      let B := AdjoinRoot f
      let : IsLocalRing B :=
        isLocalRing_adjoinRoot_X_pow_sub_C (hn (Fin.last r)) haLast
      let : Module.FaithfullyFlat T B :=
        faithfullyFlat_adjoinRoot_X_pow_sub_C
          (hn (Fin.last r)) (algebraMap A T (a (Fin.last r)))
      let : Module.FaithfullyFlat A B :=
        Module.FaithfullyFlat.trans A T B
      have hinit : Function.Bijective
          (IsLocalRing.ResidueField.map (algebraMap A T)) :=
        ih (Fin.init n) (Fin.init a)
          (fun i ↦ hn i.castSucc) (fun i ↦ ha i.castSucc)
      have hlast : Function.Bijective
          (IsLocalRing.ResidueField.map (algebraMap T B)) :=
        residueFieldMap_bijective_adjoinRoot_X_pow_sub_C
          (hn (Fin.last r)) haLast
      change Function.Bijective
        (IsLocalRing.ResidueField.map (algebraMap A B))
      constructor
      · exact (IsLocalRing.ResidueField.map (algebraMap A B)).injective
      · intro z
        obtain ⟨y, hy⟩ := hlast.2 z
        obtain ⟨x, hx⟩ := hinit.2 y
        refine ⟨x, ?_⟩
        obtain ⟨x₀, rfl⟩ := IsLocalRing.residue_surjective x
        calc
          IsLocalRing.ResidueField.map (algebraMap A B)
              (IsLocalRing.residue A x₀) =
              IsLocalRing.ResidueField.map (algebraMap T B)
                (IsLocalRing.ResidueField.map (algebraMap A T)
                  (IsLocalRing.residue A x₀)) := by
            rw [IsLocalRing.ResidueField.map_residue,
              IsLocalRing.ResidueField.map_residue,
              IsLocalRing.ResidueField.map_residue,
              IsScalarTower.algebraMap_apply A T B]
          _ = IsLocalRing.ResidueField.map (algebraMap T B) y := by rw [hx]
          _ = z := hy
theorem

isSepClosed_residueField_adjoinRoot_X_pow_sub_C

L169 ↗
EtaleFundamentalGroups.Kummer.isSepClosed_residueField_adjoinRoot_X_pow_sub_C
Documentation

A positive local Kummer root cover preserves separable closedness of the residue field.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u
Lean source · full declaration
theorem isSepClosed_residueField_adjoinRoot_X_pow_sub_C
    {R : Type u} [CommRing R] [IsLocalRing R]
    [IsSepClosed (IsLocalRing.ResidueField R)]
    {n : ℕ} (hn : 0 < n) {a : R} (ha : a ∈ IsLocalRing.maximalIdeal R) :
    let B := AdjoinRoot (X ^ n - C a)
    letI : IsLocalRing B := isLocalRing_adjoinRoot_X_pow_sub_C hn ha
    letI : Module.FaithfullyFlat R B :=
      faithfullyFlat_adjoinRoot_X_pow_sub_C hn a
    IsSepClosed (IsLocalRing.ResidueField B) := by
  dsimp only
  let f : R[X] := X ^ n - C a
  let B := AdjoinRoot f
  let : IsLocalRing B := isLocalRing_adjoinRoot_X_pow_sub_C hn ha
  let : Module.FaithfullyFlat R B :=
    faithfullyFlat_adjoinRoot_X_pow_sub_C hn a
  let e : IsLocalRing.ResidueField R ≃+*
      IsLocalRing.ResidueField B :=
    RingEquiv.ofBijective
      (IsLocalRing.ResidueField.map (algebraMap R B))
      (residueFieldMap_bijective_adjoinRoot_X_pow_sub_C hn ha)
  exact isSepClosed_of_ringEquiv e
theorem

isSepClosed_residueField_iteratedRadical

L193 ↗
EtaleFundamentalGroups.Kummer.isSepClosed_residueField_iteratedRadical
Documentation

A finite positive iterated local Kummer root cover preserves separable closedness of the residue field.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u
Lean source · full declaration
theorem isSepClosed_residueField_iteratedRadical
    {A : Type u} [CommRing A] [IsLocalRing A]
    [IsSepClosed (IsLocalRing.ResidueField A)]
    {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
    letI : Module.FaithfullyFlat A B :=
      faithfullyFlat_iteratedRadical n a hn
    IsSepClosed (IsLocalRing.ResidueField B) := by
  dsimp only
  let B := iteratedRadical A r n a
  let : IsLocalRing B := isLocalRing_iteratedRadical n a hn ha
  let : Module.FaithfullyFlat A B :=
    faithfullyFlat_iteratedRadical n a hn
  let e : IsLocalRing.ResidueField A ≃+*
      IsLocalRing.ResidueField B :=
    RingEquiv.ofBijective
      (IsLocalRing.ResidueField.map (algebraMap A B))
      (residueFieldMap_bijective_iteratedRadical n a hn ha)
  exact isSepClosed_of_ringEquiv e

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