NYLL
Module

FixedFieldValuationRing.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.FixedFieldValuationRing
24 declarations indexed from sourceView source ↗

Module documentation

Restricted valuation rings on actual fixed fields

For a normal subgroup of a finite Galois group, this file uses the literal fixed field and the restriction of the chosen top valuation ring. Unique extension identifies that restricted ring with the integral closure of the base valuation ring. It is consequently a DVR, without a completeness or Henselian assumption.

Imports2
Imported by3

Declarations

abbrev

fixedFieldDVF

L38 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldDVF
Documentation

The actual fixed field of a subgroup.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
abbrev fixedFieldDVF (H : Subgroup Gal(L/K))
def

fixedFieldValuationSubringDVF

L42 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldValuationSubringDVF
Documentation

Restriction of the chosen top valuation ring to the actual fixed field.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
def fixedFieldValuationSubringDVF (H : Subgroup Gal(L/K)) :
    ValuationSubring (fixedFieldDVF (K := K) H)
theorem

mem_fixedFieldValuationSubringDVF_iff

L48 ↗
RamificationTheory.HilbertRamification.Higher.mem_fixedFieldValuationSubringDVF_iff
Documentation

States the theorem mem_fixedFieldValuationSubringDVF_iff.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem mem_fixedFieldValuationSubringDVF_iff
    (H : Subgroup Gal(L/K)) (a : fixedFieldDVF (K := K) H) :
    a ∈ fixedFieldValuationSubringDVF (K := K) (target := target) H ↔
      algebraMap (fixedFieldDVF (K := K) H) L a ∈
        target.valuation.valuationSubring
def

fixedFieldValuationSubringDVFToTarget

L57 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldValuationSubringDVFToTarget
Documentation

Inclusion of the restricted fixed-field valuation ring into the top valuation ring.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
def fixedFieldValuationSubringDVFToTarget
    (H : Subgroup Gal(L/K)) :
    fixedFieldValuationSubringDVF (K := K) (target := target) H →+*
      target.valuationSubring
theorem

fixedFieldValuationSubringDVFToTarget_apply_coe

L66 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldValuationSubringDVFToTarget_apply_coe
Documentation

States the theorem fixedFieldValuationSubringDVFToTarget_apply_coe.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem fixedFieldValuationSubringDVFToTarget_apply_coe
    (H : Subgroup Gal(L/K))
    (a : fixedFieldValuationSubringDVF (K := K) (target := target) H) :
    ((fixedFieldValuationSubringDVFToTarget
      (K := K) (target := target) H a : target.valuationSubring) : L) =
      algebraMap (fixedFieldDVF (K := K) H) L (a : fixedFieldDVF (K := K) H)
theorem

fixedFieldValuationSubringDVFToTarget_injective

L75 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldValuationSubringDVFToTarget_injective
Documentation

States the theorem fixedFieldValuationSubringDVFToTarget_injective.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem fixedFieldValuationSubringDVFToTarget_injective
    (H : Subgroup Gal(L/K)) :
    Function.Injective
      (fixedFieldValuationSubringDVFToTarget
        (K := K) (target := target) H)
def

baseToFixedFieldValuationSubringDVF

L87 ↗
RamificationTheory.HilbertRamification.Higher.baseToFixedFieldValuationSubringDVF
Documentation

The base valuation-ring map into the restricted valuation ring of the fixed field.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
def baseToFixedFieldValuationSubringDVF
    (H : Subgroup Gal(L/K)) :
    base.valuationSubring →+*
      fixedFieldValuationSubringDVF (K := K) (target := target) H
instance

instAlgebraBaseFixedFieldValuationSubringDVF

L100 ↗
RamificationTheory.HilbertRamification.Higher.instAlgebraBaseFixedFieldValuationSubringDVF
Documentation

Provides the instance instAlgebraBaseFixedFieldValuationSubringDVF.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
instance instAlgebraBaseFixedFieldValuationSubringDVF
    (H : Subgroup Gal(L/K)) :
    Algebra base.valuationSubring
      (fixedFieldValuationSubringDVF (K := K) (target := target) H)
theorem

base_hasExtension_fixedFieldValuationSubringDVF

