Module

RamificationQuotients.lean

Nyll.ValuedFieldTheory.Ramification.GaloisValuation.RamificationQuotients

63 declarations indexed from sourceView source ↗

Module documentation

Named quotients of antitone normal-subgroup filtrations

This module owns the opaque quotient carriers of a lower ramification filtration and their construction, elimination, lifting, and mapping API. Arithmetic Herbrand functions and valuation-action specializations live in RamificationTheory.GaloisValuation.Ramification.

Named quotient boundaries

The four ramification quotient carriers are opaque public objects. Raw QuotientGroup presentations occur only in the concrete equivalences and in the implementation of the operations below.

Imports1

Mathlib.GroupTheory.QuotientGroup.Finite

Imported by2

structure

AntitoneNormalSubgroupFiltration

L30 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration

Documentation

A generic antitone filtration by normal subgroups. This interface contains only the group-theoretic laws; arithmetic lower ramification filtrations are canonical values constructed from valued extensions.

Source context 4 commands

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

noncomputable section
universe u v
namespace RamificationTheory
namespace DiscreteValuationField

Lean source · full declaration

structure AntitoneNormalSubgroupFiltration (G : Type u) [Group G] where
  /-- The subgroup at each lower-filtration index. -/
  lower : ℕ → Subgroup G
  /-- Every subgroup in the lower filtration is normal. -/
  lower_normal : ∀ n : ℕ, (lower n).Normal
  /-- The lower filtration decreases as its index increases. -/
  antitone : ∀ {m n : ℕ}, m ≤ n → lower n ≤ lower m

instance

lower_normal_instance

L43 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.lower_normal_instance

Documentation

Provides the instance lower_normal_instance.

Source context 6 commands

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

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

Lean source · statement

instance lower_normal_instance (n : ℕ) : (F.lower n).Normal

def

quotient

L47 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotient

Documentation

The quotient by the nth lower ramification group.

Source context 6 commands

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

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

Lean source · statement

def quotient (n : ℕ) : Type u

def

subquotient

L53 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.subquotient

Documentation

The subquotient G_m / G_n, used for ramification graded pieces when m ≤ n. The type is available for all m,n; under m ≤ n, G_n is a subgroup of G_m by antitonicity.

Source context 6 commands

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

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

Lean source · statement

def subquotient (m n : ℕ) : Type u

def

gradedPiece

L57 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.gradedPiece

Documentation

The lower ramification graded piece G_n/G_{n+1}.

Source context 6 commands

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

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

Lean source · statement

def gradedPiece (n : ℕ) : Type u

abbrev

inertiaSubgroup

L61 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.inertiaSubgroup

Documentation

The inertia subgroup G_0 of a lower ramification filtration.

Source context 6 commands

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

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

Lean source · statement

abbrev inertiaSubgroup : Subgroup G

theorem

lower_zero_eq_inertiaSubgroup

L65 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.lower_zero_eq_inertiaSubgroup

Documentation

States the theorem lower_zero_eq_inertiaSubgroup.

Source context 6 commands

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

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

Lean source · statement

theorem lower_zero_eq_inertiaSubgroup :
    F.lower 0 = F.inertiaSubgroup

abbrev

wildInertiaSubgroup

L70 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.wildInertiaSubgroup

Documentation

The wild inertia subgroup G_1 of a lower ramification filtration.

Source context 6 commands

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

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

Lean source · statement

abbrev wildInertiaSubgroup : Subgroup G

def

tameQuotient

L74 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.tameQuotient

Documentation

The tame quotient G_0/G_1.

Source context 6 commands

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

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

Lean source · statement

def tameQuotient : Type u

instance

inertiaSubgroup_normal

L78 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.inertiaSubgroup_normal

Documentation

Provides the instance inertiaSubgroup_normal.

Source context 6 commands

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

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

Lean source · statement

instance inertiaSubgroup_normal : F.inertiaSubgroup.Normal

instance

wildInertiaSubgroup_normal

L83 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.wildInertiaSubgroup_normal

Documentation

Provides the instance wildInertiaSubgroup_normal.

Source context 6 commands

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

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

Lean source · statement

instance wildInertiaSubgroup_normal : F.wildInertiaSubgroup.Normal

theorem

