NYLL
Module

CompleteDVF.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.CompleteDVF
25 declarations indexed from sourceView source ↗

Module documentation

Decomposition and inertia for finite extensions of complete DVFs

For a finite separable extension of complete discretely valued fields, the extension of the base valuation is unique. Consequently every base-field automorphism stabilizes the chosen target valuation ring and the full Galois group is the decomposition group. Reduction then gives the finite Galois exact sequence

1 -> I(L/K) -> Gal(L/K) -> Gal(k_L/k_K) -> 1.

The valuation-subring definitions and their ordinary exactness are reused from HilbertRamification.ValuationSubring; this file only supplies the complete-DVF specialization and the finite-Galois surjectivity theorem.

Imports6
Imported by4

Declarations

instance

decompositionGroupMulSemiringAction

L47 ↗
RamificationTheory.HilbertRamification.CompleteDVF.decompositionGroupMulSemiringAction
Source context 9 commands

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

noncomputable section
open scoped Pointwise
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
instance decompositionGroupMulSemiringAction :
    MulSemiringAction
      (ValuationSubring.decompositionGroup K
        target.valuation.valuationSubring)
      target.valuationSubring
instance

decompositionGroupResidueFieldMulSemiringAction

L57 ↗
RamificationTheory.HilbertRamification.CompleteDVF.decompositionGroupResidueFieldMulSemiringAction
Source context 9 commands

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

noncomputable section
open scoped Pointwise
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
instance decompositionGroupResidueFieldMulSemiringAction :
    MulSemiringAction
      (ValuationSubring.decompositionGroup K
        target.valuation.valuationSubring)
      target.residueField
theorem

comapValuation_hasExtension

L67 ↗
RamificationTheory.HilbertRamification.CompleteDVF.comapValuation_hasExtension
Source context 9 commands

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

noncomputable section
open scoped Pointwise
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · full declaration
theorem comapValuation_hasExtension
    (sigma : L ≃ₐ[K] L) :
    base.valuation.HasExtension
      (target.valuation.comap (sigma : L →+* L)) where
  val_isEquiv_comap := by
    rw [_root_.Valuation.isEquiv_iff_val_le_one]
    intro a
    simpa [_root_.Valuation.comap, sigma.commutes a] using
      (_root_.Valuation.HasExtension.val_map_le_one_iff
        (vR := base.valuation) (vA := target.valuation) a).symm
theorem

inv_smul_valuationSubring_eq

L84 ↗
RamificationTheory.HilbertRamification.CompleteDVF.inv_smul_valuationSubring_eq
Source context 12 commands

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

noncomputable section
open scoped Pointwise
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
section ValuationUniqueness
variable [FiniteDimensional K L]
include base target
Lean source · statement
theorem inv_smul_valuationSubring_eq
    [Algebra.IsSeparable K L]
    (sigma : L ≃ₐ[K] L) :
    sigma⁻¹ • target.valuation.valuationSubring =
      target.valuation.valuationSubring
theorem

automorphism_stabilizes_valuationSubring

L112 ↗
RamificationTheory.HilbertRamification.CompleteDVF.automorphism_stabilizes_valuationSubring
Documentation

Every automorphism of a finite separable extension of complete DVFs stabilizes the target valuation ring.

Source context 12 commands

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

noncomputable section
open scoped Pointwise
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
section ValuationUniqueness
variable [FiniteDimensional K L]
include base target
Lean source · statement
theorem automorphism_stabilizes_valuationSubring
    [Algebra.IsSeparable K L]
    (sigma : L ≃ₐ[K] L) :
    sigma • target.valuation.valuationSubring =
      target.valuation.valuationSubring
def

galEquivDecompositionGroup

L126 ↗
RamificationTheory.HilbertRamification.CompleteDVF.galEquivDecompositionGroup
Documentation

For a finite separable extension of complete DVFs, the full automorphism group is canonically the decomposition group of the target valuation ring.

Source context 12 commands

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

noncomputable section
open scoped Pointwise
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
section ValuationUniqueness
variable [FiniteDimensional K L]
include base target
Lean source · full declaration
def galEquivDecompositionGroup
    [Algebra.IsSeparable K L] :
    (L ≃ₐ[K] L) ≃*
      ValuationSubring.decompositionGroup K
        target.valuation.valuationSubring where
  toFun sigma := ⟨sigma, by
    change sigma • target.valuation.valuationSubring =
      target.valuation.valuationSubring
    exact automorphism_stabilizes_valuationSubring
      (base := base) (target := target) sigma⟩
  invFun sigma := (sigma : L ≃ₐ[K] L)
  left_inv _ := rfl
  right_inv _ := by apply Subtype.ext; rfl
  map_mul' _ _ := by apply Subtype.ext; rfl
theorem

galEquivDecompositionGroup_coe

