Module

Ramification.lean

Nyll.ValuedFieldTheory.Ramification.GaloisValuation.Ramification

167 declarations indexed from sourceView source ↗

Module documentation

Ramification filtrations

This file provides the group-theoretic lower ramification APIs used by local CFT. Concrete valued extensions supply the action quotient estimates; the subgroup and normality/antitonicity consequences are proved here.

Imports4

Mathlib.SetTheory.Cardinal.Finite
Nyll.ValuedFieldTheory.Ramification.GaloisValuation.RamificationQuotients
Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnits.Core
Mathlib.Data.Rat.Lemmas

Imported by4

def

herbrandStep

L41 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandStep

Documentation

The finite-level Herbrand step |G_i| / |G_0|, written with Nat.card so it can be used before a global fintype instance has been installed. Positivity theorems below carry the finite-level hypotheses needed to rule out the infinite-cardinality fallback of Nat.card.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

def herbrandStep (i : Nat) : Rat

def

herbrandFunctionNat

L46 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandFunctionNat

Documentation

The natural-index lower Herbrand function as the cumulative sum of the finite-level steps through 0, ..., n - 1.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

def herbrandFunctionNat (n : Nat) : Rat

theorem

herbrandFunctionNat_zero

L50 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandFunctionNat_zero

Documentation

States the theorem herbrandFunctionNat_zero.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem herbrandFunctionNat_zero :
    F.herbrandFunctionNat 0 = 0

theorem

herbrandFunctionNat_succ

L55 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandFunctionNat_succ

Documentation

States the theorem herbrandFunctionNat_succ.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem herbrandFunctionNat_succ (n : Nat) :
    F.herbrandFunctionNat (n + 1) =
      F.herbrandFunctionNat n + F.herbrandStep n

theorem

herbrandStep_nonneg

L61 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandStep_nonneg

Documentation

States the theorem herbrandStep_nonneg.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem herbrandStep_nonneg (i : Nat) :
    0 <= F.herbrandStep i

theorem

herbrandStep_pos

L66 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandStep_pos

Documentation

States the theorem herbrandStep_pos.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem herbrandStep_pos (i : Nat)
    [Finite (F.lower i)] [Finite (F.lower 0)] :
    0 < F.herbrandStep i

theorem

herbrandFunctionNat_mono

L77 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandFunctionNat_mono

Documentation

States the theorem herbrandFunctionNat_mono.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem herbrandFunctionNat_mono :
    Monotone F.herbrandFunctionNat

theorem

gradedPieceMk_eq_iff_inv_mul_mem

L89 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.gradedPieceMk_eq_iff_inv_mul_mem

Documentation

Representative equality criterion in the graded piece G_n/G_{n+1}, in left-quotient form.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem gradedPieceMk_eq_iff_inv_mul_mem (n : ℕ) (σ τ : F.lower n) :
    F.gradedPieceMk n σ = F.gradedPieceMk n τ ↔
      ((τ⁻¹ * σ : F.lower n) : G) ∈ F.lower (n + 1)

theorem

tameQuotientMk_eq_iff_inv_mul_mem

L100 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.tameQuotientMk_eq_iff_inv_mul_mem

Documentation

Representative equality criterion in the tame quotient G_0/G_1, in left-quotient form.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem tameQuotientMk_eq_iff_inv_mul_mem (σ τ : F.inertiaSubgroup) :
    F.tameQuotientMk σ = F.tameQuotientMk τ ↔
      ((τ⁻¹ * σ : F.inertiaSubgroup) : G) ∈ F.wildInertiaSubgroup

def

quotientMapOfLe

L110 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMapOfLe

Documentation

The natural quotient map G/G_n → G/G_m for m ≤ n.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

def quotientMapOfLe {m n : ℕ} (hmn : m ≤ n) :
    F.quotient n →* F.quotient m

theorem

quotientMapOfLe_apply_mk

L117 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMapOfLe_apply_mk

Documentation

States the theorem quotientMapOfLe_apply_mk.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientMapOfLe_apply_mk {m n : ℕ} (hmn : m ≤ n)
    (σ : G) :
    F.quotientMapOfLe hmn (F.quotientMk n σ) =
      F.quotientMk m σ

theorem

quotientMapOfLe_comp

L124 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMapOfLe_comp

Documentation

Level-change quotient maps compose transitively.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientMapOfLe_comp {l m n : ℕ}
    (hlm : l ≤ m) (hmn : m ≤ n) :
    (F.quotientMapOfLe hlm).comp (F.quotientMapOfLe hmn) =
      F.quotientMapOfLe (le_trans hlm hmn)

theorem

quotientMapOfLe_refl

L142 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMapOfLe_refl

Documentation

The level-change quotient map for n ≤ n is the identity.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientMapOfLe_refl (n : ℕ) :
    F.quotientMapOfLe (le_rfl : n ≤ n) = MonoidHom.id (F.quotient n)

def

quotientKernelOfLe

L157 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientKernelOfLe

Documentation

The subgroup of G/G_n represented by the coarser ramification group G_m, for m ≤ n.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

def quotientKernelOfLe {m n : ℕ} (_hmn : m ≤ n) :
    Subgroup (F.quotient n)

def

levelSubgroupToQuotient

L162 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.levelSubgroupToQuotient

Documentation

The map from the mth lower ramification group into G/G_n.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

def levelSubgroupToQuotient {m n : ℕ} (_hmn : m ≤ n) :
    F.lower m →* F.quotient n

theorem

levelSubgroupToQuotient_apply

L167 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.levelSubgroupToQuotient_apply

Documentation

States the theorem levelSubgroupToQuotient_apply.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem levelSubgroupToQuotient_apply {m n : ℕ} (hmn : m ≤ n)
    (σ : F.lower m) :
    F.levelSubgroupToQuotient hmn σ =
      F.quotientMk n (σ : G)

theorem

levelSubgroupToQuotient_ker_eq

L174 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.levelSubgroupToQuotient_ker_eq

Documentation

The kernel of G_m → G/G_n is G_n inside G_m.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem levelSubgroupToQuotient_ker_eq {m n : ℕ} (hmn : m ≤ n) :
    (F.levelSubgroupToQuotient hmn).ker =
      (F.lower n).subgroupOf (F.lower m)

theorem

levelSubgroupToQuotient_range_eq_quotientKernelOfLe

L183 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.levelSubgroupToQuotient_range_eq_quotientKernelOfLe

Documentation

The range of G_m → G/G_n is the kernel subgroup of G/G_n → G/G_m.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem levelSubgroupToQuotient_range_eq_quotientKernelOfLe {m n : ℕ}
    (hmn : m ≤ n) :
    (F.levelSubgroupToQuotient hmn).range = F.quotientKernelOfLe hmn

theorem

quotientMapOfLe_ker_eq_quotientKernelOfLe

L205 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMapOfLe_ker_eq_quotientKernelOfLe

Documentation

The kernel of G/G_n → G/G_m is the image of G_m in G/G_n.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientMapOfLe_ker_eq_quotientKernelOfLe {m n : ℕ}
    (hmn : m ≤ n) :
    (F.quotientMapOfLe hmn).ker = F.quotientKernelOfLe hmn

instance

quotientKernelOfLe_normal

L211 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientKernelOfLe_normal

Documentation

The named kernel subgroup G_m/G_n is normal in G/G_n.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

instance quotientKernelOfLe_normal {m n : ℕ} (hmn : m ≤ n) :
    (F.quotientKernelOfLe hmn).Normal

theorem

quotientMapOfLe_mk_eq_one_iff

L217 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMapOfLe_mk_eq_one_iff

Documentation

Representative kernel criterion for G/G_n → G/G_m.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientMapOfLe_mk_eq_one_iff {m n : ℕ} (hmn : m ≤ n)
    (σ : G) :
    F.quotientMapOfLe hmn (F.quotientMk n σ) = 1 ↔
      σ ∈ F.lower m

theorem

quotientMapOfLe_mk_mem_ker_iff

L224 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMapOfLe_mk_mem_ker_iff

Documentation

Representative membership criterion for the kernel of G/G_n → G/G_m.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientMapOfLe_mk_mem_ker_iff {m n : ℕ} (hmn : m ≤ n)
    (σ : G) :
    F.quotientMk n σ ∈ (F.quotientMapOfLe hmn).ker ↔
      σ ∈ F.lower m

theorem

quotientMapOfLe_mk_eq_iff_div_mem

L231 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMapOfLe_mk_eq_iff_div_mem

Documentation

Equality after changing level, in right-quotient form.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientMapOfLe_mk_eq_iff_div_mem {m n : ℕ} (hmn : m ≤ n)
    (σ τ : G) :
    F.quotientMapOfLe hmn (F.quotientMk n σ) =
        F.quotientMapOfLe hmn (F.quotientMk n τ) ↔
      σ / τ ∈ F.lower m

theorem

quotientMapOfLe_mk_eq_iff_inv_mul_mem

L240 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMapOfLe_mk_eq_iff_inv_mul_mem

Documentation

Equality after changing level, in left-quotient form.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientMapOfLe_mk_eq_iff_inv_mul_mem {m n : ℕ} (hmn : m ≤ n)
    (σ τ : G) :
    F.quotientMapOfLe hmn (F.quotientMk n σ) =
        F.quotientMapOfLe hmn (F.quotientMk n τ) ↔
      τ⁻¹ * σ ∈ F.lower m

theorem

quotientMapOfLe_eq_one_iff_exists_mem_repr

L251 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMapOfLe_eq_one_iff_exists_mem_repr

Documentation

Arbitrary class kernel criterion for G/G_n → G/G_m.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientMapOfLe_eq_one_iff_exists_mem_repr {m n : ℕ}
    (hmn : m ≤ n) (q : F.quotient n) :
    F.quotientMapOfLe hmn q = 1 ↔
      ∃ σ : G, σ ∈ F.lower m ∧
        F.quotientMk n σ = q

theorem

quotientMapOfLe_mem_ker_iff_exists_mem_repr

L267 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMapOfLe_mem_ker_iff_exists_mem_repr

Documentation

Kernel-membership criterion for an arbitrary class in G/G_n → G/G_m, expanded by a representative from G_m.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientMapOfLe_mem_ker_iff_exists_mem_repr {m n : ℕ}
    (hmn : m ≤ n) (q : F.quotient n) :
    q ∈ (F.quotientMapOfLe hmn).ker ↔
      ∃ σ : G, σ ∈ F.lower m ∧
        F.quotientMk n σ = q

theorem

mem_quotientKernelOfLe_iff_exists_mem_repr

L277 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.mem_quotientKernelOfLe_iff_exists_mem_repr

Documentation

Membership in the named kernel subgroup of G/G_n → G/G_m, expanded by a representative from G_m.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem mem_quotientKernelOfLe_iff_exists_mem_repr {m n : ℕ}
    (hmn : m ≤ n) (q : F.quotient n) :
    q ∈ F.quotientKernelOfLe hmn ↔
      ∃ σ : G, σ ∈ F.lower m ∧
        F.quotientMk n σ = q

theorem

mem_quotientKernelOfLe_iff_quotientMap_eq_one

L287 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.mem_quotientKernelOfLe_iff_quotientMap_eq_one

Documentation

Membership in the named kernel subgroup is the same as mapping to 1 under the corresponding level-change map.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem mem_quotientKernelOfLe_iff_quotientMap_eq_one {m n : ℕ}
    (hmn : m ≤ n) (q : F.quotient n) :
    q ∈ F.quotientKernelOfLe hmn ↔
      F.quotientMapOfLe hmn q = 1

