Module

NormalBasisLattice.lean

Nyll.GaloisCohomology.Cyclic.Herbrand.NormalBasisLattice

126 declarations indexed from sourceView source ↗

Module documentation

Provides the public normal-basis lattice declarations used in Herbrand computations.

Additive quotient boundary

Imports3

Mathlib.FieldTheory.Galois.NormalBasis
Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.IdealQuotients
Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.ResidueExtension

Imported by5

theorem

normalBasisConjugates_span_eq_top

L30 ↗

CyclicCohomology.normalBasisConjugates_span_eq_top

Documentation

The Gal(L/K) orbit of Mathlib's normal-basis generator spans L over K.

Source context 7 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]

Lean source · full declaration

theorem normalBasisConjugates_span_eq_top :
    Submodule.span K
        (Set.range (fun σ : Gal(L/K) =>
          σ (IsGalois.normalBasis K L (1 : Gal(L/K))))) = ⊤ := by
  have hset :
      Set.range (fun σ : Gal(L/K) =>
        σ (IsGalois.normalBasis K L (1 : Gal(L/K)))) =
        Set.range (IsGalois.normalBasis K L) := by
    ext x
    constructor
    · rintro ⟨σ, rfl⟩
      exact ⟨σ, IsGalois.normalBasis_apply (K := K) (L := L) σ⟩
    · rintro ⟨σ, rfl⟩
      exact ⟨σ, (IsGalois.normalBasis_apply (K := K) (L := L) σ).symm⟩
  rw [hset]
  exact (IsGalois.normalBasis K L).span_eq

def

chosenNormalBasisIntegerLattice

L52 ↗

CyclicCohomology.chosenNormalBasisIntegerLattice

Documentation

The classical normal-basis lattice candidate M: the 𝒪_K-span of the normal-basis orbit. Bounds comparing this lattice with 𝒪_L are deliberately made explicit in the lattice-comparison theorems below.

Source context 8 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]

Lean source · statement

def chosenNormalBasisIntegerLattice : Submodule 𝒪[K] L

theorem

chosenNormalBasisIntegerLattice_eq_span

L59 ↗

CyclicCohomology.chosenNormalBasisIntegerLattice_eq_span

Documentation

Public characterization of the chosen normal-basis lattice as the span of the chosen generator's Galois orbit.

Source context 8 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]

Lean source · full declaration

theorem chosenNormalBasisIntegerLattice_eq_span :
    chosenNormalBasisIntegerLattice K L =
      Submodule.span 𝒪[K]
        (Set.range (fun σ : Gal(L/K) =>
          σ (IsGalois.normalBasis K L (1 : Gal(L/K))))) :=
  rfl

theorem

normalBasis_mem_integerLattice

L67 ↗

CyclicCohomology.normalBasis_mem_integerLattice

Documentation

Every normal-basis vector lies in the 𝒪_K-span lattice M.

Source context 8 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]

Lean source · statement

theorem normalBasis_mem_integerLattice (σ : Gal(L/K)) :
    IsGalois.normalBasis K L σ ∈ chosenNormalBasisIntegerLattice K L

theorem

normalBasis_one_mem_integerLattice

L73 ↗

CyclicCohomology.normalBasis_one_mem_integerLattice

Documentation

Mathlib's normal-basis generator lies in the 𝒪_K-span lattice M.

Source context 8 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]

Lean source · statement

theorem normalBasis_one_mem_integerLattice :
    IsGalois.normalBasis K L (1 : Gal(L/K)) ∈
      chosenNormalBasisIntegerLattice K L

theorem

chosenNormalBasisIntegerLattice_field_span_eq_top

L80 ↗

CyclicCohomology.chosenNormalBasisIntegerLattice_field_span_eq_top

Documentation

After extending scalars back to K, the normal-basis lattice spans all of L.

Source context 8 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]

Lean source · statement

theorem chosenNormalBasisIntegerLattice_field_span_eq_top :
    Submodule.span K ((chosenNormalBasisIntegerLattice K L : Submodule 𝒪[K] L) : Set L) =
      ⊤

theorem

galoisGroup_apply_mem_chosenNormalBasisIntegerLattice

L91 ↗

CyclicCohomology.galoisGroup_apply_mem_chosenNormalBasisIntegerLattice

Documentation

The normal-basis lattice M is stable under the actual Gal(L/K) action.

Source context 8 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]

Lean source · statement

theorem galoisGroup_apply_mem_chosenNormalBasisIntegerLattice
    (τ : Gal(L/K)) {x : L}
    (hx : x ∈ chosenNormalBasisIntegerLattice K L) :
    τ x ∈ chosenNormalBasisIntegerLattice K L

theorem

chosenNormalBasisIntegerLattice_fg

L119 ↗

CyclicCohomology.chosenNormalBasisIntegerLattice_fg

Documentation

The normal-basis lattice M is finitely generated over 𝒪_K.

Source context 8 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]

Lean source · statement

theorem chosenNormalBasisIntegerLattice_fg :
    (chosenNormalBasisIntegerLattice K L).FG

def

baseIntegerScalarMulLinearMap

L126 ↗

CyclicCohomology.baseIntegerScalarMulLinearMap

Documentation

Multiplication by a base integer-ring element, as an 𝒪_K-linear endomorphism of the extension field.

Source context 8 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]

Lean source · full declaration

def baseIntegerScalarMulLinearMap (a : 𝒪[K]) : L →ₗ[𝒪[K]] L where
  toFun x := algebraMap 𝒪[K] L a * x
  map_add' := by
    intro x y
    rw [mul_add]
  map_smul' := by
    intro r x
    simp [Algebra.smul_def, mul_comm, mul_left_comm]

theorem

baseIntegerScalarMulLinearMap_apply

L138 ↗

CyclicCohomology.baseIntegerScalarMulLinearMap_apply

Documentation

Evaluates the linear map given by scalar multiplication from the base integer ring.

Source context 9 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem baseIntegerScalarMulLinearMap_apply (a : 𝒪[K]) (x : L) :
    baseIntegerScalarMulLinearMap K L a x = algebraMap 𝒪[K] L a * x

def

baseIntegerScalarMulSubmodule

L144 ↗

CyclicCohomology.baseIntegerScalarMulSubmodule

Documentation

The image of an 𝒪_K-submodule under multiplication by a base integer-ring element.

Source context 8 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]

Lean source · statement

def baseIntegerScalarMulSubmodule (a : 𝒪[K]) (N : Submodule 𝒪[K] L) :
    Submodule 𝒪[K] L

theorem

mem_baseIntegerScalarMulSubmodule_iff

L150 ↗

CyclicCohomology.mem_baseIntegerScalarMulSubmodule_iff

Documentation

Characterizes membership in the submodule generated by base-integer scalar multiples.

Source context 9 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem mem_baseIntegerScalarMulSubmodule_iff
    (a : 𝒪[K]) (N : Submodule 𝒪[K] L) (x : L) :
    x ∈ baseIntegerScalarMulSubmodule K L a N ↔
      ∃ y : L, y ∈ N ∧ algebraMap 𝒪[K] L a * y = x

theorem

baseIntegerScalarMulSubmodule_fg_of_fg

L158 ↗

CyclicCohomology.baseIntegerScalarMulSubmodule_fg_of_fg

Documentation

Scalar multiplication by base integers preserves finite generation of submodules.

Source context 9 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem baseIntegerScalarMulSubmodule_fg_of_fg
    (a : 𝒪[K]) {N : Submodule 𝒪[K] L} (hN : N.FG) :
    (baseIntegerScalarMulSubmodule K L a N).FG

def

chosenBaseUniformizerPowSubmodule

L170 ↗

CyclicCohomology.chosenBaseUniformizerPowSubmodule

Documentation

Multiplication of an 𝒪_K-submodule by a power of the chosen base uniformizer. The name deliberately records the construction's dependence on chosenIntegerRingUniformizer K; no uniformizer-independence result is part of this API. This is the concrete shape of the π_K^n lattices used in the local class-field-axiom calculation.

Source context 9 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]

Lean source · statement

def chosenBaseUniformizerPowSubmodule (n : Nat) (N : Submodule 𝒪[K] L) :
    Submodule 𝒪[K] L

theorem

mem_chosenBaseUniformizerPowSubmodule_iff

L177 ↗

CyclicCohomology.mem_chosenBaseUniformizerPowSubmodule_iff

Documentation

Characterizes membership in a chosen uniformizer-power submodule.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem mem_chosenBaseUniformizerPowSubmodule_iff
    (n : Nat) (N : Submodule 𝒪[K] L) (x : L) :
    x ∈ chosenBaseUniformizerPowSubmodule K L n N ↔
      ∃ y : L, y ∈ N ∧
        algebraMap 𝒪[K] L (chosenIntegerRingUniformizer K ^ n) * y = x

theorem

chosenBaseUniformizerPowSubmodule_fg_of_fg

L186 ↗

CyclicCohomology.chosenBaseUniformizerPowSubmodule_fg_of_fg

Documentation

Multiplication by a chosen uniformizer power preserves finite generation.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem chosenBaseUniformizerPowSubmodule_fg_of_fg
    (n : Nat) {N : Submodule 𝒪[K] L} (hN : N.FG) :
    (chosenBaseUniformizerPowSubmodule K L n N).FG

theorem

chosenBaseUniformizerPow_mul_mem_mono

L195 ↗

CyclicCohomology.chosenBaseUniformizerPow_mul_mem_mono

Documentation

Increasing the base-uniformizer exponent preserves membership after denominator clearing.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem chosenBaseUniformizerPow_mul_mem_mono
    {M : Submodule 𝒪[K] L} {m n : Nat} {x : L} (hmn : m ≤ n)
    (hx : algebraMap 𝒪[K] L (chosenIntegerRingUniformizer K ^ m) * x ∈ M) :
    algebraMap 𝒪[K] L (chosenIntegerRingUniformizer K ^ n) * x ∈ M

theorem

chosenBaseUniformizerPowSubmodule_antitone

L210 ↗

CyclicCohomology.chosenBaseUniformizerPowSubmodule_antitone

Documentation

The lattices π_K^n N form a descending filtration.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem chosenBaseUniformizerPowSubmodule_antitone
    (N : Submodule 𝒪[K] L) {m n : Nat} (hmn : m ≤ n) :
    chosenBaseUniformizerPowSubmodule K L n N ≤
      chosenBaseUniformizerPowSubmodule K L m N

theorem

chosenBaseUniformizerPowSubmodule_succ_le

L226 ↗

CyclicCohomology.chosenBaseUniformizerPowSubmodule_succ_le

Documentation

Successive chosen uniformizer-power submodules form a descending chain.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem chosenBaseUniformizerPowSubmodule_succ_le
    (n : Nat) (N : Submodule 𝒪[K] L) :
    chosenBaseUniformizerPowSubmodule K L (n + 1) N ≤
      chosenBaseUniformizerPowSubmodule K L n N

theorem

chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_fg

L233 ↗

CyclicCohomology.chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_fg

Documentation

Every chosen uniformizer-power normal-basis lattice is finitely generated.

Source context 9 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]

Lean source · statement

theorem chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_fg (n : Nat) :
    (chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L)).FG

theorem

exists_chosenBaseUniformizerPow_mul_mem_of_field_span_eq_top

L243 ↗

CyclicCohomology.exists_chosenBaseUniformizerPow_mul_mem_of_field_span_eq_top

Documentation

If an 𝒪_K-submodule spans L after extending scalars to K, then every element of L enters that submodule after multiplying by a high enough power of the base prime element. The scalar-denominator step is exactly the local DVR denominator clearing in IdealQuotients.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem exists_chosenBaseUniformizerPow_mul_mem_of_field_span_eq_top
    {M : Submodule 𝒪[K] L}
    (hMspan : Submodule.span K ((M : Set L)) = ⊤) (x : L) :
    ∃ n : Nat, algebraMap 𝒪[K] L (chosenIntegerRingUniformizer K ^ n) * x ∈ M

theorem

exists_chosenBaseUniformizerPowSubmodule_le_of_fg_of_field_span_eq_top

L295 ↗

CyclicCohomology.exists_chosenBaseUniformizerPowSubmodule_le_of_fg_of_field_span_eq_top

Documentation

