NYLL
Module

ResidueAlgebraicallyClosed.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.ResidueAlgebraicallyClosed
6 declarations indexed from sourceView source ↗

Module documentation

Residues of algebraically closed valued fields

The residue field of a valuation ring in an algebraically closed field is algebraically closed. This is the missing source needed to apply the intrinsic finite-field degree map to the residue of an algebraic closure of a local field.

Residues under a purely inseparable ambient extension

Imports4
Imported by3

Declarations

theorem

valuationSubring_residueField_isAlgClosed

L35 ↗
LocalClassFieldTheory.valuationSubring_residueField_isAlgClosed
Documentation

The residue field of a valuation subring of an algebraically closed field is algebraically closed. A monic irreducible residue polynomial is lifted monically to the valuation ring. A root in the ambient algebraically closed field is integral, hence lies back in the valuation ring and can be reduced.

Source context 4 commands

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

namespace LocalClassFieldTheory
noncomputable section
universe u
variable {Omega : Type u} [Field Omega] [IsAlgClosed Omega]
Lean source · statement
theorem valuationSubring_residueField_isAlgClosed
    (A : ValuationSubring Omega) :
    IsAlgClosed (IsLocalRing.ResidueField A)
def

valuationSubringComapMap

L87 ↗
LocalClassFieldTheory.valuationSubringComapMap
Documentation

The inclusion from the pullback of a valuation ring to the ambient valuation ring.

Source context 6 commands

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

namespace LocalClassFieldTheory
noncomputable section
universe u
variable {Omega : Type u} [Field Omega] [IsAlgClosed Omega]
section PurelyInseparableComap
variable {F Omega : Type u} [Field F] [Field Omega] [Algebra F Omega]
Lean source · full declaration
def valuationSubringComapMap (A : ValuationSubring Omega) :
    A.comap (algebraMap F Omega) →+* A where
  toFun x := ⟨algebraMap F Omega x, x.property⟩
  map_one' := by ext; simp
  map_mul' x y := by ext; simp
  map_zero' := by ext; simp
  map_add' x y := by ext; simp
theorem

valuationSubringComapMap_isLocalHom

L96 ↗
LocalClassFieldTheory.valuationSubringComapMap_isLocalHom
Documentation

Pullback along a field embedding gives a local map of valuation rings.

Source context 6 commands

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

namespace LocalClassFieldTheory
noncomputable section
universe u
variable {Omega : Type u} [Field Omega] [IsAlgClosed Omega]
section PurelyInseparableComap
variable {F Omega : Type u} [Field F] [Field Omega] [Algebra F Omega]
Lean source · statement
theorem valuationSubringComapMap_isLocalHom (A : ValuationSubring Omega) :
    IsLocalHom (valuationSubringComapMap (F := F) A)
def

valuationSubringComapResidueMap

L131 ↗
LocalClassFieldTheory.valuationSubringComapResidueMap
Documentation

The residue-field embedding induced by pullback of a valuation ring.

Source context 6 commands

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

namespace LocalClassFieldTheory
noncomputable section
universe u
variable {Omega : Type u} [Field Omega] [IsAlgClosed Omega]
section PurelyInseparableComap
variable {F Omega : Type u} [Field F] [Field Omega] [Algebra F Omega]
Lean source · statement
def valuationSubringComapResidueMap
    (A : ValuationSubring Omega) :
    IsLocalRing.ResidueField (A.comap (algebraMap F Omega)) →+*
      IsLocalRing.ResidueField A
theorem

valuationSubringComapResidueMap_residue

L140 ↗
LocalClassFieldTheory.valuationSubringComapResidueMap_residue
Documentation

States the theorem valuationSubringComapResidueMap_residue.

Source context 6 commands

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

namespace LocalClassFieldTheory
noncomputable section
universe u
variable {Omega : Type u} [Field Omega] [IsAlgClosed Omega]
section PurelyInseparableComap
variable {F Omega : Type u} [Field F] [Field Omega] [Algebra F Omega]
Lean source · statement
theorem valuationSubringComapResidueMap_residue
    (A : ValuationSubring Omega)
    (x : A.comap (algebraMap F Omega)) :
    valuationSubringComapResidueMap (F := F) A
        (IsLocalRing.residue (A.comap (algebraMap F Omega)) x) =
      IsLocalRing.residue A (valuationSubringComapMap (F := F) A x)
