Module

Tower.lean

Nyll.ValuedFieldTheory.Ramification.Herbrand.Tower

22 declarations indexed from sourceView source ↗

Module documentation

Finite-group sources for Herbrand's theorem

This file isolates the part of the Herbrand quotient theorem which is independent of valuations. A discrete nonarchimedean depth has the two properties of i(σ) = v(σ(a) - a) used in the ramification-depth proof: multiplication does not decrease the minimum depth, and it is exactly the minimum when the two depths differ.

For a finite group modulo a normal subgroup, every nontrivial quotient fibre has a representative of maximal (finite) depth. The main result below proves the identity

i(σ τ) = min (i(σ), i(τ))

for such a representative σ and every τ in the normal subgroup. The remaining valued-field input for the Herbrand quotient theorem is the quotient-depth identity: the depth on the quotient is the normalized sum of the depths in this fibre. That input is deliberately not packaged here as a hypothesis or data field.

Imports1

Nyll.ValuedFieldTheory.Ramification.GaloisValuation.Ramification

Imported by2

structure

NonarchimedeanDepth

L44 ↗

RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth

Documentation

The purely group-theoretic laws of the discrete depth used in the proof of Herbrand's theorem. The value ⊤ occurs exactly at the identity.

Source context 5 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
variable {G : Type u} [Group G]

Lean source · full declaration

structure NonarchimedeanDepth (G : Type u) [Group G] where
  /-- The discrete nonarchimedean depth of each group element. -/
  depth : G → WithTop ℕ
  /-- An element has infinite depth exactly when it is the identity. -/
  depth_eq_top_iff : ∀ σ, depth σ = ⊤ ↔ σ = 1
  /-- The depth of a product is at least the minimum depth of its factors. -/
  depth_mul_ge_min : ∀ σ τ, min (depth σ) (depth τ) ≤ depth (σ * τ)
  /-- Factors of unequal depth give a product whose depth is their minimum. -/
  depth_mul_eq_min_of_ne :
    ∀ {σ τ}, depth σ ≠ depth τ → depth (σ * τ) = min (depth σ) (depth τ)
  /-- Depth is invariant under conjugation. -/
  depth_conj : ∀ γ σ, depth (γ * σ * γ⁻¹) = depth σ

theorem

depth_one

L62 ↗

RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.depth_one

Documentation

States the theorem depth_one.

Source context 7 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
variable {G : Type u} [Group G]
namespace NonarchimedeanDepth
variable (D : NonarchimedeanDepth G)

Lean source · statement

theorem depth_one : D.depth 1 = ⊤

theorem

depth_ne_top_iff

L66 ↗

RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.depth_ne_top_iff

Documentation

States the theorem depth_ne_top_iff.

Source context 7 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
variable {G : Type u} [Group G]
namespace NonarchimedeanDepth
variable (D : NonarchimedeanDepth G)

Lean source · statement

theorem depth_ne_top_iff {σ : G} : D.depth σ ≠ ⊤ ↔ σ ≠ 1

abbrev

QuotientFiber

L73 ↗

RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.QuotientFiber

Documentation

The fibre of the canonical quotient map over q.

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
variable {G : Type u} [Group G]
namespace NonarchimedeanDepth
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]

Lean source · statement

abbrev QuotientFiber (q : G ⧸ H) : Type u

instance

subgroupFintype

L76 ↗

RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.subgroupFintype

Source context 8 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
variable {G : Type u} [Group G]
namespace NonarchimedeanDepth
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]

Lean source · statement

instance subgroupFintype [Finite G] : Fintype H

instance

groupFintype

L79 ↗

RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.groupFintype

Source context 9 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
variable {G : Type u} [Group G]
namespace NonarchimedeanDepth
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance subgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H

Lean source · statement

instance groupFintype [Finite G] : Fintype G

instance

quotientFiberFintype

L82 ↗

RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.quotientFiberFintype

Source context 10 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
variable {G : Type u} [Group G]
namespace NonarchimedeanDepth
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance subgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance groupFintype [Finite G] : Fintype G :=
  Fintype.ofFinite G

Lean source · statement

instance quotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q)

instance

quotientFintype

L86 ↗

RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.quotientFintype

Source context 11 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
variable {G : Type u} [Group G]
namespace NonarchimedeanDepth
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance subgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance groupFintype [Finite G] : Fintype G :=
  Fintype.ofFinite G
noncomputable local instance quotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)

Lean source · statement

instance quotientFintype [Finite G] : Fintype (G ⧸ H)

instance

quotientFiber_nonempty

L90 ↗

RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.quotientFiber_nonempty

Documentation

Provides the instance quotientFiber_nonempty.

Source context 12 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
variable {G : Type u} [Group G]
namespace NonarchimedeanDepth
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance subgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance groupFintype [Finite G] : Fintype G :=
  Fintype.ofFinite G
noncomputable local instance quotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
noncomputable local instance quotientFintype [Finite G] : Fintype (G ⧸ H) :=
  Fintype.ofFinite (G ⧸ H)

Lean source · statement

instance quotientFiber_nonempty (q : G ⧸ H) : Nonempty (QuotientFiber H q)

theorem

ne_one_of_mem_quotientFiber

L95 ↗

RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.ne_one_of_mem_quotientFiber

Documentation

States the theorem ne_one_of_mem_quotientFiber.

Source context 12 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
variable {G : Type u} [Group G]
namespace NonarchimedeanDepth
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance subgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance groupFintype [Finite G] : Fintype G :=
  Fintype.ofFinite G
noncomputable local instance quotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
noncomputable local instance quotientFintype [Finite G] : Fintype (G ⧸ H) :=
  Fintype.ofFinite (G ⧸ H)

Lean source · statement

theorem ne_one_of_mem_quotientFiber {q : G ⧸ H} (hq : q ≠ 1)
    (σ : QuotientFiber H q) : (σ : G) ≠ 1

theorem

depth_ne_top_of_mem_quotientFiber

L103 ↗

RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.depth_ne_top_of_mem_quotientFiber

Documentation

States the theorem depth_ne_top_of_mem_quotientFiber.

Source context 12 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
variable {G : Type u} [Group G]
namespace NonarchimedeanDepth
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance subgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance groupFintype [Finite G] : Fintype G :=
  Fintype.ofFinite G
noncomputable local instance quotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
noncomputable local instance quotientFintype [Finite G] : Fintype (G ⧸ H) :=
  Fintype.ofFinite (G ⧸ H)

Lean source · statement

theorem depth_ne_top_of_mem_quotientFiber {q : G ⧸ H} (hq : q ≠ 1)
    (σ : QuotientFiber H q) : D.depth (σ : G) ≠ ⊤

def

quotientFiberDepth

L108 ↗

RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.quotientFiberDepth

Documentation

The finite natural depth of an element in a nontrivial quotient fibre.

Source context 12 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
variable {G : Type u} [Group G]
namespace NonarchimedeanDepth
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance subgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance groupFintype [Finite G] : Fintype G :=
  Fintype.ofFinite G
noncomputable local instance quotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
noncomputable local instance quotientFintype [Finite G] : Fintype (G ⧸ H) :=
  Fintype.ofFinite (G ⧸ H)

Lean source · statement

def quotientFiberDepth {q : G ⧸ H} (hq : q ≠ 1)
    (σ : QuotientFiber H q) : ℕ

theorem

coe_quotientFiberDepth

L113 ↗

RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.coe_quotientFiberDepth

Documentation

States the theorem coe_quotientFiberDepth.

Source context 12 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
variable {G : Type u} [Group G]
namespace NonarchimedeanDepth
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance subgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance groupFintype [Finite G] : Fintype G :=
  Fintype.ofFinite G
noncomputable local instance quotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
noncomputable local instance quotientFintype [Finite G] : Fintype (G ⧸ H) :=
  Fintype.ofFinite (G ⧸ H)

Lean source · statement

theorem coe_quotientFiberDepth {q : G ⧸ H} (hq : q ≠ 1)
    (σ : QuotientFiber H q) :
    (D.quotientFiberDepth H hq σ : WithTop ℕ) = D.depth (σ : G)

theorem

exists_maximal_depth_representative

L122 ↗

RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.exists_maximal_depth_representative

Documentation

Every nontrivial fibre of a finite quotient has a representative of maximal depth. The conclusion is stated back in WithTop ℕ, rather than in terms of the auxiliary untop, so it can be fed directly into the valuation identity used in the Herbrand quotient theorem.

Source context 12 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
variable {G : Type u} [Group G]
namespace NonarchimedeanDepth
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance subgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance groupFintype [Finite G] : Fintype G :=
  Fintype.ofFinite G
noncomputable local instance quotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
noncomputable local instance quotientFintype [Finite G] : Fintype (G ⧸ H) :=
  Fintype.ofFinite (G ⧸ H)

Lean source · statement

theorem exists_maximal_depth_representative [Finite G]
    {q : G ⧸ H} (hq : q ≠ 1) :
    ∃ σ : G, QuotientGroup.mk' H σ = q ∧
      ∀ γ : G, QuotientGroup.mk' H γ = q → D.depth γ ≤ D.depth σ