theorem

quotientKernelOfLe_le

L296 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientKernelOfLe_le

Documentation

Kernel subgroups are nested as the target quotient is coarsened: G_m/G_n is contained in G_l/G_n for l ≤ m ≤ n.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientKernelOfLe_le {l m n : ℕ}
    (hlm : l ≤ m) (hmn : m ≤ n) :
    F.quotientKernelOfLe hmn ≤
      F.quotientKernelOfLe (le_trans hlm hmn)

theorem

quotientMapOfLe_mem_quotientKernelOfLe_iff

L308 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMapOfLe_mem_quotientKernelOfLe_iff

Documentation

Membership in the coarser kernel after applying a level-change map is equivalent to membership in the corresponding direct kernel.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientMapOfLe_mem_quotientKernelOfLe_iff {l m n : ℕ}
    (hlm : l ≤ m) (hmn : m ≤ n) (q : F.quotient n) :
    F.quotientMapOfLe hmn q ∈ F.quotientKernelOfLe hlm ↔
      q ∈ F.quotientKernelOfLe (le_trans hlm hmn)

theorem

quotientMapOfLe_comap_quotientKernelOfLe_eq

L320 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMapOfLe_comap_quotientKernelOfLe_eq

Documentation

The preimage of the coarser kernel subgroup under a level-change map is the corresponding direct kernel subgroup.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientMapOfLe_comap_quotientKernelOfLe_eq {l m n : ℕ}
    (hlm : l ≤ m) (hmn : m ≤ n) :
    Subgroup.comap (F.quotientMapOfLe hmn) (F.quotientKernelOfLe hlm) =
      F.quotientKernelOfLe (le_trans hlm hmn)

theorem

quotientMapOfLe_mk_mem_quotientKernelOfLe_iff

L329 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMapOfLe_mk_mem_quotientKernelOfLe_iff

Documentation

Representative version of quotientMapOfLe_mem_quotientKernelOfLe_iff.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientMapOfLe_mk_mem_quotientKernelOfLe_iff {l m n : ℕ}
    (hlm : l ≤ m) (hmn : m ≤ n) (σ : G) :
    F.quotientMapOfLe hmn (F.quotientMk n σ) ∈
        F.quotientKernelOfLe hlm ↔
      σ ∈ F.lower l

theorem

quotientMapOfLe_eq_iff_div_mem_ker

L339 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMapOfLe_eq_iff_div_mem_ker

Documentation

Equality after changing level is kernel membership of the quotient q / r.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientMapOfLe_eq_iff_div_mem_ker {m n : ℕ} (hmn : m ≤ n)
    (q r : F.quotient n) :
    F.quotientMapOfLe hmn q = F.quotientMapOfLe hmn r ↔
      q / r ∈ (F.quotientMapOfLe hmn).ker

theorem

quotientMapOfLe_eq_iff_div_mem_quotientKernelOfLe

L353 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMapOfLe_eq_iff_div_mem_quotientKernelOfLe

Documentation

Equality after changing level is membership of q / r in the named kernel subgroup of G/G_n → G/G_m.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientMapOfLe_eq_iff_div_mem_quotientKernelOfLe {m n : ℕ}
    (hmn : m ≤ n) (q r : F.quotient n) :
    F.quotientMapOfLe hmn q = F.quotientMapOfLe hmn r ↔
      q / r ∈ F.quotientKernelOfLe hmn

theorem

quotientMapOfLe_map_quotientKernelOfLe_eq

L362 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMapOfLe_map_quotientKernelOfLe_eq

Documentation

Level-change maps send the larger kernel subgroup G_l/G_n onto the corresponding kernel subgroup G_l/G_m, for l ≤ m ≤ n.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientMapOfLe_map_quotientKernelOfLe_eq {l m n : ℕ}
    (hlm : l ≤ m) (hmn : m ≤ n) :
    Subgroup.map (F.quotientMapOfLe hmn)
        (F.quotientKernelOfLe (le_trans hlm hmn)) =
      F.quotientKernelOfLe hlm

theorem

quotientMapOfLe_map_quotientKernelOfLe_eq_bot

L389 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMapOfLe_map_quotientKernelOfLe_eq_bot

Documentation

A level-change map kills exactly the kernel subgroup it is named by.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientMapOfLe_map_quotientKernelOfLe_eq_bot {m n : ℕ}
    (hmn : m ≤ n) :
    Subgroup.map (F.quotientMapOfLe hmn) (F.quotientKernelOfLe hmn) = ⊥

def

quotientKernelMapOfLe

L407 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientKernelMapOfLe

Documentation

The level-change map restricted to kernel subgroups: G_l/G_n → G_l/G_m, for l ≤ m ≤ n.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

def quotientKernelMapOfLe {l m n : ℕ} (hlm : l ≤ m) (hmn : m ≤ n) :
    F.quotientKernelOfLe (le_trans hlm hmn) →*
      F.quotientKernelOfLe hlm

theorem

quotientKernelMapOfLe_apply

L419 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientKernelMapOfLe_apply

Documentation

States the theorem quotientKernelMapOfLe_apply.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientKernelMapOfLe_apply {l m n : ℕ}
    (hlm : l ≤ m) (hmn : m ≤ n)
    (q : F.quotientKernelOfLe (le_trans hlm hmn)) :
    ((F.quotientKernelMapOfLe hlm hmn q :
      F.quotientKernelOfLe hlm) : F.quotient m) =
      F.quotientMapOfLe hmn (q : F.quotient n)

theorem

quotientKernelMapOfLe_refl

L429 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientKernelMapOfLe_refl

Documentation

Restricted level-change maps on ramification kernels are identities at a fixed quotient level.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientKernelMapOfLe_refl {l m : ℕ} (hlm : l ≤ m) :
    F.quotientKernelMapOfLe hlm (le_rfl : m ≤ m) =
      MonoidHom.id (F.quotientKernelOfLe hlm)

theorem

quotientKernelMapOfLe_comp

L442 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientKernelMapOfLe_comp

Documentation

Restricted level-change maps on ramification kernels compose transitively.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientKernelMapOfLe_comp {k l m n : ℕ}
    (hkl : k ≤ l) (hlm : l ≤ m) (hmn : m ≤ n) :
    (F.quotientKernelMapOfLe hkl hlm).comp
        (F.quotientKernelMapOfLe (le_trans hkl hlm) hmn) =
      F.quotientKernelMapOfLe hkl (le_trans hlm hmn)

theorem

quotientKernelMapOfLe_ker_eq

L459 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientKernelMapOfLe_ker_eq

Documentation

The restricted map G_l/G_n → G_l/G_m has kernel G_m/G_n.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientKernelMapOfLe_ker_eq {l m n : ℕ}
    (hlm : l ≤ m) (hmn : m ≤ n) :
    (F.quotientKernelMapOfLe hlm hmn).ker =
      (F.quotientKernelOfLe hmn).subgroupOf
        (F.quotientKernelOfLe (le_trans hlm hmn))

theorem

quotientKernelMapOfLe_surjective

L479 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientKernelMapOfLe_surjective

Documentation

The restricted map G_l/G_n → G_l/G_m is surjective.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientKernelMapOfLe_surjective {l m n : ℕ}
    (hlm : l ≤ m) (hmn : m ≤ n) :
    Function.Surjective (F.quotientKernelMapOfLe hlm hmn)

def

quotientKernelQuotientKerEquivQuotientKernelOfLe

L498 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientKernelQuotientKerEquivQuotientKernelOfLe

Documentation

First isomorphism theorem inside ramification kernels: (G_l/G_n)/ker(G_l/G_n → G_l/G_m) ≃ G_l/G_m, for l ≤ m ≤ n. The kernel is identified with G_m/G_n by quotientKernelMapOfLe_ker_eq.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

def quotientKernelQuotientKerEquivQuotientKernelOfLe {l m n : ℕ}
    (hlm : l ≤ m) (hmn : m ≤ n) :
    F.quotientKernelOfLe (le_trans hlm hmn) ⧸
        (F.quotientKernelMapOfLe hlm hmn).ker ≃*
      F.quotientKernelOfLe hlm

theorem

quotientKernelQuotientKerEquivQuotientKernelOfLe_mk'

L508 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientKernelQuotientKerEquivQuotientKernelOfLe_mk'

Documentation

States the theorem quotientKernelQuotientKerEquivQuotientKernelOfLe_mk'.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientKernelQuotientKerEquivQuotientKernelOfLe_mk'
    {l m n : ℕ} (hlm : l ≤ m) (hmn : m ≤ n)
    (q : F.quotientKernelOfLe (le_trans hlm hmn)) :
    F.quotientKernelQuotientKerEquivQuotientKernelOfLe hlm hmn
        (QuotientGroup.mk'
          (F.quotientKernelMapOfLe hlm hmn).ker q) =
      F.quotientKernelMapOfLe hlm hmn q

def

quotientKernelQuotientSubgroupOfEquivQuotientKernelOfLe

L519 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientKernelQuotientSubgroupOfEquivQuotientKernelOfLe

Documentation

Second-isomorphism-style form of the ramification-kernel quotient: (G_l/G_n)/(G_m/G_n) ≃ G_l/G_m, for l ≤ m ≤ n.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

def quotientKernelQuotientSubgroupOfEquivQuotientKernelOfLe {l m n : ℕ}
    (hlm : l ≤ m) (hmn : m ≤ n) :
    F.quotientKernelOfLe (le_trans hlm hmn) ⧸
        (F.quotientKernelOfLe hmn).subgroupOf
          (F.quotientKernelOfLe (le_trans hlm hmn)) ≃*
      F.quotientKernelOfLe hlm

theorem

quotientKernelQuotientSubgroupOfEquivQuotientKernelOfLe_mk'

L530 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientKernelQuotientSubgroupOfEquivQuotientKernelOfLe_mk'

Documentation

States the theorem quotientKernelQuotientSubgroupOfEquivQuotientKernelOfLe_mk'.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientKernelQuotientSubgroupOfEquivQuotientKernelOfLe_mk'
    {l m n : ℕ} (hlm : l ≤ m) (hmn : m ≤ n)
    (q : F.quotientKernelOfLe (le_trans hlm hmn)) :
    F.quotientKernelQuotientSubgroupOfEquivQuotientKernelOfLe hlm hmn
        (QuotientGroup.mk'
          ((F.quotientKernelOfLe hmn).subgroupOf
            (F.quotientKernelOfLe (le_trans hlm hmn))) q) =
      F.quotientKernelMapOfLe hlm hmn q

theorem

card_quotientKernelQuotientSubgroupOfLe

L543 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.card_quotientKernelQuotientSubgroupOfLe

Documentation

Cardinality form of the second-isomorphism quotient compatibility (G_l/G_n)/(G_m/G_n) ≃ G_l/G_m.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem card_quotientKernelQuotientSubgroupOfLe {l m n : ℕ}
    (hlm : l ≤ m) (hmn : m ≤ n) [Finite G] :
    Nat.card
        (F.quotientKernelOfLe (le_trans hlm hmn) ⧸
          (F.quotientKernelOfLe hmn).subgroupOf
            (F.quotientKernelOfLe (le_trans hlm hmn))) =
      Nat.card (F.quotientKernelOfLe hlm)

theorem

