Module

FilteredLiftingSequence.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.ClassFormation.FilteredLiftingSequence

12 declarations indexed from sourceView source ↗

Module documentation

Recursive correction sequences

This file isolates the dependent-choice bookkeeping in the infinite-product argument of the local class-field-axiom theorem. A one-step lift in a filtered commutative group produces compatible correction and remainder sequences. No cohomological input is hidden here: the existence of each one-step lift is an explicit parameter, discharged for the normal-basis filtration in the next file.

Imports1

Nyll.ClassFieldTheory.LocalClassFieldTheory.ClassFormation.NormalBasisInfiniteProduct

Imported by2

def

filteredCorrectionProduct

L29 ↗

LocalClassFieldTheory.filteredCorrectionProduct

Documentation

Left-to-right finite products of a correction sequence.

Source context 3 commands

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

namespace LocalClassFieldTheory
noncomputable section
universe u

Lean source · full declaration

def filteredCorrectionProduct {A : Type u} [Monoid A] (z : Nat → A) : Nat → A
  | 0 => 1
  | d + 1 => filteredCorrectionProduct z d * z d

theorem

filteredCorrectionProduct_zero

L35 ↗

LocalClassFieldTheory.filteredCorrectionProduct_zero

Documentation

The empty correction product is the identity.

Source context 3 commands

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

namespace LocalClassFieldTheory
noncomputable section
universe u

Lean source · statement

theorem filteredCorrectionProduct_zero {A : Type u} [Monoid A] (z : Nat → A) :
    filteredCorrectionProduct z 0 = 1

theorem

filteredCorrectionProduct_succ

L41 ↗

LocalClassFieldTheory.filteredCorrectionProduct_succ

Documentation

A successor correction product appends the correction at the preceding index.

Source context 3 commands

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

namespace LocalClassFieldTheory
noncomputable section
universe u

Lean source · statement

theorem filteredCorrectionProduct_succ {A : Type u} [Monoid A]
    (z : Nat → A) (d : Nat) :
    filteredCorrectionProduct z (d + 1) = filteredCorrectionProduct z d * z d

structure

FilteredLiftState

L48 ↗

LocalClassFieldTheory.FilteredLiftState

Documentation

A remainder at depth n + i, carrying both its filtration condition and the condition that must be preserved by one-step lifting.

Source context 3 commands

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

namespace LocalClassFieldTheory
noncomputable section
universe u

Lean source · full declaration

structure FilteredLiftState (A : Type u) (P : Nat → A → Prop)
    (R : A → Prop) (n i : Nat) where
  /-- The current remainder at relative depth `i`. -/
  value : A
  /-- The current remainder lies in filtration level `n + i`. -/
  mem : P (n + i) value
  /-- The current remainder satisfies the condition preserved by each lifting step. -/
  stable : R value

structure

FilteredLiftStep

L58 ↗

LocalClassFieldTheory.FilteredLiftStep

Documentation

One correction step a_i = F(b_i) a_(i+1).

Source context 3 commands

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

namespace LocalClassFieldTheory
noncomputable section
universe u

Lean source · full declaration

structure FilteredLiftStep (A : Type u) [CommGroup A]
    (P : Nat → A → Prop) (R : A → Prop) (F : A →* A)
    (n i : Nat) (s : FilteredLiftState A P R n i) where
  /-- The correction chosen at relative depth `i`. -/
  correction : A
  /-- The correction lies in the same filtration level `n + i` as the current remainder. -/
  correction_mem : P (n + i) correction
  /-- The remainder state after removing the current correction, one level deeper. -/
  next : FilteredLiftState A P R n (i + 1)
  /-- The current remainder is the image of the correction under `F` times the next remainder. -/
  equation : s.value = F correction * next.value

def

chosenFilteredLiftStateSequence

L71 ↗

LocalClassFieldTheory.chosenFilteredLiftStateSequence

Documentation

The recursively chosen remainder sequence.

Source context 3 commands

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

namespace LocalClassFieldTheory
noncomputable section
universe u

Lean source · full declaration

def chosenFilteredLiftStateSequence
    (A : Type u) [CommGroup A] (P : Nat → A → Prop) (R : A → Prop)
    (F : A →* A) (n : Nat) (initial : FilteredLiftState A P R n 0)
    (step : ∀ i (s : FilteredLiftState A P R n i),
      Nonempty (FilteredLiftStep A P R F n i s)) :
    (i : Nat) → FilteredLiftState A P R n i
  | 0 => initial
  | i + 1 =>
      (Classical.choice
        (step i (chosenFilteredLiftStateSequence A P R F n initial step i))).next

def

chosenFilteredLiftCorrectionSequence

L83 ↗

LocalClassFieldTheory.chosenFilteredLiftCorrectionSequence

Documentation

The recursively chosen correction at depth n + i.

Source context 3 commands

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

namespace LocalClassFieldTheory
noncomputable section
universe u

Lean source · statement