wildInertiaSubgroup_le_inertiaSubgroup

L88 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.wildInertiaSubgroup_le_inertiaSubgroup

Documentation

States the theorem wildInertiaSubgroup_le_inertiaSubgroup.

Source context 6 commands

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

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

Lean source · statement

theorem wildInertiaSubgroup_le_inertiaSubgroup :
    F.wildInertiaSubgroup ≤ F.inertiaSubgroup

instance

wildInertiaSubgroup_subgroupOf_inertiaSubgroup_normal

L93 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.wildInertiaSubgroup_subgroupOf_inertiaSubgroup_normal

Documentation

Provides the instance wildInertiaSubgroup_subgroupOf_inertiaSubgroup_normal.

Source context 6 commands

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

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

Lean source · statement

instance wildInertiaSubgroup_subgroupOf_inertiaSubgroup_normal :
    ((F.wildInertiaSubgroup).subgroupOf F.inertiaSubgroup).Normal

instance

quotientGroup

L105 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientGroup

Documentation

Provides the instance quotientGroup.

Source context 6 commands

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

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

Lean source · statement

instance quotientGroup (n : ℕ) : Group (F.quotient n)

instance

subquotientGroup

L110 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.subquotientGroup

Documentation

Provides the instance subquotientGroup.

Source context 6 commands

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

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

Lean source · statement

instance subquotientGroup (m n : ℕ) : Group (F.subquotient m n)

instance

gradedPieceGroup

L116 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.gradedPieceGroup

Documentation

Provides the instance gradedPieceGroup.

Source context 6 commands

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

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

Lean source · statement

instance gradedPieceGroup (n : ℕ) : Group (F.gradedPiece n)

instance

tameQuotientGroup

L123 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.tameQuotientGroup

Documentation

Provides the instance tameQuotientGroup.

Source context 6 commands

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

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

Lean source · statement

instance tameQuotientGroup : Group F.tameQuotient

def

quotientConcreteMulEquiv

L130 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientConcreteMulEquiv

Documentation

Concrete presentation of G/G_n.

Source context 6 commands

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

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

Lean source · statement

def quotientConcreteMulEquiv (n : ℕ) :
    F.quotient n ≃* G ⧸ F.lower n

def

subquotientConcreteMulEquiv

L135 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.subquotientConcreteMulEquiv

Documentation

Concrete presentation of G_m/G_n.

Source context 6 commands

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

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

Lean source · statement

def subquotientConcreteMulEquiv (m n : ℕ) :
    F.subquotient m n ≃*
      F.lower m ⧸ (F.lower n).subgroupOf (F.lower m)

def

gradedPieceEquivSubquotient

L141 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.gradedPieceEquivSubquotient

Documentation

The graded piece as its adjacent named subquotient.

Source context 6 commands

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

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

Lean source · statement

def gradedPieceEquivSubquotient (n : ℕ) :
    F.gradedPiece n ≃* F.subquotient n (n + 1)

def

gradedPieceConcreteMulEquiv

L146 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.gradedPieceConcreteMulEquiv

Documentation

Concrete presentation of G_n/G_{n+1}.

Source context 6 commands

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

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

Lean source · statement

def gradedPieceConcreteMulEquiv (n : ℕ) :
    F.gradedPiece n ≃*
      F.lower n ⧸ (F.lower (n + 1)).subgroupOf (F.lower n)

def

tameQuotientEquivGradedPiece

L153 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.tameQuotientEquivGradedPiece

Documentation

The tame quotient as the zeroth named graded piece.

Source context 6 commands

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

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

Lean source · statement

def tameQuotientEquivGradedPiece :
    F.tameQuotient ≃* F.gradedPiece 0

def

tameQuotientConcreteMulEquiv

L158 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.tameQuotientConcreteMulEquiv

Documentation

Concrete presentation of G_0/G_1.

Source context 6 commands

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

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

Lean source · statement

def tameQuotientConcreteMulEquiv :
    F.tameQuotient ≃*
      F.inertiaSubgroup ⧸
        (F.wildInertiaSubgroup).subgroupOf F.inertiaSubgroup

def

quotientMk

L166 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMk

Documentation

Canonical projection to G/G_n.

Source context 6 commands

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

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

Lean source · statement