L108 ↗
RamificationTheory.HilbertRamification.Higher.base_hasExtension_fixedFieldValuationSubringDVF
Documentation

The restricted valuation on the fixed field extends the base valuation.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem base_hasExtension_fixedFieldValuationSubringDVF
    (H : Subgroup Gal(L/K)) :
    base.valuation.HasExtension
      (fixedFieldValuationSubringDVF
        (K := K) (target := target) H).valuation
instance

instBaseHasExtensionFixedFieldValuationSubringDVF

L122 ↗
RamificationTheory.HilbertRamification.Higher.instBaseHasExtensionFixedFieldValuationSubringDVF
Documentation

Provides the instance instBaseHasExtensionFixedFieldValuationSubringDVF.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
instance instBaseHasExtensionFixedFieldValuationSubringDVF
    (H : Subgroup Gal(L/K)) :
    base.valuation.HasExtension
      (fixedFieldValuationSubringDVF
        (K := K) (target := target) H).valuation
def

fixedFieldValuationSubringDVFToTargetAlgHom

L132 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldValuationSubringDVFToTargetAlgHom
Documentation

The inclusion of valuation rings, as an algebra homomorphism over the base valuation ring.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · full declaration
def fixedFieldValuationSubringDVFToTargetAlgHom
    (H : Subgroup Gal(L/K)) :
    fixedFieldValuationSubringDVF (K := K) (target := target) H →ₐ[
      base.valuationSubring] target.valuationSubring where
  toRingHom := fixedFieldValuationSubringDVFToTarget
    (K := K) (target := target) H
  commutes' a := by
    apply Subtype.ext
    rfl
theorem

fixedFieldValuationSubringDVFToTargetAlgHom_injective

L143 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldValuationSubringDVFToTargetAlgHom_injective
Documentation

States the theorem fixedFieldValuationSubringDVFToTargetAlgHom_injective.

Source context 9 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem fixedFieldValuationSubringDVFToTargetAlgHom_injective
    (H : Subgroup Gal(L/K)) :
    Function.Injective
      (fixedFieldValuationSubringDVFToTargetAlgHom
        (K := K) (base := base) (target := target) H)
theorem

fixedFieldValuationSubringDVF_isIntegral

L156 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldValuationSubringDVF_isIntegral
Documentation

The restricted fixed-field valuation ring is integral over the base valuation ring.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
variable [IsGalois K L]
Lean source · statement
theorem fixedFieldValuationSubringDVF_isIntegral
    (huniq :
      HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) :
    Algebra.IsIntegral base.valuationSubring
      (fixedFieldValuationSubringDVF (K := K) (target := target) H)
theorem

fixedFieldValuationSubringDVF_isIntegralClosure

L174 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldValuationSubringDVF_isIntegralClosure
Documentation

The restricted fixed-field valuation ring is the actual integral closure of the base valuation ring in the fixed field.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
variable [IsGalois K L]
Lean source · statement
theorem fixedFieldValuationSubringDVF_isIntegralClosure
    (huniq :
      HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) :
    IsIntegralClosure
      (fixedFieldValuationSubringDVF (K := K) (target := target) H)
      base.valuationSubring (fixedFieldDVF (K := K) H)
theorem

fixedFieldValuationSubringDVF_moduleFinite

L217 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldValuationSubringDVF_moduleFinite
Documentation

Module finiteness of the restricted integral closure.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
variable [IsGalois K L]
Lean source · statement
theorem fixedFieldValuationSubringDVF_moduleFinite
    (huniq :
      HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] :
    Module.Finite base.valuationSubring
      (fixedFieldValuationSubringDVF (K := K) (target := target) H)
theorem

fixedFieldValuationSubringDVF_isDiscreteValuationRing

L242 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldValuationSubringDVF_isDiscreteValuationRing
Documentation

The restricted valuation ring on a nontrivial finite fixed field is a DVR. This is an algebraic consequence of module finiteness and does not use completeness.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
variable [IsGalois K L]
Lean source · statement
theorem fixedFieldValuationSubringDVF_isDiscreteValuationRing
    (huniq :
      HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal] :
    IsDiscreteValuationRing
      (fixedFieldValuationSubringDVF (K := K) (target := target) H)