Finite-generation version of exists_chosenBaseUniformizerPow_mul_mem_of_field_span_eq_top: one exponent works for all elements of a finitely generated 𝒪_K-submodule.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem exists_chosenBaseUniformizerPowSubmodule_le_of_fg_of_field_span_eq_top
    {M N : Submodule 𝒪[K] L} (hN : N.FG)
    (hMspan : Submodule.span K ((M : Set L)) = ⊤) :
    ∃ n : Nat, chosenBaseUniformizerPowSubmodule K L n N ≤ M

theorem

exists_chosenBaseUniformizerPow_mul_mul_mem_of_fg_of_field_span_eq_top

L356 ↗

CyclicCohomology.exists_chosenBaseUniformizerPow_mul_mul_mem_of_fg_of_field_span_eq_top

Documentation

Product-denominator bound for multiplicative lattice control. If N and P are finitely generated 𝒪_K-submodules and M spans L after inverting 𝒪_K, then one power of the base prime element sends every product xy, x ∈ N, y ∈ P, back into M.

This is the multiplicative source needed before proving that 1 + π_K^n M is closed under multiplication for large n.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem exists_chosenBaseUniformizerPow_mul_mul_mem_of_fg_of_field_span_eq_top
    {M N P : Submodule 𝒪[K] L} (hN : N.FG) (hP : P.FG)
    (hMspan : Submodule.span K ((M : Set L)) = ⊤) :
    ∃ n : Nat, ∀ x : L, x ∈ N → ∀ y : L, y ∈ P →
      algebraMap 𝒪[K] L (chosenIntegerRingUniformizer K ^ n) * (x * y) ∈ M

theorem

exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_mul_mul_mem

L432 ↗

CyclicCohomology.exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_mul_mul_mem

Documentation

A sufficiently deep uniformizer-power normal-basis lattice absorbs the indicated products.

Source context 9 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]

Lean source · statement

theorem exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_mul_mul_mem :
    ∃ n : Nat, ∀ x : L, x ∈ chosenNormalBasisIntegerLattice K L →
      ∀ y : L, y ∈ chosenNormalBasisIntegerLattice K L →
        algebraMap 𝒪[K] L (chosenIntegerRingUniformizer K ^ n) * (x * y) ∈
          chosenNormalBasisIntegerLattice K L

theorem

exists_chosenBaseUniformizerPowSubmodule_mul_mul_mem_self_of_fg_of_field_span_eq_top

L450 ↗

CyclicCohomology.exists_chosenBaseUniformizerPowSubmodule_mul_mul_mem_self_of_fg_of_field_span_eq_top

Documentation

For sufficiently large n, the lattice π_K^n M is closed under multiplication. It supplies the multiplicative closure of 1 + π_K^n M in the principal-unit lattice.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem exists_chosenBaseUniformizerPowSubmodule_mul_mul_mem_self_of_fg_of_field_span_eq_top
    {M : Submodule 𝒪[K] L} (hMfg : M.FG)
    (hMspan : Submodule.span K ((M : Set L)) = ⊤) :
    ∃ c : Nat, ∀ n : Nat, c ≤ n → ∀ x : L,
      x ∈ chosenBaseUniformizerPowSubmodule K L n M →
      ∀ y : L, y ∈ chosenBaseUniformizerPowSubmodule K L n M →
        x * y ∈ chosenBaseUniformizerPowSubmodule K L n M

theorem

exists_chosenBaseUniformizerPowSubmodule_mul_mul_mem_succ_of_fg_of_field_span_eq_top

L481 ↗

CyclicCohomology.exists_chosenBaseUniformizerPowSubmodule_mul_mul_mem_succ_of_fg_of_field_span_eq_top

Documentation

For sufficiently large n, products of two elements of π_K^n M land in the next lattice step π_K^(n+1) M.

This is the product-depth estimate needed before the map V^n/V^(n+1) -> π_K^nM/π_K^(n+1)M can be made well-defined.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem exists_chosenBaseUniformizerPowSubmodule_mul_mul_mem_succ_of_fg_of_field_span_eq_top
    {M : Submodule 𝒪[K] L} (hMfg : M.FG)
    (hMspan : Submodule.span K ((M : Set L)) = ⊤) :
    ∃ c : Nat, ∀ n : Nat, c ≤ n → ∀ x : L,
      x ∈ chosenBaseUniformizerPowSubmodule K L n M →
      ∀ y : L, y ∈ chosenBaseUniformizerPowSubmodule K L n M →
        x * y ∈ chosenBaseUniformizerPowSubmodule K L (n + 1) M

theorem

exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_mul_mul_mem_self

L511 ↗

CyclicCohomology.exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_mul_mul_mem_self

Documentation

A sufficiently deep uniformizer-power normal-basis lattice is closed under the indicated self-products.

Source context 9 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]

Lean source · statement

theorem exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_mul_mul_mem_self :
    ∃ c : Nat, ∀ n : Nat, c ≤ n → ∀ x : L,
      x ∈ chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) →
      ∀ y : L,
        y ∈ chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) →
          x * y ∈
            chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L)

theorem

exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_mul_mul_mem_succ

L525 ↗

CyclicCohomology.exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_mul_mul_mem_succ

Documentation

A sufficiently deep lattice sends the indicated products into the next uniformizer level.

Source context 9 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]

Lean source · statement

theorem exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_mul_mul_mem_succ :
    ∃ c : Nat, ∀ n : Nat, c ≤ n → ∀ x : L,
      x ∈ chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) →
      ∀ y : L,
        y ∈ chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) →
          x * y ∈
            chosenBaseUniformizerPowSubmodule K L (n + 1) (chosenNormalBasisIntegerLattice K L)

theorem

submodule_pow_succ_mem_of_mul_closed

L544 ↗

CyclicCohomology.submodule_pow_succ_mem_of_mul_closed

Documentation

Powers of an element stay in a multiplicatively closed additive lattice.

This is the finite algebraic input to the geometric-series inverse argument; completeness supplies the limit of these finite approximations.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
omit [FiniteDimensional K L] [IsGalois K L]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] in

Lean source · statement

theorem submodule_pow_succ_mem_of_mul_closed
    {E : Submodule 𝒪[K] L}
    (hmul : ∀ x : L, x ∈ E → ∀ y : L, y ∈ E → x * y ∈ E)
    {x : L} (hx : x ∈ E) :
    ∀ m : Nat, x ^ (m + 1) ∈ E

def

inverseCorrectionPartialSum

L563 ↗

CyclicCohomology.inverseCorrectionPartialSum

Documentation

The finite inverse-correction sum (-x) + (-x)^2 + ... + (-x)^d.

When x is topologically nilpotent and the lattice is complete, these are the finite approximations to (1+x)⁻¹ - 1.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

def inverseCorrectionPartialSum (x : L) (d : Nat) : L

theorem

inverseCorrectionPartialSum_zero

L569 ↗

CyclicCohomology.inverseCorrectionPartialSum_zero

Documentation

The zeroth inverse-correction partial sum is its initial term.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem inverseCorrectionPartialSum_zero (x : L) :
    inverseCorrectionPartialSum (L := L) x 0 = 0

theorem

inverseCorrectionPartialSum_succ

L575 ↗

CyclicCohomology.inverseCorrectionPartialSum_succ

Documentation

Expands the inverse-correction partial sum at a successor index.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem inverseCorrectionPartialSum_succ (x : L) (d : Nat) :
    inverseCorrectionPartialSum (L := L) x (d + 1) =
      inverseCorrectionPartialSum (L := L) x d + (-x) ^ (d + 1)

theorem

one_add_inverseCorrectionPartialSum_eq_geom_sum

L583 ↗

CyclicCohomology.one_add_inverseCorrectionPartialSum_eq_geom_sum

Documentation

Adding 1 turns the inverse-correction sum into the usual finite geometric sum with ratio -x.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · full declaration

theorem one_add_inverseCorrectionPartialSum_eq_geom_sum (x : L) (d : Nat) :
    1 + inverseCorrectionPartialSum (L := L) x d =
      (Finset.range (d + 1)).sum fun i => (-x) ^ i := by
  induction d with
  | zero =>
      simp [inverseCorrectionPartialSum]
  | succ d ih =>
      rw [inverseCorrectionPartialSum_succ, Finset.sum_range_succ, ← ih]
      simp [add_assoc]

theorem

one_add_mul_one_add_inverseCorrectionPartialSum

L595 ↗

CyclicCohomology.one_add_mul_one_add_inverseCorrectionPartialSum

Documentation

Finite geometric inverse identity for the approximants to (1+x)⁻¹.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem one_add_mul_one_add_inverseCorrectionPartialSum (x : L) (d : Nat) :
    (1 + x) * (1 + inverseCorrectionPartialSum (L := L) x d) =
      1 - (-x) ^ (d + 1)

theorem

one_add_mul_one_add_inverseCorrectionPartialSum_sub_one

L604 ↗

CyclicCohomology.one_add_mul_one_add_inverseCorrectionPartialSum_sub_one

Documentation

The residual error after applying a finite inverse correction.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem one_add_mul_one_add_inverseCorrectionPartialSum_sub_one
    (x : L) (d : Nat) :
    (1 + x) * (1 + inverseCorrectionPartialSum (L := L) x d) - 1 =
      -((-x) ^ (d + 1))

theorem

inverseCorrectionPartialSum_mem_of_mul_closed

L614 ↗

CyclicCohomology.inverseCorrectionPartialSum_mem_of_mul_closed

Documentation

Inverse-correction partial sums remain in any additive set closed under multiplication.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
omit [FiniteDimensional K L] [IsGalois K L]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] in

Lean source · statement

theorem inverseCorrectionPartialSum_mem_of_mul_closed
    {E : Submodule 𝒪[K] L}
    (hmul : ∀ x : L, x ∈ E → ∀ y : L, y ∈ E → x * y ∈ E)
    {x : L} (hx : x ∈ E) (d : Nat) :
    inverseCorrectionPartialSum (L := L) x d ∈ E

theorem

inverseCorrectionPartialProductError_mem_of_mul_closed

L629 ↗

CyclicCohomology.inverseCorrectionPartialProductError_mem_of_mul_closed

Documentation

A finite inverse correction kills 1+x modulo the same multiplicatively closed additive lattice.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
omit [FiniteDimensional K L] [IsGalois K L]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] in

Lean source · statement

theorem inverseCorrectionPartialProductError_mem_of_mul_closed
    {E : Submodule 𝒪[K] L}
    (hmul : ∀ x : L, x ∈ E → ∀ y : L, y ∈ E → x * y ∈ E)
    {x : L} (hx : x ∈ E) (d : Nat) :
    (1 + x) * (1 + inverseCorrectionPartialSum (L := L) x d) - 1 ∈ E

theorem

submodule_isOpen_of_mem_nhds_zero

L642 ↗

CyclicCohomology.submodule_isOpen_of_mem_nhds_zero

Documentation

An additive 𝒪_K-submodule containing a neighborhood of 0 is open.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
omit [FiniteDimensional K L] [IsGalois K L]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] in

Lean source · statement

theorem submodule_isOpen_of_mem_nhds_zero
    [TopologicalSpace L] [IsTopologicalAddGroup L]
    {E : Submodule 𝒪[K] L} (hE : (E : Set L) ∈ nhds (0 : L)) :
    IsOpen (E : Set L)

theorem

submodule_isClosed_of_isOpen

L651 ↗

CyclicCohomology.submodule_isClosed_of_isOpen

Documentation

An open additive 𝒪_K-submodule is closed.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
omit [FiniteDimensional K L] [IsGalois K L]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] in

Lean source · statement

theorem submodule_isClosed_of_isOpen
    [TopologicalSpace L] [IsTopologicalAddGroup L]
    {E : Submodule 𝒪[K] L} (hE : IsOpen (E : Set L)) :
    IsClosed (E : Set L)

theorem

submodule_isClosed_of_mem_nhds_zero

L660 ↗

CyclicCohomology.submodule_isClosed_of_mem_nhds_zero

Documentation

A neighborhood submodule is closed in a topological additive group.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
omit [FiniteDimensional K L] [IsGalois K L]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] in

Lean source · statement

theorem submodule_isClosed_of_mem_nhds_zero
    [TopologicalSpace L] [IsTopologicalAddGroup L]
    {E : Submodule 𝒪[K] L} (hE : (E : Set L) ∈ nhds (0 : L)) :
    IsClosed (E : Set L)

