NYLL
Module

BaseChange.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.BaseChange
16 declarations indexed from sourceView source ↗

Module documentation

Conjugation and base change

This file proves functoriality of the decomposition, inertia, and ramification groups under a commutative square of field embeddings. Only normality of the lower extension is needed to restrict conjugation to its Galois group. The decomposition statement for absolute values includes the archimedean case; the valuation-subring statements give the three nonarchimedean homomorphisms.

Imports2
Imported by10

Declarations

def

galoisPullbackElement

L44 ↗
HilbertRamification.galoisPullbackElement
Source context 13 commands

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

noncomputable section
universe u v u' v'
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} {K' : Type u'} {L' : Type v'}
variable [Field K] [Field L] [Field K'] [Field L']
variable [Algebra K L] [Algebra K' L']
section GaloisPullback
variable (tauK : K →+* K') (tauL : L →+* L')
variable (hsquare : tauL.comp (algebraMap K L) =
  (algebraMap K' L').comp tauK)
variable [Normal K L]
include hsquare in
Lean source · statement
def galoisPullbackElement (sigma : L' ≃ₐ[K'] L') : L ≃ₐ[K] L
theorem

galoisPullbackElement_commutes

L63 ↗
HilbertRamification.galoisPullbackElement_commutes
Source context 12 commands

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

noncomputable section
universe u v u' v'
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} {K' : Type u'} {L' : Type v'}
variable [Field K] [Field L] [Field K'] [Field L']
variable [Algebra K L] [Algebra K' L']
section GaloisPullback
variable (tauK : K →+* K') (tauL : L →+* L')
variable (hsquare : tauL.comp (algebraMap K L) =
  (algebraMap K' L').comp tauK)
variable [Normal K L]
Lean source · statement
theorem galoisPullbackElement_commutes
    (sigma : L' ≃ₐ[K'] L') (x : L) :
    tauL (galoisPullbackElement tauK tauL hsquare sigma x) =
      sigma (tauL x)
def

galoisPullback_galoisPullback

L95 ↗
HilbertRamification.galoisPullback_galoisPullback
Documentation

The conjugation and base-change law: conjugation along a commutative square restricts to a homomorphism on Galois groups.

Source context 13 commands

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

noncomputable section
universe u v u' v'
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} {K' : Type u'} {L' : Type v'}
variable [Field K] [Field L] [Field K'] [Field L']
variable [Algebra K L] [Algebra K' L']
section GaloisPullback
variable (tauK : K →+* K') (tauL : L →+* L')
variable (hsquare : tauL.comp (algebraMap K L) =
  (algebraMap K' L').comp tauK)
variable [Normal K L]
include hsquare in
Lean source · full declaration
def galoisPullback_galoisPullback : (L' ≃ₐ[K'] L') →* (L ≃ₐ[K] L) where
  toFun := galoisPullbackElement tauK tauL hsquare
  map_one' := by
    ext x
    apply tauL.injective
    rw [galoisPullbackElement_commutes]
    simp
  map_mul' sigma rho := by
    ext x
    apply tauL.injective
    rw [galoisPullbackElement_commutes]
    change sigma (rho (tauL x)) =
      tauL (galoisPullbackElement tauK tauL hsquare sigma
        (galoisPullbackElement tauK tauL hsquare rho x))
    rw [galoisPullbackElement_commutes, galoisPullbackElement_commutes]
theorem

galoisPullback_galoisPullback_commutes

L112 ↗
HilbertRamification.galoisPullback_galoisPullback_commutes
Documentation

The defining equation tauL (tau^* sigma x) = sigma (tauL x).

Source context 12 commands

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

noncomputable section
universe u v u' v'
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} {K' : Type u'} {L' : Type v'}
variable [Field K] [Field L] [Field K'] [Field L']
variable [Algebra K L] [Algebra K' L']
section GaloisPullback
variable (tauK : K →+* K') (tauL : L →+* L')
variable (hsquare : tauL.comp (algebraMap K L) =
  (algebraMap K' L').comp tauK)
variable [Normal K L]
Lean source · statement
theorem galoisPullback_galoisPullback_commutes
    (sigma : L' ≃ₐ[K'] L') (x : L) :
    tauL (galoisPullback_galoisPullback tauK tauL hsquare sigma x) =
      sigma (tauL x)