def quotientMk (n : ℕ) : G →* F.quotient n

theorem

quotientMk_apply

L172 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMk_apply

Documentation

States the theorem quotientMk_apply.

Source context 6 commands

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

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

Lean source · statement

theorem quotientMk_apply (n : ℕ) (σ : G) :
    F.quotientConcreteMulEquiv n (F.quotientMk n σ) =
      QuotientGroup.mk' (F.lower n) σ

theorem

quotientMk_eq_one_iff

L179 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMk_eq_one_iff

Documentation

States the theorem quotientMk_eq_one_iff.

Source context 6 commands

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

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

Lean source · statement

theorem quotientMk_eq_one_iff (n : ℕ) (σ : G) :
    F.quotientMk n σ = 1 ↔ σ ∈ F.lower n

theorem

quotientMk_eq_iff

L193 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMk_eq_iff

Documentation

States the theorem quotientMk_eq_iff.

Source context 6 commands

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

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

Lean source · statement

theorem quotientMk_eq_iff (n : ℕ) (σ τ : G) :
    F.quotientMk n σ = F.quotientMk n τ ↔ σ / τ ∈ F.lower n

theorem

quotient_inductionOn

L207 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotient_inductionOn

Documentation

Eliminate a named ramification quotient through canonical representatives.

Source context 6 commands

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

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

Lean source · statement

theorem quotient_inductionOn (n : ℕ)
    {motive : F.quotient n → Prop} (q : F.quotient n)
    (h : ∀ σ : G, motive (F.quotientMk n σ)) :
    motive q

def

quotientLift

L217 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientLift

Documentation

Descend a homomorphism that kills the nth lower group.

Source context 6 commands

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

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

Lean source · statement

def quotientLift {H : Type v} [Group H] (n : ℕ)
    (f : G →* H) (h : F.lower n ≤ f.ker) :
    F.quotient n →* H

theorem

quotientLift_mk

L225 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientLift_mk

Documentation

States the theorem quotientLift_mk.

Source context 6 commands

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

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

Lean source · statement

theorem quotientLift_mk {H : Type v} [Group H] (n : ℕ)
    (f : G →* H) (h : F.lower n ≤ f.ker) (σ : G) :
    F.quotientLift n f h (F.quotientMk n σ) = f σ

def

quotientMap

L232 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMap

Documentation

Map between named ramification quotients induced by a group homomorphism.

Source context 6 commands

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

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

Lean source · statement

def quotientMap {H : Type v} [Group H]
    (E : AntitoneNormalSubgroupFiltration H) (n m : ℕ)
    (f : G →* H)
    (h : ∀ σ : G, σ ∈ F.lower n → f σ ∈ E.lower m) :
    F.quotient n →* E.quotient m

theorem

quotientMap_apply_mk

L244 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientMap_apply_mk

Documentation

States the theorem quotientMap_apply_mk.

Source context 6 commands

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

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

Lean source · statement

theorem quotientMap_apply_mk {H : Type v} [Group H]
    (E : AntitoneNormalSubgroupFiltration H) (n m : ℕ)
    (f : G →* H)
    (h : ∀ σ : G, σ ∈ F.lower n → f σ ∈ E.lower m) (σ : G) :
    F.quotientMap E n m f h (F.quotientMk n σ) =
      E.quotientMk m (f σ)

def

subquotientMk

L253 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.subquotientMk

Documentation

Canonical projection to G_m/G_n.

Source context 6 commands

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

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

Lean source · statement

def subquotientMk (m n : ℕ) : F.lower m →* F.subquotient m n

theorem

subquotientMk_apply

L259 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.subquotientMk_apply

Documentation

States the theorem subquotientMk_apply.

Source context 6 commands

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

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

Lean source · statement

theorem subquotientMk_apply (m n : ℕ) (σ : F.lower m) :
    F.subquotientConcreteMulEquiv m n (F.subquotientMk m n σ) =
      QuotientGroup.mk' ((F.lower n).subgroupOf (F.lower m)) σ

theorem

subquotientMk_eq_one_iff

L266 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.subquotientMk_eq_one_iff

Documentation

States the theorem subquotientMk_eq_one_iff.

Source context 6 commands

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

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

Lean source · statement