theorem

submodule_mem_of_tendsto_of_forall_mem_of_closed

L671 ↗

CyclicCohomology.submodule_mem_of_tendsto_of_forall_mem_of_closed

Documentation

If every term of a convergent sequence lies in a closed submodule, then the limit lies in that submodule.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
omit [FiniteDimensional K L] [IsGalois K L]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] in

Lean source · statement

theorem submodule_mem_of_tendsto_of_forall_mem_of_closed
    [TopologicalSpace L] {E : Submodule 𝒪[K] L} {f : Nat → L} {x : L}
    (hclosed : IsClosed (E : Set L)) (hf : Tendsto f atTop (nhds x))
    (hmem : ∀ d : Nat, f d ∈ E) :
    x ∈ E

theorem

integerRingMap_uniformizer_mem_maximalIdeal_of_valuationExtension

L684 ↗

CyclicCohomology.integerRingMap_uniformizer_mem_maximalIdeal_of_valuationExtension

Documentation

Under a valuation extension, the chosen base prime element maps into the maximal ideal of the extension valuation ring.

Source context 11 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem integerRingMap_uniformizer_mem_maximalIdeal_of_valuationExtension :
    integerRingMapOfValuationExtension K L (chosenIntegerRingUniformizer K) ∈
      (𝓂[L] : Ideal 𝒪[L])

theorem

exists_chosenBaseUniformizerPow_mul_mem_integerRing_of_valuationExtension

L702 ↗

CyclicCohomology.exists_chosenBaseUniformizerPow_mul_mem_integerRing_of_valuationExtension

Documentation

Extension-field denominator clearing by powers of the base prime element.

For any x : L, a sufficiently high power of the chosen prime element of 𝒪[K], mapped to L, sends x into 𝒪[L]. This is the denominator-clearing input used before comparing the normal-basis lattice with 𝒪_L: it uses only the DVR structure of 𝒪_L and the fact that the image of the base prime lies in 𝓂_L.

Source context 11 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem exists_chosenBaseUniformizerPow_mul_mem_integerRing_of_valuationExtension
    [TopologicalSpace L] [IsNonarchimedeanLocalField L] (x : L) :
    ∃ n : Nat,
      algebraMap 𝒪[K] L (chosenIntegerRingUniformizer K ^ n) * x ∈ 𝒪[L]

def

integerRingToFieldLinearMap

L781 ↗

CyclicCohomology.integerRingToFieldLinearMap

Documentation

The inclusion 𝒪_L -> L as an 𝒪_K-linear map, using the valuation-extension map 𝒪_K -> 𝒪_L for the scalar action.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · full declaration

def integerRingToFieldLinearMap : 𝒪[L] →ₗ[𝒪[K]] L where
  toFun x := (x : L)
  map_add' := by
    intro x y
    rfl
  map_smul' := by
    intro a x
    rfl

def

integerRingFieldSubmodule

L792 ↗

CyclicCohomology.integerRingFieldSubmodule

Documentation

The valuation integer ring of L, viewed as an 𝒪_K-submodule of L. This is the 𝒪_L lattice compared with the normal-basis lattice.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · full declaration

def integerRingFieldSubmodule : Submodule 𝒪[K] L where
  carrier := {x | x ∈ 𝒪[L]}
  zero_mem' := by
    change (0 : L) ∈ 𝒪[L]
    exact zero_mem _
  add_mem' := by
    intro x y hx hy
    change x + y ∈ 𝒪[L]
    exact add_mem hx hy
  smul_mem' := by
    intro a x hx
    change a • x ∈ 𝒪[L]
    rw [Algebra.smul_def]
    have ha : algebraMap 𝒪[K] L a ∈ 𝒪[L] := by
      change algebraMap K L (a : K) ∈ 𝒪[L]
      exact (integerRingMapOfValuationExtension K L a).2
    exact mul_mem ha hx

theorem

mem_integerRingFieldSubmodule_iff

L814 ↗

CyclicCohomology.mem_integerRingFieldSubmodule_iff

Documentation

Characterizes the field elements lying in the embedded integer-ring submodule.

Source context 11 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [FiniteDimensional K L] [IsGalois K L] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K] in

Lean source · statement

theorem mem_integerRingFieldSubmodule_iff (x : L) :
    x ∈ integerRingFieldSubmodule K L ↔ x ∈ 𝒪[L]

theorem

integerRing_mem_integerRingFieldSubmodule

L821 ↗

CyclicCohomology.integerRing_mem_integerRingFieldSubmodule

Documentation

Every integer-ring element lies in the corresponding field submodule.

Source context 11 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [FiniteDimensional K L] [IsGalois K L] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K] in

Lean source · statement

theorem integerRing_mem_integerRingFieldSubmodule (x : 𝒪[L]) :
    (x : L) ∈ integerRingFieldSubmodule K L

theorem

chosenBaseUniformizerPow_integerRingFieldSubmodule_mem_nhds_zero

L827 ↗

CyclicCohomology.chosenBaseUniformizerPow_integerRingFieldSubmodule_mem_nhds_zero

Documentation

A base-uniformizer multiple of 𝒪_L is a zero-neighborhood in L.

Source context 11 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem chosenBaseUniformizerPow_integerRingFieldSubmodule_mem_nhds_zero
    [TopologicalSpace L] [IsNonarchimedeanLocalField L] (m : Nat) :
    ((chosenBaseUniformizerPowSubmodule K L m
      (integerRingFieldSubmodule K L) : Set L)) ∈ nhds (0 : L)

def

maximalIdealFieldSubmodule

L865 ↗

CyclicCohomology.maximalIdealFieldSubmodule

Documentation

The maximal ideal 𝓂_L, viewed inside L as an 𝒪_K-submodule.

Source context 11 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [FiniteDimensional K L] [IsGalois K L] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K] in

Lean source · full declaration

def maximalIdealFieldSubmodule : Submodule 𝒪[K] L where
  carrier := {x | ∃ a : 𝒪[L], a ∈ (𝓂[L] : Ideal 𝒪[L]) ∧ (a : L) = x}
  zero_mem' := by
    refine ⟨0, by simp, by simp⟩
  add_mem' := by
    intro x y hx hy
    rcases hx with ⟨a, ha, rfl⟩
    rcases hy with ⟨b, hb, rfl⟩
    refine ⟨a + b, (𝓂[L] : Ideal 𝒪[L]).add_mem ha hb, by simp⟩
  smul_mem' := by
    intro c x hx
    rcases hx with ⟨a, ha, rfl⟩
    refine ⟨integerRingMapOfValuationExtension K L c * a, ?_, ?_⟩
    · exact Ideal.mul_mem_left _ (integerRingMapOfValuationExtension K L c) ha
    · change ((integerRingMapOfValuationExtension K L c : 𝒪[L]) : L) * (a : L) =
        c • (a : L)
      rw [Algebra.smul_def]
      congr 1

theorem

mem_maximalIdealFieldSubmodule_iff

L888 ↗

CyclicCohomology.mem_maximalIdealFieldSubmodule_iff

Documentation

Characterizes membership in the field submodule induced by the maximal ideal.

Source context 11 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [FiniteDimensional K L] [IsGalois K L] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K] in

Lean source · statement

theorem mem_maximalIdealFieldSubmodule_iff (x : L) :
    x ∈ maximalIdealFieldSubmodule K L ↔
      ∃ a : 𝒪[L], a ∈ (𝓂[L] : Ideal 𝒪[L]) ∧ (a : L) = x

theorem

maximalIdealFieldSubmodule_le_integerRingFieldSubmodule

L896 ↗

CyclicCohomology.maximalIdealFieldSubmodule_le_integerRingFieldSubmodule

Documentation

The maximal-ideal field submodule is contained in the integer-ring field submodule.

Source context 11 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [FiniteDimensional K L] [IsGalois K L] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K] in

Lean source · statement

theorem maximalIdealFieldSubmodule_le_integerRingFieldSubmodule :
    maximalIdealFieldSubmodule K L ≤ integerRingFieldSubmodule K L

theorem

exists_chosenBaseUniformizerPowSubmodule_le_integerRingFieldSubmodule_of_fg

L910 ↗

CyclicCohomology.exists_chosenBaseUniformizerPowSubmodule_le_integerRingFieldSubmodule_of_fg

Documentation

A finitely generated 𝒪_K-submodule of L is sent into 𝒪_L after multiplication by a single sufficiently high power of the base prime element.

This proves the π_K^b N ≤ 𝒪_L first direction of the lattice-bound statement for any finitely generated N; applying it to the normal-basis lattice gives the needed denominator bound for M.

Source context 11 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem exists_chosenBaseUniformizerPowSubmodule_le_integerRingFieldSubmodule_of_fg
    [TopologicalSpace L] [IsNonarchimedeanLocalField L]
    {N : Submodule 𝒪[K] L} (hN : N.FG) :
    ∃ n : Nat,
      chosenBaseUniformizerPowSubmodule K L n N ≤ integerRingFieldSubmodule K L

theorem

exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_le_integerRingFieldSubmodule

L966 ↗

CyclicCohomology.exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_le_integerRingFieldSubmodule

Documentation

Some uniformizer-power normal-basis lattice lies inside the integer-ring field submodule.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

theorem exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_le_integerRingFieldSubmodule
    [TopologicalSpace L] [IsNonarchimedeanLocalField L] :
    ∃ n : Nat,
      chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) ≤
        integerRingFieldSubmodule K L

theorem

chosenBaseUniformizerPowSubmodule_add_le_chosenBaseUniformizerPowSubmodule_of_le

L977 ↗

CyclicCohomology.chosenBaseUniformizerPowSubmodule_add_le_chosenBaseUniformizerPowSubmodule_of_le

Documentation

Multiplying an existing containment by a further base-uniformizer power.

Source context 11 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [FiniteDimensional K L] [IsGalois K L] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] in

Lean source · statement

theorem chosenBaseUniformizerPowSubmodule_add_le_chosenBaseUniformizerPowSubmodule_of_le
    {N M : Submodule 𝒪[K] L} {a n : Nat}
    (h : chosenBaseUniformizerPowSubmodule K L a N ≤ M) :
    chosenBaseUniformizerPowSubmodule K L (a + n) N ≤
      chosenBaseUniformizerPowSubmodule K L n M

theorem

chosenBaseUniformizerPowSubmodule_succ_le_maximalIdealFieldSubmodule_of_le_integerRingFieldSubmodule

L994 ↗

CyclicCohomology.chosenBaseUniformizerPowSubmodule_succ_le_maximalIdealFieldSubmodule_of_le_integerRingFieldSubmodule

Documentation

If π_K^b N is integral, then π_K^(b+1) N lands in the maximal ideal of 𝒪_L.

Source context 11 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem
chosenBaseUniformizerPowSubmodule_succ_le_maximalIdealFieldSubmodule_of_le_integerRingFieldSubmodule
    {N : Submodule 𝒪[K] L} {b : Nat}
    (hb : chosenBaseUniformizerPowSubmodule K L b N ≤ integerRingFieldSubmodule K L) :
    chosenBaseUniformizerPowSubmodule K L (b + 1) N ≤
      maximalIdealFieldSubmodule K L

theorem

exists_chosenBaseUniformizerPowSubmodule_le_maximalIdealFieldSubmodule_of_fg

L1031 ↗

CyclicCohomology.exists_chosenBaseUniformizerPowSubmodule_le_maximalIdealFieldSubmodule_of_fg

Documentation

A finitely generated submodule has a sufficiently deep uniformizer multiple inside the maximal ideal.

Source context 11 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem exists_chosenBaseUniformizerPowSubmodule_le_maximalIdealFieldSubmodule_of_fg
    [TopologicalSpace L] [IsNonarchimedeanLocalField L]
    {N : Submodule 𝒪[K] L} (hN : N.FG) :
    ∃ n : Nat,
      chosenBaseUniformizerPowSubmodule K L n N ≤ maximalIdealFieldSubmodule K L

theorem

exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_le_maximalIdealFieldSubmodule

L1044 ↗

CyclicCohomology.exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_le_maximalIdealFieldSubmodule

Documentation

Some uniformizer-power normal-basis lattice lies inside the maximal-ideal field submodule.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