def

galoisPullback_absoluteValueDecompositionGroupMap

L122 ↗
HilbertRamification.galoisPullback_absoluteValueDecompositionGroupMap
Documentation

The conjugation and base-change law, including the archimedean case: the pullback on Galois groups sends the decomposition group of w' to the decomposition group of the pulled-back absolute value.

Source context 13 commands

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

noncomputable section
universe u v u' v'
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} {K' : Type u'} {L' : Type v'}
variable [Field K] [Field L] [Field K'] [Field L']
variable [Algebra K L] [Algebra K' L']
section GaloisPullback
variable (tauK : K →+* K') (tauL : L →+* L')
variable (hsquare : tauL.comp (algebraMap K L) =
  (algebraMap K' L').comp tauK)
variable [Normal K L]
include hsquare in
Lean source · full declaration
def galoisPullback_absoluteValueDecompositionGroupMap (w' : AbsoluteValue L' ℝ) :
    absoluteValueDecompositionGroup K' w' →*
      absoluteValueDecompositionGroup K (w'.comp (f := tauL) tauL.injective) where
  toFun sigma :=
    ⟨galoisPullback_galoisPullback tauK tauL hsquare (sigma : L' ≃ₐ[K'] L'), by
      intro x
      change w' (tauL
          (galoisPullback_galoisPullback tauK tauL hsquare
            (sigma : L' ≃ₐ[K'] L') x)) < 1 ↔
        w' (tauL x) < 1
      rw [galoisPullback_galoisPullback_commutes]
      exact sigma.property (tauL x)⟩
  map_one' := by
    apply Subtype.ext
    exact map_one (galoisPullback_galoisPullback tauK tauL hsquare)
  map_mul' sigma rho := by
    apply Subtype.ext
    exact map_mul (galoisPullback_galoisPullback tauK tauL hsquare)
      (sigma : L' ≃ₐ[K'] L') (rho : L' ≃ₐ[K'] L')
abbrev

pulledValuationSubring

L148 ↗
HilbertRamification.ValuationSubring.pulledValuationSubring
Source context 15 commands

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

noncomputable section
universe u v u' v'
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} {K' : Type u'} {L' : Type v'}
variable [Field K] [Field L] [Field K'] [Field L']
variable [Algebra K L] [Algebra K' L']
section GaloisPullback
variable (tauK : K →+* K') (tauL : L →+* L')
variable (hsquare : tauL.comp (algebraMap K L) =
  (algebraMap K' L').comp tauK)
variable [Normal K L]
namespace ValuationSubring
open RamificationTheory.HilbertRamification.ValuationSubring
variable (A' : _root_.ValuationSubring L')
Lean source · statement
abbrev pulledValuationSubring : _root_.ValuationSubring L
theorem

mem_nonunits_pulled_iff

L151 ↗
HilbertRamification.ValuationSubring.mem_nonunits_pulled_iff
Source context 15 commands

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

noncomputable section
universe u v u' v'
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} {K' : Type u'} {L' : Type v'}
variable [Field K] [Field L] [Field K'] [Field L']
variable [Algebra K L] [Algebra K' L']
section GaloisPullback
variable (tauK : K →+* K') (tauL : L →+* L')
variable (hsquare : tauL.comp (algebraMap K L) =
  (algebraMap K' L').comp tauK)
variable [Normal K L]
namespace ValuationSubring
open RamificationTheory.HilbertRamification.ValuationSubring
variable (A' : _root_.ValuationSubring L')
Lean source · statement
theorem mem_nonunits_pulled_iff (x : L) :
    x ∈ (pulledValuationSubring tauL A').nonunits ↔
      tauL x ∈ A'.nonunits
theorem

units_map_mem_principalUnitGroup_iff

L166 ↗
HilbertRamification.ValuationSubring.units_map_mem_principalUnitGroup_iff
Source context 15 commands

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

noncomputable section
universe u v u' v'
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} {K' : Type u'} {L' : Type v'}
variable [Field K] [Field L] [Field K'] [Field L']
variable [Algebra K L] [Algebra K' L']
section GaloisPullback
variable (tauK : K →+* K') (tauL : L →+* L')
variable (hsquare : tauL.comp (algebraMap K L) =
  (algebraMap K' L').comp tauK)