L143 ↗
RamificationTheory.HilbertRamification.CompleteDVF.galEquivDecompositionGroup_coe
Documentation

States the theorem galEquivDecompositionGroup_coe.

Source context 12 commands

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

noncomputable section
open scoped Pointwise
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
section ValuationUniqueness
variable [FiniteDimensional K L]
include base target
Lean source · statement
theorem galEquivDecompositionGroup_coe
    [Algebra.IsSeparable K L]
    (sigma : L ≃ₐ[K] L) :
    ((galEquivDecompositionGroup (base := base) (target := target) sigma :
        ValuationSubring.decompositionGroup K
      target.valuation.valuationSubring) : L ≃ₐ[K] L) = sigma
def

decompositionResidueAction

L155 ↗
RamificationTheory.HilbertRamification.CompleteDVF.decompositionResidueAction
Documentation

Reduction of the decomposition-group action, as automorphisms over the base residue field.

Source context 9 commands

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

noncomputable section
open scoped Pointwise
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · full declaration
def decompositionResidueAction :
    ValuationSubring.decompositionGroup K
        target.valuation.valuationSubring →*
      (target.residueField ≃ₐ[base.residueField] target.residueField) where
  toFun sigma :=
    { ValuationSubring.residueAction K target.valuation.valuationSubring sigma with
      commutes' := by
        intro z
        obtain ⟨a, rfl⟩ := IsLocalRing.residue_surjective z
        change
          ValuationSubring.residueAction K target.valuation.valuationSubring sigma
              (IsLocalRing.residue target.valuationSubring
                (algebraMap base.valuationSubring target.valuationSubring a)) =
            IsLocalRing.residue target.valuationSubring
              (algebraMap base.valuationSubring target.valuationSubring a)
        change
          sigma •
              (IsLocalRing.residue target.valuationSubring
                (algebraMap base.valuationSubring target.valuationSubring a)) =
            IsLocalRing.residue target.valuationSubring
              (algebraMap base.valuationSubring target.valuationSubring a)
        change
          IsLocalRing.residue target.valuationSubring
              (sigma •
                algebraMap base.valuationSubring target.valuationSubring a) =
            IsLocalRing.residue target.valuationSubring
              (algebraMap base.valuationSubring target.valuationSubring a)
        congr 1
        apply Subtype.ext
        change
          (sigma : L ≃ₐ[K] L) (algebraMap K L (a : K)) =
            algebraMap K L (a : K)
        exact (sigma : L ≃ₐ[K] L).commutes (a : K) }
  map_one' := by
    apply AlgEquiv.ext
    intro z
    change
      ValuationSubring.residueAction K target.valuation.valuationSubring 1 z =
        (1 : target.residueField ≃ₐ[base.residueField] target.residueField) z
    rw [MonoidHom.map_one]
    exact AlgEquiv.one_apply (R := base.residueField) (A₁ := target.residueField) z
  map_mul' := by
    intro sigma tau
    apply AlgEquiv.ext
    intro z
    change
      ValuationSubring.residueAction K target.valuation.valuationSubring
          (sigma * tau) z =
        (ValuationSubring.residueAction K target.valuation.valuationSubring sigma *
          ValuationSubring.residueAction K target.valuation.valuationSubring tau) z
    rw [MonoidHom.map_mul]
theorem

decompositionResidueAction_apply

L209 ↗
RamificationTheory.HilbertRamification.CompleteDVF.decompositionResidueAction_apply
Documentation

States the theorem decompositionResidueAction_apply.

Source context 9 commands

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

noncomputable section
open scoped Pointwise
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem decompositionResidueAction_apply
    (sigma : ValuationSubring.decompositionGroup K
      target.valuation.valuationSubring)
    (z : target.residueField) :
    decompositionResidueAction (K := K) (base := base) (target := target) sigma z =
      ValuationSubring.residueAction K
        target.valuation.valuationSubring sigma z
theorem

decompositionResidueAction_algebraMap

L220 ↗
RamificationTheory.HilbertRamification.CompleteDVF.decompositionResidueAction_algebraMap
Documentation

States the theorem decompositionResidueAction_algebraMap.

Source context 9 commands

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

noncomputable section
open scoped Pointwise
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem decompositionResidueAction_algebraMap
    (sigma : ValuationSubring.decompositionGroup K
      target.valuation.valuationSubring)
    (z : base.residueField) :
    decompositionResidueAction (K := K) (base := base) (target := target) sigma
        (algebraMap base.residueField target.residueField z) =
      algebraMap base.residueField target.residueField z
theorem

decompositionResidueAction_ker

L231 ↗
RamificationTheory.HilbertRamification.CompleteDVF.decompositionResidueAction_ker
Documentation

The kernel of reduction on the decomposition group is its inertia group.

Source context 9 commands

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