theorem
  exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_le_maximalIdealFieldSubmodule
    [TopologicalSpace L] [IsNonarchimedeanLocalField L] :
    ∃ n : Nat,
      chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) ≤
        maximalIdealFieldSubmodule K L

theorem

exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_le_maximalIdeal_and_mul_closed

L1055 ↗

CyclicCohomology.exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_le_maximalIdeal_and_mul_closed

Documentation

A sufficiently deep normal-basis lattice lies in the maximal ideal and is multiplicatively closed.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

theorem
  exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_le_maximalIdeal_and_mul_closed
    [TopologicalSpace L] [IsNonarchimedeanLocalField L] :
    ∃ c : Nat, ∀ n : Nat, c ≤ n →
      chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) ≤
        maximalIdealFieldSubmodule K L ∧
      ∀ x : L,
        x ∈ chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) →
        ∀ y : L,
          y ∈ chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) →
            x * y ∈
              chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L)

def

chosenNormalBasisPrincipalUnitSet

L1088 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSet

Documentation

The actual carrier of the classical auxiliary principal-unit lattice V^n = 1 + π_K^n M, viewed as a set of units of 𝒪_L.

This set becomes a subgroup once inverse closure is supplied by the complete geometric-series argument.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

def chosenNormalBasisPrincipalUnitSet (n : Nat) : Set 𝒪[L]ˣ

theorem

mem_chosenNormalBasisPrincipalUnitSet_iff

L1096 ↗

CyclicCohomology.mem_chosenNormalBasisPrincipalUnitSet_iff

Documentation

Characterizes membership in the principal-unit set arising from a normal-basis lattice.

Source context 11 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [Valuation.HasExtension
  (ValuativeRel.valuation K) (ValuativeRel.valuation L)] in

Lean source · statement

theorem mem_chosenNormalBasisPrincipalUnitSet_iff (n : Nat) (u : 𝒪[L]ˣ) :
    u ∈ chosenNormalBasisPrincipalUnitSet K L n ↔
      ((((u : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) ∈
        chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L)

theorem

chosenNormalBasisPrincipalUnitSet_one_mem

L1105 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSet_one_mem

Documentation

The identity belongs to the chosen normal-basis principal-unit set.

Source context 11 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [Valuation.HasExtension
  (ValuativeRel.valuation K) (ValuativeRel.valuation L)] in

Lean source · statement

theorem chosenNormalBasisPrincipalUnitSet_one_mem (n : Nat) :
    (1 : 𝒪[L]ˣ) ∈ chosenNormalBasisPrincipalUnitSet K L n

theorem

chosenNormalBasisPrincipalUnitSet_mul_mem

L1113 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSet_mul_mem

Documentation

The chosen normal-basis principal-unit set is closed under multiplication.

Source context 11 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [Valuation.HasExtension
  (ValuativeRel.valuation K) (ValuativeRel.valuation L)] in

Lean source · statement

theorem chosenNormalBasisPrincipalUnitSet_mul_mem {n : Nat}
    (hmul : ∀ x : L,
      x ∈ chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) →
      ∀ y : L,
        y ∈ chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) →
          x * y ∈ chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L))
    {u v : 𝒪[L]ˣ}
    (hu : u ∈ chosenNormalBasisPrincipalUnitSet K L n)
    (hv : v ∈ chosenNormalBasisPrincipalUnitSet K L n) :
    u * v ∈ chosenNormalBasisPrincipalUnitSet K L n

theorem

chosenNormalBasisPrincipalUnitSet_mem_principalUnits_one

L1143 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSet_mem_principalUnits_one

Documentation

Every chosen normal-basis principal unit belongs to the first principal-unit group.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

theorem chosenNormalBasisPrincipalUnitSet_mem_principalUnits_one {n : Nat}
    (hle : chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) ≤
      maximalIdealFieldSubmodule K L)
    {u : 𝒪[L]ˣ} (hu : u ∈ chosenNormalBasisPrincipalUnitSet K L n) :
    u ∈ principalUnits L 1

theorem

exists_chosenNormalBasisPrincipalUnitSet_mul_closed_le_principalUnits_one

L1162 ↗

CyclicCohomology.exists_chosenNormalBasisPrincipalUnitSet_mul_closed_le_principalUnits_one

Documentation

There is a multiplicatively closed normal-basis principal-unit set inside the first principal-unit group.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

theorem exists_chosenNormalBasisPrincipalUnitSet_mul_closed_le_principalUnits_one
    [TopologicalSpace L] [IsNonarchimedeanLocalField L] :
    ∃ c : Nat, ∀ n : Nat, c ≤ n →
      (∀ u : 𝒪[L]ˣ, u ∈ chosenNormalBasisPrincipalUnitSet K L n →
        ∀ v : 𝒪[L]ˣ, v ∈ chosenNormalBasisPrincipalUnitSet K L n →
          u * v ∈ chosenNormalBasisPrincipalUnitSet K L n) ∧
      ∀ u : 𝒪[L]ˣ, u ∈ chosenNormalBasisPrincipalUnitSet K L n →
        u ∈ principalUnits L 1

theorem

chosenNormalBasisPrincipalUnitSet_inverseCorrectionPartialSum_mem

L1187 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSet_inverseCorrectionPartialSum_mem

Documentation

The inverse-correction partial sums remain in the lattice underlying the principal-unit set.

Source context 11 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [Valuation.HasExtension
  (ValuativeRel.valuation K) (ValuativeRel.valuation L)] in

Lean source · statement