variable [Normal K L]
namespace ValuationSubring
open RamificationTheory.HilbertRamification.ValuationSubring
variable (A' : _root_.ValuationSubring L')
Lean source · statement
theorem units_map_mem_principalUnitGroup_iff (x : Lˣ) :
    Units.map tauL x ∈ A'.principalUnitGroup ↔
      x ∈ (pulledValuationSubring tauL A').principalUnitGroup
theorem

mem_inertiaGroup_iff_sub_mem_nonunits

L179 ↗
HilbertRamification.ValuationSubring.mem_inertiaGroup_iff_sub_mem_nonunits
Source context 15 commands

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

noncomputable section
universe u v u' v'
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} {K' : Type u'} {L' : Type v'}
variable [Field K] [Field L] [Field K'] [Field L']
variable [Algebra K L] [Algebra K' L']
section GaloisPullback
variable (tauK : K →+* K') (tauL : L →+* L')
variable (hsquare : tauL.comp (algebraMap K L) =
  (algebraMap K' L').comp tauK)
variable [Normal K L]
namespace ValuationSubring
open RamificationTheory.HilbertRamification.ValuationSubring
variable (A' : _root_.ValuationSubring L')
Lean source · statement
theorem mem_inertiaGroup_iff_sub_mem_nonunits
    {F : Type*} {E : Type*} [Field F] [Field E] [Algebra F E]
    (A : _root_.ValuationSubring E) (sigma : decompositionGroup F A) :
    sigma ∈ inertiaGroup F A ↔
      ∀ x : A,
        ((sigma : E ≃ₐ[F] E) (x : E) - (x : E)) ∈ A.nonunits
def

galoisPullback_decompositionGroupMap

L212 ↗
HilbertRamification.ValuationSubring.galoisPullback_decompositionGroupMap
Documentation

The conjugation and base-change law in the valuation-subring model: decomposition groups map under pullback along the commutative square.

Source context 16 commands

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

noncomputable section
universe u v u' v'
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} {K' : Type u'} {L' : Type v'}
variable [Field K] [Field L] [Field K'] [Field L']
variable [Algebra K L] [Algebra K' L']
section GaloisPullback
variable (tauK : K →+* K') (tauL : L →+* L')
variable (hsquare : tauL.comp (algebraMap K L) =
  (algebraMap K' L').comp tauK)
