Module

DecompositionGroup.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.DecompositionGroup

9 declarations indexed from sourceView source ↗

Module documentation

Decomposition-group restriction law

This file gives the three tower-intersection formulas in their common ambient Galois group. The decomposition-group statement is formulated for arbitrary absolute values, including the archimedean case. The inertia and ramification statements use valuation subrings and therefore cover the nonarchimedean case in which those groups are defined.

Imports2

Imported by8

def

absoluteValueDecompositionGroup

L35 ↗

HilbertRamification.absoluteValueDecompositionGroup

Documentation

The decomposition group of an absolute-value class. Membership says that pullback by the automorphism preserves the strict unit ball, equivalently the valuation class, rather than requiring equality of chosen absolute-value representatives.

Source context 6 commands

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

noncomputable section
universe u v w
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open RamificationTheory.HilbertRamification.ValuationSubring
variable (K : Type u) {L : Type w} [Field K] [Field L] [Algebra K L]

Lean source · full declaration

def absoluteValueDecompositionGroup (w : AbsoluteValue L ℝ) :
    Subgroup (L ≃ₐ[K] L) where
  carrier := { σ | ∀ x : L, w (σ x) < 1 ↔ w x < 1 }
  one_mem' := by
    intro x
    rfl
  mul_mem' := by
    intro σ τ hσ hτ x
    exact (hσ (τ x)).trans (hτ x)
  inv_mem' := by
    intro σ hσ x
    have h := hσ (σ⁻¹ x)
    simpa using h.symm

theorem

mem_absoluteValueDecompositionGroup_iff

L49 ↗

HilbertRamification.mem_absoluteValueDecompositionGroup_iff

Source context 6 commands

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

noncomputable section
universe u v w
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open RamificationTheory.HilbertRamification.ValuationSubring
variable (K : Type u) {L : Type w} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem mem_absoluteValueDecompositionGroup_iff
    (w : AbsoluteValue L ℝ) (σ : L ≃ₐ[K] L) :
    σ ∈ absoluteValueDecompositionGroup K w ↔
      ∀ x : L, w (σ x) < 1 ↔ w x < 1

theorem

mem_absoluteValueDecompositionGroup_iff_equivalent

L57 ↗

HilbertRamification.mem_absoluteValueDecompositionGroup_iff_equivalent

Documentation

Membership really is preservation of the absolute-value class: the pullback absolute value is equivalent to the chosen representative.

Source context 6 commands

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

noncomputable section
universe u v w
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open RamificationTheory.HilbertRamification.ValuationSubring
variable (K : Type u) {L : Type w} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem mem_absoluteValueDecompositionGroup_iff_equivalent
    (w : AbsoluteValue L ℝ) (σ : L ≃ₐ[K] L) :
    σ ∈ absoluteValueDecompositionGroup K w ↔
      LubinTate.Valuations.EquivalentAbsoluteValues
        (w.comp (f := σ.toRingEquiv.toRingHom) σ.injective) w

theorem

mem_absoluteValueDecompositionGroup_iff_extensionConjugate_eq

L69 ↗

HilbertRamification.mem_absoluteValueDecompositionGroup_iff_extensionConjugate_eq

Documentation

The decomposition and inertia definition: on the normalized extension type, the decomposition group is exactly the stabilizer of the chosen extension under w ↦ w ∘ σ.

Source context 6 commands

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

noncomputable section
universe u v w
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open RamificationTheory.HilbertRamification.ValuationSubring
variable (K : Type u) {L : Type w} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem mem_absoluteValueDecompositionGroup_iff_extensionConjugate_eq
    {K₀ : Type u} {L₀ : Type w} [Field K₀] [Field L₀] [Algebra K₀ L₀]
    (vK : AbsoluteValue K₀ ℝ) (hvK : vK.IsNontrivial)
    (vL : AbsoluteValueExtension vK L₀) (σ : L₀ ≃ₐ[K₀] L₀) :
    σ ∈ absoluteValueDecompositionGroup K₀ vL.1 ↔
      absoluteValueExtensionConjugate vK vL σ = vL

theorem

decompositionGroupRestriction_restrictAutomorphismScalars_injective

L93 ↗

HilbertRamification.decompositionGroupRestriction_restrictAutomorphismScalars_injective

Documentation

The scalar-restriction map in the decomposition-group restriction law is the canonical inclusion G(L/M) → G(L/K).

Source context 8 commands

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

noncomputable section
universe u v w
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open RamificationTheory.HilbertRamification.ValuationSubring
variable (K : Type u) {L : Type w} [Field K] [Field L] [Algebra K L]
section IntermediateField
variable {M : Type v} [Field M] [Algebra K M] [Algebra M L]
  [IsScalarTower K M L]

Lean source · statement

theorem decompositionGroupRestriction_restrictAutomorphismScalars_injective :
    Function.Injective
      (RamificationTheory.HilbertRamification.ValuationSubring.restrictAutomorphismScalars
        (K := K) (M := M) (L := L))