def

rightCosetEquivQuotientFiber

L142 ↗

RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.rightCosetEquivQuotientFiber

Documentation

A right coset is naturally equivalent to the corresponding quotient fibre. This is the finite-sum reindexing used after choosing a maximal-depth representative.

Source context 12 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
variable {G : Type u} [Group G]
namespace NonarchimedeanDepth
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance subgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance groupFintype [Finite G] : Fintype G :=
  Fintype.ofFinite G
noncomputable local instance quotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
noncomputable local instance quotientFintype [Finite G] : Fintype (G ⧸ H) :=
  Fintype.ofFinite (G ⧸ H)

Lean source · full declaration

def rightCosetEquivQuotientFiber (σ : G) : H ≃ QuotientFiber H (QuotientGroup.mk' H σ) where
  toFun τ := ⟨σ * τ, by
    rw [map_mul]
    simp [(QuotientGroup.eq_one_iff (N := H) (x := (τ : G))).2 τ.property]⟩
  invFun γ := ⟨σ⁻¹ * γ, by
    apply (QuotientGroup.eq_one_iff (N := H) (x := σ⁻¹ * (γ : G))).1
    change QuotientGroup.mk' H (σ⁻¹ * (γ : G)) = 1
    rw [map_mul, map_inv, γ.property]
    simp⟩
  left_inv τ := by
    apply Subtype.ext
    simp
  right_inv γ := by
    apply Subtype.ext
    simp

theorem

card_quotientFiber

L159 ↗

RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.card_quotientFiber

Documentation

States the theorem card_quotientFiber.

Source context 12 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
variable {G : Type u} [Group G]
namespace NonarchimedeanDepth
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance subgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance groupFintype [Finite G] : Fintype G :=
  Fintype.ofFinite G
noncomputable local instance quotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
noncomputable local instance quotientFintype [Finite G] : Fintype (G ⧸ H) :=
  Fintype.ofFinite (G ⧸ H)

Lean source · statement

theorem card_quotientFiber [Finite G] (σ : G) :
    Fintype.card (QuotientFiber H (QuotientGroup.mk' H σ)) = Fintype.card H

theorem

sum_quotientFiber_eq_sum_subgroup

L166 ↗

RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.sum_quotientFiber_eq_sum_subgroup

Documentation

Reindex a sum over a quotient fibre by multiplication with elements of the normal subgroup.

Source context 12 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
variable {G : Type u} [Group G]
namespace NonarchimedeanDepth
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance subgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance groupFintype [Finite G] : Fintype G :=
  Fintype.ofFinite G
noncomputable local instance quotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
noncomputable local instance quotientFintype [Finite G] : Fintype (G ⧸ H) :=
  Fintype.ofFinite (G ⧸ H)

Lean source · statement

theorem sum_quotientFiber_eq_sum_subgroup [Finite G]
    {M : Type*} [AddCommMonoid M] (f : G → M) (σ : G) :
    (∑ γ : QuotientFiber H (QuotientGroup.mk' H σ), f (γ : G)) =
      ∑ τ : H, f (σ * τ)

theorem

sum_quotientFiber

L179 ↗

RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.sum_quotientFiber

Documentation

Partition a finite sum over G into the fibres of the quotient map.

Source context 12 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
variable {G : Type u} [Group G]
namespace NonarchimedeanDepth
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance subgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance groupFintype [Finite G] : Fintype G :=
  Fintype.ofFinite G
noncomputable local instance quotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
noncomputable local instance quotientFintype [Finite G] : Fintype (G ⧸ H) :=
  Fintype.ofFinite (G ⧸ H)

Lean source · statement

theorem sum_quotientFiber [Finite G]
    {M : Type*} [AddCommMonoid M] (f : G → M) :
    (∑ q : G ⧸ H, ∑ σ : QuotientFiber H q, f (σ : G)) = ∑ σ : G, f σ

theorem

depth_mul_eq_min_of_maximal_representative

L196 ↗

RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.depth_mul_eq_min_of_maximal_representative

Documentation

The maximal-representative identity in the proof of Herbrand's theorem. If σ has maximal depth in its quotient fibre, then multiplication by every τ ∈ H truncates the depth exactly at i(σ).

Source context 12 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
variable {G : Type u} [Group G]
namespace NonarchimedeanDepth
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance subgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance groupFintype [Finite G] : Fintype G :=
  Fintype.ofFinite G
noncomputable local instance quotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
noncomputable local instance quotientFintype [Finite G] : Fintype (G ⧸ H) :=
  Fintype.ofFinite (G ⧸ H)

Lean source · statement

theorem depth_mul_eq_min_of_maximal_representative
    {σ : G}
    (hmax : ∀ γ : G, QuotientGroup.mk' H γ = QuotientGroup.mk' H σ →
      D.depth γ ≤ D.depth σ)
    (τ : H) :
    D.depth (σ * τ) = min (D.depth (τ : G)) (D.depth σ)

theorem

sum_depth_quotientFiber_eq_sum_min_of_maximal_representative

L216 ↗

RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.sum_depth_quotientFiber_eq_sum_min_of_maximal_representative

Documentation

The fibre-sum form of the maximal-representative identity. Composing f with a finite-depth cast gives exactly the sum appearing in the Herbrand quotient theorem, after the quotient-depth identity supplies the quotient-depth average.

Source context 12 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
variable {G : Type u} [Group G]
namespace NonarchimedeanDepth
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance subgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance groupFintype [Finite G] : Fintype G :=
  Fintype.ofFinite G
noncomputable local instance quotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
noncomputable local instance quotientFintype [Finite G] : Fintype (G ⧸ H) :=
  Fintype.ofFinite (G ⧸ H)

Lean source · statement

theorem sum_depth_quotientFiber_eq_sum_min_of_maximal_representative
    [Finite G] {M : Type*} [AddCommMonoid M]
    (f : WithTop ℕ → M) {σ : G}
    (hmax : ∀ γ : G, QuotientGroup.mk' H γ = QuotientGroup.mk' H σ →
      D.depth γ ≤ D.depth σ) :
    (∑ γ : QuotientFiber H (QuotientGroup.mk' H σ), f (D.depth (γ : G))) =
      ∑ τ : H, f (min (D.depth (τ : G)) (D.depth σ))

theorem

exists_representative_depth_mul_eq_min

L230 ↗

RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.exists_representative_depth_mul_eq_min

Documentation

Combined existence form used verbatim in the group-theoretic step of the Herbrand quotient theorem.

Source context 12 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
variable {G : Type u} [Group G]
namespace NonarchimedeanDepth
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance subgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance groupFintype [Finite G] : Fintype G :=
  Fintype.ofFinite G
noncomputable local instance quotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
noncomputable local instance quotientFintype [Finite G] : Fintype (G ⧸ H) :=
  Fintype.ofFinite (G ⧸ H)

Lean source · statement

theorem exists_representative_depth_mul_eq_min [Finite G]
    {q : G ⧸ H} (hq : q ≠ 1) :
    ∃ σ : G, QuotientGroup.mk' H σ = q ∧
      ∀ τ : H, D.depth (σ * τ) = min (D.depth (τ : G)) (D.depth σ)

theorem

exists_representative_sum_depth_eq_sum_min

L243 ↗

RamificationTheory.DiscreteValuationField.HerbrandGroupTheory.NonarchimedeanDepth.exists_representative_sum_depth_eq_sum_min

Documentation

Existence form of the fibre-sum identity for a nontrivial quotient element.

Source context 12 commands

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

noncomputable section
universe u
namespace RamificationTheory.DiscreteValuationField
namespace HerbrandGroupTheory
variable {G : Type u} [Group G]
namespace NonarchimedeanDepth
variable (D : NonarchimedeanDepth G)
variable (H : Subgroup G) [H.Normal]
noncomputable local instance subgroupFintype [Finite G] : Fintype H :=
  Fintype.ofFinite H
noncomputable local instance groupFintype [Finite G] : Fintype G :=
  Fintype.ofFinite G
noncomputable local instance quotientFiberFintype [Finite G] (q : G ⧸ H) :
    Fintype (QuotientFiber H q) :=
  Fintype.ofFinite (QuotientFiber H q)
noncomputable local instance quotientFintype [Finite G] : Fintype (G ⧸ H) :=
  Fintype.ofFinite (G ⧸ H)

Lean source · statement

theorem exists_representative_sum_depth_eq_sum_min [Finite G]
    {M : Type*} [AddCommMonoid M] (f : WithTop ℕ → M)
    {q : G ⧸ H} (hq : q ≠ 1) :
    ∃ σ : G, QuotientGroup.mk' H σ = q ∧
      (∑ γ : QuotientFiber H q, f (D.depth (γ : G))) =
        ∑ τ : H, f (min (D.depth (τ : G)) (D.depth σ))

Module documentation

Finite-group sources for Herbrand's theorem

Declarations