theorem chosenNormalBasisPrincipalUnitSet_inverseCorrectionPartialSum_mem {n : Nat}
    (hmul : ∀ x : L,
      x ∈ chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) →
      ∀ y : L,
        y ∈ chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) →
          x * y ∈ chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L))
    {u : 𝒪[L]ˣ} (hu : u ∈ chosenNormalBasisPrincipalUnitSet K L n) (d : Nat) :
    inverseCorrectionPartialSum (L := L)
        ((((u : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) d ∈
      chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L)

theorem

exists_chosenNormalBasisPrincipalUnitSet_inverseCorrectionPartialSum_mem

L1202 ↗

CyclicCohomology.exists_chosenNormalBasisPrincipalUnitSet_inverseCorrectionPartialSum_mem

Documentation

A suitable normal-basis principal-unit set contains every inverse-correction partial sum.

Source context 11 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [Valuation.HasExtension
  (ValuativeRel.valuation K) (ValuativeRel.valuation L)] in

Lean source · statement

theorem exists_chosenNormalBasisPrincipalUnitSet_inverseCorrectionPartialSum_mem :
    ∃ c : Nat, ∀ n : Nat, c ≤ n →
      ∀ u : 𝒪[L]ˣ, u ∈ chosenNormalBasisPrincipalUnitSet K L n → ∀ d : Nat,
        inverseCorrectionPartialSum (L := L)
            ((((u : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) d ∈
          chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L)

theorem

chosenNormalBasisPrincipalUnitSet_inverseCorrectionPartialProductError_mem

L1219 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSet_inverseCorrectionPartialProductError_mem

Documentation

The inverse-correction product error remains in the chosen lattice.

Source context 11 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [Valuation.HasExtension
  (ValuativeRel.valuation K) (ValuativeRel.valuation L)] in

Lean source · statement

theorem chosenNormalBasisPrincipalUnitSet_inverseCorrectionPartialProductError_mem {n : Nat}
    (hmul : ∀ x : L,
      x ∈ chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) →
      ∀ y : L,
        y ∈ chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) →
          x * y ∈ chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L))
    {u : 𝒪[L]ˣ} (hu : u ∈ chosenNormalBasisPrincipalUnitSet K L n) (d : Nat) :
    (((u : 𝒪[L]ˣ) : 𝒪[L]) : L) *
        (1 + inverseCorrectionPartialSum (L := L)
          ((((u : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) d) - 1 ∈
      chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L)

theorem

exists_chosenNormalBasisPrincipalUnitSet_inverseCorrectionPartialProductError_mem

L1245 ↗

CyclicCohomology.exists_chosenNormalBasisPrincipalUnitSet_inverseCorrectionPartialProductError_mem

Documentation

A suitable normal-basis principal-unit set contains every inverse-correction product error.

Source context 11 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [Valuation.HasExtension
  (ValuativeRel.valuation K) (ValuativeRel.valuation L)] in

Lean source · statement

theorem exists_chosenNormalBasisPrincipalUnitSet_inverseCorrectionPartialProductError_mem :
    ∃ c : Nat, ∀ n : Nat, c ≤ n →
      ∀ u : 𝒪[L]ˣ, u ∈ chosenNormalBasisPrincipalUnitSet K L n → ∀ d : Nat,
        (((u : 𝒪[L]ˣ) : 𝒪[L]) : L) *
            (1 + inverseCorrectionPartialSum (L := L)
              ((((u : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) d) - 1 ∈
          chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L)

theorem

chosenNormalBasisPrincipalUnitSet_neg_sub_one_pow_succ_tendsto_zero

L1261 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSet_neg_sub_one_pow_succ_tendsto_zero

Documentation

Successive powers of the negative deviation from one converge to zero.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · full declaration

theorem chosenNormalBasisPrincipalUnitSet_neg_sub_one_pow_succ_tendsto_zero
    [TopologicalSpace L] [IsNonarchimedeanLocalField L] {n : Nat}
    (hle : chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) ≤
      maximalIdealFieldSubmodule K L)
    {u : 𝒪[L]ˣ} (hu : u ∈ chosenNormalBasisPrincipalUnitSet K L n) :
    Tendsto
      (fun d : Nat => (-(((u : 𝒪[L]ˣ) : 𝒪[L]) - 1)) ^ (d + 1))
      atTop (nhds (0 : 𝒪[L])) := by
  have hu_one : u ∈ principalUnits L 1 :=
    chosenNormalBasisPrincipalUnitSet_mem_principalUnits_one
      (K := K) (L := L) hle hu
  have hpow :
      (((u : 𝒪[L]ˣ) : 𝒪[L]) - 1) ∈ (𝓂[L] ^ 1 : Ideal 𝒪[L]) :=
    (mem_principalUnits_iff L u 1).1 hu_one
  have hmax :
      (((u : 𝒪[L]ˣ) : 𝒪[L]) - 1) ∈ (𝓂[L] : Ideal 𝒪[L]) := by
    simpa [pow_one] using hpow
  exact tendsto_neg_pow_succ_of_mem_maximalIdeal L hmax

theorem

exists_chosenNormalBasisPrincipalUnitSet_neg_sub_one_pow_succ_tendsto_zero

L1282 ↗

CyclicCohomology.exists_chosenNormalBasisPrincipalUnitSet_neg_sub_one_pow_succ_tendsto_zero

Documentation

A suitable normal-basis principal-unit set has powers of the negative deviation converging to zero.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · full declaration

theorem exists_chosenNormalBasisPrincipalUnitSet_neg_sub_one_pow_succ_tendsto_zero
    [TopologicalSpace L] [IsNonarchimedeanLocalField L] :
    ∃ c : Nat, ∀ n : Nat, c ≤ n →
      ∀ u : 𝒪[L]ˣ, u ∈ chosenNormalBasisPrincipalUnitSet K L n →
        Tendsto
          (fun d : Nat => (-(((u : 𝒪[L]ˣ) : 𝒪[L]) - 1)) ^ (d + 1))
          atTop (nhds (0 : 𝒪[L])) := by
  rcases
    exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_le_maximalIdealFieldSubmodule
      (K := K) (L := L) with
    ⟨c, hc⟩
  refine ⟨c, ?_⟩
  intro n hcn u hu
  have hle :
      chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) ≤
        maximalIdealFieldSubmodule K L :=
    (chosenBaseUniformizerPowSubmodule_antitone
      (K := K) (L := L) (m := c) (n := n)
      (chosenNormalBasisIntegerLattice K L) hcn).trans hc
  exact chosenNormalBasisPrincipalUnitSet_neg_sub_one_pow_succ_tendsto_zero
    (K := K) (L := L) hle hu

theorem

chosenNormalBasisPrincipalUnitSet_inverseCorrectionProduct_tendsto_one

L1305 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSet_inverseCorrectionProduct_tendsto_one

Documentation

The inverse-correction partial products converge to one.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · full declaration

theorem chosenNormalBasisPrincipalUnitSet_inverseCorrectionProduct_tendsto_one
    [TopologicalSpace L] [IsNonarchimedeanLocalField L] {n : Nat}
    (hle : chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) ≤
      maximalIdealFieldSubmodule K L)
    {u : 𝒪[L]ˣ} (hu : u ∈ chosenNormalBasisPrincipalUnitSet K L n) :
    Tendsto
      (fun d : Nat =>
        (((u : 𝒪[L]ˣ) : 𝒪[L]) : L) *
          (1 + inverseCorrectionPartialSum (L := L)
            ((((u : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) d))
      atTop (nhds (1 : L)) := by
  let x𝒪 : 𝒪[L] := ((u : 𝒪[L]ˣ) : 𝒪[L]) - 1
  let x : L := (x𝒪 : L)
  have hres𝒪 :
      Tendsto (fun d : Nat => (-x𝒪) ^ (d + 1)) atTop (nhds (0 : 𝒪[L])) := by
    simpa [x𝒪] using
      chosenNormalBasisPrincipalUnitSet_neg_sub_one_pow_succ_tendsto_zero
        (K := K) (L := L) hle hu
  have hresL :
      Tendsto (fun d : Nat => ((((-x𝒪) ^ (d + 1) : 𝒪[L]) : L)))
        atTop (nhds (0 : L)) :=
    (continuous_subtype_val.tendsto (0 : 𝒪[L])).comp hres𝒪
  have htarget :
      Tendsto (fun d : Nat => (1 : L) - ((((-x𝒪) ^ (d + 1) : 𝒪[L]) : L)))
        atTop (nhds (1 : L)) := by
    simpa using (tendsto_const_nhds (x := (1 : L))).sub hresL
  refine htarget.congr' (Eventually.of_forall ?_)
  intro d
  have hgeom :
      (1 + x) * (1 + inverseCorrectionPartialSum (L := L) x d) =
        1 - (-x) ^ (d + 1) :=
    one_add_mul_one_add_inverseCorrectionPartialSum (L := L) x d
  have hu_eq : 1 + x = (((u : 𝒪[L]ˣ) : 𝒪[L]) : L) := by
    simp [x, x𝒪]
  simpa [x, x𝒪, hu_eq] using hgeom.symm

theorem

chosenNormalBasisPrincipalUnitSet_one_add_inverseCorrection_tendsto_inv

L1342 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSet_one_add_inverseCorrection_tendsto_inv

Documentation

One plus the inverse correction converges to the multiplicative inverse.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · full declaration

theorem chosenNormalBasisPrincipalUnitSet_one_add_inverseCorrection_tendsto_inv
    [TopologicalSpace L] [IsNonarchimedeanLocalField L] {n : Nat}
    (hle : chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) ≤
      maximalIdealFieldSubmodule K L)
    {u : 𝒪[L]ˣ} (hu : u ∈ chosenNormalBasisPrincipalUnitSet K L n) :
    Tendsto
      (fun d : Nat =>
        1 + inverseCorrectionPartialSum (L := L)
          ((((u : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) d)
      atTop (nhds ((((u⁻¹ : 𝒪[L]ˣ) : 𝒪[L]) : L))) := by
  have hprod :=
    chosenNormalBasisPrincipalUnitSet_inverseCorrectionProduct_tendsto_one
      (K := K) (L := L) hle hu
  have hmul :
      Tendsto
        (fun d : Nat =>
          (((u⁻¹ : 𝒪[L]ˣ) : 𝒪[L]) : L) *
            ((((u : 𝒪[L]ˣ) : 𝒪[L]) : L) *
              (1 + inverseCorrectionPartialSum (L := L)
                ((((u : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) d)))
        atTop (nhds ((((u⁻¹ : 𝒪[L]ˣ) : 𝒪[L]) : L))) := by
    simpa using
      (tendsto_const_nhds (x := (((u⁻¹ : 𝒪[L]ˣ) : 𝒪[L]) : L))).mul hprod
  refine hmul.congr' (Eventually.of_forall ?_)
  intro d
  have huinv :
      ((((u⁻¹ : 𝒪[L]ˣ) : 𝒪[L]) : L)) *
          ((((u : 𝒪[L]ˣ) : 𝒪[L]) : L)) = 1 := by
    have huinvₒ :
        (((u⁻¹ : 𝒪[L]ˣ) : 𝒪[L]) * ((u : 𝒪[L]ˣ) : 𝒪[L])) = 1 :=
      Units.inv_mul u
    exact congrArg (algebraMap 𝒪[L] L) huinvₒ
  rw [← mul_assoc, huinv, one_mul]

theorem

chosenNormalBasisPrincipalUnitSet_inverseCorrection_tendsto_inv_sub_one

L1377 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSet_inverseCorrection_tendsto_inv_sub_one

Documentation

The inverse correction converges to the inverse minus one.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · full declaration

theorem chosenNormalBasisPrincipalUnitSet_inverseCorrection_tendsto_inv_sub_one
    [TopologicalSpace L] [IsNonarchimedeanLocalField L] {n : Nat}
    (hle : chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) ≤
      maximalIdealFieldSubmodule K L)
    {u : 𝒪[L]ˣ} (hu : u ∈ chosenNormalBasisPrincipalUnitSet K L n) :
    Tendsto
      (fun d : Nat =>
        inverseCorrectionPartialSum (L := L)
          ((((u : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) d)
      atTop (nhds (((((u⁻¹ : 𝒪[L]ˣ) : 𝒪[L]) : L) - 1))) := by
  have h :=
    chosenNormalBasisPrincipalUnitSet_one_add_inverseCorrection_tendsto_inv
      (K := K) (L := L) hle hu
  simpa [sub_eq_add_neg, add_assoc, add_comm, add_left_comm] using
    h.sub (tendsto_const_nhds (x := (1 : L)))

theorem

exists_chosenNormalBasisPrincipalUnitSet_inverseCorrection_tendsto_inv_sub_one

L1395 ↗

CyclicCohomology.exists_chosenNormalBasisPrincipalUnitSet_inverseCorrection_tendsto_inv_sub_one

Documentation

A suitable normal-basis principal-unit set admits inverse corrections converging to the inverse minus one.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · full declaration

theorem exists_chosenNormalBasisPrincipalUnitSet_inverseCorrection_tendsto_inv_sub_one
    [TopologicalSpace L] [IsNonarchimedeanLocalField L] :
    ∃ c : Nat, ∀ n : Nat, c ≤ n →
      ∀ u : 𝒪[L]ˣ, u ∈ chosenNormalBasisPrincipalUnitSet K L n →
        Tendsto
          (fun d : Nat =>
            inverseCorrectionPartialSum (L := L)
              ((((u : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) d)
          atTop (nhds (((((u⁻¹ : 𝒪[L]ˣ) : 𝒪[L]) : L) - 1))) := by
  rcases
    exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_le_maximalIdealFieldSubmodule
      (K := K) (L := L) with
    ⟨c, hc⟩
  refine ⟨c, ?_⟩
  intro n hcn u hu
  have hle :
      chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) ≤
        maximalIdealFieldSubmodule K L :=
    (chosenBaseUniformizerPowSubmodule_antitone
      (K := K) (L := L) (m := c) (n := n)
      (chosenNormalBasisIntegerLattice K L) hcn).trans hc
  exact chosenNormalBasisPrincipalUnitSet_inverseCorrection_tendsto_inv_sub_one
    (K := K) (L := L) hle hu

theorem

chosenNormalBasisPrincipalUnitSet_inverse_sub_one_mem_of_closed

L1420 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSet_inverse_sub_one_mem_of_closed

Documentation

Closedness of the lattice puts the inverse minus one back in the lattice.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

theorem chosenNormalBasisPrincipalUnitSet_inverse_sub_one_mem_of_closed
    [TopologicalSpace L] [IsNonarchimedeanLocalField L] {n : Nat}
    (hclosed : IsClosed
      ((chosenBaseUniformizerPowSubmodule K L n
        (chosenNormalBasisIntegerLattice K L) : Set L)))
    (hle : chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) ≤
      maximalIdealFieldSubmodule K L)
    (hmul : ∀ x : L,
      x ∈ chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) →
      ∀ y : L,
        y ∈ chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) →
          x * y ∈ chosenBaseUniformizerPowSubmodule K L n
            (chosenNormalBasisIntegerLattice K L))
    {u : 𝒪[L]ˣ} (hu : u ∈ chosenNormalBasisPrincipalUnitSet K L n) :
    ((((u⁻¹ : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) ∈
      chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L)

theorem

chosenNormalBasisPrincipalUnitSet_inv_mem_of_closed

L1449 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSet_inv_mem_of_closed

Documentation

A closed normal-basis principal-unit set is closed under inversion.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

theorem chosenNormalBasisPrincipalUnitSet_inv_mem_of_closed
    [TopologicalSpace L] [IsNonarchimedeanLocalField L] {n : Nat}
    (hclosed : IsClosed
      ((chosenBaseUniformizerPowSubmodule K L n
        (chosenNormalBasisIntegerLattice K L) : Set L)))
    (hle : chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) ≤
      maximalIdealFieldSubmodule K L)
    (hmul : ∀ x : L,
      x ∈ chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) →
      ∀ y : L,
        y ∈ chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) →
          x * y ∈ chosenBaseUniformizerPowSubmodule K L n
            (chosenNormalBasisIntegerLattice K L))
    {u : 𝒪[L]ˣ} (hu : u ∈ chosenNormalBasisPrincipalUnitSet K L n) :
    u⁻¹ ∈ chosenNormalBasisPrincipalUnitSet K L n

theorem

exists_chosenNormalBasisPrincipalUnitSet_inv_mem_of_closed

L1469 ↗

CyclicCohomology.exists_chosenNormalBasisPrincipalUnitSet_inv_mem_of_closed

Documentation

There is a closed normal-basis principal-unit set stable under inversion.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

theorem exists_chosenNormalBasisPrincipalUnitSet_inv_mem_of_closed
    [TopologicalSpace L] [IsNonarchimedeanLocalField L] :
    ∃ c : Nat, ∀ n : Nat, c ≤ n →
      IsClosed
        ((chosenBaseUniformizerPowSubmodule K L n
          (chosenNormalBasisIntegerLattice K L) : Set L)) →
      ∀ u : 𝒪[L]ˣ, u ∈ chosenNormalBasisPrincipalUnitSet K L n →
        u⁻¹ ∈ chosenNormalBasisPrincipalUnitSet K L n

theorem

integerRingToFieldLinearMap_range_eq

L1490 ↗

CyclicCohomology.integerRingToFieldLinearMap_range_eq

Documentation

The range of the integer-ring inclusion is the integer-ring field submodule.

Source context 11 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [FiniteDimensional K L] [IsGalois K L] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K] in

Lean source · statement

theorem integerRingToFieldLinearMap_range_eq :
    LinearMap.range (integerRingToFieldLinearMap K L) =
      integerRingFieldSubmodule K L

theorem

integerRingFieldSubmodule_fg_of_moduleFinite

L1504 ↗

CyclicCohomology.integerRingFieldSubmodule_fg_of_moduleFinite

Documentation

If the extension valuation ring is finite over the base valuation ring, then 𝒪_L, viewed inside L, is a finitely generated 𝒪_K-submodule.

Source context 11 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [FiniteDimensional K L] [IsGalois K L] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K] in

Lean source · statement

theorem integerRingFieldSubmodule_fg_of_moduleFinite
    [Module.Finite 𝒪[K] 𝒪[L]] :
    (integerRingFieldSubmodule K L).FG

theorem

exists_chosenBaseUniformizerPow_integerRingFieldSubmodule_le_chosenNormalBasisIntegerLattice

L1522 ↗

CyclicCohomology.exists_chosenBaseUniformizerPow_integerRingFieldSubmodule_le_chosenNormalBasisIntegerLattice

Documentation

The reverse lattice bound: if 𝒪_L is finite over 𝒪_K, then a single high enough base-uniformizer power sends 𝒪_L into the normal-basis lattice M.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

theorem exists_chosenBaseUniformizerPow_integerRingFieldSubmodule_le_chosenNormalBasisIntegerLattice
    [Module.Finite 𝒪[K] 𝒪[L]] :
    ∃ n : Nat,
      chosenBaseUniformizerPowSubmodule K L n (integerRingFieldSubmodule K L) ≤
        chosenNormalBasisIntegerLattice K L

theorem

exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_mem_nhds_zero

L1535 ↗

CyclicCohomology.exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_mem_nhds_zero

Documentation

Some uniformizer-power normal-basis lattice is a neighborhood of zero.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

theorem exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_mem_nhds_zero
    [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Module.Finite 𝒪[K] 𝒪[L]] :
    ∃ c : Nat, ∀ n : Nat, c ≤ n →
      ((chosenBaseUniformizerPowSubmodule K L n
        (chosenNormalBasisIntegerLattice K L) : Set L)) ∈ nhds (0 : L)

theorem

exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_isClosed

L1555 ↗

CyclicCohomology.exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_isClosed

Documentation

Some uniformizer-power normal-basis lattice is closed.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

theorem exists_chosenBaseUniformizerPow_chosenNormalBasisIntegerLattice_isClosed
    [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Module.Finite 𝒪[K] 𝒪[L]] :
    ∃ c : Nat, ∀ n : Nat, c ≤ n →
      IsClosed
        ((chosenBaseUniformizerPowSubmodule K L n
          (chosenNormalBasisIntegerLattice K L) : Set L))

theorem

exists_chosenNormalBasisPrincipalUnitSet_inv_mem

L1571 ↗

CyclicCohomology.exists_chosenNormalBasisPrincipalUnitSet_inv_mem

Documentation

There is a chosen normal-basis principal-unit set stable under inversion.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

theorem exists_chosenNormalBasisPrincipalUnitSet_inv_mem
    [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Module.Finite 𝒪[K] 𝒪[L]] :
    ∃ c : Nat, ∀ n : Nat, c ≤ n →
      ∀ u : 𝒪[L]ˣ, u ∈ chosenNormalBasisPrincipalUnitSet K L n →
        u⁻¹ ∈ chosenNormalBasisPrincipalUnitSet K L n

theorem

exists_chosenNormalBasisPrincipalUnitSubgroup

L1589 ↗

CyclicCohomology.exists_chosenNormalBasisPrincipalUnitSubgroup

Documentation

There exists a principal-unit subgroup arising from a chosen normal-basis lattice.

Source context 10 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K]
variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

theorem exists_chosenNormalBasisPrincipalUnitSubgroup
    [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Module.Finite 𝒪[K] 𝒪[L]] :
    ∃ c : Nat, ∀ n : Nat, c ≤ n →
      ∃ V : Subgroup 𝒪[L]ˣ,
        (V : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L n ∧
        V ≤ principalUnits L 1

theorem

chosenNormalBasisPrincipalUnitSet_succ_subset

L1643 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSet_succ_subset

Documentation

The principal-unit lattice carriers form a descending filtration.

Source context 8 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [Valuation.HasExtension
  (ValuativeRel.valuation K) (ValuativeRel.valuation L)] in

Lean source · statement

theorem chosenNormalBasisPrincipalUnitSet_succ_subset (n : Nat) :
    chosenNormalBasisPrincipalUnitSet K L (n + 1) ⊆
      chosenNormalBasisPrincipalUnitSet K L n

def

chosenNormalBasisLatticeSuccSubmodule

L1652 ↗

CyclicCohomology.chosenNormalBasisLatticeSuccSubmodule

Documentation

The denominator submodule π_K^(n+1)M, viewed inside π_K^nM.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

def chosenNormalBasisLatticeSuccSubmodule (n : Nat) :
    Submodule 𝒪[K]
      (chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L))

def

chosenNormalBasisLatticeSuccQuot

L1661 ↗

CyclicCohomology.chosenNormalBasisLatticeSuccQuot

Documentation

The additive quotient π_K^nM / π_K^(n+1)M used in the local class-field calculation.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

def chosenNormalBasisLatticeSuccQuot (n : Nat) : Type u

instance

chosenNormalBasisLatticeSuccQuotAddCommGroup

L1666 ↗

CyclicCohomology.chosenNormalBasisLatticeSuccQuotAddCommGroup

Documentation

A successive quotient of normal-basis lattices is an additive commutative group.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

instance chosenNormalBasisLatticeSuccQuotAddCommGroup (n : Nat) :
    AddCommGroup (chosenNormalBasisLatticeSuccQuot K L n)

instance

chosenNormalBasisLatticeSuccQuotModule

L1675 ↗

CyclicCohomology.chosenNormalBasisLatticeSuccQuotModule

Documentation

A successive normal-basis lattice quotient carries the natural residue-field module structure.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

instance chosenNormalBasisLatticeSuccQuotModule (n : Nat) :
    Module 𝒪[K] (chosenNormalBasisLatticeSuccQuot K L n)

def

chosenNormalBasisLatticeSuccQuotConcreteLinearEquiv

L1684 ↗

CyclicCohomology.chosenNormalBasisLatticeSuccQuotConcreteLinearEquiv

Documentation

Explicit access to the concrete submodule quotient implementing the chosen normal-basis lattice graded piece.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

def chosenNormalBasisLatticeSuccQuotConcreteLinearEquiv (n : Nat) :
    chosenNormalBasisLatticeSuccQuot K L n ≃ₗ[𝒪[K]]
      ((chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L)) ⧸
        chosenNormalBasisLatticeSuccSubmodule K L n)

theorem

mem_chosenNormalBasisLatticeSuccSubmodule_iff

L1699 ↗

CyclicCohomology.mem_chosenNormalBasisLatticeSuccSubmodule_iff

Documentation

Characterizes membership in the next normal-basis lattice submodule.

Source context 8 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] in

Lean source · statement

theorem mem_chosenNormalBasisLatticeSuccSubmodule_iff (n : Nat)
    (x : chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L)) :
    x ∈ chosenNormalBasisLatticeSuccSubmodule K L n ↔
      (x : L) ∈ chosenBaseUniformizerPowSubmodule K L (n + 1)
        (chosenNormalBasisIntegerLattice K L)

def

chosenNormalBasisLatticeSuccQuotMk

L1707 ↗

CyclicCohomology.chosenNormalBasisLatticeSuccQuotMk

Documentation

The quotient map π_K^nM -> π_K^nM / π_K^(n+1)M.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

def chosenNormalBasisLatticeSuccQuotMk (n : Nat) :
    chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) →ₗ[𝒪[K]]
      chosenNormalBasisLatticeSuccQuot K L n

theorem

chosenNormalBasisLatticeSuccQuotConcreteLinearEquiv_mk

L1720 ↗

CyclicCohomology.chosenNormalBasisLatticeSuccQuotConcreteLinearEquiv_mk

Documentation

The concrete linear equivalence sends a lattice element to its canonical quotient class.

Source context 8 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] in

Lean source · statement

theorem chosenNormalBasisLatticeSuccQuotConcreteLinearEquiv_mk (n : Nat)
    (x : chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L)) :
    chosenNormalBasisLatticeSuccQuotConcreteLinearEquiv K L n
        (chosenNormalBasisLatticeSuccQuotMk K L n x) =
      Submodule.Quotient.mk x

theorem

chosenNormalBasisLatticeSuccQuotMk_surjective

L1730 ↗

CyclicCohomology.chosenNormalBasisLatticeSuccQuotMk_surjective

Documentation

Every successive lattice-quotient class has a representative.

Source context 8 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] in