theorem

valuationSubring_comap_residueField_isPurelyInseparable

L152 ↗
LocalClassFieldTheory.valuationSubring_comap_residueField_isPurelyInseparable
Documentation

A purely inseparable extension remains purely inseparable after passing to the residue fields of a valuation ring and its pullback. In positive characteristic this is the same Frobenius-power argument; in characteristic zero the ambient purely inseparable extension is already trivial.

Source context 6 commands

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

namespace LocalClassFieldTheory
noncomputable section
universe u
variable {Omega : Type u} [Field Omega] [IsAlgClosed Omega]
section PurelyInseparableComap
variable {F Omega : Type u} [Field F] [Field Omega] [Algebra F Omega]
Lean source · full declaration
theorem valuationSubring_comap_residueField_isPurelyInseparable
    [IsPurelyInseparable F Omega] (A : ValuationSubring Omega) :
    letI : Algebra
        (IsLocalRing.ResidueField (A.comap (algebraMap F Omega)))
        (IsLocalRing.ResidueField A) :=
      (valuationSubringComapResidueMap (F := F) A).toAlgebra
    IsPurelyInseparable
      (IsLocalRing.ResidueField (A.comap (algebraMap F Omega)))
      (IsLocalRing.ResidueField A) := by
  let B := A.comap (algebraMap F Omega)
  let barI := valuationSubringComapResidueMap (F := F) A
  let : Algebra (IsLocalRing.ResidueField B)
      (IsLocalRing.ResidueField A) := barI.toAlgebra
  obtain ⟨q, hqF⟩ := ExpChar.exists F
  let : ExpChar F q := hqF
  cases hqF with
  | zero =>
      let : Algebra.IsSeparable F Omega := inferInstance
      rw [isPurelyInseparable_iff_pow_mem
        (IsLocalRing.ResidueField B)
        (ringExpChar (IsLocalRing.ResidueField B))]
      intro y
      obtain ⟨a, rfl⟩ := IsLocalRing.residue_surjective y
      obtain ⟨z, hz⟩ :=
        IsPurelyInseparable.surjective_algebraMap_of_isSeparable F Omega
          (a : Omega)
      let zB : B := ⟨z, by
        change algebraMap F Omega z ∈ A
        rw [hz]
        exact a.property⟩
      refine ⟨0, IsLocalRing.residue B zB, ?_⟩
      simp only [pow_zero, pow_one]
      change barI (IsLocalRing.residue B zB) = IsLocalRing.residue A a
      dsimp only [barI, B]
      rw [valuationSubringComapResidueMap_residue]
      apply congrArg (IsLocalRing.residue A)
      apply Subtype.ext
      exact hz
  | prime hq =>
      let : CharP Omega q :=
        charP_of_injective_algebraMap (algebraMap F Omega).injective q
      let : CharP A q := A.subtype.charP A.subtype_injective q
      let : CharP (IsLocalRing.ResidueField A) q :=
        CharP.of_ringHom_of_ne_zero (IsLocalRing.residue A) q hq.ne_zero
      let : CharP (IsLocalRing.ResidueField B) q :=
        barI.charP barI.injective q
      let : ExpChar (IsLocalRing.ResidueField B) q := ExpChar.prime hq
      rw [isPurelyInseparable_iff_pow_mem
        (IsLocalRing.ResidueField B) q]
      intro y
      obtain ⟨a, rfl⟩ := IsLocalRing.residue_surjective y
      obtain ⟨n, z, hz⟩ := IsPurelyInseparable.pow_mem F q (a : Omega)
      let zB : B := ⟨z, by
        change algebraMap F Omega z ∈ A
        rw [hz]
        exact pow_mem a.property _⟩
      refine ⟨n, IsLocalRing.residue B zB, ?_⟩
      change barI (IsLocalRing.residue B zB) =
        (IsLocalRing.residue A a) ^ q ^ n
      dsimp only [barI, B]
      rw [valuationSubringComapResidueMap_residue]
      rw [← map_pow]
      apply congrArg (IsLocalRing.residue A)
      apply Subtype.ext
      exact hz

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