theorem

algebraMap_normalAutEquivQuotient_apply_dvf

L274 ↗
RamificationTheory.HilbertRamification.Higher.algebraMap_normalAutEquivQuotient_apply_dvf
Documentation

The quotient automorphism on the fixed field commutes with inclusion into the top field.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
variable [IsGalois K L]
Lean source · statement
theorem algebraMap_normalAutEquivQuotient_apply_dvf
    (H : Subgroup Gal(L/K)) [H.Normal]
    (sigma : Gal(L/K)) (a : fixedFieldDVF (K := K) H) :
    algebraMap (fixedFieldDVF (K := K) H) L
        (IsGalois.normalAutEquivQuotient H sigma a) =
      sigma (algebraMap (fixedFieldDVF (K := K) H) L a)
def

fixedFieldValuationSubringLiftedAutDVF

L286 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldValuationSubringLiftedAutDVF
Documentation

Restriction of the quotient automorphism to the actual fixed-field valuation ring.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
variable [IsGalois K L]
Lean source · full declaration
def fixedFieldValuationSubringLiftedAutDVF
    (huniq :
      HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal]
    (sigma : Gal(L/K)) :
    fixedFieldValuationSubringDVF (K := K) (target := target) H ≃+*
      fixedFieldValuationSubringDVF (K := K) (target := target) H where
  toFun a :=
    ⟨IsGalois.normalAutEquivQuotient H sigma (a : fixedFieldDVF (K := K) H), by
      rw [mem_fixedFieldValuationSubringDVF_iff,
        algebraMap_normalAutEquivQuotient_apply_dvf
          (K := K) H sigma]
      exact
        (mem_valuationSubring_algEquiv_iff_of_hasUniqueValuationExtension
          (base := base) (target := target) huniq sigma _).1 a.property⟩
  invFun a :=
    ⟨(IsGalois.normalAutEquivQuotient H sigma).symm
        (a : fixedFieldDVF (K := K) H), by
      rw [mem_fixedFieldValuationSubringDVF_iff]
      have hEq :
          algebraMap (fixedFieldDVF (K := K) H) L
              ((IsGalois.normalAutEquivQuotient H sigma).symm
                (a : fixedFieldDVF (K := K) H)) =
            sigma⁻¹ (algebraMap (fixedFieldDVF (K := K) H) L a) := by
        simpa using algebraMap_normalAutEquivQuotient_apply_dvf
          (K := K) H (sigma⁻¹) (a : fixedFieldDVF (K := K) H)
      rw [hEq]
      exact
        (mem_valuationSubring_algEquiv_iff_of_hasUniqueValuationExtension
          (base := base) (target := target) huniq (sigma⁻¹) _).1 a.property⟩
  left_inv a := by
    ext
    simp
  right_inv a := by
    ext
    simp
  map_mul' a b := by
    ext
    simp
  map_add' a b := by
    ext
    simp
theorem

fixedFieldValuationSubringDVFToTarget_aut_apply

L331 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldValuationSubringDVFToTarget_aut_apply
Documentation

States the theorem fixedFieldValuationSubringDVFToTarget_aut_apply.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
variable [IsGalois K L]
Lean source · statement
theorem fixedFieldValuationSubringDVFToTarget_aut_apply
    (huniq :
      HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal]
    (sigma : Gal(L/K))
    (a : fixedFieldValuationSubringDVF (K := K) (target := target) H) :
    fixedFieldValuationSubringDVFToTarget
        (K := K) (target := target) H
        (fixedFieldValuationSubringLiftedAutDVF
          (base := base) (target := target) huniq H sigma a) =
      valuationSubringAutOfUniqueExtension
        (base := base) (target := target) huniq sigma
        (fixedFieldValuationSubringDVFToTarget
          (K := K) (target := target) H a)
theorem

fixedFieldDVF_aut_mem_valuationSubring_iff

L354 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldDVF_aut_mem_valuationSubring_iff
Documentation