Lean source · statement

theorem chosenNormalBasisLatticeSuccQuotMk_surjective (n : Nat) :
    Function.Surjective (chosenNormalBasisLatticeSuccQuotMk K L n)

theorem

inductionOn

L1738 ↗

CyclicCohomology.chosenNormalBasisLatticeSuccQuot.inductionOn

Documentation

Eliminate a chosen normal-basis lattice quotient through arbitrary representatives and its canonical class map.

Source context 8 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] in

Lean source · statement

theorem chosenNormalBasisLatticeSuccQuot.inductionOn
    (n : Nat)
    {motive : chosenNormalBasisLatticeSuccQuot K L n → Prop}
    (q : chosenNormalBasisLatticeSuccQuot K L n)
    (h : ∀ x :
      chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L),
      motive (chosenNormalBasisLatticeSuccQuotMk K L n x)) :
    motive q

def

chosenNormalBasisLatticeSuccQuotLift

L1756 ↗

CyclicCohomology.chosenNormalBasisLatticeSuccQuotLift

Documentation

Descend a representative-level function constant modulo the next chosen normal-basis lattice.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

def chosenNormalBasisLatticeSuccQuotLift
    {P : Sort*} (n : Nat)
    (f :
      chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) → P)
    (h : ∀ x y, x - y ∈ chosenNormalBasisLatticeSuccSubmodule K L n →
      f x = f y) :
    chosenNormalBasisLatticeSuccQuot K L n → P

theorem

chosenNormalBasisLatticeSuccQuotLift_mk

L1782 ↗

CyclicCohomology.chosenNormalBasisLatticeSuccQuotLift_mk

Documentation

The lifted map on a successive lattice quotient evaluates to the original map on representatives.

Source context 8 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] in

Lean source · statement

theorem chosenNormalBasisLatticeSuccQuotLift_mk
    {P : Sort*} (n : Nat)
    (f :
      chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) → P)
    (h : ∀ x y, x - y ∈ chosenNormalBasisLatticeSuccSubmodule K L n →
      f x = f y)
    (x : chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L)) :
    chosenNormalBasisLatticeSuccQuotLift K L n f h
        (chosenNormalBasisLatticeSuccQuotMk K L n x) = f x

def

chosenNormalBasisLatticeSuccQuotLinearLift

L1794 ↗

CyclicCohomology.chosenNormalBasisLatticeSuccQuotLinearLift

Documentation

Descend a linear map vanishing on the next chosen normal-basis lattice.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

def chosenNormalBasisLatticeSuccQuotLinearLift
    {M : Type*} [AddCommGroup M] [Module 𝒪[K] M] (n : Nat)
    (f :
      chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L)
        →ₗ[𝒪[K]] M)
    (h : chosenNormalBasisLatticeSuccSubmodule K L n ≤ f.ker) :
    chosenNormalBasisLatticeSuccQuot K L n →ₗ[𝒪[K]] M

theorem

chosenNormalBasisLatticeSuccQuotLinearLift_mk

L1809 ↗

CyclicCohomology.chosenNormalBasisLatticeSuccQuotLinearLift_mk

Documentation

The lifted linear map agrees with the original linear map on quotient representatives.

Source context 8 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] in

Lean source · statement

theorem chosenNormalBasisLatticeSuccQuotLinearLift_mk
    {M : Type*} [AddCommGroup M] [Module 𝒪[K] M] (n : Nat)
    (f :
      chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L)
        →ₗ[𝒪[K]] M)
    (h : chosenNormalBasisLatticeSuccSubmodule K L n ≤ f.ker)
    (x : chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L)) :
    chosenNormalBasisLatticeSuccQuotLinearLift K L n f h
        (chosenNormalBasisLatticeSuccQuotMk K L n x) = f x

theorem

chosenNormalBasisLatticeSuccQuotMk_eq_zero_iff

L1824 ↗

CyclicCohomology.chosenNormalBasisLatticeSuccQuotMk_eq_zero_iff

Documentation

A lattice representative gives zero in the successive quotient exactly when it lies at the next level.

Source context 8 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] in

Lean source · statement

theorem chosenNormalBasisLatticeSuccQuotMk_eq_zero_iff (n : Nat)
    (x : chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L)) :
    chosenNormalBasisLatticeSuccQuotMk K L n x = 0 ↔
      (x : L) ∈ chosenBaseUniformizerPowSubmodule K L (n + 1)
        (chosenNormalBasisIntegerLattice K L)

theorem

chosenNormalBasisLatticeSuccQuotMk_eq_iff

L1841 ↗

CyclicCohomology.chosenNormalBasisLatticeSuccQuotMk_eq_iff

Documentation

Two lattice representatives agree in the successive quotient exactly when their difference lies at the next level.

Source context 8 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] in

Lean source · statement

theorem chosenNormalBasisLatticeSuccQuotMk_eq_iff (n : Nat)
    (x y :
      chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L)) :
    chosenNormalBasisLatticeSuccQuotMk K L n x =
        chosenNormalBasisLatticeSuccQuotMk K L n y ↔
      x - y ∈ chosenNormalBasisLatticeSuccSubmodule K L n

def