quotientMapOfLe_eq_iff_exists_mem_div_repr

L555 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMapOfLe_eq_iff_exists_mem_div_repr

Documentation

Arbitrary class equality criterion for G/G_n → G/G_m, expanded as a representative of q / r from G_m.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientMapOfLe_eq_iff_exists_mem_div_repr {m n : ℕ}
    (hmn : m ≤ n) (q r : F.quotient n) :
    F.quotientMapOfLe hmn q = F.quotientMapOfLe hmn r ↔
      ∃ σ : G, σ ∈ F.lower m ∧
        F.quotientMk n σ = q / r

def

subquotientEquivQuotientKernelOfLe

L565 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.subquotientEquivQuotientKernelOfLe

Documentation

The ramification subquotient G_m/G_n is canonically the kernel of G/G_n → G/G_m.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

def subquotientEquivQuotientKernelOfLe {m n : ℕ} (hmn : m ≤ n) :
    F.subquotient m n ≃*
      F.quotientKernelOfLe hmn

theorem

coe_subquotientEquivQuotientKernelOfLe_mk

L577 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.coe_subquotientEquivQuotientKernelOfLe_mk

Documentation

States the theorem coe_subquotientEquivQuotientKernelOfLe_mk.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem coe_subquotientEquivQuotientKernelOfLe_mk
    {m n : ℕ} (hmn : m ≤ n) (σ : F.lower m) :
    ((F.subquotientEquivQuotientKernelOfLe hmn
        (F.subquotientMk m n σ) :
      F.quotientKernelOfLe hmn) : F.quotient n) =
      F.quotientMk n (σ : G)

def

gradedPieceEquivQuotientKernel

L588 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.gradedPieceEquivQuotientKernel

Documentation

The graded piece G_n/G_{n+1} as the kernel of G/G_{n+1} → G/G_n.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

def gradedPieceEquivQuotientKernel (n : ℕ) :
    F.gradedPiece n ≃*
      F.quotientKernelOfLe (Nat.le_succ n)

theorem

coe_gradedPieceEquivQuotientKernel_mk

L595 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.coe_gradedPieceEquivQuotientKernel_mk

Documentation

States the theorem coe_gradedPieceEquivQuotientKernel_mk.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem coe_gradedPieceEquivQuotientKernel_mk
    (n : ℕ) (σ : F.lower n) :
    ((F.gradedPieceEquivQuotientKernel n
        (F.gradedPieceMk n σ) :
      F.quotientKernelOfLe (Nat.le_succ n)) : F.quotient (n + 1)) =
      F.quotientMk (n + 1) (σ : G)

def

quotientKernelByNextKernelEquivGradedPiece

L605 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientKernelByNextKernelEquivGradedPiece

Documentation

At every finite level N ≥ n + 1, the nth graded piece is the quotient of finite-level kernels (G_n/G_N)/(G_{n+1}/G_N).

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

def quotientKernelByNextKernelEquivGradedPiece {n N : ℕ} (hN : n + 1 ≤ N) :
    F.quotientKernelOfLe (le_trans (Nat.le_succ n) hN) ⧸
        (F.quotientKernelOfLe hN).subgroupOf
          (F.quotientKernelOfLe (le_trans (Nat.le_succ n) hN)) ≃*
      F.gradedPiece n

theorem

gradedPieceEquivQuotientKernel_quotientKernelByNextKernel_mk'

L614 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.gradedPieceEquivQuotientKernel_quotientKernelByNextKernel_mk'

Documentation

States the theorem gradedPieceEquivQuotientKernel_quotientKernelByNextKernel_mk'.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem gradedPieceEquivQuotientKernel_quotientKernelByNextKernel_mk'
    {n N : ℕ} (hN : n + 1 ≤ N)
    (q : F.quotientKernelOfLe (le_trans (Nat.le_succ n) hN)) :
    F.gradedPieceEquivQuotientKernel n
        (F.quotientKernelByNextKernelEquivGradedPiece hN
          (QuotientGroup.mk'
            ((F.quotientKernelOfLe hN).subgroupOf
              (F.quotientKernelOfLe (le_trans (Nat.le_succ n) hN))) q)) =
      F.quotientKernelMapOfLe (Nat.le_succ n) hN q

theorem

card_quotientKernelByNextKernel_eq_gradedPiece

L629 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.card_quotientKernelByNextKernel_eq_gradedPiece

Documentation

Cardinality form of the finite-level graded-piece compatibility (G_n/G_N)/(G_{n+1}/G_N) ≃ G_n/G_{n+1}.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem card_quotientKernelByNextKernel_eq_gradedPiece {n N : ℕ}
    (hN : n + 1 ≤ N) [Finite G] :
    Nat.card
        (F.quotientKernelOfLe (le_trans (Nat.le_succ n) hN) ⧸
          (F.quotientKernelOfLe hN).subgroupOf
            (F.quotientKernelOfLe (le_trans (Nat.le_succ n) hN))) =
      Nat.card (F.gradedPiece n)

theorem

quotientMapOfLe_surjective

L639 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMapOfLe_surjective

Documentation

The natural level-change map G/G_n → G/G_m is surjective.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientMapOfLe_surjective {m n : ℕ} (hmn : m ≤ n) :
    Function.Surjective (F.quotientMapOfLe hmn)

theorem

quotientMapOfLe_range_eq_top

L648 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMapOfLe_range_eq_top

Documentation

States the theorem quotientMapOfLe_range_eq_top.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientMapOfLe_range_eq_top {m n : ℕ} (hmn : m ≤ n) :
    (F.quotientMapOfLe hmn).range = ⊤

def

tameQuotientEquivQuotientKernel

L653 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.tameQuotientEquivQuotientKernel

Documentation

The tame quotient G_0/G_1 as the kernel of G/G_1 → G/G_0.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

def tameQuotientEquivQuotientKernel :
    F.tameQuotient ≃* F.quotientKernelOfLe (Nat.zero_le 1)

theorem

coe_tameQuotientEquivQuotientKernel_mk

L659 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.coe_tameQuotientEquivQuotientKernel_mk

Documentation

States the theorem coe_tameQuotientEquivQuotientKernel_mk.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem coe_tameQuotientEquivQuotientKernel_mk
    (σ : F.inertiaSubgroup) :
    ((F.tameQuotientEquivQuotientKernel
        (F.tameQuotientMk σ) :
      F.quotientKernelOfLe (Nat.zero_le 1)) : F.quotient 1) =
      F.quotientMk 1 (σ : G)

def

quotientInertiaByWildKernelEquivTameQuotient

L670 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientInertiaByWildKernelEquivTameQuotient

Documentation

At every finite level n ≥ 1, the tame quotient is the quotient of finite-level inertia by finite-level wild inertia: (G_0/G_n)/(G_1/G_n) ≃ G_0/G_1.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

def quotientInertiaByWildKernelEquivTameQuotient {n : ℕ} (hn : 1 ≤ n) :
    F.quotientKernelOfLe (le_trans (Nat.zero_le 1) hn) ⧸
        (F.quotientKernelOfLe hn).subgroupOf
          (F.quotientKernelOfLe (le_trans (Nat.zero_le 1) hn)) ≃*
      F.tameQuotient

theorem

tameQuotientEquivQuotientKernel_quotientInertiaByWildKernel_mk'

L679 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.tameQuotientEquivQuotientKernel_quotientInertiaByWildKernel_mk'

Documentation

States the theorem tameQuotientEquivQuotientKernel_quotientInertiaByWildKernel_mk'.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem tameQuotientEquivQuotientKernel_quotientInertiaByWildKernel_mk'
    {n : ℕ} (hn : 1 ≤ n)
    (q : F.quotientKernelOfLe (le_trans (Nat.zero_le 1) hn)) :
    F.tameQuotientEquivQuotientKernel
        (F.quotientInertiaByWildKernelEquivTameQuotient hn
          (QuotientGroup.mk'
            ((F.quotientKernelOfLe hn).subgroupOf
              (F.quotientKernelOfLe (le_trans (Nat.zero_le 1) hn))) q)) =
      F.quotientKernelMapOfLe (Nat.zero_le 1) hn q

theorem

card_quotientInertiaByWildKernel_eq_tameQuotient

L694 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.card_quotientInertiaByWildKernel_eq_tameQuotient

Documentation

Cardinality form of the finite-level tame quotient compatibility (G_0/G_n)/(G_1/G_n) ≃ G_0/G_1.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem card_quotientInertiaByWildKernel_eq_tameQuotient {n : ℕ}
    (hn : 1 ≤ n) [Finite G] :
    Nat.card
        (F.quotientKernelOfLe (le_trans (Nat.zero_le 1) hn) ⧸
          (F.quotientKernelOfLe hn).subgroupOf
            (F.quotientKernelOfLe (le_trans (Nat.zero_le 1) hn))) =
      Nat.card F.tameQuotient

theorem

mem_tameQuotientKernel_iff_exists_inertia_repr

L705 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.mem_tameQuotientKernel_iff_exists_inertia_repr

Documentation

Kernel membership for G/G_1 → G/G_0, with a representative already in the inertia subgroup.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem mem_tameQuotientKernel_iff_exists_inertia_repr
    (q : F.quotient 1) :
    q ∈ F.quotientKernelOfLe (Nat.zero_le 1) ↔
      ∃ σ : F.inertiaSubgroup,
        F.quotientMk 1 (σ : G) = q

def

quotientQuotientKernelOfLeEquivQuotient

L719 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientQuotientKernelOfLeEquivQuotient

Documentation

First isomorphism theorem for level-change maps: (G/G_n)/(G_m/G_n) ≃ G/G_m.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

def quotientQuotientKernelOfLeEquivQuotient {m n : ℕ} (hmn : m ≤ n) :
    F.quotient n ⧸ F.quotientKernelOfLe hmn ≃* F.quotient m

theorem

quotientQuotientKernelOfLeEquivQuotient_mk'

L727 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientQuotientKernelOfLeEquivQuotient_mk'

Documentation