def chosenFilteredLiftCorrectionSequence
    (A : Type u) [CommGroup A] (P : Nat → A → Prop) (R : A → Prop)
    (F : A →* A) (n : Nat) (initial : FilteredLiftState A P R n 0)
    (step : ∀ i (s : FilteredLiftState A P R n i),
      Nonempty (FilteredLiftStep A P R F n i s)) (i : Nat) : A

theorem

chosenFilteredLiftStateSequence_zero

L93 ↗

LocalClassFieldTheory.chosenFilteredLiftStateSequence_zero

Documentation

The chosen filtered-lift sequence starts at the supplied initial state.

Source context 3 commands

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

namespace LocalClassFieldTheory
noncomputable section
universe u

Lean source · statement

theorem chosenFilteredLiftStateSequence_zero
    (A : Type u) [CommGroup A] (P : Nat → A → Prop) (R : A → Prop)
    (F : A →* A) (n : Nat) (initial : FilteredLiftState A P R n 0)
    (step : ∀ i (s : FilteredLiftState A P R n i),
      Nonempty (FilteredLiftStep A P R F n i s)) :
    chosenFilteredLiftStateSequence A P R F n initial step 0 = initial

theorem

chosenFilteredLiftStateSequence_succ

L103 ↗

LocalClassFieldTheory.chosenFilteredLiftStateSequence_succ

Documentation

Each successor state is the next state of the chosen lifting step.

Source context 3 commands

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

namespace LocalClassFieldTheory
noncomputable section
universe u

Lean source · statement

theorem chosenFilteredLiftStateSequence_succ
    (A : Type u) [CommGroup A] (P : Nat → A → Prop) (R : A → Prop)
    (F : A →* A) (n : Nat) (initial : FilteredLiftState A P R n 0)
    (step : ∀ i (s : FilteredLiftState A P R n i),
      Nonempty (FilteredLiftStep A P R F n i s)) (i : Nat) :
    chosenFilteredLiftStateSequence A P R F n initial step (i + 1) =
      (Classical.choice
        (step i (chosenFilteredLiftStateSequence A P R F n initial step i))).next

theorem

chosenFilteredLiftCorrectionSequence_mem

L114 ↗

LocalClassFieldTheory.chosenFilteredLiftCorrectionSequence_mem

Documentation

Every chosen correction lies at the advertised filtration level.

Source context 3 commands

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

namespace LocalClassFieldTheory
noncomputable section
universe u

Lean source · statement

theorem chosenFilteredLiftCorrectionSequence_mem
    (A : Type u) [CommGroup A] (P : Nat → A → Prop) (R : A → Prop)
    (F : A →* A) (n : Nat) (initial : FilteredLiftState A P R n 0)
    (step : ∀ i (s : FilteredLiftState A P R n i),
      Nonempty (FilteredLiftStep A P R F n i s)) (i : Nat) :
    P (n + i)
      (chosenFilteredLiftCorrectionSequence A P R F n initial step i)

theorem

chosenFilteredLiftStateSequence_equation

L125 ↗

LocalClassFieldTheory.chosenFilteredLiftStateSequence_equation

Documentation

The defining one-step recurrence for the chosen sequences.

Source context 3 commands

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

namespace LocalClassFieldTheory
noncomputable section
universe u

Lean source · statement

theorem chosenFilteredLiftStateSequence_equation
    (A : Type u) [CommGroup A] (P : Nat → A → Prop) (R : A → Prop)
    (F : A →* A) (n : Nat) (initial : FilteredLiftState A P R n 0)
    (step : ∀ i (s : FilteredLiftState A P R n i),
      Nonempty (FilteredLiftStep A P R F n i s)) (i : Nat) :
    (chosenFilteredLiftStateSequence A P R F n initial step i).value =
      F (chosenFilteredLiftCorrectionSequence A P R F n initial step i) *
        (chosenFilteredLiftStateSequence A P R F n initial step (i + 1)).value

theorem

filteredLift_initial_eq_correctionProduct_mul_state

L138 ↗

LocalClassFieldTheory.filteredLift_initial_eq_correctionProduct_mul_state

Documentation

The initial remainder equals the image under F of the first d corrections, times the depth-d remainder.

Source context 3 commands

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

namespace LocalClassFieldTheory
noncomputable section
universe u

Lean source · statement

theorem filteredLift_initial_eq_correctionProduct_mul_state
    (A : Type u) [CommGroup A] (P : Nat → A → Prop) (R : A → Prop)
    (F : A →* A) (n : Nat) (initial : FilteredLiftState A P R n 0)
    (step : ∀ i (s : FilteredLiftState A P R n i),
      Nonempty (FilteredLiftStep A P R F n i s)) (d : Nat) :
    initial.value =
      F (filteredCorrectionProduct
          (chosenFilteredLiftCorrectionSequence A P R F n initial step) d) *
        (chosenFilteredLiftStateSequence A P R F n initial step d).value

Module documentation

Recursive correction sequences

Declarations