Module

Filtration.lean

Nyll.ValuedFieldTheory.Ramification.Filtration

8 declarations indexed from sourceView source ↗

Module documentation

Natural-ceiling subgroup filtrations

Generic order-theoretic infrastructure for extending a natural-number-indexed subgroup filtration to the real line by the natural-number ceiling.

Imports3

Mathlib.Algebra.Group.Subgroup.Lattice
Mathlib.Algebra.Order.Floor.Ring
Mathlib.Algebra.Order.Archimedean.Real.Basic

Imported by4

def

natCeilStepFiltration

L29 ↗

RamificationTheory.natCeilStepFiltration

Documentation

Extend a subgroup filtration indexed by natural numbers to the real line by taking the natural-number ceiling. This is the ceiling-indexed step filtration relevant to the principal-unit filtration.

Source context 4 commands

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

noncomputable section
namespace RamificationTheory
section IntegerStepFiltration
variable {G : Type*} [Group G]

Lean source · statement

def natCeilStepFiltration
    (F : ℕ → Subgroup G) (t : ℝ) : Subgroup G

def

natCeilStepFiltrationAfter

L34 ↗

RamificationTheory.natCeilStepFiltrationAfter

Documentation

The right-limit subgroup of a natural-ceiling step filtration.

Source context 4 commands

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

noncomputable section
namespace RamificationTheory
section IntegerStepFiltration
variable {G : Type*} [Group G]

Lean source · statement

def natCeilStepFiltrationAfter
    (F : ℕ → Subgroup G) (t : ℝ) : Subgroup G

def

IsNatCeilStepFiltrationJump

L40 ↗

RamificationTheory.IsNatCeilStepFiltrationJump

Documentation

A jump of a natural-ceiling step filtration is a strict drop from the group at the index to its right-limit subgroup.

Source context 4 commands

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

noncomputable section
namespace RamificationTheory
section IntegerStepFiltration
variable {G : Type*} [Group G]

Lean source · statement

def IsNatCeilStepFiltrationJump
    (F : ℕ → Subgroup G) (t : ℝ) : Prop

theorem

natCeilStepFiltration_antitone

L46 ↗

RamificationTheory.natCeilStepFiltration_antitone

Documentation

An antitone natural-number filtration remains antitone after extension by the natural-number ceiling.

Source context 4 commands

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

noncomputable section
namespace RamificationTheory
section IntegerStepFiltration
variable {G : Type*} [Group G]

Lean source · statement

theorem natCeilStepFiltration_antitone
    {F : ℕ → Subgroup G} (hF : Antitone F) :
    Antitone (natCeilStepFiltration F)

theorem

natCeilStepFiltrationAfter_le

L54 ↗

RamificationTheory.natCeilStepFiltrationAfter_le

Documentation

The right-limit subgroup of an antitone natural-ceiling filtration lies in the group at the limiting index.

Source context 4 commands

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

noncomputable section
namespace RamificationTheory
section IntegerStepFiltration
variable {G : Type*} [Group G]

Lean source · statement

theorem natCeilStepFiltrationAfter_le
    {F : ℕ → Subgroup G} (hF : Antitone F) (t : ℝ) :
    natCeilStepFiltrationAfter F t ≤ natCeilStepFiltration F t

theorem

natCeilStepFiltrationAfter_natCast

L63 ↗

RamificationTheory.natCeilStepFiltrationAfter_natCast

Documentation

At a natural-number index, the right-limit of a ceiling-indexed antitone filtration is exactly the next group.

Source context 4 commands

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

noncomputable section
namespace RamificationTheory
section IntegerStepFiltration
variable {G : Type*} [Group G]

Lean source · statement

theorem natCeilStepFiltrationAfter_natCast
    {F : ℕ → Subgroup G} (hF : Antitone F) (n : ℕ) :
    natCeilStepFiltrationAfter F (n : ℝ) = F (n + 1)

theorem

isNatCeilStepFiltrationJump_natCast_iff

L82 ↗

RamificationTheory.isNatCeilStepFiltrationJump_natCast_iff

Documentation

At a natural-number index, being a jump is equivalent to a strict change between two consecutive groups.

Source context 4 commands

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

noncomputable section
namespace RamificationTheory
section IntegerStepFiltration
variable {G : Type*} [Group G]

Lean source · statement

theorem isNatCeilStepFiltrationJump_natCast_iff
    {F : ℕ → Subgroup G} (hF : Antitone F) (n : ℕ) :
    IsNatCeilStepFiltrationJump F (n : ℝ) ↔
      F n ≠ F (n + 1)

theorem

isNatCeilStepFiltrationJump_integer

L91 ↗

RamificationTheory.isNatCeilStepFiltrationJump_integer

Documentation

Every jump of an antitone natural-ceiling step filtration is a nonnegative rational integer.

Source context 4 commands

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

noncomputable section
namespace RamificationTheory
section IntegerStepFiltration
variable {G : Type*} [Group G]

Lean source · statement

theorem isNatCeilStepFiltrationJump_integer
    {F : ℕ → Subgroup G} (hF : Antitone F) {t : ℝ}
    (ht : IsNatCeilStepFiltrationJump F t) :
    ∃ n : ℕ, t = n

Module documentation

Natural-ceiling subgroup filtrations

Declarations