theorem subquotientMk_eq_one_iff (m n : ℕ) (σ : F.lower m) :
    F.subquotientMk m n σ = 1 ↔ (σ : G) ∈ F.lower n

theorem

subquotientMk_eq_iff

L284 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.subquotientMk_eq_iff

Documentation

States the theorem subquotientMk_eq_iff.

Source context 6 commands

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

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

Lean source · statement

theorem subquotientMk_eq_iff (m n : ℕ) (σ τ : F.lower m) :
    F.subquotientMk m n σ = F.subquotientMk m n τ ↔
      ((σ / τ : F.lower m) : G) ∈ F.lower n

theorem

subquotient_inductionOn

L304 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.subquotient_inductionOn

Documentation

Eliminate a named ramification subquotient.

Source context 6 commands

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

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

Lean source · statement

theorem subquotient_inductionOn (m n : ℕ)
    {motive : F.subquotient m n → Prop} (q : F.subquotient m n)
    (h : ∀ σ : F.lower m, motive (F.subquotientMk m n σ)) :
    motive q

def

subquotientLift

L315 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.subquotientLift

Documentation

Descend a homomorphism from G_m that kills the copy of G_n.

Source context 6 commands

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

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

Lean source · statement

def subquotientLift {H : Type v} [Group H] (m n : ℕ)
    (f : F.lower m →* H)
    (h : (F.lower n).subgroupOf (F.lower m) ≤ f.ker) :
    F.subquotient m n →* H

theorem

subquotientLift_mk

L325 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.subquotientLift_mk

Documentation

States the theorem subquotientLift_mk.

Source context 6 commands

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

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

Lean source · statement

theorem subquotientLift_mk {H : Type v} [Group H] (m n : ℕ)
    (f : F.lower m →* H)
    (h : (F.lower n).subgroupOf (F.lower m) ≤ f.ker)
    (σ : F.lower m) :
    F.subquotientLift m n f h (F.subquotientMk m n σ) = f σ

def

subquotientMap

L334 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.subquotientMap

Documentation

Map between named subquotients induced by a homomorphism of their upper groups which sends the lower relation into the target lower group.

Source context 6 commands

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

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

Lean source · statement

def subquotientMap {H : Type v} [Group H]
    (E : AntitoneNormalSubgroupFiltration H)
    (m n p q : ℕ) (f : F.lower m →* E.lower p)
    (h : ∀ σ : F.lower m, (σ : G) ∈ F.lower n →
      ((f σ : E.lower p) : H) ∈ E.lower q) :
    F.subquotient m n →* E.subquotient p q

theorem

subquotientMap_apply_mk

L347 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.subquotientMap_apply_mk

Documentation

States the theorem subquotientMap_apply_mk.

Source context 6 commands

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

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

Lean source · statement

theorem subquotientMap_apply_mk {H : Type v} [Group H]
    (E : AntitoneNormalSubgroupFiltration H)
    (m n p q : ℕ) (f : F.lower m →* E.lower p)
    (h : ∀ σ : F.lower m, (σ : G) ∈ F.lower n →
      ((f σ : E.lower p) : H) ∈ E.lower q)
    (σ : F.lower m) :
    F.subquotientMap E m n p q f h (F.subquotientMk m n σ) =
      E.subquotientMk p q (f σ)

def

gradedPieceMk

L358 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.gradedPieceMk

Documentation

Canonical projection to G_n/G_{n+1}.

Source context 6 commands

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

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

Lean source · statement

def gradedPieceMk (n : ℕ) : F.lower n →* F.gradedPiece n

theorem

gradedPieceMk_apply

L365 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.gradedPieceMk_apply

Documentation

States the theorem gradedPieceMk_apply.

Source context 6 commands

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

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

Lean source · statement

theorem gradedPieceMk_apply (n : ℕ) (σ : F.lower n) :
    F.gradedPieceConcreteMulEquiv n (F.gradedPieceMk n σ) =
      QuotientGroup.mk'
        ((F.lower (n + 1)).subgroupOf (F.lower n)) σ

theorem

gradedPieceMk_eq_one_iff

L373 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.gradedPieceMk_eq_one_iff

Documentation

States the theorem gradedPieceMk_eq_one_iff.