States the theorem quotientQuotientKernelOfLeEquivQuotient_mk'.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientQuotientKernelOfLeEquivQuotient_mk'
    {m n : ℕ} (hmn : m ≤ n) (q : F.quotient n) :
    F.quotientQuotientKernelOfLeEquivQuotient hmn
        (QuotientGroup.mk' (F.quotientKernelOfLe hmn) q) =
      F.quotientMapOfLe hmn q

theorem

quotientQuotientKernelOfLeEquivQuotient_mk'_mk'

L735 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientQuotientKernelOfLeEquivQuotient_mk'_mk'

Documentation

States the theorem quotientQuotientKernelOfLeEquivQuotient_mk'_mk'.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientQuotientKernelOfLeEquivQuotient_mk'_mk'
    {m n : ℕ} (hmn : m ≤ n) (σ : G) :
    F.quotientQuotientKernelOfLeEquivQuotient hmn
        (QuotientGroup.mk' (F.quotientKernelOfLe hmn)
          (F.quotientMk n σ)) =
      F.quotientMk m σ

theorem

quotientKernelOfLe_refl_eq_bot

L745 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientKernelOfLe_refl_eq_bot

Documentation

The kernel subgroup for the identity level-change map is trivial.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace AntitoneNormalSubgroupFiltration
variable {G : Type u} [Group G] (F : AntitoneNormalSubgroupFiltration G)

Lean source · statement

theorem quotientKernelOfLe_refl_eq_bot (n : ℕ) :
    F.quotientKernelOfLe (le_rfl : n ≤ n) = ⊥

structure

LowerRamificationDepth

L754 ↗

RamificationTheory.DiscreteValuationField.LowerRamificationDepth

Documentation

A depth function whose threshold subgroups form a lower ramification filtration.

Source context 5 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField

Lean source · full declaration

structure LowerRamificationDepth (G : Type u) [Group G] where
  /-- The lower ramification depth of each group element. -/
  depth : G → WithTop ℕ
  /-- The identity has infinite ramification depth. -/
  depth_one : depth 1 = ⊤
  /-- Each depth threshold is closed under multiplication. -/
  depth_mul_mem :
    ∀ {n : ℕ} {σ τ : G},
      (n : WithTop ℕ) ≤ depth σ →
      (n : WithTop ℕ) ≤ depth τ →
      (n : WithTop ℕ) ≤ depth (σ * τ)
  /-- Each depth threshold is closed under inversion. -/
  depth_inv_mem :
    ∀ {n : ℕ} {σ : G},
      (n : WithTop ℕ) ≤ depth σ →
      (n : WithTop ℕ) ≤ depth σ⁻¹
  /-- Each depth threshold is preserved under conjugation. -/
  depth_conj_mem :
    ∀ {n : ℕ} {γ σ : G},
      (n : WithTop ℕ) ≤ depth σ →
      (n : WithTop ℕ) ≤ depth (γ * σ * γ⁻¹)

def

lowerRamificationGroup

L781 ↗

RamificationTheory.DiscreteValuationField.LowerRamificationDepth.lowerRamificationGroup

Documentation

The threshold subgroup cut out by a ramification depth function.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace LowerRamificationDepth
variable {G : Type u} [Group G] (D : LowerRamificationDepth G)

Lean source · full declaration

def lowerRamificationGroup (n : ℕ) : Subgroup G where
  carrier := {σ | (n : WithTop ℕ) ≤ D.depth σ}
  one_mem' := by
    change (n : WithTop ℕ) ≤ D.depth 1
    rw [D.depth_one]
    exact le_top
  mul_mem' := by
    intro σ τ hσ hτ
    exact D.depth_mul_mem hσ hτ
  inv_mem' := by
    intro σ hσ
    exact D.depth_inv_mem hσ

theorem

mem_lowerRamificationGroup_iff

L795 ↗

RamificationTheory.DiscreteValuationField.LowerRamificationDepth.mem_lowerRamificationGroup_iff

Documentation

States the theorem mem_lowerRamificationGroup_iff.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace LowerRamificationDepth
variable {G : Type u} [Group G] (D : LowerRamificationDepth G)

Lean source · statement

theorem mem_lowerRamificationGroup_iff (n : ℕ) (σ : G) :
    σ ∈ D.lowerRamificationGroup n ↔ (n : WithTop ℕ) ≤ D.depth σ

theorem

lowerRamificationGroup_normal

L800 ↗

RamificationTheory.DiscreteValuationField.LowerRamificationDepth.lowerRamificationGroup_normal

Documentation

States the theorem lowerRamificationGroup_normal.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace LowerRamificationDepth
variable {G : Type u} [Group G] (D : LowerRamificationDepth G)

Lean source · full declaration

theorem lowerRamificationGroup_normal (n : ℕ) :
    (D.lowerRamificationGroup n).Normal where
  conj_mem := by
    intro σ hσ γ
    exact D.depth_conj_mem (γ := γ) hσ

instance

lowerRamificationGroup_normal_instance

L807 ↗

RamificationTheory.DiscreteValuationField.LowerRamificationDepth.lowerRamificationGroup_normal_instance

Documentation

Provides the instance lowerRamificationGroup_normal_instance.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace LowerRamificationDepth
variable {G : Type u} [Group G] (D : LowerRamificationDepth G)

Lean source · statement

instance lowerRamificationGroup_normal_instance (n : ℕ) :
    (D.lowerRamificationGroup n).Normal

theorem

lowerRamificationGroup_antitone

L812 ↗

RamificationTheory.DiscreteValuationField.LowerRamificationDepth.lowerRamificationGroup_antitone

Documentation

States the theorem lowerRamificationGroup_antitone.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace LowerRamificationDepth
variable {G : Type u} [Group G] (D : LowerRamificationDepth G)

Lean source · statement

theorem lowerRamificationGroup_antitone {m n : ℕ} (hmn : m ≤ n) :
    D.lowerRamificationGroup n ≤ D.lowerRamificationGroup m

theorem

mem_lowerRamificationGroup_of_le

L821 ↗

RamificationTheory.DiscreteValuationField.LowerRamificationDepth.mem_lowerRamificationGroup_of_le

Documentation

States the theorem mem_lowerRamificationGroup_of_le.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace LowerRamificationDepth
variable {G : Type u} [Group G] (D : LowerRamificationDepth G)

Lean source · statement

theorem mem_lowerRamificationGroup_of_le {m n : ℕ} (hmn : m ≤ n) {σ : G}
    (hσ : σ ∈ D.lowerRamificationGroup n) :
    σ ∈ D.lowerRamificationGroup m

def

toLowerRamificationFiltration

L827 ↗

RamificationTheory.DiscreteValuationField.LowerRamificationDepth.toLowerRamificationFiltration

Documentation

Package a depth function as a lower ramification filtration.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace LowerRamificationDepth
variable {G : Type u} [Group G] (D : LowerRamificationDepth G)

Lean source · full declaration

def toLowerRamificationFiltration : AntitoneNormalSubgroupFiltration G where
  lower := D.lowerRamificationGroup
  lower_normal := D.lowerRamificationGroup_normal
  antitone := by
    intro m n hmn
    exact D.lowerRamificationGroup_antitone hmn

theorem

toLowerRamificationFiltration_apply

L835 ↗

RamificationTheory.DiscreteValuationField.LowerRamificationDepth.toLowerRamificationFiltration_apply

Documentation

States the theorem toLowerRamificationFiltration_apply.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace LowerRamificationDepth
variable {G : Type u} [Group G] (D : LowerRamificationDepth G)

Lean source · statement

theorem toLowerRamificationFiltration_apply (n : ℕ) :
    D.toLowerRamificationFiltration.lower n = D.lowerRamificationGroup n

def

herbrandStep

L840 ↗

RamificationTheory.DiscreteValuationField.LowerRamificationDepth.herbrandStep

Documentation

Herbrand step attached to a depth-defined lower filtration.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace LowerRamificationDepth
variable {G : Type u} [Group G] (D : LowerRamificationDepth G)

Lean source · statement

def herbrandStep (i : Nat) : Rat

def

herbrandFunctionNat

L845 ↗

RamificationTheory.DiscreteValuationField.LowerRamificationDepth.herbrandFunctionNat

Documentation

Natural-index Herbrand function attached to a depth-defined lower filtration.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace LowerRamificationDepth
variable {G : Type u} [Group G] (D : LowerRamificationDepth G)

Lean source · statement

def herbrandFunctionNat (n : Nat) : Rat

theorem

herbrandStep_pos

L849 ↗

RamificationTheory.DiscreteValuationField.LowerRamificationDepth.herbrandStep_pos

Documentation

States the theorem herbrandStep_pos.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace LowerRamificationDepth
variable {G : Type u} [Group G] (D : LowerRamificationDepth G)

Lean source · statement

theorem herbrandStep_pos (i : Nat)
    [Finite (D.lowerRamificationGroup i)]
    [Finite (D.lowerRamificationGroup 0)] :
    0 < D.herbrandStep i

theorem

herbrandFunctionNat_mono

L863 ↗

RamificationTheory.DiscreteValuationField.LowerRamificationDepth.herbrandFunctionNat_mono

Documentation

States the theorem herbrandFunctionNat_mono.

Source context 7 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace LowerRamificationDepth
variable {G : Type u} [Group G] (D : LowerRamificationDepth G)

Lean source · statement

theorem herbrandFunctionNat_mono :
    Monotone D.herbrandFunctionNat

structure

ValuationActionRamification

L872 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification

Documentation

A ramification filtration coming from an action quotient tested against principal units.

Source context 5 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField

Lean source · full declaration

structure ValuationActionRamification (G : Type u) [Group G]
    (K : Type v) [Group K] where
  /-- The principal-unit filtration used to test action quotients. -/
  principalUnits : LocalFieldTheory.DiscreteValuationField.AntitoneSubgroupFiltration K
  /-- The action of `G` on `K` by multiplicative automorphisms. -/
  action : G →* MulAut K
  /-- The element of `K` on which action quotients are evaluated. -/
  probe : K
  /-- Membership of action quotients at a fixed level is closed under multiplication. -/
  quotient_mul_mem :
    ∀ {n : ℕ} {σ τ : G},
      ((action σ) probe / probe) ∈ principalUnits.subgroup n →
      ((action τ) probe / probe) ∈ principalUnits.subgroup n →
      ((action (σ * τ)) probe / probe) ∈ principalUnits.subgroup n
  /-- Membership of action quotients at a fixed level is closed under inversion. -/
  quotient_inv_mem :
    ∀ {n : ℕ} {σ : G},
      ((action σ) probe / probe) ∈ principalUnits.subgroup n →
      ((action σ⁻¹) probe / probe) ∈ principalUnits.subgroup n
  /-- Membership of action quotients at a fixed level is preserved under conjugation. -/
  quotient_conj_mem :
    ∀ {n : ℕ} {γ σ : G},
      ((action σ) probe / probe) ∈ principalUnits.subgroup n →
      ((action (γ * σ * γ⁻¹)) probe / probe) ∈ principalUnits.subgroup n

def

actionQuotient

L903 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.actionQuotient

Documentation

The action quotient used to test ramification depth.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

def actionQuotient (σ : G) : K

theorem

actionQuotient_one

L907 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.actionQuotient_one

Documentation

States the theorem actionQuotient_one.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem actionQuotient_one :
    A.actionQuotient 1 = 1

def

actionDepthAtLeast

L912 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.actionDepthAtLeast

Documentation

Defines actionDepthAtLeast.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

def actionDepthAtLeast (n : ℕ) (σ : G) : Prop

theorem

actionDepthAtLeast_iff

L916 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.actionDepthAtLeast_iff

Documentation

States the theorem actionDepthAtLeast_iff.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem actionDepthAtLeast_iff (n : ℕ) (σ : G) :
    A.actionDepthAtLeast n σ ↔
      A.actionQuotient σ ∈ A.principalUnits.subgroup n

theorem

actionDepthAtLeast_one

L922 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.actionDepthAtLeast_one

Documentation

States the theorem actionDepthAtLeast_one.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem actionDepthAtLeast_one (n : ℕ) :
    A.actionDepthAtLeast n 1

theorem

actionDepthAtLeast_mul

L928 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.actionDepthAtLeast_mul

Documentation

States the theorem actionDepthAtLeast_mul.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem actionDepthAtLeast_mul {n : ℕ} {σ τ : G}
    (hσ : A.actionDepthAtLeast n σ) (hτ : A.actionDepthAtLeast n τ) :
    A.actionDepthAtLeast n (σ * τ)

theorem

actionDepthAtLeast_inv

L934 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.actionDepthAtLeast_inv

Documentation

States the theorem actionDepthAtLeast_inv.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem actionDepthAtLeast_inv {n : ℕ} {σ : G}
    (hσ : A.actionDepthAtLeast n σ) :
    A.actionDepthAtLeast n σ⁻¹

theorem

actionDepthAtLeast_conj

L940 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.actionDepthAtLeast_conj

Documentation

States the theorem actionDepthAtLeast_conj.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem actionDepthAtLeast_conj {n : ℕ} {γ σ : G}
    (hσ : A.actionDepthAtLeast n σ) :
    A.actionDepthAtLeast n (γ * σ * γ⁻¹)

def

lowerRamificationGroup

L946 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.lowerRamificationGroup

Documentation

The action-defined lower ramification group.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · full declaration

def lowerRamificationGroup (n : ℕ) : Subgroup G where
  carrier := {σ | A.actionDepthAtLeast n σ}
  one_mem' := A.actionDepthAtLeast_one n
  mul_mem' := by
    intro σ τ hσ hτ
    exact A.actionDepthAtLeast_mul hσ hτ
  inv_mem' := by
    intro σ hσ
    exact A.actionDepthAtLeast_inv hσ

theorem

mem_lowerRamificationGroup_iff

L957 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.mem_lowerRamificationGroup_iff

Documentation

States the theorem mem_lowerRamificationGroup_iff.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem mem_lowerRamificationGroup_iff (n : ℕ) (σ : G) :
    σ ∈ A.lowerRamificationGroup n ↔ A.actionDepthAtLeast n σ

theorem

mem_lowerRamificationGroup_iff_actionQuotient

L963 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.mem_lowerRamificationGroup_iff_actionQuotient

Documentation

Membership in the action-defined lower ramification group, expanded as a principal-unit condition on the action quotient.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem mem_lowerRamificationGroup_iff_actionQuotient (n : ℕ) (σ : G) :
    σ ∈ A.lowerRamificationGroup n ↔
      A.actionQuotient σ ∈ A.principalUnits.subgroup n

theorem

lowerRamificationGroup_normal

L970 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.lowerRamificationGroup_normal

Documentation

States the theorem lowerRamificationGroup_normal.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · full declaration

theorem lowerRamificationGroup_normal (n : ℕ) :
    (A.lowerRamificationGroup n).Normal where
  conj_mem := by
    intro σ hσ γ
    exact A.actionDepthAtLeast_conj (γ := γ) hσ

instance

lowerRamificationGroup_normal_instance

L977 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.lowerRamificationGroup_normal_instance

Documentation

Provides the instance lowerRamificationGroup_normal_instance.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

instance lowerRamificationGroup_normal_instance (n : ℕ) :
    (A.lowerRamificationGroup n).Normal

theorem

lowerRamificationGroup_antitone

L982 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.lowerRamificationGroup_antitone

Documentation

States the theorem lowerRamificationGroup_antitone.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem lowerRamificationGroup_antitone {m n : ℕ} (hmn : m ≤ n) :
    A.lowerRamificationGroup n ≤ A.lowerRamificationGroup m

def

toLowerRamificationFiltration

L988 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.toLowerRamificationFiltration

Documentation

Package the action-defined groups as a lower ramification filtration.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · full declaration

def toLowerRamificationFiltration : AntitoneNormalSubgroupFiltration G where
  lower := A.lowerRamificationGroup
  lower_normal := A.lowerRamificationGroup_normal
  antitone := by
    intro m n hmn
    exact A.lowerRamificationGroup_antitone hmn

theorem

toLowerRamificationFiltration_apply

L996 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.toLowerRamificationFiltration_apply

Documentation

States the theorem toLowerRamificationFiltration_apply.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem toLowerRamificationFiltration_apply (n : ℕ) :
    A.toLowerRamificationFiltration.lower n = A.lowerRamificationGroup n

def

herbrandStep

L1001 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.herbrandStep

Documentation

Herbrand step attached to an action-defined lower filtration.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

def herbrandStep (i : Nat) : Rat

def

herbrandFunctionNat

L1006 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.herbrandFunctionNat

Documentation

Natural-index Herbrand function attached to an action-defined lower filtration.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

def herbrandFunctionNat (n : Nat) : Rat

theorem

herbrandStep_pos

L1010 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.herbrandStep_pos

Documentation

States the theorem herbrandStep_pos.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem herbrandStep_pos (i : Nat)
    [Finite (A.lowerRamificationGroup i)]
    [Finite (A.lowerRamificationGroup 0)] :
    0 < A.herbrandStep i

theorem

herbrandFunctionNat_mono

L1024 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.herbrandFunctionNat_mono

Documentation

States the theorem herbrandFunctionNat_mono.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem herbrandFunctionNat_mono :
    Monotone A.herbrandFunctionNat

abbrev

inertiaSubgroup

L1030 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.inertiaSubgroup

Documentation

The inertia subgroup G_0 for an action-defined filtration.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

abbrev inertiaSubgroup : Subgroup G

theorem

lowerRamificationGroup_zero_eq_inertiaSubgroup

L1034 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.lowerRamificationGroup_zero_eq_inertiaSubgroup

Documentation

States the theorem lowerRamificationGroup_zero_eq_inertiaSubgroup.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem lowerRamificationGroup_zero_eq_inertiaSubgroup :
    A.lowerRamificationGroup 0 = A.inertiaSubgroup

abbrev

wildInertiaSubgroup

L1039 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.wildInertiaSubgroup

Documentation

The wild inertia subgroup G_1 for an action-defined filtration.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

abbrev wildInertiaSubgroup : Subgroup G

def

tameQuotient

L1043 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.tameQuotient

Documentation

The tame quotient G_0/G_1 for an action-defined filtration.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

def tameQuotient : Type u

instance

tameQuotientGroup

L1047 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.tameQuotientGroup

Documentation

Provides the instance tameQuotientGroup.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

instance tameQuotientGroup : Group A.tameQuotient

def

tameQuotientEquivLowerFiltration

L1053 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.tameQuotientEquivLowerFiltration

Documentation

The action-defined tame quotient is canonically identified with the underlying lower-filtration model.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

def tameQuotientEquivLowerFiltration :
    A.tameQuotient ≃*
      A.toLowerRamificationFiltration.tameQuotient

instance

tameQuotientFinite

L1059 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.tameQuotientFinite

Documentation

Provides the instance tameQuotientFinite.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

instance tameQuotientFinite [Finite G] : Finite A.tameQuotient

def

tameQuotientMk

L1064 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.tameQuotientMk

Documentation

Canonical projection to the action-defined tame quotient.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

def tameQuotientMk : A.inertiaSubgroup →* A.tameQuotient

theorem

tameQuotientEquivLowerFiltration_apply_mk

L1070 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.tameQuotientEquivLowerFiltration_apply_mk

Documentation

States the theorem tameQuotientEquivLowerFiltration_apply_mk.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem tameQuotientEquivLowerFiltration_apply_mk
    (σ : A.inertiaSubgroup) :
    A.tameQuotientEquivLowerFiltration (A.tameQuotientMk σ) =
      A.toLowerRamificationFiltration.tameQuotientMk σ

theorem

tameQuotientMk_surjective

L1077 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.tameQuotientMk_surjective

Documentation

States the theorem tameQuotientMk_surjective.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem tameQuotientMk_surjective :
    Function.Surjective A.tameQuotientMk

theorem

tameQuotientMk_eq_one_iff

L1092 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.tameQuotientMk_eq_one_iff

Documentation

States the theorem tameQuotientMk_eq_one_iff.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem tameQuotientMk_eq_one_iff (σ : A.inertiaSubgroup) :
    A.tameQuotientMk σ = 1 ↔ (σ : G) ∈ A.wildInertiaSubgroup

theorem

tameQuotientMk_eq_iff

L1109 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.tameQuotientMk_eq_iff

Documentation

States the theorem tameQuotientMk_eq_iff.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem tameQuotientMk_eq_iff (σ τ : A.inertiaSubgroup) :
    A.tameQuotientMk σ = A.tameQuotientMk τ ↔
      ((σ / τ : A.inertiaSubgroup) : G) ∈ A.wildInertiaSubgroup

theorem

tameQuotient_inductionOn

L1133 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.tameQuotient_inductionOn

Documentation

Eliminate the action-defined tame quotient through inertia representatives.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem tameQuotient_inductionOn
    {motive : A.tameQuotient → Prop} (q : A.tameQuotient)
    (h : ∀ σ : A.inertiaSubgroup, motive (A.tameQuotientMk σ)) :
    motive q

def

tameCharacterOfUniformizer

L1146 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.tameCharacterOfUniformizer

Documentation

The tame character attached to the chosen action probe.

For valued-extension applications the probe is the chosen uniformizer and the action quotient is σ ϖ / ϖ; at this abstraction level the target is the tame quotient G_0/G_1. Residue-field unit realizations can be composed on top once the concrete unit quotient has been constructed.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

def tameCharacterOfUniformizer : A.inertiaSubgroup →* A.tameQuotient

theorem

tameCharacterOfUniformizer_apply

L1150 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.tameCharacterOfUniformizer_apply

Documentation

States the theorem tameCharacterOfUniformizer_apply.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem tameCharacterOfUniformizer_apply (σ : A.inertiaSubgroup) :
    A.tameCharacterOfUniformizer σ =
      A.tameQuotientMk σ

theorem

tameCharacter_ker_eq_wildInertia

L1156 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.tameCharacter_ker_eq_wildInertia

Documentation

The kernel of the action-probe tame character is wild inertia.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem tameCharacter_ker_eq_wildInertia :
    MonoidHom.ker A.tameCharacterOfUniformizer =
      (A.wildInertiaSubgroup).subgroupOf A.inertiaSubgroup

theorem

mem_inertiaSubgroup_iff_actionDepthAtLeast

L1164 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.mem_inertiaSubgroup_iff_actionDepthAtLeast

Documentation

States the theorem mem_inertiaSubgroup_iff_actionDepthAtLeast.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem mem_inertiaSubgroup_iff_actionDepthAtLeast (σ : G) :
    σ ∈ A.inertiaSubgroup ↔ A.actionDepthAtLeast 0 σ

theorem

mem_wildInertiaSubgroup_iff_actionDepthAtLeast

L1169 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.mem_wildInertiaSubgroup_iff_actionDepthAtLeast

Documentation

States the theorem mem_wildInertiaSubgroup_iff_actionDepthAtLeast.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem mem_wildInertiaSubgroup_iff_actionDepthAtLeast (σ : G) :
    σ ∈ A.wildInertiaSubgroup ↔ A.actionDepthAtLeast 1 σ

theorem

mem_inertiaSubgroup_iff_actionQuotient

L1175 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.mem_inertiaSubgroup_iff_actionQuotient

Documentation

Membership in inertia, expanded as a principal-unit condition on the action quotient.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem mem_inertiaSubgroup_iff_actionQuotient (σ : G) :
    σ ∈ A.inertiaSubgroup ↔
      A.actionQuotient σ ∈ A.principalUnits.subgroup 0

theorem

mem_wildInertiaSubgroup_iff_actionQuotient

L1182 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.mem_wildInertiaSubgroup_iff_actionQuotient

Documentation

Membership in wild inertia, expanded as a principal-unit condition on the action quotient.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem mem_wildInertiaSubgroup_iff_actionQuotient (σ : G) :
    σ ∈ A.wildInertiaSubgroup ↔
      A.actionQuotient σ ∈ A.principalUnits.subgroup 1

theorem

wildInertiaSubgroup_le_inertiaSubgroup

L1188 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.wildInertiaSubgroup_le_inertiaSubgroup

Documentation

States the theorem wildInertiaSubgroup_le_inertiaSubgroup.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem wildInertiaSubgroup_le_inertiaSubgroup :
    A.wildInertiaSubgroup ≤ A.inertiaSubgroup

def

tameQuotientEquivQuotientKernel

L1193 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.tameQuotientEquivQuotientKernel

Documentation

Defines tameQuotientEquivQuotientKernel.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

def tameQuotientEquivQuotientKernel :
    A.tameQuotient ≃*
      A.toLowerRamificationFiltration.quotientKernelOfLe (Nat.zero_le 1)

theorem

coe_tameQuotientEquivQuotientKernel_mk

L1200 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.coe_tameQuotientEquivQuotientKernel_mk

Documentation

States the theorem coe_tameQuotientEquivQuotientKernel_mk.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem coe_tameQuotientEquivQuotientKernel_mk
    (σ : A.inertiaSubgroup) :
    ((A.tameQuotientEquivQuotientKernel
        (A.tameQuotientMk σ) :
      A.toLowerRamificationFiltration.quotientKernelOfLe (Nat.zero_le 1)) :
      A.toLowerRamificationFiltration.quotient 1) =
      A.toLowerRamificationFiltration.quotientMk 1 (σ : G)

def

quotientInertiaByWildKernelEquivTameQuotient

L1213 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.quotientInertiaByWildKernelEquivTameQuotient

Documentation

At every finite level n ≥ 1, the action-defined tame quotient is the quotient of finite-level inertia by finite-level wild inertia: (G_0/G_n)/(G_1/G_n) ≃ G_0/G_1.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

def quotientInertiaByWildKernelEquivTameQuotient {n : ℕ} (hn : 1 ≤ n) :
    A.toLowerRamificationFiltration.quotientKernelOfLe
        (le_trans (Nat.zero_le 1) hn) ⧸
        (A.toLowerRamificationFiltration.quotientKernelOfLe hn).subgroupOf
          (A.toLowerRamificationFiltration.quotientKernelOfLe
            (le_trans (Nat.zero_le 1) hn)) ≃*
      A.tameQuotient

theorem

tameQuotientEquivQuotientKernel_quotientInertiaByWildKernel_mk'

L1225 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.tameQuotientEquivQuotientKernel_quotientInertiaByWildKernel_mk'

Documentation

States the theorem tameQuotientEquivQuotientKernel_quotientInertiaByWildKernel_mk'.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem tameQuotientEquivQuotientKernel_quotientInertiaByWildKernel_mk'
    {n : ℕ} (hn : 1 ≤ n)
    (q :
      A.toLowerRamificationFiltration.quotientKernelOfLe
        (le_trans (Nat.zero_le 1) hn)) :
    A.tameQuotientEquivQuotientKernel
        (A.quotientInertiaByWildKernelEquivTameQuotient hn
          (QuotientGroup.mk'
            ((A.toLowerRamificationFiltration.quotientKernelOfLe hn).subgroupOf
              (A.toLowerRamificationFiltration.quotientKernelOfLe
                (le_trans (Nat.zero_le 1) hn))) q)) =
      A.toLowerRamificationFiltration.quotientKernelMapOfLe
        (Nat.zero_le 1) hn q

theorem

card_quotientInertiaByWildKernel_eq_tameQuotient

L1243 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.card_quotientInertiaByWildKernel_eq_tameQuotient

Documentation

Cardinality form of the action-defined finite-level tame quotient compatibility (G_0/G_n)/(G_1/G_n) ≃ G_0/G_1.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem card_quotientInertiaByWildKernel_eq_tameQuotient {n : ℕ}
    (hn : 1 ≤ n) [Finite G] :
    Nat.card
        (A.toLowerRamificationFiltration.quotientKernelOfLe
            (le_trans (Nat.zero_le 1) hn) ⧸
          (A.toLowerRamificationFiltration.quotientKernelOfLe hn).subgroupOf
            (A.toLowerRamificationFiltration.quotientKernelOfLe
              (le_trans (Nat.zero_le 1) hn))) =
      Nat.card A.tameQuotient

theorem

mem_tameQuotientKernel_iff_exists_inertia_repr

L1262 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.mem_tameQuotientKernel_iff_exists_inertia_repr

Documentation

Kernel membership for the action-defined map G/G_1 → G/G_0, with a representative already in inertia.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem mem_tameQuotientKernel_iff_exists_inertia_repr
    (q : A.toLowerRamificationFiltration.quotient 1) :
    q ∈ A.toLowerRamificationFiltration.quotientKernelOfLe (Nat.zero_le 1) ↔
      ∃ σ : A.inertiaSubgroup,
        A.toLowerRamificationFiltration.quotientMk 1 (σ : G) = q

theorem

mem_tameQuotientKernel_iff_exists_actionQuotient_mem_repr

L1272 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.mem_tameQuotientKernel_iff_exists_actionQuotient_mem_repr

Documentation

Kernel membership for the action-defined map G/G_1 → G/G_0, expanded by an action-quotient representative in U^0.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem mem_tameQuotientKernel_iff_exists_actionQuotient_mem_repr
    (q : A.toLowerRamificationFiltration.quotient 1) :
    q ∈ A.toLowerRamificationFiltration.quotientKernelOfLe (Nat.zero_le 1) ↔
      ∃ σ : G, A.actionQuotient σ ∈ A.principalUnits.subgroup 0 ∧
        A.toLowerRamificationFiltration.quotientMk 1 σ = q

instance

lowerRamificationGroup_subgroupOf_normal_instance

L1286 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.lowerRamificationGroup_subgroupOf_normal_instance

Documentation

Provides the instance lowerRamificationGroup_subgroupOf_normal_instance.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

instance lowerRamificationGroup_subgroupOf_normal_instance (n : ℕ) :
    ((A.lowerRamificationGroup (n + 1)).subgroupOf
      (A.lowerRamificationGroup n)).Normal

theorem

tameQuotientMk_eq_one_iff_actionDepthAtLeast

L1295 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.tameQuotientMk_eq_one_iff_actionDepthAtLeast

Documentation

Representative criterion for the identity class in the action-defined tame quotient G_0/G_1.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem tameQuotientMk_eq_one_iff_actionDepthAtLeast
    (σ : A.inertiaSubgroup) :
    A.tameQuotientMk σ = 1 ↔
      A.actionDepthAtLeast 1 (σ : G)

theorem

tameQuotientMk_eq_one_iff_actionQuotient_mem

L1304 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.tameQuotientMk_eq_one_iff_actionQuotient_mem

Documentation

Representative criterion for the identity class in the action-defined tame quotient G_0/G_1, expanded as membership of the action quotient in U^1.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem tameQuotientMk_eq_one_iff_actionQuotient_mem
    (σ : A.inertiaSubgroup) :
    A.tameQuotientMk σ = 1 ↔
      A.actionQuotient (σ : G) ∈ A.principalUnits.subgroup 1

theorem

tameQuotientMk_eq_iff_actionDepthAtLeast_div

L1313 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.tameQuotientMk_eq_iff_actionDepthAtLeast_div

Documentation

Representative equality criterion in the action-defined tame quotient G_0/G_1, in right-quotient form.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem tameQuotientMk_eq_iff_actionDepthAtLeast_div
    (σ τ : A.inertiaSubgroup) :
    A.tameQuotientMk σ = A.tameQuotientMk τ ↔
      A.actionDepthAtLeast 1 ((σ / τ : A.inertiaSubgroup) : G)

theorem

tameQuotientMk_eq_iff_actionQuotient_div_mem

L1324 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.tameQuotientMk_eq_iff_actionQuotient_div_mem

Documentation

Representative equality criterion in the action-defined tame quotient G_0/G_1, in right-quotient form, expanded as membership of the action quotient in U^1.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem tameQuotientMk_eq_iff_actionQuotient_div_mem
    (σ τ : A.inertiaSubgroup) :
    A.tameQuotientMk σ = A.tameQuotientMk τ ↔
      A.actionQuotient (((σ / τ : A.inertiaSubgroup) : G)) ∈
        A.principalUnits.subgroup 1

theorem

tameQuotientMk_eq_iff_actionDepthAtLeast_inv_mul

L1334 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.tameQuotientMk_eq_iff_actionDepthAtLeast_inv_mul

Documentation

Representative equality criterion in the action-defined tame quotient G_0/G_1, in left-quotient form.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem tameQuotientMk_eq_iff_actionDepthAtLeast_inv_mul
    (σ τ : A.inertiaSubgroup) :
    A.tameQuotientMk σ = A.tameQuotientMk τ ↔
      A.actionDepthAtLeast 1 ((τ⁻¹ * σ : A.inertiaSubgroup) : G)

theorem

tameQuotientMk_eq_iff_actionQuotient_inv_mul_mem

L1352 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.tameQuotientMk_eq_iff_actionQuotient_inv_mul_mem

Documentation

Representative equality criterion in the action-defined tame quotient G_0/G_1, in left-quotient form, expanded as membership of the action quotient in U^1.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem tameQuotientMk_eq_iff_actionQuotient_inv_mul_mem
    (σ τ : A.inertiaSubgroup) :
    A.tameQuotientMk σ = A.tameQuotientMk τ ↔
      A.actionQuotient (((τ⁻¹ * σ : A.inertiaSubgroup) : G)) ∈
        A.principalUnits.subgroup 1

theorem

quotientMapOfLe_mk_eq_one_iff_actionDepthAtLeast

L1362 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.quotientMapOfLe_mk_eq_one_iff_actionDepthAtLeast

Documentation

Representative kernel criterion for the action-defined quotient map G/G_n → G/G_m, expressed by the action-depth predicate.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem quotientMapOfLe_mk_eq_one_iff_actionDepthAtLeast {m n : ℕ}
    (hmn : m ≤ n) (σ : G) :
    A.toLowerRamificationFiltration.quotientMapOfLe hmn
        (A.toLowerRamificationFiltration.quotientMk n σ) = 1 ↔
      A.actionDepthAtLeast m σ

theorem

quotientMapOfLe_mk_eq_one_iff_actionQuotient_mem

L1373 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.quotientMapOfLe_mk_eq_one_iff_actionQuotient_mem

Documentation

Representative kernel criterion for the action-defined quotient map G/G_n → G/G_m, expanded as membership of the action quotient in U^m.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem quotientMapOfLe_mk_eq_one_iff_actionQuotient_mem {m n : ℕ}
    (hmn : m ≤ n) (σ : G) :
    A.toLowerRamificationFiltration.quotientMapOfLe hmn
        (A.toLowerRamificationFiltration.quotientMk n σ) = 1 ↔
      A.actionQuotient σ ∈ A.principalUnits.subgroup m

theorem

quotientMapOfLe_mk_mem_ker_iff_actionQuotient_mem

L1383 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.quotientMapOfLe_mk_mem_ker_iff_actionQuotient_mem

Documentation

Representative kernel-membership criterion for the action-defined quotient map G/G_n → G/G_m, expanded as membership of the action quotient in U^m.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem quotientMapOfLe_mk_mem_ker_iff_actionQuotient_mem {m n : ℕ}
    (hmn : m ≤ n) (σ : G) :
    A.toLowerRamificationFiltration.quotientMk n σ ∈
        (A.toLowerRamificationFiltration.quotientMapOfLe hmn).ker ↔
      A.actionQuotient σ ∈ A.principalUnits.subgroup m

theorem

quotientMapOfLe_mk_eq_iff_actionDepthAtLeast_div

L1394 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.quotientMapOfLe_mk_eq_iff_actionDepthAtLeast_div

Documentation

Representative equality criterion for the action-defined quotient map G/G_n → G/G_m, in right-quotient form.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem quotientMapOfLe_mk_eq_iff_actionDepthAtLeast_div {m n : ℕ}
    (hmn : m ≤ n) (σ τ : G) :
    A.toLowerRamificationFiltration.quotientMapOfLe hmn
        (A.toLowerRamificationFiltration.quotientMk n σ) =
      A.toLowerRamificationFiltration.quotientMapOfLe hmn
        (A.toLowerRamificationFiltration.quotientMk n τ) ↔
      A.actionDepthAtLeast m (σ / τ)

theorem

quotientMapOfLe_mk_eq_iff_actionQuotient_div_mem

L1408 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.quotientMapOfLe_mk_eq_iff_actionQuotient_div_mem

Documentation

Representative equality criterion for the action-defined quotient map G/G_n → G/G_m, in right-quotient form, expanded as membership of the action quotient in U^m.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem quotientMapOfLe_mk_eq_iff_actionQuotient_div_mem {m n : ℕ}
    (hmn : m ≤ n) (σ τ : G) :
    A.toLowerRamificationFiltration.quotientMapOfLe hmn
        (A.toLowerRamificationFiltration.quotientMk n σ) =
      A.toLowerRamificationFiltration.quotientMapOfLe hmn
        (A.toLowerRamificationFiltration.quotientMk n τ) ↔
      A.actionQuotient (σ / τ) ∈ A.principalUnits.subgroup m

theorem

quotientMapOfLe_mk_eq_iff_actionDepthAtLeast_inv_mul

L1420 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.quotientMapOfLe_mk_eq_iff_actionDepthAtLeast_inv_mul

Documentation

Representative equality criterion for the action-defined quotient map G/G_n → G/G_m, in left-quotient form.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem quotientMapOfLe_mk_eq_iff_actionDepthAtLeast_inv_mul {m n : ℕ}
    (hmn : m ≤ n) (σ τ : G) :
    A.toLowerRamificationFiltration.quotientMapOfLe hmn
        (A.toLowerRamificationFiltration.quotientMk n σ) =
      A.toLowerRamificationFiltration.quotientMapOfLe hmn
        (A.toLowerRamificationFiltration.quotientMk n τ) ↔
      A.actionDepthAtLeast m (τ⁻¹ * σ)

theorem

quotientMapOfLe_mk_eq_iff_actionQuotient_inv_mul_mem

L1435 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.quotientMapOfLe_mk_eq_iff_actionQuotient_inv_mul_mem

Documentation

Representative equality criterion for the action-defined quotient map G/G_n → G/G_m, in left-quotient form, expanded as membership of the action quotient in U^m.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem quotientMapOfLe_mk_eq_iff_actionQuotient_inv_mul_mem {m n : ℕ}
    (hmn : m ≤ n) (σ τ : G) :
    A.toLowerRamificationFiltration.quotientMapOfLe hmn
        (A.toLowerRamificationFiltration.quotientMk n σ) =
      A.toLowerRamificationFiltration.quotientMapOfLe hmn
        (A.toLowerRamificationFiltration.quotientMk n τ) ↔
      A.actionQuotient (τ⁻¹ * σ) ∈ A.principalUnits.subgroup m

theorem

quotientMapOfLe_eq_one_iff_exists_actionQuotient_mem_repr

L1447 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.quotientMapOfLe_eq_one_iff_exists_actionQuotient_mem_repr

Documentation

Arbitrary-class kernel criterion for the action-defined quotient map G/G_n → G/G_m, expressed by an action quotient representative in U^m.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem quotientMapOfLe_eq_one_iff_exists_actionQuotient_mem_repr
    {m n : ℕ} (hmn : m ≤ n)
    (q : A.toLowerRamificationFiltration.quotient n) :
    A.toLowerRamificationFiltration.quotientMapOfLe hmn q = 1 ↔
      ∃ σ : G, A.actionQuotient σ ∈ A.principalUnits.subgroup m ∧
        A.toLowerRamificationFiltration.quotientMk n σ = q

theorem

quotientMapOfLe_mem_ker_iff_exists_actionQuotient_mem_repr

L1461 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.quotientMapOfLe_mem_ker_iff_exists_actionQuotient_mem_repr

Documentation

Kernel-membership criterion for an arbitrary class in the action-defined quotient map G/G_n → G/G_m, expressed by an action quotient representative in U^m.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem quotientMapOfLe_mem_ker_iff_exists_actionQuotient_mem_repr
    {m n : ℕ} (hmn : m ≤ n)
    (q : A.toLowerRamificationFiltration.quotient n) :
    q ∈ (A.toLowerRamificationFiltration.quotientMapOfLe hmn).ker ↔
      ∃ σ : G, A.actionQuotient σ ∈ A.principalUnits.subgroup m ∧
        A.toLowerRamificationFiltration.quotientMk n σ = q

theorem

mem_quotientKernelOfLe_iff_exists_actionQuotient_mem_repr

L1474 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.mem_quotientKernelOfLe_iff_exists_actionQuotient_mem_repr

Documentation

Membership in the named kernel subgroup of the action-defined quotient map G/G_n → G/G_m, expressed by an action quotient representative in U^m.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem mem_quotientKernelOfLe_iff_exists_actionQuotient_mem_repr
    {m n : ℕ} (hmn : m ≤ n)
    (q : A.toLowerRamificationFiltration.quotient n) :
    q ∈ A.toLowerRamificationFiltration.quotientKernelOfLe hmn ↔
      ∃ σ : G, A.actionQuotient σ ∈ A.principalUnits.subgroup m ∧
        A.toLowerRamificationFiltration.quotientMk n σ = q

def

quotientKernelQuotientKerEquivQuotientKernelOfLe

L1489 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.quotientKernelQuotientKerEquivQuotientKernelOfLe

Documentation

First isomorphism theorem inside action-defined ramification kernels: (G_l/G_n)/ker(G_l/G_n → G_l/G_m) ≃ G_l/G_m, for l ≤ m ≤ n. The kernel is identified with G_m/G_n by AntitoneNormalSubgroupFiltration.quotientKernelMapOfLe_ker_eq.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

def quotientKernelQuotientKerEquivQuotientKernelOfLe {l m n : ℕ}
    (hlm : l ≤ m) (hmn : m ≤ n) :
      A.toLowerRamificationFiltration.quotientKernelOfLe
        (le_trans hlm hmn) ⧸
        (A.toLowerRamificationFiltration.quotientKernelMapOfLe hlm hmn).ker ≃*
      A.toLowerRamificationFiltration.quotientKernelOfLe hlm

theorem

quotientKernelQuotientKerEquivQuotientKernelOfLe_mk'

L1499 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.quotientKernelQuotientKerEquivQuotientKernelOfLe_mk'

Documentation

States the theorem quotientKernelQuotientKerEquivQuotientKernelOfLe_mk'.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem quotientKernelQuotientKerEquivQuotientKernelOfLe_mk'
    {l m n : ℕ} (hlm : l ≤ m) (hmn : m ≤ n)
    (q :
      A.toLowerRamificationFiltration.quotientKernelOfLe
        (le_trans hlm hmn)) :
    A.quotientKernelQuotientKerEquivQuotientKernelOfLe hlm hmn
        (QuotientGroup.mk'
          (A.toLowerRamificationFiltration.quotientKernelMapOfLe hlm hmn).ker q) =
      A.toLowerRamificationFiltration.quotientKernelMapOfLe hlm hmn q

def

quotientKernelQuotientSubgroupOfEquivQuotientKernelOfLe

L1513 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.quotientKernelQuotientSubgroupOfEquivQuotientKernelOfLe

Documentation

Second-isomorphism-style form for action-defined ramification kernels: (G_l/G_n)/(G_m/G_n) ≃ G_l/G_m, for l ≤ m ≤ n.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

def quotientKernelQuotientSubgroupOfEquivQuotientKernelOfLe {l m n : ℕ}
    (hlm : l ≤ m) (hmn : m ≤ n) :
      A.toLowerRamificationFiltration.quotientKernelOfLe
        (le_trans hlm hmn) ⧸
        (A.toLowerRamificationFiltration.quotientKernelOfLe hmn).subgroupOf
          (A.toLowerRamificationFiltration.quotientKernelOfLe
            (le_trans hlm hmn)) ≃*
      A.toLowerRamificationFiltration.quotientKernelOfLe hlm

theorem

quotientKernelQuotientSubgroupOfEquivQuotientKernelOfLe_mk'

L1525 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.quotientKernelQuotientSubgroupOfEquivQuotientKernelOfLe_mk'

Documentation

States the theorem quotientKernelQuotientSubgroupOfEquivQuotientKernelOfLe_mk'.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem quotientKernelQuotientSubgroupOfEquivQuotientKernelOfLe_mk'
    {l m n : ℕ} (hlm : l ≤ m) (hmn : m ≤ n)
    (q :
      A.toLowerRamificationFiltration.quotientKernelOfLe
        (le_trans hlm hmn)) :
    A.quotientKernelQuotientSubgroupOfEquivQuotientKernelOfLe hlm hmn
        (QuotientGroup.mk'
          ((A.toLowerRamificationFiltration.quotientKernelOfLe hmn).subgroupOf
            (A.toLowerRamificationFiltration.quotientKernelOfLe
              (le_trans hlm hmn))) q) =
      A.toLowerRamificationFiltration.quotientKernelMapOfLe hlm hmn q

theorem

card_quotientKernelQuotientSubgroupOfLe

L1541 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.card_quotientKernelQuotientSubgroupOfLe

Documentation

Cardinality form of the action-defined second-isomorphism quotient compatibility (G_l/G_n)/(G_m/G_n) ≃ G_l/G_m.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem card_quotientKernelQuotientSubgroupOfLe {l m n : ℕ}
    (hlm : l ≤ m) (hmn : m ≤ n) [Finite G] :
    Nat.card
        (A.toLowerRamificationFiltration.quotientKernelOfLe
            (le_trans hlm hmn) ⧸
          (A.toLowerRamificationFiltration.quotientKernelOfLe hmn).subgroupOf
            (A.toLowerRamificationFiltration.quotientKernelOfLe
              (le_trans hlm hmn))) =
      Nat.card (A.toLowerRamificationFiltration.quotientKernelOfLe hlm)

def

quotientQuotientKernelOfLeEquivQuotient

L1555 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.quotientQuotientKernelOfLeEquivQuotient

Documentation

First isomorphism theorem for action-defined level-change maps: (G/G_n)/(G_m/G_n) ≃ G/G_m.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

def quotientQuotientKernelOfLeEquivQuotient
    {m n : ℕ} (hmn : m ≤ n) :
    A.toLowerRamificationFiltration.quotient n ⧸
        A.toLowerRamificationFiltration.quotientKernelOfLe hmn ≃*
      A.toLowerRamificationFiltration.quotient m

theorem

quotientQuotientKernelOfLeEquivQuotient_mk'

L1563 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.quotientQuotientKernelOfLeEquivQuotient_mk'

Documentation

States the theorem quotientQuotientKernelOfLeEquivQuotient_mk'.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem quotientQuotientKernelOfLeEquivQuotient_mk'
    {m n : ℕ} (hmn : m ≤ n)
    (q : A.toLowerRamificationFiltration.quotient n) :
    A.quotientQuotientKernelOfLeEquivQuotient hmn
        (QuotientGroup.mk'
          (A.toLowerRamificationFiltration.quotientKernelOfLe hmn) q) =
      A.toLowerRamificationFiltration.quotientMapOfLe hmn q

theorem

quotientQuotientKernelOfLeEquivQuotient_mk'_mk'

L1574 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.quotientQuotientKernelOfLeEquivQuotient_mk'_mk'

Documentation

States the theorem quotientQuotientKernelOfLeEquivQuotient_mk'_mk'.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem quotientQuotientKernelOfLeEquivQuotient_mk'_mk'
    {m n : ℕ} (hmn : m ≤ n) (σ : G) :
    A.quotientQuotientKernelOfLeEquivQuotient hmn
        (QuotientGroup.mk'
          (A.toLowerRamificationFiltration.quotientKernelOfLe hmn)
          (A.toLowerRamificationFiltration.quotientMk n σ)) =
      A.toLowerRamificationFiltration.quotientMk m σ

theorem

quotientKernelOfLe_refl_eq_bot

L1586 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.quotientKernelOfLe_refl_eq_bot

Documentation

The action-defined kernel subgroup for the identity level-change map is trivial.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem quotientKernelOfLe_refl_eq_bot (n : ℕ) :
    A.toLowerRamificationFiltration.quotientKernelOfLe
      (le_rfl : n ≤ n) = ⊥

theorem

quotientMapOfLe_mk_mem_quotientKernelOfLe_iff_actionQuotient_mem

L1594 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.quotientMapOfLe_mk_mem_quotientKernelOfLe_iff_actionQuotient_mem

Documentation

Representative criterion for the image of an action-defined quotient class to lie in a coarser kernel subgroup, expanded as membership of the action quotient in U^l.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem quotientMapOfLe_mk_mem_quotientKernelOfLe_iff_actionQuotient_mem
    {l m n : ℕ} (hlm : l ≤ m) (hmn : m ≤ n) (σ : G) :
    A.toLowerRamificationFiltration.quotientMapOfLe hmn
        (A.toLowerRamificationFiltration.quotientMk n σ) ∈
      A.toLowerRamificationFiltration.quotientKernelOfLe hlm ↔
      A.actionQuotient σ ∈ A.principalUnits.subgroup l

theorem

quotientMapOfLe_mem_quotientKernelOfLe_iff_exists_actionQuotient_mem_repr

L1608 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.quotientMapOfLe_mem_quotientKernelOfLe_iff_exists_actionQuotient_mem_repr

Documentation

Arbitrary-class criterion for the image of an action-defined quotient class to lie in a coarser kernel subgroup, expressed by an action quotient representative in U^l.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem quotientMapOfLe_mem_quotientKernelOfLe_iff_exists_actionQuotient_mem_repr
    {l m n : ℕ} (hlm : l ≤ m) (hmn : m ≤ n)
    (q : A.toLowerRamificationFiltration.quotient n) :
    A.toLowerRamificationFiltration.quotientMapOfLe hmn q ∈
        A.toLowerRamificationFiltration.quotientKernelOfLe hlm ↔
      ∃ σ : G, A.actionQuotient σ ∈ A.principalUnits.subgroup l ∧
        A.toLowerRamificationFiltration.quotientMk n σ = q

theorem

quotientMapOfLe_eq_iff_exists_actionQuotient_mem_div_repr

L1624 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.quotientMapOfLe_eq_iff_exists_actionQuotient_mem_div_repr

Documentation

Arbitrary-class equality criterion for the action-defined quotient map G/G_n → G/G_m, expressed by an action quotient representative of q / r in U^m.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem quotientMapOfLe_eq_iff_exists_actionQuotient_mem_div_repr
    {m n : ℕ} (hmn : m ≤ n)
    (q r : A.toLowerRamificationFiltration.quotient n) :
    A.toLowerRamificationFiltration.quotientMapOfLe hmn q =
        A.toLowerRamificationFiltration.quotientMapOfLe hmn r ↔
      ∃ σ : G, A.actionQuotient σ ∈ A.principalUnits.subgroup m ∧
        A.toLowerRamificationFiltration.quotientMk n σ = q / r

def

quotientKernelByNextKernelEquivGradedPiece

L1638 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.quotientKernelByNextKernelEquivGradedPiece

Documentation

At every finite level N ≥ n + 1, the action-defined nth graded piece is the quotient of finite-level kernels (G_n/G_N)/(G_{n+1}/G_N).

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

def quotientKernelByNextKernelEquivGradedPiece {n N : ℕ} (hN : n + 1 ≤ N) :
    A.toLowerRamificationFiltration.quotientKernelOfLe
        (le_trans (Nat.le_succ n) hN) ⧸
        (A.toLowerRamificationFiltration.quotientKernelOfLe hN).subgroupOf
          (A.toLowerRamificationFiltration.quotientKernelOfLe
            (le_trans (Nat.le_succ n) hN)) ≃*
      A.toLowerRamificationFiltration.gradedPiece n

theorem

gradedPieceEquivQuotientKernel_quotientKernelByNextKernel_mk'

L1648 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.gradedPieceEquivQuotientKernel_quotientKernelByNextKernel_mk'

Documentation

States the theorem gradedPieceEquivQuotientKernel_quotientKernelByNextKernel_mk'.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem gradedPieceEquivQuotientKernel_quotientKernelByNextKernel_mk'
    {n N : ℕ} (hN : n + 1 ≤ N)
    (q :
      A.toLowerRamificationFiltration.quotientKernelOfLe
        (le_trans (Nat.le_succ n) hN)) :
    A.toLowerRamificationFiltration.gradedPieceEquivQuotientKernel n
        (A.quotientKernelByNextKernelEquivGradedPiece hN
          (QuotientGroup.mk'
            ((A.toLowerRamificationFiltration.quotientKernelOfLe hN).subgroupOf
              (A.toLowerRamificationFiltration.quotientKernelOfLe
                (le_trans (Nat.le_succ n) hN))) q)) =
      A.toLowerRamificationFiltration.quotientKernelMapOfLe (Nat.le_succ n) hN q

theorem

card_quotientKernelByNextKernel_eq_gradedPiece

L1665 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.card_quotientKernelByNextKernel_eq_gradedPiece

Documentation

Cardinality form of the action-defined finite-level graded-piece compatibility (G_n/G_N)/(G_{n+1}/G_N) ≃ G_n/G_{n+1}.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem card_quotientKernelByNextKernel_eq_gradedPiece {n N : ℕ}
    (hN : n + 1 ≤ N) [Finite G] :
    Nat.card
        (A.toLowerRamificationFiltration.quotientKernelOfLe
            (le_trans (Nat.le_succ n) hN) ⧸
          (A.toLowerRamificationFiltration.quotientKernelOfLe hN).subgroupOf
            (A.toLowerRamificationFiltration.quotientKernelOfLe
              (le_trans (Nat.le_succ n) hN))) =
      Nat.card (A.toLowerRamificationFiltration.gradedPiece n)

theorem

gradedPieceMk_eq_one_iff_actionDepthAtLeast

L1679 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.gradedPieceMk_eq_one_iff_actionDepthAtLeast

Documentation

Representative criterion for the identity class in the action-defined graded piece G_n/G_{n+1}.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem gradedPieceMk_eq_one_iff_actionDepthAtLeast
    (n : ℕ) (σ : A.lowerRamificationGroup n) :
    A.toLowerRamificationFiltration.gradedPieceMk n σ = 1 ↔
      A.actionDepthAtLeast (n + 1) (σ : G)

theorem

gradedPieceMk_eq_one_iff_actionQuotient_mem

L1690 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.gradedPieceMk_eq_one_iff_actionQuotient_mem

Documentation

Representative criterion for the identity class in the action-defined graded piece G_n/G_{n+1}, expanded as membership of the action quotient in U^{n+1}.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem gradedPieceMk_eq_one_iff_actionQuotient_mem
    (n : ℕ) (σ : A.lowerRamificationGroup n) :
    A.toLowerRamificationFiltration.gradedPieceMk n σ = 1 ↔
      A.actionQuotient (σ : G) ∈ A.principalUnits.subgroup (n + 1)

theorem

gradedPieceMk_eq_iff_actionDepthAtLeast_div

L1699 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.gradedPieceMk_eq_iff_actionDepthAtLeast_div

Documentation

Representative equality criterion in the action-defined graded piece G_n/G_{n+1}, in right-quotient form.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem gradedPieceMk_eq_iff_actionDepthAtLeast_div
    (n : ℕ) (σ τ : A.lowerRamificationGroup n) :
    A.toLowerRamificationFiltration.gradedPieceMk n σ =
      A.toLowerRamificationFiltration.gradedPieceMk n τ ↔
      A.actionDepthAtLeast (n + 1)
        ((σ / τ : A.lowerRamificationGroup n) : G)

theorem

gradedPieceMk_eq_iff_actionQuotient_div_mem

L1713 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.gradedPieceMk_eq_iff_actionQuotient_div_mem

Documentation

Representative equality criterion in the action-defined graded piece G_n/G_{n+1}, in right-quotient form, expanded as membership of the action quotient in U^{n+1}.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem gradedPieceMk_eq_iff_actionQuotient_div_mem
    (n : ℕ) (σ τ : A.lowerRamificationGroup n) :
    A.toLowerRamificationFiltration.gradedPieceMk n σ =
      A.toLowerRamificationFiltration.gradedPieceMk n τ ↔
      A.actionQuotient
          (((σ / τ : A.lowerRamificationGroup n) : G)) ∈
        A.principalUnits.subgroup (n + 1)

theorem

gradedPieceMk_eq_iff_actionDepthAtLeast_inv_mul

L1726 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.gradedPieceMk_eq_iff_actionDepthAtLeast_inv_mul

Documentation

Representative equality criterion in the action-defined graded piece G_n/G_{n+1}, in left-quotient form.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem gradedPieceMk_eq_iff_actionDepthAtLeast_inv_mul
    (n : ℕ) (σ τ : A.lowerRamificationGroup n) :
    A.toLowerRamificationFiltration.gradedPieceMk n σ =
      A.toLowerRamificationFiltration.gradedPieceMk n τ ↔
      A.actionDepthAtLeast (n + 1)
        ((τ⁻¹ * σ : A.lowerRamificationGroup n) : G)

theorem

gradedPieceMk_eq_iff_actionQuotient_inv_mul_mem

L1741 ↗

RamificationTheory.DiscreteValuationField.ValuationActionRamification.gradedPieceMk_eq_iff_actionQuotient_inv_mul_mem

Documentation

Representative equality criterion in the action-defined graded piece G_n/G_{n+1}, in left-quotient form, expanded as membership of the action quotient in U^{n+1}.

Source context 8 commands

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

namespace RamificationTheory
open LocalFieldTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace ValuationActionRamification
variable {G : Type u} [Group G] {K : Type v} [Group K]
variable (A : ValuationActionRamification G K)

Lean source · statement

theorem gradedPieceMk_eq_iff_actionQuotient_inv_mul_mem
    (n : ℕ) (σ τ : A.lowerRamificationGroup n) :
    A.toLowerRamificationFiltration.gradedPieceMk n σ =
      A.toLowerRamificationFiltration.gradedPieceMk n τ ↔
      A.actionQuotient
          (((τ⁻¹ * σ : A.lowerRamificationGroup n) : G)) ∈
        A.principalUnits.subgroup (n + 1)

Module documentation

Ramification filtrations

Declarations