chosenNormalBasisPrincipalUnitLatticeClass

L1855 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitLatticeClass

Documentation

The additive quotient class of u - 1 for u ∈ V^n.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

def chosenNormalBasisPrincipalUnitLatticeClass (n : Nat)
    (u : 𝒪[L]ˣ) (hu : u ∈ chosenNormalBasisPrincipalUnitSet K L n) :
    chosenNormalBasisLatticeSuccQuot K L n

theorem

chosenNormalBasisPrincipalUnitLatticeClass_eq_zero_iff

L1865 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitLatticeClass_eq_zero_iff

Documentation

A principal unit has zero lattice class exactly when its deviation from one lies at the next level.

Source context 8 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [Valuation.HasExtension
  (ValuativeRel.valuation K) (ValuativeRel.valuation L)] in

Lean source · statement

theorem chosenNormalBasisPrincipalUnitLatticeClass_eq_zero_iff {n : Nat}
    (u : 𝒪[L]ˣ) (hu : u ∈ chosenNormalBasisPrincipalUnitSet K L n) :
    chosenNormalBasisPrincipalUnitLatticeClass K L n u hu = 0 ↔
      u ∈ chosenNormalBasisPrincipalUnitSet K L (n + 1)

theorem

chosenNormalBasisPrincipalUnitSet_mul_error_mem_succ

L1877 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSet_mul_error_mem_succ

Documentation

The multiplicative error term for units in V^n is one lattice step deeper whenever products of elements of π_K^nM land in π_K^(n+1)M.

Source context 8 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [Valuation.HasExtension
  (ValuativeRel.valuation K) (ValuativeRel.valuation L)] in

Lean source · statement