variable [Normal K L]
namespace ValuationSubring
open RamificationTheory.HilbertRamification.ValuationSubring
variable (A' : _root_.ValuationSubring L')
include hsquare in
Lean source · full declaration
def galoisPullback_decompositionGroupMap :
    decompositionGroup K' A' →*
      decompositionGroup K (pulledValuationSubring tauL A') where
  toFun sigma :=
    ⟨galoisPullback_galoisPullback tauK tauL hsquare (sigma : L' ≃ₐ[K'] L'), by
      ext x
      rw [_root_.ValuationSubring.mem_pointwise_smul_iff_inv_smul_mem]
      change tauL
          ((galoisPullback_galoisPullback tauK tauL hsquare
            (sigma : L' ≃ₐ[K'] L'))⁻¹ x) ∈ A' ↔
        tauL x ∈ A'
      have hinv := galoisPullback_galoisPullback_commutes
        tauK tauL hsquare ((sigma : L' ≃ₐ[K'] L')⁻¹) x
      rw [← map_inv, hinv]
      have hsigma : (sigma : L' ≃ₐ[K'] L') • A' = A' := sigma.property
      have hmem :=
        congrArg (fun B : _root_.ValuationSubring L' => tauL x ∈ B) hsigma
      simp only [_root_.ValuationSubring.mem_pointwise_smul_iff_inv_smul_mem,
        AlgEquiv.smul_def] at hmem
      exact ⟨fun h => hmem.mp h, fun h => hmem.symm.mp h⟩⟩
  map_one' := by
    apply Subtype.ext
    exact map_one (galoisPullback_galoisPullback tauK tauL hsquare)
  map_mul' sigma rho := by
    apply Subtype.ext
    exact map_mul (galoisPullback_galoisPullback tauK tauL hsquare)
      (sigma : L' ≃ₐ[K'] L') (rho : L' ≃ₐ[K'] L')
theorem

decompositionGroupMap_commutes

L240 ↗
HilbertRamification.ValuationSubring.decompositionGroupMap_commutes
Source context 15 commands

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

noncomputable section
universe u v u' v'
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} {K' : Type u'} {L' : Type v'}
variable [Field K] [Field L] [Field K'] [Field L']
variable [Algebra K L] [Algebra K' L']
section GaloisPullback
variable (tauK : K →+* K') (tauL : L →+* L')
variable (hsquare : tauL.comp (algebraMap K L) =
  (algebraMap K' L').comp tauK)
variable [Normal K L]
namespace ValuationSubring
open RamificationTheory.HilbertRamification.ValuationSubring
variable (A' : _root_.ValuationSubring L')
Lean source · statement
theorem decompositionGroupMap_commutes
    (sigma : decompositionGroup K' A') (x : L) :
    tauL ((((galoisPullback_decompositionGroupMap tauK tauL hsquare A' sigma :
      decompositionGroup K (pulledValuationSubring tauL A')) :
        L ≃ₐ[K] L) x)) =
      (sigma : L' ≃ₐ[K'] L') (tauL x)
def

galoisPullback_inertiaGroupMap

L252 ↗
HilbertRamification.ValuationSubring.galoisPullback_inertiaGroupMap
Documentation

The conjugation and base-change law in the valuation-subring model: inertia groups map under pullback along the commutative square.

Source context 16 commands

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

noncomputable section
universe u v u' v'
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} {K' : Type u'} {L' : Type v'}
variable [Field K] [Field L] [Field K'] [Field L']
variable [Algebra K L] [Algebra K' L']
section GaloisPullback
variable (tauK : K →+* K') (tauL : L →+* L')
variable (hsquare : tauL.comp (algebraMap K L) =
  (algebraMap K' L').comp tauK)
variable [Normal K L]
namespace ValuationSubring
open RamificationTheory.HilbertRamification.ValuationSubring
variable (A' : _root_.ValuationSubring L')
include hsquare in
Lean source · full declaration
def galoisPullback_inertiaGroupMap :
    inertiaGroup K' A' →*
      inertiaGroup K (pulledValuationSubring tauL A') where
  toFun sigma := by
    let delta := galoisPullback_decompositionGroupMap tauK tauL hsquare A'
      (sigma : decompositionGroup K' A')
    refine ⟨delta, ?_⟩
    rw [mem_inertiaGroup_iff_sub_mem_nonunits]
    intro x
    rw [mem_nonunits_pulled_iff]
    rw [map_sub, decompositionGroupMap_commutes]
    exact (mem_inertiaGroup_iff_sub_mem_nonunits A'
      (sigma : decompositionGroup K' A')).mp sigma.property
      ⟨tauL (x : L), x.property⟩
  map_one' := by
    apply Subtype.ext
    exact map_one (galoisPullback_decompositionGroupMap tauK tauL hsquare A')
  map_mul' sigma rho := by
    apply Subtype.ext
    exact map_mul (galoisPullback_decompositionGroupMap tauK tauL hsquare A')
      (sigma : decompositionGroup K' A') (rho : decompositionGroup K' A')
theorem

inertiaGroupMap_commutes

L274 ↗
HilbertRamification.ValuationSubring.inertiaGroupMap_commutes
Source context 15 commands

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

noncomputable section
universe u v u' v'
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} {K' : Type u'} {L' : Type v'}
variable [Field K] [Field L] [Field K'] [Field L']
variable [Algebra K L] [Algebra K' L']
section GaloisPullback
variable (tauK : K →+* K') (tauL : L →+* L')
variable (hsquare : tauL.comp (algebraMap K L) =
  (algebraMap K' L').comp tauK)
variable [Normal K L]
namespace ValuationSubring
open RamificationTheory.HilbertRamification.ValuationSubring
variable (A' : _root_.ValuationSubring L')
Lean source · statement
theorem inertiaGroupMap_commutes
    (sigma : inertiaGroup K' A') (x : L) :
    tauL (((((galoisPullback_inertiaGroupMap tauK tauL hsquare A' sigma :
      inertiaGroup K (pulledValuationSubring tauL A')) :
        decompositionGroup K (pulledValuationSubring tauL A')) :
          L ≃ₐ[K] L) x)) =
      (((sigma : inertiaGroup K' A') : decompositionGroup K' A') :
        L' ≃ₐ[K'] L') (tauL x)
theorem

automorphismUnitQuotient_map

L286 ↗
HilbertRamification.ValuationSubring.automorphismUnitQuotient_map
Source context 15 commands

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

noncomputable section
universe u v u' v'
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} {K' : Type u'} {L' : Type v'}
variable [Field K] [Field L] [Field K'] [Field L']
variable [Algebra K L] [Algebra K' L']
section GaloisPullback
variable (tauK : K →+* K') (tauL : L →+* L')
variable (hsquare : tauL.comp (algebraMap K L) =
  (algebraMap K' L').comp tauK)
variable [Normal K L]
namespace ValuationSubring
open RamificationTheory.HilbertRamification.ValuationSubring
variable (A' : _root_.ValuationSubring L')
Lean source · statement
theorem automorphismUnitQuotient_map
    (sigma : inertiaGroup K' A') (x : Lˣ) :
    Units.map tauL
        (automorphismUnitQuotient K (pulledValuationSubring tauL A')
          ((galoisPullback_inertiaGroupMap tauK tauL hsquare A' sigma :
            inertiaGroup K (pulledValuationSubring tauL A')) :
              decompositionGroup K (pulledValuationSubring tauL A')) x) =
      automorphismUnitQuotient K' A'
        (sigma : decompositionGroup K' A') (Units.map tauL x)
theorem

ramificationPredicate_map

L298 ↗
HilbertRamification.ValuationSubring.ramificationPredicate_map
Source context 15 commands

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

noncomputable section
universe u v u' v'
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} {K' : Type u'} {L' : Type v'}
variable [Field K] [Field L] [Field K'] [Field L']
variable [Algebra K L] [Algebra K' L']
section GaloisPullback
variable (tauK : K →+* K') (tauL : L →+* L')
variable (hsquare : tauL.comp (algebraMap K L) =
  (algebraMap K' L').comp tauK)
variable [Normal K L]
namespace ValuationSubring
open RamificationTheory.HilbertRamification.ValuationSubring
variable (A' : _root_.ValuationSubring L')
Lean source · statement
theorem ramificationPredicate_map
    (sigma : inertiaGroup K' A')
    (hsigma : ∀ y : L'ˣ,
      automorphismUnitQuotient K' A' (sigma : decompositionGroup K' A') y ∈
        A'.principalUnitGroup) :
    ∀ x : Lˣ,
    automorphismUnitQuotient K (pulledValuationSubring tauL A')
        ((galoisPullback_inertiaGroupMap tauK tauL hsquare A' sigma :
          inertiaGroup K (pulledValuationSubring tauL A')) :
            decompositionGroup K (pulledValuationSubring tauL A')) x ∈
      (pulledValuationSubring tauL A').principalUnitGroup
def

galoisPullback_ramificationGroupMap

L318 ↗
HilbertRamification.ValuationSubring.galoisPullback_ramificationGroupMap
Documentation

The conjugation and base-change law in the valuation-subring model: ramification groups map under pullback along the commutative square.

Source context 16 commands

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

noncomputable section
universe u v u' v'
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open scoped Pointwise
variable {K : Type u} {L : Type v} {K' : Type u'} {L' : Type v'}
variable [Field K] [Field L] [Field K'] [Field L']
variable [Algebra K L] [Algebra K' L']
section GaloisPullback
variable (tauK : K →+* K') (tauL : L →+* L')
variable (hsquare : tauL.comp (algebraMap K L) =
  (algebraMap K' L').comp tauK)
variable [Normal K L]
namespace ValuationSubring
open RamificationTheory.HilbertRamification.ValuationSubring
variable (A' : _root_.ValuationSubring L')
include hsquare in
Lean source · statement
def galoisPullback_ramificationGroupMap :
    ramificationGroup K' A' →*
      ramificationGroup K (pulledValuationSubring tauL A')

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