Every automorphism of the fixed field preserves its restricted valuation ring. Surjectivity in the finite Galois correspondence is used only to prove preservation; the automorphism appearing in the statement is an automorphism of L ^ H itself.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
variable [IsGalois K L]
Lean source · statement
theorem fixedFieldDVF_aut_mem_valuationSubring_iff
    (huniq :
      HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal]
    (q : Gal((fixedFieldDVF (K := K) H)/K))
    (a : fixedFieldDVF (K := K) H) :
    a ∈ fixedFieldValuationSubringDVF (K := K) (target := target) H ↔
      q a ∈ fixedFieldValuationSubringDVF (K := K) (target := target) H
def

fixedFieldValuationSubringAutDVF

L380 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldValuationSubringAutDVF
Documentation

The canonical action of the fixed-field Galois group on its restricted valuation ring.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
variable [IsGalois K L]
Lean source · full declaration
def fixedFieldValuationSubringAutDVF
    (huniq :
      HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal]
    (q : Gal((fixedFieldDVF (K := K) H)/K)) :
    fixedFieldValuationSubringDVF (K := K) (target := target) H ≃+*
      fixedFieldValuationSubringDVF (K := K) (target := target) H where
  toFun a := ⟨q (a : fixedFieldDVF (K := K) H),
    (fixedFieldDVF_aut_mem_valuationSubring_iff
      (base := base) (target := target) huniq H q _).1 a.property⟩
  invFun a := ⟨q⁻¹ (a : fixedFieldDVF (K := K) H),
    (fixedFieldDVF_aut_mem_valuationSubring_iff
      (base := base) (target := target) huniq H q⁻¹ _).1 a.property⟩
  left_inv a := by ext; simp
  right_inv a := by ext; simp
  map_mul' a b := by ext; simp
  map_add' a b := by ext; simp
theorem

fixedFieldValuationSubringAutDVF_apply_coe

L400 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldValuationSubringAutDVF_apply_coe
Documentation

States the theorem fixedFieldValuationSubringAutDVF_apply_coe.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
variable [IsGalois K L]
Lean source · statement
theorem fixedFieldValuationSubringAutDVF_apply_coe
    (huniq :
      HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal]
    (q : Gal((fixedFieldDVF (K := K) H)/K))
    (a : fixedFieldValuationSubringDVF (K := K) (target := target) H) :
    ((fixedFieldValuationSubringAutDVF
      (base := base) (target := target) huniq H q a :
        fixedFieldValuationSubringDVF (K := K) (target := target) H) :
      fixedFieldDVF (K := K) H) = q (a : fixedFieldDVF (K := K) H)
theorem

fixedFieldValuationSubringAutDVF_mul_apply

L414 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldValuationSubringAutDVF_mul_apply
Documentation

States the theorem fixedFieldValuationSubringAutDVF_mul_apply.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
variable [IsGalois K L]
Lean source · statement
theorem fixedFieldValuationSubringAutDVF_mul_apply
    (huniq :
      HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal]
    (q r : Gal((fixedFieldDVF (K := K) H)/K))
    (a : fixedFieldValuationSubringDVF (K := K) (target := target) H) :
    fixedFieldValuationSubringAutDVF
        (base := base) (target := target) huniq H (q * r) a =
      fixedFieldValuationSubringAutDVF
        (base := base) (target := target) huniq H q
        (fixedFieldValuationSubringAutDVF
          (base := base) (target := target) huniq H r a)
theorem

fixedFieldValuationSubringAutDVF_normalAutEquivQuotient

L432 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldValuationSubringAutDVF_normalAutEquivQuotient
Documentation

The fixed-field action agrees with the lifted action obtained from any chosen lift in the top Galois group.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L]
variable [IsGalois K L]
Lean source · statement
theorem fixedFieldValuationSubringAutDVF_normalAutEquivQuotient
    (huniq :
      HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal]
    (sigma : Gal(L/K))
    (a : fixedFieldValuationSubringDVF (K := K) (target := target) H) :
    fixedFieldValuationSubringAutDVF
        (base := base) (target := target) huniq H
        (IsGalois.normalAutEquivQuotient H sigma) a =
      fixedFieldValuationSubringLiftedAutDVF
        (base := base) (target := target) huniq H sigma a

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