theorem

decompositionGroupRestriction_mem_absoluteValueDecompositionGroup_restrictScalars_iff

L103 ↗

HilbertRamification.decompositionGroupRestriction_mem_absoluteValueDecompositionGroup_restrictScalars_iff

Documentation

The decomposition-group restriction law, decomposition-group membership form: scalar restriction does not change the action on the chosen valuation of L.

Source context 8 commands

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

noncomputable section
universe u v w
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open RamificationTheory.HilbertRamification.ValuationSubring
variable (K : Type u) {L : Type w} [Field K] [Field L] [Algebra K L]
section IntermediateField
variable {M : Type v} [Field M] [Algebra K M] [Algebra M L]
  [IsScalarTower K M L]

Lean source · statement

theorem decompositionGroupRestriction_mem_absoluteValueDecompositionGroup_restrictScalars_iff
    (w : AbsoluteValue L ℝ) (σ : L ≃ₐ[M] L) :
    RamificationTheory.HilbertRamification.ValuationSubring.restrictAutomorphismScalars (K := K) (M
      := M) σ ∈
        absoluteValueDecompositionGroup K w ↔
      σ ∈ absoluteValueDecompositionGroup M w

theorem

decompositionGroupRestriction_absoluteValueDecompositionGroup_range_eq_inf

L114 ↗

HilbertRamification.decompositionGroupRestriction_absoluteValueDecompositionGroup_range_eq_inf

Documentation

The decomposition-group restriction law, including the archimedean case: inside G(L/K), the decomposition group over M is G_w(L/K) ∩ G(L/M).

Source context 8 commands

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

noncomputable section
universe u v w
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open RamificationTheory.HilbertRamification.ValuationSubring
variable (K : Type u) {L : Type w} [Field K] [Field L] [Algebra K L]
section IntermediateField
variable {M : Type v} [Field M] [Algebra K M] [Algebra M L]
  [IsScalarTower K M L]

Lean source · statement

theorem decompositionGroupRestriction_absoluteValueDecompositionGroup_range_eq_inf
    (w : AbsoluteValue L ℝ) :
    Subgroup.map
        (RamificationTheory.HilbertRamification.ValuationSubring.restrictAutomorphismScalars (K :=
          K) (M := M))
        (absoluteValueDecompositionGroup M w) =
      absoluteValueDecompositionGroup K w ⊓
        (RamificationTheory.HilbertRamification.ValuationSubring.restrictAutomorphismScalars
          (K := K) (M := M)).range

theorem

decompositionGroupRestriction_inertiaGroupInAut_range_eq_inf

L148 ↗

HilbertRamification.ValuationSubring.decompositionGroupRestriction_inertiaGroupInAut_range_eq_inf

Documentation

The decomposition-group restriction law, ambient-automorphism form: inside G(L/K), one has I_w(L/M) = I_w(L/K) ∩ G(L/M).

Source context 9 commands

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

noncomputable section
universe u v w
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open RamificationTheory.HilbertRamification.ValuationSubring
variable (K : Type u) {L : Type w} [Field K] [Field L] [Algebra K L]
namespace ValuationSubring
section NonarchimedeanIntermediateField
variable {M : Type v} [Field M] [Algebra K M] [Algebra M L]
  [IsScalarTower K M L]

Lean source · statement

theorem decompositionGroupRestriction_inertiaGroupInAut_range_eq_inf
    (A : _root_.ValuationSubring L) :
    Subgroup.map (restrictAutomorphismScalars (K := K) (M := M))
        (inertiaGroupInAut M A) =
      inertiaGroupInAut K A ⊓
        (restrictAutomorphismScalars (K := K) (M := M)).range

theorem

decompositionGroupRestriction_ramificationGroupInAut_range_eq_inf

L181 ↗

HilbertRamification.ValuationSubring.decompositionGroupRestriction_ramificationGroupInAut_range_eq_inf

Documentation

The decomposition-group restriction law, ambient-automorphism form: inside G(L/K), one has R_w(L/M) = R_w(L/K) ∩ G(L/M).

Source context 9 commands

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

noncomputable section
universe u v w
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
open RamificationTheory.HilbertRamification.ValuationSubring
variable (K : Type u) {L : Type w} [Field K] [Field L] [Algebra K L]
namespace ValuationSubring
section NonarchimedeanIntermediateField
variable {M : Type v} [Field M] [Algebra K M] [Algebra M L]
  [IsScalarTower K M L]

Lean source · statement

theorem decompositionGroupRestriction_ramificationGroupInAut_range_eq_inf
    (A : _root_.ValuationSubring L) :
    Subgroup.map (restrictAutomorphismScalars (K := K) (M := M))
        (ramificationGroupInAut M A) =
      ramificationGroupInAut K A ⊓
        (restrictAutomorphismScalars (K := K) (M := M)).range

Module documentation

Decomposition-group restriction law

Declarations