theorem chosenNormalBasisPrincipalUnitSet_mul_error_mem_succ {n : Nat}
    (hmul_succ : ∀ x : L,
      x ∈ chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) →
      ∀ y : L,
        y ∈ chosenBaseUniformizerPowSubmodule K L n (chosenNormalBasisIntegerLattice K L) →
          x * y ∈
            chosenBaseUniformizerPowSubmodule K L (n + 1) (chosenNormalBasisIntegerLattice K L))
    {u v : 𝒪[L]ˣ}
    (hu : u ∈ chosenNormalBasisPrincipalUnitSet K L n)
    (hv : v ∈ chosenNormalBasisPrincipalUnitSet K L n) :
    (((((u * v : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) -
        (((((u : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) +
          ((((v : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L))) ∈
      chosenBaseUniformizerPowSubmodule K L (n + 1)
        (chosenNormalBasisIntegerLattice K L)

theorem

exists_chosenNormalBasisPrincipalUnitSet_mul_error_mem_succ

L1918 ↗

CyclicCohomology.exists_chosenNormalBasisPrincipalUnitSet_mul_error_mem_succ

Documentation

A suitable normal-basis principal-unit set has multiplication error in the next lattice level.

Source context 8 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [Valuation.HasExtension
  (ValuativeRel.valuation K) (ValuativeRel.valuation L)] in

Lean source · statement

theorem exists_chosenNormalBasisPrincipalUnitSet_mul_error_mem_succ :
    ∃ c : Nat, ∀ n : Nat, c ≤ n →
      ∀ u : 𝒪[L]ˣ, u ∈ chosenNormalBasisPrincipalUnitSet K L n →
        ∀ v : 𝒪[L]ˣ, v ∈ chosenNormalBasisPrincipalUnitSet K L n →
          (((((u * v : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) -
              (((((u : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) +
                ((((v : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L))) ∈
            chosenBaseUniformizerPowSubmodule K L (n + 1)
              (chosenNormalBasisIntegerLattice K L)

theorem

chosenNormalBasisPrincipalUnitLatticeClass_mul_eq_add

L1938 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitLatticeClass_mul_eq_add

Documentation

The lattice class of a product of principal units is the sum of their lattice classes.

Source context 8 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [Valuation.HasExtension
  (ValuativeRel.valuation K) (ValuativeRel.valuation L)] in

Lean source · statement

theorem chosenNormalBasisPrincipalUnitLatticeClass_mul_eq_add {n : Nat}
    (hmul_error : ∀ u : 𝒪[L]ˣ, u ∈ chosenNormalBasisPrincipalUnitSet K L n →
      ∀ v : 𝒪[L]ˣ, v ∈ chosenNormalBasisPrincipalUnitSet K L n →
        (((((u * v : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) -
            (((((u : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) +
              ((((v : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L))) ∈
          chosenBaseUniformizerPowSubmodule K L (n + 1)
            (chosenNormalBasisIntegerLattice K L))
    (u v : 𝒪[L]ˣ)
    (hu : u ∈ chosenNormalBasisPrincipalUnitSet K L n)
    (hv : v ∈ chosenNormalBasisPrincipalUnitSet K L n)
    (huv : u * v ∈ chosenNormalBasisPrincipalUnitSet K L n) :
    chosenNormalBasisPrincipalUnitLatticeClass K L n (u * v) huv =
      chosenNormalBasisPrincipalUnitLatticeClass K L n u hu +
        chosenNormalBasisPrincipalUnitLatticeClass K L n v hv

theorem

exists_chosenNormalBasisPrincipalUnitSubgroupSuccPair

L1966 ↗

CyclicCohomology.exists_chosenNormalBasisPrincipalUnitSubgroupSuccPair

Documentation

There exists a nested pair of normal-basis principal-unit subgroups at successive levels.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

theorem exists_chosenNormalBasisPrincipalUnitSubgroupSuccPair
    [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Module.Finite 𝒪[K] 𝒪[L]] :
    ∃ c : Nat, ∀ n : Nat, c ≤ n →
      ∃ Vn Vsucc : Subgroup 𝒪[L]ˣ,
        (Vn : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L n ∧
        (Vsucc : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L (n + 1) ∧
        Vsucc ≤ Vn ∧
        Vn ≤ principalUnits L 1

def

chosenNormalBasisPrincipalUnitSuccSubgroup

L1993 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSuccSubgroup

Documentation

The subgroup of Vn obtained from an included next-step subgroup Vsucc ≤ Vn. This is the denominator used for the multiplicative quotient V^n / V^(n+1).

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

def chosenNormalBasisPrincipalUnitSuccSubgroup {Vn Vsucc : Subgroup 𝒪[L]ˣ}
    (_hV : Vsucc ≤ Vn) : Subgroup Vn

theorem

mem_chosenNormalBasisPrincipalUnitSuccSubgroup_iff

L1998 ↗

CyclicCohomology.mem_chosenNormalBasisPrincipalUnitSuccSubgroup_iff

Documentation

Characterizes membership in the next normal-basis principal-unit subgroup.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

theorem mem_chosenNormalBasisPrincipalUnitSuccSubgroup_iff
    {Vn Vsucc : Subgroup 𝒪[L]ˣ} (hV : Vsucc ≤ Vn) (u : Vn) :
    u ∈ chosenNormalBasisPrincipalUnitSuccSubgroup (L := L) hV ↔
      (u : 𝒪[L]ˣ) ∈ Vsucc

def

chosenNormalBasisPrincipalUnitSuccQuot

L2007 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSuccQuot

Documentation

The multiplicative successive quotient Vn / Vsucc, for an actual inclusion Vsucc ≤ Vn.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

def chosenNormalBasisPrincipalUnitSuccQuot
    {Vn Vsucc : Subgroup 𝒪[L]ˣ} (hV : Vsucc ≤ Vn) : Type u

instance

chosenNormalBasisPrincipalUnitSuccQuotCommGroup

L2012 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSuccQuotCommGroup

Documentation

The quotient by the next normal-basis principal-unit subgroup is a commutative group.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

instance chosenNormalBasisPrincipalUnitSuccQuotCommGroup
    {Vn Vsucc : Subgroup 𝒪[L]ˣ} (hV : Vsucc ≤ Vn) :
    CommGroup (chosenNormalBasisPrincipalUnitSuccQuot (L := L) hV)

def

chosenNormalBasisPrincipalUnitSuccQuotConcreteEquiv

L2021 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSuccQuotConcreteEquiv

Documentation

Explicit access to the concrete group quotient implementing the chosen normal-basis principal-unit graded piece.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

def chosenNormalBasisPrincipalUnitSuccQuotConcreteEquiv
    {Vn Vsucc : Subgroup 𝒪[L]ˣ} (hV : Vsucc ≤ Vn) :
    chosenNormalBasisPrincipalUnitSuccQuot (L := L) hV ≃*
      (Vn ⧸ chosenNormalBasisPrincipalUnitSuccSubgroup (L := L) hV)

def

chosenNormalBasisPrincipalUnitSuccQuotMk

L2031 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSuccQuotMk

Documentation

The quotient map Vn -> Vn / Vsucc.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

def chosenNormalBasisPrincipalUnitSuccQuotMk
    {Vn Vsucc : Subgroup 𝒪[L]ˣ} (hV : Vsucc ≤ Vn) :
    Vn →* chosenNormalBasisPrincipalUnitSuccQuot (L := L) hV

theorem

chosenNormalBasisPrincipalUnitSuccQuotConcreteEquiv_mk

L2040 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSuccQuotConcreteEquiv_mk

Documentation

The concrete principal-unit quotient equivalence sends an element to its canonical class.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

theorem chosenNormalBasisPrincipalUnitSuccQuotConcreteEquiv_mk
    {Vn Vsucc : Subgroup 𝒪[L]ˣ} (hV : Vsucc ≤ Vn) (u : Vn) :
    chosenNormalBasisPrincipalUnitSuccQuotConcreteEquiv (L := L) hV
        (chosenNormalBasisPrincipalUnitSuccQuotMk (L := L) hV u) =
      QuotientGroup.mk u

theorem

chosenNormalBasisPrincipalUnitSuccQuotMk_surjective

L2048 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSuccQuotMk_surjective

Documentation

Every successive principal-unit quotient class has a representative.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

theorem chosenNormalBasisPrincipalUnitSuccQuotMk_surjective
    {Vn Vsucc : Subgroup 𝒪[L]ˣ} (hV : Vsucc ≤ Vn) :
    Function.Surjective
      (chosenNormalBasisPrincipalUnitSuccQuotMk (L := L) hV)

theorem

inductionOn

L2057 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSuccQuot.inductionOn

Documentation

Eliminate a chosen normal-basis principal-unit quotient through arbitrary representatives and its canonical class map.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

theorem chosenNormalBasisPrincipalUnitSuccQuot.inductionOn
    {Vn Vsucc : Subgroup 𝒪[L]ˣ} (hV : Vsucc ≤ Vn)
    {motive : chosenNormalBasisPrincipalUnitSuccQuot (L := L) hV → Prop}
    (q : chosenNormalBasisPrincipalUnitSuccQuot (L := L) hV)
    (h : ∀ u : Vn,
      motive (chosenNormalBasisPrincipalUnitSuccQuotMk (L := L) hV u)) :
    motive q

def

chosenNormalBasisPrincipalUnitSuccQuotLift

L2071 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSuccQuotLift

Documentation

Descend a homomorphism that kills the included next-step subgroup.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

def chosenNormalBasisPrincipalUnitSuccQuotLift
    {Vn Vsucc : Subgroup 𝒪[L]ˣ} {H : Type*} [Group H]
    (hV : Vsucc ≤ Vn) (f : Vn →* H)
    (h : chosenNormalBasisPrincipalUnitSuccSubgroup (L := L) hV ≤ f.ker) :
    chosenNormalBasisPrincipalUnitSuccQuot (L := L) hV →* H

theorem

chosenNormalBasisPrincipalUnitSuccQuotLift_mk

L2082 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSuccQuotLift_mk

Documentation

A map lifted from the successive principal-unit quotient agrees on representatives.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

theorem chosenNormalBasisPrincipalUnitSuccQuotLift_mk
    {Vn Vsucc : Subgroup 𝒪[L]ˣ} {H : Type*} [Group H]
    (hV : Vsucc ≤ Vn) (f : Vn →* H)
    (h : chosenNormalBasisPrincipalUnitSuccSubgroup (L := L) hV ≤ f.ker)
    (u : Vn) :
    chosenNormalBasisPrincipalUnitSuccQuotLift (L := L) hV f h
        (chosenNormalBasisPrincipalUnitSuccQuotMk (L := L) hV u) = f u

theorem

chosenNormalBasisPrincipalUnitSuccQuotMk_eq_one_iff

L2092 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSuccQuotMk_eq_one_iff

Documentation

A principal unit represents the identity exactly when it lies in the next subgroup.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

theorem chosenNormalBasisPrincipalUnitSuccQuotMk_eq_one_iff
    {Vn Vsucc : Subgroup 𝒪[L]ˣ} (hV : Vsucc ≤ Vn) (u : Vn) :
    chosenNormalBasisPrincipalUnitSuccQuotMk (L := L) hV u = 1 ↔
      (u : 𝒪[L]ˣ) ∈ Vsucc

theorem

chosenNormalBasisPrincipalUnitSuccQuotMk_eq_iff_div_mem

L2104 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSuccQuotMk_eq_iff_div_mem

Documentation

Two principal units represent the same class exactly when their quotient lies in the next subgroup.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

theorem chosenNormalBasisPrincipalUnitSuccQuotMk_eq_iff_div_mem
    {Vn Vsucc : Subgroup 𝒪[L]ˣ} (hV : Vsucc ≤ Vn) (u v : Vn) :
    chosenNormalBasisPrincipalUnitSuccQuotMk (L := L) hV u =
        chosenNormalBasisPrincipalUnitSuccQuotMk (L := L) hV v ↔
      u / v ∈ chosenNormalBasisPrincipalUnitSuccSubgroup (L := L) hV

def

chosenNormalBasisPrincipalUnitToLatticeSuccQuotHom

L2118 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitToLatticeSuccQuotHom

Documentation

The map u ↦ u - 1 from a subgroup Vn = V^n to the additive successive quotient, viewed multiplicatively on the target.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · full declaration

def chosenNormalBasisPrincipalUnitToLatticeSuccQuotHom (n : Nat)
    {Vn : Subgroup 𝒪[L]ˣ}
    (hVn : (Vn : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L n)
    (hmul_error : ∀ u : 𝒪[L]ˣ, u ∈ chosenNormalBasisPrincipalUnitSet K L n →
      ∀ v : 𝒪[L]ˣ, v ∈ chosenNormalBasisPrincipalUnitSet K L n →
        (((((u * v : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) -
            (((((u : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) +
              ((((v : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L))) ∈
          chosenBaseUniformizerPowSubmodule K L (n + 1)
            (chosenNormalBasisIntegerLattice K L)) :
    Vn →* Multiplicative (chosenNormalBasisLatticeSuccQuot K L n) where
  toFun u :=
    Multiplicative.ofAdd
      (chosenNormalBasisPrincipalUnitLatticeClass K L n (u : 𝒪[L]ˣ)
        (by
          exact hVn ▸ u.2))
  map_one' := by
    change chosenNormalBasisPrincipalUnitLatticeClass K L n
      (1 : 𝒪[L]ˣ) (by exact hVn ▸ (1 : Vn).2) = 0
    rw [chosenNormalBasisPrincipalUnitLatticeClass,
      chosenNormalBasisLatticeSuccQuotMk_eq_zero_iff]
    simp
  map_mul' := by
    intro u v
    have hu : (u : 𝒪[L]ˣ) ∈ chosenNormalBasisPrincipalUnitSet K L n := by
      exact hVn ▸ u.2
    have hv : (v : 𝒪[L]ˣ) ∈ chosenNormalBasisPrincipalUnitSet K L n := by
      exact hVn ▸ v.2
    have huv : ((u * v : Vn) : 𝒪[L]ˣ) ∈ chosenNormalBasisPrincipalUnitSet K L n := by
      exact hVn ▸ (u * v).2
    have hclass :=
      chosenNormalBasisPrincipalUnitLatticeClass_mul_eq_add
        (K := K) (L := L) hmul_error (u : 𝒪[L]ˣ) (v : 𝒪[L]ˣ) hu hv huv
    simpa using congrArg Multiplicative.ofAdd hclass

theorem

chosenNormalBasisPrincipalUnitToLatticeSuccQuotHom_mem_ker_of_mem_succ

L2156 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitToLatticeSuccQuotHom_mem_ker_of_mem_succ

Documentation

Principal units from the next level lie in the kernel of the lattice-class homomorphism.

Source context 8 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [Valuation.HasExtension
  (ValuativeRel.valuation K) (ValuativeRel.valuation L)] in

Lean source · statement

theorem chosenNormalBasisPrincipalUnitToLatticeSuccQuotHom_mem_ker_of_mem_succ
    {n : Nat} {Vn Vsucc : Subgroup 𝒪[L]ˣ}
    (hVn : (Vn : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L n)
    (hVsucc : (Vsucc : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L (n + 1))
    (hmul_error : ∀ u : 𝒪[L]ˣ, u ∈ chosenNormalBasisPrincipalUnitSet K L n →
      ∀ v : 𝒪[L]ˣ, v ∈ chosenNormalBasisPrincipalUnitSet K L n →
        (((((u * v : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) -
            (((((u : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) +
              ((((v : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L))) ∈
          chosenBaseUniformizerPowSubmodule K L (n + 1)
            (chosenNormalBasisIntegerLattice K L))
    (u : Vn) (hu : (u : 𝒪[L]ˣ) ∈ Vsucc) :
    u ∈ (chosenNormalBasisPrincipalUnitToLatticeSuccQuotHom
      K L n hVn hmul_error).ker

def

chosenNormalBasisPrincipalUnitSuccQuotToLatticeSuccQuotHom

L2186 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSuccQuotToLatticeSuccQuotHom

Documentation

The induced map Vn/Vsucc -> π_K^nM/π_K^(n+1)M, with the additive quotient target viewed as a multiplicative group.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

def chosenNormalBasisPrincipalUnitSuccQuotToLatticeSuccQuotHom (n : Nat)
    {Vn Vsucc : Subgroup 𝒪[L]ˣ}
    (hVn : (Vn : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L n)
    (hVsucc : (Vsucc : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L (n + 1))
    (hV : Vsucc ≤ Vn)
    (hmul_error : ∀ u : 𝒪[L]ˣ, u ∈ chosenNormalBasisPrincipalUnitSet K L n →
      ∀ v : 𝒪[L]ˣ, v ∈ chosenNormalBasisPrincipalUnitSet K L n →
        (((((u * v : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) -
            (((((u : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) +
              ((((v : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L))) ∈
          chosenBaseUniformizerPowSubmodule K L (n + 1)
            (chosenNormalBasisIntegerLattice K L)) :
    chosenNormalBasisPrincipalUnitSuccQuot (L := L) hV →*
      Multiplicative (chosenNormalBasisLatticeSuccQuot K L n)

theorem

chosenNormalBasisPrincipalUnitSuccQuotToLatticeSuccQuotHom_mk

L2212 ↗

CyclicCohomology.chosenNormalBasisPrincipalUnitSuccQuotToLatticeSuccQuotHom_mk

Documentation

The induced quotient homomorphism sends a principal-unit class to its lattice class.

Source context 8 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
omit [Valuation.HasExtension
  (ValuativeRel.valuation K) (ValuativeRel.valuation L)] in

Lean source · statement

theorem chosenNormalBasisPrincipalUnitSuccQuotToLatticeSuccQuotHom_mk
    {n : Nat} {Vn Vsucc : Subgroup 𝒪[L]ˣ}
    (hVn : (Vn : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L n)
    (hVsucc : (Vsucc : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L (n + 1))
    (hV : Vsucc ≤ Vn)
    (hmul_error : ∀ u : 𝒪[L]ˣ, u ∈ chosenNormalBasisPrincipalUnitSet K L n →
      ∀ v : 𝒪[L]ˣ, v ∈ chosenNormalBasisPrincipalUnitSet K L n →
        (((((u * v : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) -
            (((((u : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L) +
              ((((v : 𝒪[L]ˣ) : 𝒪[L]) - 1 : 𝒪[L]) : L))) ∈
          chosenBaseUniformizerPowSubmodule K L (n + 1)
            (chosenNormalBasisIntegerLattice K L))
    (u : Vn) :
    chosenNormalBasisPrincipalUnitSuccQuotToLatticeSuccQuotHom
        K L n hVn hVsucc hV hmul_error
        (chosenNormalBasisPrincipalUnitSuccQuotMk (L := L) hV u) =
      chosenNormalBasisPrincipalUnitToLatticeSuccQuotHom K L n hVn hmul_error u

theorem

exists_chosenNormalBasisPrincipalUnitSuccQuotBoundary

L2232 ↗

CyclicCohomology.exists_chosenNormalBasisPrincipalUnitSuccQuotBoundary

Documentation

There exists a boundary map for the successive normal-basis principal-unit quotient.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · statement

theorem exists_chosenNormalBasisPrincipalUnitSuccQuotBoundary
    [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Module.Finite 𝒪[K] 𝒪[L]] :
    ∃ c : Nat, ∀ n : Nat, c ≤ n →
      ∃ Vn Vsucc : Subgroup 𝒪[L]ˣ,
        ∃ hV : Vsucc ≤ Vn,
          (Vn : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L n ∧
          (Vsucc : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L (n + 1) ∧
          Vn ≤ principalUnits L 1 ∧
          ∀ u : Vn,
            chosenNormalBasisPrincipalUnitSuccQuotMk (L := L) hV u = 1 ↔
              (u : 𝒪[L]ˣ) ∈ Vsucc

theorem

exists_chosenNormalBasisPrincipalUnitSuccQuotToLatticeSuccQuotHom

L2254 ↗

CyclicCohomology.exists_chosenNormalBasisPrincipalUnitSuccQuotToLatticeSuccQuotHom

Documentation

There exists a homomorphism from the successive principal-unit quotient to the lattice quotient.

Source context 7 commands

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

universe u
namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
open scoped ValuativeRel
open Filter
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ValuativeRel L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]

Lean source · full declaration

theorem exists_chosenNormalBasisPrincipalUnitSuccQuotToLatticeSuccQuotHom
    [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Module.Finite 𝒪[K] 𝒪[L]] :
    ∃ c : Nat, ∀ n : Nat, c ≤ n →
      ∃ Vn Vsucc : Subgroup 𝒪[L]ˣ,
        ∃ hV : Vsucc ≤ Vn,
          ∃ hVn : (Vn : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L n,
            ∃ _hVsucc :
              (Vsucc : Set 𝒪[L]ˣ) = chosenNormalBasisPrincipalUnitSet K L (n + 1),
              ∃ Φ : chosenNormalBasisPrincipalUnitSuccQuot (L := L) hV →*
                  Multiplicative (chosenNormalBasisLatticeSuccQuot K L n),
                ∀ u : Vn,
                  Φ (chosenNormalBasisPrincipalUnitSuccQuotMk (L := L) hV u) =
                    Multiplicative.ofAdd
                      (chosenNormalBasisPrincipalUnitLatticeClass K L n
                        (u : 𝒪[L]ˣ) (by
                          exact hVn ▸ u.2)) := by
  rcases exists_chosenNormalBasisPrincipalUnitSubgroupSuccPair (K := K) (L := L) with
    ⟨c₁, hc₁⟩
  rcases exists_chosenNormalBasisPrincipalUnitSet_mul_error_mem_succ (K := K) (L := L) with
    ⟨c₂, hc₂⟩
  refine ⟨max c₁ c₂, ?_⟩
  intro n hmaxn
  have hc₁n : c₁ ≤ n := le_trans (le_max_left c₁ c₂) hmaxn
  have hc₂n : c₂ ≤ n := le_trans (le_max_right c₁ c₂) hmaxn
  rcases hc₁ n hc₁n with ⟨Vn, Vsucc, hVn, hVsucc, hV, _hVnle⟩
  let hmul_error := hc₂ n hc₂n
  let Φ : chosenNormalBasisPrincipalUnitSuccQuot (L := L) hV →*
      Multiplicative (chosenNormalBasisLatticeSuccQuot K L n) :=
    chosenNormalBasisPrincipalUnitSuccQuotToLatticeSuccQuotHom
      K L n hVn hVsucc hV hmul_error
  refine ⟨Vn, Vsucc, hV, hVn, hVsucc, Φ, ?_⟩
  intro u
  dsimp [Φ]
  rw [chosenNormalBasisPrincipalUnitSuccQuotToLatticeSuccQuotHom_mk]
  rfl

Module documentation

Additive quotient boundary

Declarations