Source context 6 commands

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

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

Lean source · statement

theorem gradedPieceMk_eq_one_iff (n : ℕ) (σ : F.lower n) :
    F.gradedPieceMk n σ = 1 ↔ (σ : G) ∈ F.lower (n + 1)

theorem

gradedPieceMk_eq_iff

L391 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.gradedPieceMk_eq_iff

Documentation

States the theorem gradedPieceMk_eq_iff.

Source context 6 commands

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

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

Lean source · statement

theorem gradedPieceMk_eq_iff (n : ℕ) (σ τ : F.lower n) :
    F.gradedPieceMk n σ = F.gradedPieceMk n τ ↔
      ((σ / τ : F.lower n) : G) ∈ F.lower (n + 1)

theorem

gradedPiece_inductionOn

L411 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.gradedPiece_inductionOn

Documentation

Eliminate a named graded piece.

Source context 6 commands

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

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

Lean source · statement

theorem gradedPiece_inductionOn (n : ℕ)
    {motive : F.gradedPiece n → Prop} (q : F.gradedPiece n)
    (h : ∀ σ : F.lower n, motive (F.gradedPieceMk n σ)) :
    motive q

def

gradedPieceLift

L422 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.gradedPieceLift

Documentation

Descend a homomorphism from G_n that kills G_{n+1}.

Source context 6 commands

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

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

Lean source · statement

def gradedPieceLift {H : Type v} [Group H] (n : ℕ)
    (f : F.lower n →* H)
    (h : (F.lower (n + 1)).subgroupOf (F.lower n) ≤ f.ker) :
    F.gradedPiece n →* H

theorem

gradedPieceLift_mk

L432 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.gradedPieceLift_mk

Documentation

States the theorem gradedPieceLift_mk.

Source context 6 commands

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

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

Lean source · statement

theorem gradedPieceLift_mk {H : Type v} [Group H] (n : ℕ)
    (f : F.lower n →* H)
    (h : (F.lower (n + 1)).subgroupOf (F.lower n) ≤ f.ker)
    (σ : F.lower n) :
    F.gradedPieceLift n f h (F.gradedPieceMk n σ) = f σ

def

gradedPieceMap

L440 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.gradedPieceMap

Documentation

Map between named graded pieces.

Source context 6 commands

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

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

Lean source · statement

def gradedPieceMap {H : Type v} [Group H]
    (E : AntitoneNormalSubgroupFiltration H) (n m : ℕ)
    (f : F.lower n →* E.lower m)
    (h : ∀ σ : F.lower n, (σ : G) ∈ F.lower (n + 1) →
      ((f σ : E.lower m) : H) ∈ E.lower (m + 1)) :
    F.gradedPiece n →* E.gradedPiece m

theorem

gradedPieceMap_apply_mk

L453 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.gradedPieceMap_apply_mk

Documentation

States the theorem gradedPieceMap_apply_mk.

Source context 6 commands

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

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

Lean source · statement

theorem gradedPieceMap_apply_mk {H : Type v} [Group H]
    (E : AntitoneNormalSubgroupFiltration H) (n m : ℕ)
    (f : F.lower n →* E.lower m)
    (h : ∀ σ : F.lower n, (σ : G) ∈ F.lower (n + 1) →
      ((f σ : E.lower m) : H) ∈ E.lower (m + 1))
    (σ : F.lower n) :
    F.gradedPieceMap E n m f h (F.gradedPieceMk n σ) =
      E.gradedPieceMk m (f σ)

def

tameQuotientMk

L464 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.tameQuotientMk

Documentation

Canonical projection to G_0/G_1.

Source context 6 commands

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

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

Lean source · statement

def tameQuotientMk : F.inertiaSubgroup →* F.tameQuotient

theorem

tameQuotientMk_apply

L471 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.tameQuotientMk_apply

Documentation

States the theorem tameQuotientMk_apply.

Source context 6 commands

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

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

Lean source · statement

theorem tameQuotientMk_apply (σ : F.inertiaSubgroup) :
    F.tameQuotientConcreteMulEquiv (F.tameQuotientMk σ) =
      QuotientGroup.mk'
        ((F.wildInertiaSubgroup).subgroupOf F.inertiaSubgroup) σ

theorem