noncomputable section
open scoped Pointwise
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem decompositionResidueAction_ker :
    MonoidHom.ker
        (decompositionResidueAction
          (K := K) (base := base) (target := target)) =
      ValuationSubring.inertiaGroup K
        target.valuation.valuationSubring
theorem

maximalIdealInertia_eq_decompositionInertia

L262 ↗
RamificationTheory.HilbertRamification.CompleteDVF.maximalIdealInertia_eq_decompositionInertia
Documentation

Ideal-theoretic inertia of the target maximal ideal, for the canonical decomposition-group action on the valuation ring, is the ordinary valuation-subring inertia group.

Source context 10 commands

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

noncomputable section
open scoped Pointwise
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
omit [base.valuation.HasExtension target.valuation] in
Lean source · statement
theorem maximalIdealInertia_eq_decompositionInertia :
    target.maximalIdeal.toAddSubgroup.inertia
        (ValuationSubring.decompositionGroup K
          target.valuation.valuationSubring) =
      ValuationSubring.inertiaGroup K
        target.valuation.valuationSubring
theorem

decompositionInertia_mulExact_decompositionResidueAction

L300 ↗
RamificationTheory.HilbertRamification.CompleteDVF.decompositionInertia_mulExact_decompositionResidueAction
Documentation

Exactness of inertia inclusion followed by reduction on the decomposition group.

Source context 9 commands

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

noncomputable section
open scoped Pointwise
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem decompositionInertia_mulExact_decompositionResidueAction :
    Function.MulExact
      (ValuationSubring.inertiaGroup K
        target.valuation.valuationSubring).subtype
      (decompositionResidueAction
        (K := K) (base := base) (target := target))
def

residueAction

L317 ↗
RamificationTheory.HilbertRamification.CompleteDVF.residueAction
Documentation

The residue action of the full automorphism group, transported through the canonical identification with the decomposition group.

Source context 12 commands

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

noncomputable section
open scoped Pointwise
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
section FullGaloisGroup
variable [FiniteDimensional K L]
include base target
Lean source · statement
def residueAction
    [Algebra.IsSeparable K L] :
    (L ≃ₐ[K] L) →*
      (target.residueField ≃ₐ[base.residueField] target.residueField)
theorem

residueAction_apply

L328 ↗
RamificationTheory.HilbertRamification.CompleteDVF.residueAction_apply
Documentation

States the theorem residueAction_apply.

Source context 12 commands

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

noncomputable section
open scoped Pointwise
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
section FullGaloisGroup
variable [FiniteDimensional K L]
include base target
Lean source · statement
theorem residueAction_apply
    [Algebra.IsSeparable K L]
    (sigma : L ≃ₐ[K] L) :
    residueAction (K := K) (base := base) (target := target) sigma =
      decompositionResidueAction
        (K := K) (base := base) (target := target)
        (galEquivDecompositionGroup
          (base := base) (target := target) sigma)
def

inertiaGroup

L340 ↗
RamificationTheory.HilbertRamification.CompleteDVF.inertiaGroup
Documentation

Inertia inside the full Galois group is the inverse image of the ordinary decomposition-side inertia group.

Source context 12 commands

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

noncomputable section
open scoped Pointwise
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
section FullGaloisGroup
variable [FiniteDimensional K L]
include base target
Lean source · statement
def inertiaGroup
    [Algebra.IsSeparable K L] :
    Subgroup (L ≃ₐ[K] L)
theorem

mem_inertiaGroup_iff

L351 ↗
RamificationTheory.HilbertRamification.CompleteDVF.mem_inertiaGroup_iff
Documentation

States the theorem mem_inertiaGroup_iff.

Source context 12 commands

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

noncomputable section
open scoped Pointwise
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
section FullGaloisGroup
variable [FiniteDimensional K L]
include base target
Lean source · statement
theorem mem_inertiaGroup_iff
    [Algebra.IsSeparable K L]
    (sigma : L ≃ₐ[K] L) :
    sigma ∈ inertiaGroup (K := K) (base := base) (target := target) ↔
      galEquivDecompositionGroup
          (base := base) (target := target) sigma ∈
        ValuationSubring.inertiaGroup K
          target.valuation.valuationSubring
theorem

inertiaGroup_map_galEquivDecompositionGroup

L363 ↗
RamificationTheory.HilbertRamification.CompleteDVF.inertiaGroup_map_galEquivDecompositionGroup
Documentation

Transporting full inertia through Gal(L/K) ≃ D(L/K) gives exactly the ordinary decomposition-side inertia group.

Source context 12 commands

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