tameQuotientMk_eq_one_iff

L479 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.tameQuotientMk_eq_one_iff

Documentation

States the theorem tameQuotientMk_eq_one_iff.

Source context 6 commands

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

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

Lean source · statement

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

theorem

tameQuotientMk_eq_iff

L497 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.tameQuotientMk_eq_iff

Documentation

States the theorem tameQuotientMk_eq_iff.

Source context 6 commands

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

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

Lean source · statement

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

theorem

tameQuotient_inductionOn

L517 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.tameQuotient_inductionOn

Documentation

Eliminate the named tame quotient.

Source context 6 commands

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

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

Lean source · statement

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

def

tameQuotientLift

L528 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.tameQuotientLift

Documentation

Descend an inertia homomorphism which kills wild inertia.

Source context 6 commands

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

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

Lean source · statement

def tameQuotientLift {H : Type v} [Group H]
    (f : F.inertiaSubgroup →* H)
    (h : (F.wildInertiaSubgroup).subgroupOf F.inertiaSubgroup ≤ f.ker) :
    F.tameQuotient →* H

theorem

tameQuotientLift_mk

L538 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.tameQuotientLift_mk

Documentation

States the theorem tameQuotientLift_mk.

Source context 6 commands

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

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

Lean source · statement

theorem tameQuotientLift_mk {H : Type v} [Group H]
    (f : F.inertiaSubgroup →* H)
    (h : (F.wildInertiaSubgroup).subgroupOf F.inertiaSubgroup ≤ f.ker)
    (σ : F.inertiaSubgroup) :
    F.tameQuotientLift f h (F.tameQuotientMk σ) = f σ

def

tameQuotientMap

L546 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.tameQuotientMap

Documentation

Map between named tame quotients.

Source context 6 commands

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

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

Lean source · statement

def tameQuotientMap {H : Type v} [Group H]
    (E : AntitoneNormalSubgroupFiltration H)
    (f : F.inertiaSubgroup →* E.inertiaSubgroup)
    (h : ∀ σ : F.inertiaSubgroup, (σ : G) ∈ F.wildInertiaSubgroup →
      ((f σ : E.inertiaSubgroup) : H) ∈ E.wildInertiaSubgroup) :
    F.tameQuotient →* E.tameQuotient

theorem

tameQuotientMap_apply_mk

L559 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.tameQuotientMap_apply_mk

Documentation

States the theorem tameQuotientMap_apply_mk.

Source context 6 commands

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

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

Lean source · statement

theorem tameQuotientMap_apply_mk {H : Type v} [Group H]
    (E : AntitoneNormalSubgroupFiltration H)
    (f : F.inertiaSubgroup →* E.inertiaSubgroup)
    (h : ∀ σ : F.inertiaSubgroup, (σ : G) ∈ F.wildInertiaSubgroup →
      ((f σ : E.inertiaSubgroup) : H) ∈ E.wildInertiaSubgroup)
    (σ : F.inertiaSubgroup) :
    F.tameQuotientMap E f h (F.tameQuotientMk σ) =
      E.tameQuotientMk (f σ)

instance

quotientFinite

L570 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.quotientFinite

Documentation

Provides the instance quotientFinite.

Source context 6 commands

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

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

Lean source · statement

instance quotientFinite [Finite G] (n : ℕ) : Finite (F.quotient n)

instance

subquotientFinite

L577 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.subquotientFinite

Documentation

Provides the instance subquotientFinite.

Source context 6 commands

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

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

Lean source · statement

instance subquotientFinite [Finite G] (m n : ℕ) :
    Finite (F.subquotient m n)

instance

gradedPieceFinite

L585 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.gradedPieceFinite

Documentation

Provides the instance gradedPieceFinite.

Source context 6 commands

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

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

Lean source · statement

instance gradedPieceFinite [Finite G] (n : ℕ) :
    Finite (F.gradedPiece n)

instance

tameQuotientFinite

L593 ↗

RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.tameQuotientFinite

Documentation

Provides the instance tameQuotientFinite.

Source context 6 commands

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

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

Lean source · statement

instance tameQuotientFinite [Finite G] : Finite F.tameQuotient

Module documentation

Named quotients of antitone normal-subgroup filtrations

Named quotient boundaries

Declarations