noncomputable section
open scoped Pointwise
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
section FullGaloisGroup
variable [FiniteDimensional K L]
include base target
Lean source · statement
theorem inertiaGroup_map_galEquivDecompositionGroup
    [Algebra.IsSeparable K L] :
    Subgroup.map
        (galEquivDecompositionGroup
          (base := base) (target := target)).toMonoidHom
        (inertiaGroup (K := K) (base := base) (target := target)) =
      ValuationSubring.inertiaGroup K
        target.valuation.valuationSubring
theorem

residueAction_ker

L388 ↗
RamificationTheory.HilbertRamification.CompleteDVF.residueAction_ker
Documentation

The kernel of the full residue action is the full inertia group.

Source context 12 commands

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

noncomputable section
open scoped Pointwise
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
section FullGaloisGroup
variable [FiniteDimensional K L]
include base target
Lean source · statement
theorem residueAction_ker
    [Algebra.IsSeparable K L] :
    MonoidHom.ker
        (residueAction (K := K) (base := base) (target := target)) =
      inertiaGroup (K := K) (base := base) (target := target)
instance

inertiaGroup_normal

L408 ↗
RamificationTheory.HilbertRamification.CompleteDVF.inertiaGroup_normal
Documentation

Provides the instance inertiaGroup_normal.

Source context 12 commands

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

noncomputable section
open scoped Pointwise
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
section FullGaloisGroup
variable [FiniteDimensional K L]
include base target
Lean source · statement
instance inertiaGroup_normal
    [Algebra.IsSeparable K L] :
    (inertiaGroup (K := K) (base := base) (target := target)).Normal
theorem

inertia_mulExact_residueAction

L415 ↗
RamificationTheory.HilbertRamification.CompleteDVF.inertia_mulExact_residueAction
Documentation

Exactness of full inertia inclusion followed by reduction.

Source context 12 commands

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

noncomputable section
open scoped Pointwise
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
section FullGaloisGroup
variable [FiniteDimensional K L]
include base target
Lean source · statement
theorem inertia_mulExact_residueAction
    [Algebra.IsSeparable K L] :
    Function.MulExact
      (inertiaGroup (K := K) (base := base) (target := target)).subtype
      (residueAction (K := K) (base := base) (target := target))
theorem

residueAction_surjective_of_isGalois

L425 ↗
RamificationTheory.HilbertRamification.CompleteDVF.residueAction_surjective_of_isGalois
Documentation

For a finite Galois extension of complete DVFs, reduction of the full Galois group is onto the residue-field Galois group.

Source context 12 commands

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

noncomputable section
open scoped Pointwise
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
section FullGaloisGroup
variable [FiniteDimensional K L]
include base target
Lean source · statement
theorem residueAction_surjective_of_isGalois
    [IsGalois K L] :
    Function.Surjective
      (residueAction (K := K) (base := base) (target := target))
theorem

decompositionResidueAction_surjective_of_isGalois

L465 ↗
RamificationTheory.HilbertRamification.CompleteDVF.decompositionResidueAction_surjective_of_isGalois
Documentation

The decomposition-group residue action is also onto in the finite Galois case.

Source context 12 commands

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

noncomputable section
open scoped Pointwise
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
section FullGaloisGroup
variable [FiniteDimensional K L]
include base target
Lean source · statement
theorem decompositionResidueAction_surjective_of_isGalois
    [IsGalois K L] :
    Function.Surjective
      (decompositionResidueAction
        (K := K) (base := base) (target := target))
def

galQuotientInertiaEquivResidueGalois

L478 ↗
RamificationTheory.HilbertRamification.CompleteDVF.galQuotientInertiaEquivResidueGalois
Documentation

The finite-Galois residue exact sequence in quotient form.

Source context 12 commands

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

noncomputable section
open scoped Pointwise
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
section FullGaloisGroup
variable [FiniteDimensional K L]
include base target
Lean source · statement
def galQuotientInertiaEquivResidueGalois
    [IsGalois K L] :
    (L ≃ₐ[K] L) ⧸
        inertiaGroup (K := K) (base := base) (target := target) ≃*
      (target.residueField ≃ₐ[base.residueField] target.residueField)
theorem

galQuotientInertiaEquivResidueGalois_mk

L493 ↗
RamificationTheory.HilbertRamification.CompleteDVF.galQuotientInertiaEquivResidueGalois_mk
Documentation

States the theorem galQuotientInertiaEquivResidueGalois_mk.

Source context 12 commands

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

noncomputable section
open scoped Pointwise
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
section FullGaloisGroup
variable [FiniteDimensional K L]
include base target
Lean source · statement
theorem galQuotientInertiaEquivResidueGalois_mk
    [IsGalois K L]
    (sigma : L ≃ₐ[K] L) :
    galQuotientInertiaEquivResidueGalois
        (K := K) (base := base) (target := target)
        (QuotientGroup.mk'
          (inertiaGroup (K := K) (base := base) (target := target)) sigma) =
      residueAction (K := K) (base := base) (target := target) sigma

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