Module

QuotientTower.lean

Nyll.GaloisCohomology.Cyclic.Herbrand.PrincipalUnits.QuotientTower

31 declarations indexed from sourceView source ↗

Module documentation

Provides the public declarations in the CyclicCohomology.Herbrand.PrincipalUnits.QuotientTower Lean module.

Imports4

Imported by3

def

integerUnitsModPrincipalUnitsMapOfLe

L27 ↗

CyclicCohomology.integerUnitsModPrincipalUnitsMapOfLe

Documentation

The natural projection 𝒪_Kˣ/U_K^m → 𝒪_Kˣ/U_K^n for n ≤ m.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def integerUnitsModPrincipalUnitsMapOfLe
    (K : Type u) [Field K] [ValuativeRel K] {n m : Nat} (hnm : n ≤ m) :
    IntegerUnitsModPrincipalUnitsAtLevel K m →*
      IntegerUnitsModPrincipalUnitsAtLevel K n

theorem

integerUnitsModPrincipalUnitsMapOfLe_mk

L41 ↗

CyclicCohomology.integerUnitsModPrincipalUnitsMapOfLe_mk

Documentation

The level-change map sends a unit class to the class of the same unit.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerUnitsModPrincipalUnitsMapOfLe_mk
    (K : Type u) [Field K] [ValuativeRel K] {n m : Nat} (hnm : n ≤ m)
    (x : 𝒪[K]ˣ) :
    integerUnitsModPrincipalUnitsMapOfLe K hnm
        (integerUnitsModPrincipalUnitsAtLevelMk K m x) =
      integerUnitsModPrincipalUnitsAtLevelMk K n x

def

integerUnitsModPrincipalUnitsSuccMap

L51 ↗

CyclicCohomology.integerUnitsModPrincipalUnitsSuccMap

Documentation

The successive projection 𝒪_Kˣ/U_K^(n+1) → 𝒪_Kˣ/U_K^n.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def integerUnitsModPrincipalUnitsSuccMap
    (K : Type u) [Field K] [ValuativeRel K] (n : Nat) :
    IntegerUnitsModPrincipalUnitsAtLevel K (n + 1) →*
      IntegerUnitsModPrincipalUnitsAtLevel K n

theorem

integerUnitsModPrincipalUnitsSuccMap_mk

L59 ↗

CyclicCohomology.integerUnitsModPrincipalUnitsSuccMap_mk

Documentation

The successor-level map sends a unit representative to its successor quotient class.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerUnitsModPrincipalUnitsSuccMap_mk
    (K : Type u) [Field K] [ValuativeRel K] (n : Nat)
    (x : 𝒪[K]ˣ) :
    integerUnitsModPrincipalUnitsSuccMap K n
        (integerUnitsModPrincipalUnitsAtLevelMk K (n + 1) x) =
      integerUnitsModPrincipalUnitsAtLevelMk K n x

theorem

integerUnitsModPrincipalUnitsSuccMap_surjective

L68 ↗

CyclicCohomology.integerUnitsModPrincipalUnitsSuccMap_surjective

Documentation

The map to the successor principal-unit quotient is surjective.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerUnitsModPrincipalUnitsSuccMap_surjective
    (K : Type u) [Field K] [ValuativeRel K] (n : Nat) :
    Function.Surjective (integerUnitsModPrincipalUnitsSuccMap K n)

def

integerUnitsModPrincipalUnitsMapOfIntegerRingEquiv

L79 ↗

CyclicCohomology.integerUnitsModPrincipalUnitsMapOfIntegerRingEquiv

Documentation

The induced homomorphism on the finite quotient 𝒪_Kˣ/U_K^n.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def integerUnitsModPrincipalUnitsMapOfIntegerRingEquiv
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (e : 𝒪[K] ≃+* 𝒪[K]) :
    IntegerUnitsModPrincipalUnitsAtLevel K n →*
      IntegerUnitsModPrincipalUnitsAtLevel K n

theorem

integerUnitsModPrincipalUnitsMapOfIntegerRingEquiv_mk

L95 ↗

CyclicCohomology.integerUnitsModPrincipalUnitsMapOfIntegerRingEquiv_mk

Documentation

An integer-ring equivalence maps a unit quotient class via its representative.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerUnitsModPrincipalUnitsMapOfIntegerRingEquiv_mk
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (e : 𝒪[K] ≃+* 𝒪[K]) (u : 𝒪[K]ˣ) :
    integerUnitsModPrincipalUnitsMapOfIntegerRingEquiv K n e
        (integerUnitsModPrincipalUnitsAtLevelMk K n u) =
      integerUnitsModPrincipalUnitsAtLevelMk K n
        (Units.mapEquiv e.toMulEquiv u)

def

integerUnitsModPrincipalUnitsMapEquivOfIntegerRingEquiv

L108 ↗

CyclicCohomology.integerUnitsModPrincipalUnitsMapEquivOfIntegerRingEquiv

Documentation

A valuation-integer-ring equivalence descends to the finite quotient 𝒪_Kˣ/U_K^n.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

def integerUnitsModPrincipalUnitsMapEquivOfIntegerRingEquiv
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (e : 𝒪[K] ≃+* 𝒪[K]) :
    IntegerUnitsModPrincipalUnitsAtLevel K n ≃*
      IntegerUnitsModPrincipalUnitsAtLevel K n where
  toFun := integerUnitsModPrincipalUnitsMapOfIntegerRingEquiv K n e
  invFun := integerUnitsModPrincipalUnitsMapOfIntegerRingEquiv K n e.symm
  left_inv := by
    intro x
    refine IntegerUnitsModPrincipalUnitsAtLevel.inductionOn n
      (motive := fun x =>
        integerUnitsModPrincipalUnitsMapOfIntegerRingEquiv K n e.symm
            (integerUnitsModPrincipalUnitsMapOfIntegerRingEquiv K n e x) = x)
      x ?_
    intro u
    rw [integerUnitsModPrincipalUnitsMapOfIntegerRingEquiv_mk,
      integerUnitsModPrincipalUnitsMapOfIntegerRingEquiv_mk]
    have h :
        Units.mapEquiv e.symm.toMulEquiv (Units.mapEquiv e.toMulEquiv u) = u := by
      ext
      simp
    exact congrArg
      (integerUnitsModPrincipalUnitsAtLevelMk K n) h
  right_inv := by
    intro x
    refine IntegerUnitsModPrincipalUnitsAtLevel.inductionOn n
      (motive := fun x =>
        integerUnitsModPrincipalUnitsMapOfIntegerRingEquiv K n e
            (integerUnitsModPrincipalUnitsMapOfIntegerRingEquiv K n e.symm x) = x)
      x ?_
    intro u
    rw [integerUnitsModPrincipalUnitsMapOfIntegerRingEquiv_mk,
      integerUnitsModPrincipalUnitsMapOfIntegerRingEquiv_mk]
    have h :
        Units.mapEquiv e.toMulEquiv (Units.mapEquiv e.symm.toMulEquiv u) = u := by
      ext
      simp
    exact congrArg
      (integerUnitsModPrincipalUnitsAtLevelMk K n) h
  map_mul' := by
    intro x y
    exact map_mul (integerUnitsModPrincipalUnitsMapOfIntegerRingEquiv K n e) x y

theorem

integerUnitsModPrincipalUnitsMapEquivOfIntegerRingEquiv_mk

L153 ↗

CyclicCohomology.integerUnitsModPrincipalUnitsMapEquivOfIntegerRingEquiv_mk

Documentation

The induced quotient equivalence acts on a class through its unit representative.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerUnitsModPrincipalUnitsMapEquivOfIntegerRingEquiv_mk
    (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (e : 𝒪[K] ≃+* 𝒪[K]) (u : 𝒪[K]ˣ) :
    integerUnitsModPrincipalUnitsMapEquivOfIntegerRingEquiv K n e
        (integerUnitsModPrincipalUnitsAtLevelMk K n u) =
      integerUnitsModPrincipalUnitsAtLevelMk K n
        (Units.mapEquiv e.toMulEquiv u)

def

principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc

L164 ↗

CyclicCohomology.principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc

Documentation

The graded quotient U_K^n/U_K^(n+1) as the kernel source inside 𝒪_Kˣ/U_K^(n+1).

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc
    (K : Type u) [Field K] [ValuativeRel K] (n : Nat) :
    PrincipalUnitsSuccQuot K n →*
      IntegerUnitsModPrincipalUnitsAtLevel K (n + 1)

theorem

principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc_mk

L179 ↗

CyclicCohomology.principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc_mk

Documentation

The principal-unit quotient map sends a representative to its integer-unit class.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc_mk
    (K : Type u) [Field K] [ValuativeRel K] (n : Nat)
    (u : principalUnits K n) :
    principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc K n
        (principalUnitsSuccQuotMk K n u) =
      integerUnitsModPrincipalUnitsAtLevelMk K (n + 1) (u : 𝒪[K]ˣ)

theorem

integerUnitsSuccMap_comp_principalUnitsSuccQuot

L190 ↗

CyclicCohomology.integerUnitsSuccMap_comp_principalUnitsSuccQuot

Documentation

The principal-unit inclusion followed by the successor map is the canonical quotient map.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerUnitsSuccMap_comp_principalUnitsSuccQuot
    (K : Type u) [Field K] [ValuativeRel K] (n : Nat) :
    (integerUnitsModPrincipalUnitsSuccMap K n).comp
        (principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc K n) = 1

theorem

principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc_range_eq_ker

L212 ↗

CyclicCohomology.principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc_range_eq_ker

Documentation

Exactness of U_K^n/U_K^(n+1) → 𝒪_Kˣ/U_K^(n+1) → 𝒪_Kˣ/U_K^n at the middle finite-filtration quotient.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc_range_eq_ker
    (K : Type u) [Field K] [ValuativeRel K] (n : Nat) :
    MonoidHom.range (principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc K n) =
      MonoidHom.ker (integerUnitsModPrincipalUnitsSuccMap K n)

theorem

principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc_injective

L240 ↗

CyclicCohomology.principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc_injective

Documentation

The induced map from the successive principal-unit quotient is injective.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc_injective
    (K : Type u) [Field K] [ValuativeRel K] (n : Nat) :
    Function.Injective (principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc K n)

theorem

integerUnitsModPrincipalUnitsSuccMap_eq_one_iff_exists

L259 ↗

CyclicCohomology.integerUnitsModPrincipalUnitsSuccMap_eq_one_iff_exists

Documentation

A unit maps to the identity at the successor level exactly when it has a principal-unit lift.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerUnitsModPrincipalUnitsSuccMap_eq_one_iff_exists
    (K : Type u) [Field K] [ValuativeRel K] (n : Nat)
    (x : IntegerUnitsModPrincipalUnitsAtLevel K (n + 1)) :
    integerUnitsModPrincipalUnitsSuccMap K n x = 1 ↔
      ∃ y : PrincipalUnitsSuccQuot K n,
        principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc K n y = x

def

galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure

L271 ↗

CyclicCohomology.galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure

Documentation

Integral-closure Galois action on the finite quotient 𝒪_Lˣ/U_L^n.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) (σ : Gal(L/K)) :
    IntegerUnitsModPrincipalUnitsAtLevel L n ≃*
      IntegerUnitsModPrincipalUnitsAtLevel L n

theorem

galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure_mk

L284 ↗

CyclicCohomology.galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure_mk

Documentation

The Galois-induced quotient equivalence acts on a class through its representative.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure_mk
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) (σ : Gal(L/K)) (u : 𝒪[L]ˣ) :
    galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure K L n σ
        (integerUnitsModPrincipalUnitsAtLevelMk L n u) =
      integerUnitsModPrincipalUnitsAtLevelMk L n
        (Units.mapEquiv
          (galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ).toMulEquiv u)

def

galoisGroupIntegerUnitsModPrincipalUnitsMapEquivHomOfIsIntegralClosure

L300 ↗

CyclicCohomology.galoisGroupIntegerUnitsModPrincipalUnitsMapEquivHomOfIsIntegralClosure

Documentation

Integral-closure Galois action on finite principal-unit quotients as a group homomorphism.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

def galoisGroupIntegerUnitsModPrincipalUnitsMapEquivHomOfIsIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) :
    Gal(L / K) →*
      (IntegerUnitsModPrincipalUnitsAtLevel L n ≃*
        IntegerUnitsModPrincipalUnitsAtLevel L n) where
  toFun := galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure K L n
  map_one' := by
    ext x
    refine IntegerUnitsModPrincipalUnitsAtLevel.inductionOn n
      (motive := fun x =>
        galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure
            K L n 1 x = x)
      x ?_
    intro u
    rw [galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure_mk]
    congr 1
  map_mul' := by
    intro σ τ
    ext x
    refine IntegerUnitsModPrincipalUnitsAtLevel.inductionOn n
      (motive := fun x =>
        galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure
            K L n (σ * τ) x =
          (galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure
              K L n σ *
            galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure
              K L n τ) x)
      x ?_
    intro u
    rw [galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure_mk]
    change
      integerUnitsModPrincipalUnitsAtLevelMk L n
          (Units.mapEquiv
            (galoisGroupIntegerRingEquivOfIsIntegralClosure K L (σ * τ)).toMulEquiv u) =
        galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure K L n σ
          (galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure K L n τ
            (integerUnitsModPrincipalUnitsAtLevelMk L n u))
    rw [
      galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure_mk,
      galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure_mk]
    congr 1

def

galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure

L349 ↗

CyclicCohomology.galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure

Documentation

Integral-closure Galois action on finite principal-unit quotients, packaged for low-degree Herbrand quotients.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

def galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) :
    MulDistribMulAction (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L n) where
  smul σ x := galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure K L n σ x
  one_smul := by
    intro x
    change galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure K L n 1 x = x
    have h := congrArg (fun e : IntegerUnitsModPrincipalUnitsAtLevel L n ≃*
        IntegerUnitsModPrincipalUnitsAtLevel L n => e x)
      (map_one (galoisGroupIntegerUnitsModPrincipalUnitsMapEquivHomOfIsIntegralClosure K L n))
    exact h
  mul_smul := by
    intro σ τ x
    change galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure K L n
        (σ * τ) x =
      galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure K L n σ
        (galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure K L n τ x)
    have h := congrArg (fun e : IntegerUnitsModPrincipalUnitsAtLevel L n ≃*
        IntegerUnitsModPrincipalUnitsAtLevel L n => e x)
      (map_mul (galoisGroupIntegerUnitsModPrincipalUnitsMapEquivHomOfIsIntegralClosure K L n)
        σ τ)
    exact h
  smul_mul := by
    intro σ x y
    exact map_mul (galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure
      K L n σ) x y
  smul_one := by
    intro σ
    exact map_one (galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure K L n σ)

theorem

galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure_smul

L384 ↗

CyclicCohomology.galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure_smul

Documentation

The Galois action on integer units modulo principal units is induced on representatives.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

theorem galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure_smul
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) (σ : Gal(L/K)) (x : IntegerUnitsModPrincipalUnitsAtLevel L n) :
    letI := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure
      K L n
    σ • x = galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure K L n σ x :=
  rfl

theorem

integerUnitsModPrincipalUnitsSuccMap_galoisGroup_of_isIntegralClosure

L397 ↗

CyclicCohomology.integerUnitsModPrincipalUnitsSuccMap_galoisGroup_of_isIntegralClosure

Documentation

The successive finite-principal-unit quotient map is equivariant for the integral-closure Galois actions.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

theorem integerUnitsModPrincipalUnitsSuccMap_galoisGroup_of_isIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) (σ : Gal(L/K))
    (x : IntegerUnitsModPrincipalUnitsAtLevel L (n + 1)) :
    letI := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure
      K L (n + 1)
    letI := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure
      K L n
    integerUnitsModPrincipalUnitsSuccMap L n (σ • x) =
      σ • integerUnitsModPrincipalUnitsSuccMap L n x := by
  let := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure
    K L (n + 1)
  let := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure K L n
  refine IntegerUnitsModPrincipalUnitsAtLevel.inductionOn (n + 1)
    (motive := fun x =>
      integerUnitsModPrincipalUnitsSuccMap L n (σ • x) =
        σ • integerUnitsModPrincipalUnitsSuccMap L n x)
    x ?_
  intro u
  rw [galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure_smul,
    galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure_mk,
    integerUnitsModPrincipalUnitsSuccMap_mk,
    integerUnitsModPrincipalUnitsSuccMap_mk,
    galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure_smul,
    galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure_mk]

theorem

principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc_galoisGroup_of_isIntegralClosure

L428 ↗

CyclicCohomology.principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc_galoisGroup_of_isIntegralClosure

Documentation

The kernel-source map U_L^n/U_L^(n+1) → 𝒪_Lˣ/U_L^(n+1) is equivariant for the integral-closure Galois actions.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

theorem principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc_galoisGroup_of_isIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (n : Nat) (σ : Gal(L/K)) (x : PrincipalUnitsSuccQuot L n) :
    letI := galoisGroupPrincipalUnitsSuccQuotMulDistribMulActionOfIsIntegralClosure K L n
    letI := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure
      K L (n + 1)
    principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc L n (σ • x) =
      σ • principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc L n x := by
  let := galoisGroupPrincipalUnitsSuccQuotMulDistribMulActionOfIsIntegralClosure K L n
  let := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure
    K L (n + 1)
  refine PrincipalUnitsSuccQuot.inductionOn n
    (motive := fun x =>
      principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc L n (σ • x) =
        σ • principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc L n x)
    x ?_
  intro u
  rw [galoisGroupPrincipalUnitsSuccQuotMulDistribMulActionOfIsIntegralClosure_smul,
    galoisGroupPrincipalUnitsSuccQuotMapEquivOfIsIntegralClosure,
    principalUnitsSuccQuotMapEquivOfIntegerRingEquiv_apply,
    principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc_mk,
    principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc_mk,
    galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure_smul,
    galoisGroupIntegerUnitsModPrincipalUnitsMapEquivOfIsIntegralClosure_mk]
  rfl

theorem

integerUnitsModPrincipalUnitsAtLevel_finite_zero

L458 ↗

CyclicCohomology.integerUnitsModPrincipalUnitsAtLevel_finite_zero

Documentation

The quotient 𝒪_Kˣ/U_K^0 is finite because U_K^0 = 𝒪_Kˣ.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerUnitsModPrincipalUnitsAtLevel_finite_zero
    (K : Type u) [Field K] [ValuativeRel K] :
    Finite (IntegerUnitsModPrincipalUnitsAtLevel K 0)

theorem

integerUnitsModPrincipalUnitsAtLevel_finite_one_of_isNonarchimedeanLocalField

L469 ↗

CyclicCohomology.integerUnitsModPrincipalUnitsAtLevel_finite_one_of_isNonarchimedeanLocalField

Documentation

The initial nontrivial quotient 𝒪_Kˣ/U_K^1 is finite via 𝒪_Kˣ/U_K^1 ≃ 𝓀_Kˣ.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerUnitsModPrincipalUnitsAtLevel_finite_one_of_isNonarchimedeanLocalField
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    Finite (IntegerUnitsModPrincipalUnitsAtLevel K 1)

theorem

integerUnitsModPrincipalUnitsAtLevel_finite_succ_of_finite

L481 ↗

CyclicCohomology.integerUnitsModPrincipalUnitsAtLevel_finite_succ_of_finite

Documentation

If the previous finite quotient and the graded quotient are finite, then the next finite quotient is finite.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerUnitsModPrincipalUnitsAtLevel_finite_succ_of_finite
    (K : Type u) [Field K] [ValuativeRel K] (n : Nat)
    [Finite (PrincipalUnitsSuccQuot K n)]
    [Finite (IntegerUnitsModPrincipalUnitsAtLevel K n)] :
    Finite (IntegerUnitsModPrincipalUnitsAtLevel K (n + 1))

theorem

integerUnitsModPrincipalUnitsAtLevel_finite_of_isNonarchimedeanLocalField

L503 ↗

CyclicCohomology.integerUnitsModPrincipalUnitsAtLevel_finite_of_isNonarchimedeanLocalField

Documentation

Every finite principal-unit quotient 𝒪_Kˣ/U_K^n is finite over a nonarchimedean local field.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerUnitsModPrincipalUnitsAtLevel_finite_of_isNonarchimedeanLocalField
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (n : Nat) :
    Finite (IntegerUnitsModPrincipalUnitsAtLevel K n)

theorem

integerUnitsModPrincipalUnitsAtLevel_herbrandH0_finite_of_isNonarchimedeanLocalField

L520 ↗

CyclicCohomology.integerUnitsModPrincipalUnitsAtLevel_herbrandH0_finite_of_isNonarchimedeanLocalField

Documentation

Actual H⁰ finiteness for the finite quotient 𝒪_Lˣ/U_L^n.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

theorem integerUnitsModPrincipalUnitsAtLevel_herbrandH0_finite_of_isNonarchimedeanLocalField
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Fintype (Gal(L/K))] (n : Nat) :
    letI := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure K L n
    Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandH0
      (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L n)) := by
  let := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure K L n
  let : Finite (IntegerUnitsModPrincipalUnitsAtLevel L n) :=
    integerUnitsModPrincipalUnitsAtLevel_finite_of_isNonarchimedeanLocalField L n
  infer_instance

theorem

integerUnitsModPrincipalUnitsAtLevel_herbrandHMinusOne_finite_of_isNonarchimedeanLocalField

L535 ↗

CyclicCohomology.integerUnitsModPrincipalUnitsAtLevel_herbrandHMinusOne_finite_of_isNonarchimedeanLocalField

Documentation

Actual H^{-1} finiteness for the finite quotient 𝒪_Lˣ/U_L^n.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

theorem integerUnitsModPrincipalUnitsAtLevel_herbrandHMinusOne_finite_of_isNonarchimedeanLocalField
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Fintype (Gal(L/K))] (n : Nat) (σ : Gal(L/K)) :
    letI := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure K L n
    Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandHMinusOne
      (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L n) σ) := by
  let := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure K L n
  let : Finite (IntegerUnitsModPrincipalUnitsAtLevel L n) :=
    integerUnitsModPrincipalUnitsAtLevel_finite_of_isNonarchimedeanLocalField L n
  infer_instance

theorem

integerUnitsModPrincipalUnitsAtLevel_herbrandQuotient_eq_one_of_isNonarchimedeanLocalField

L551 ↗

CyclicCohomology.integerUnitsModPrincipalUnitsAtLevel_herbrandQuotient_eq_one_of_isNonarchimedeanLocalField

Documentation

Actual finite-cyclic-module endpoint for the finite quotient 𝒪_Lˣ/U_L^n.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

theorem integerUnitsModPrincipalUnitsAtLevel_herbrandQuotient_eq_one_of_isNonarchimedeanLocalField
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Fintype (Gal(L/K))] (n : Nat) (σ : Gal(L/K))
    (hgen : ∀ g : Gal(L / K), g ∈ Subgroup.zpowers σ) :
    letI := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure K L n
    letI : Finite (IntegerUnitsModPrincipalUnitsAtLevel L n) :=
      integerUnitsModPrincipalUnitsAtLevel_finite_of_isNonarchimedeanLocalField L n
    CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandQuotient
      (G := Gal(L / K)) (A := IntegerUnitsModPrincipalUnitsAtLevel L n) σ = 1 := by
  let := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure K L n
  let : Finite (IntegerUnitsModPrincipalUnitsAtLevel L n) :=
    integerUnitsModPrincipalUnitsAtLevel_finite_of_isNonarchimedeanLocalField L n
  exact CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandQuotient_finite_module_eq_one
    (G := Gal(L / K)) (A := IntegerUnitsModPrincipalUnitsAtLevel L n) σ hgen

theorem

integerUnitsModPrincipalUnitsSucc_herbrandQuotient_exact_multiplicative_of_isIntegralClosure

L572 ↗

CyclicCohomology.integerUnitsModPrincipalUnitsSucc_herbrandQuotient_exact_multiplicative_of_isIntegralClosure

Documentation

GC Herbrand multiplicativity specialized to the actual finite principal-unit quotient tower U_L^n/U_L^(n+1) → 𝒪_Lˣ/U_L^(n+1) → 𝒪_Lˣ/U_L^n.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

theorem integerUnitsModPrincipalUnitsSucc_herbrandQuotient_exact_multiplicative_of_isIntegralClosure
    (K L : Type) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Fintype (Gal(L/K))] (n : Nat) (σ : Gal(L/K))
    (hgen : ∀ g : Gal(L / K), g ∈ Subgroup.zpowers σ)
    (hA0 :
      letI := galoisGroupPrincipalUnitsSuccQuotMulDistribMulActionOfIsIntegralClosure K L n
      Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandH0
        (Gal(L / K)) (PrincipalUnitsSuccQuot L n)))
    (hAm :
      letI := galoisGroupPrincipalUnitsSuccQuotMulDistribMulActionOfIsIntegralClosure K L n
      Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandHMinusOne
        (Gal(L / K)) (PrincipalUnitsSuccQuot L n) σ))
    (hB0 :
      letI := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure
        K L (n + 1)
      Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandH0
        (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L (n + 1))))
    (hBm :
      letI := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure
        K L (n + 1)
      Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandHMinusOne
        (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L (n + 1)) σ))
    (hC0 :
      letI := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure
        K L n
      Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandH0
        (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L n)))
    (hCm :
      letI := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure
        K L n
      Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandHMinusOne
        (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L n) σ)) :
    letI := galoisGroupPrincipalUnitsSuccQuotMulDistribMulActionOfIsIntegralClosure K L n
    letI := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure
      K L (n + 1)
    letI := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure K L n
    letI : Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandH0
        (Gal(L / K)) (PrincipalUnitsSuccQuot L n)) := hA0
    letI : Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandHMinusOne
        (Gal(L / K)) (PrincipalUnitsSuccQuot L n) σ) := hAm
    letI : Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandH0
        (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L (n + 1))) := hB0
    letI : Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandHMinusOne
        (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L (n + 1)) σ) := hBm
    letI : Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandH0
        (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L n)) := hC0
    letI : Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandHMinusOne
        (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L n) σ) := hCm
    CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandQuotient
        (G := Gal(L / K)) (A := IntegerUnitsModPrincipalUnitsAtLevel L (n + 1)) σ =
      CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandQuotient
          (G := Gal(L / K)) (A := PrincipalUnitsSuccQuot L n) σ *
        CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandQuotient
          (G := Gal(L / K)) (A := IntegerUnitsModPrincipalUnitsAtLevel L n) σ := by
  let := galoisGroupPrincipalUnitsSuccQuotMulDistribMulActionOfIsIntegralClosure K L n
  let := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure
    K L (n + 1)
  let := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure K L n
  let : Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandH0
      (Gal(L / K)) (PrincipalUnitsSuccQuot L n)) := hA0
  let : Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandHMinusOne
      (Gal(L / K)) (PrincipalUnitsSuccQuot L n) σ) := hAm
  let : Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandH0
      (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L (n + 1))) := hB0
  let : Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandHMinusOne
      (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L (n + 1)) σ) := hBm
  let : Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandH0
      (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L n)) := hC0
  let : Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandHMinusOne
      (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L n) σ) := hCm
  exact CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandQuotient_exact_multiplicative
    (G := Gal(L / K))
    (A := PrincipalUnitsSuccQuot L n)
    (B := IntegerUnitsModPrincipalUnitsAtLevel L (n + 1))
    (C := IntegerUnitsModPrincipalUnitsAtLevel L n)
    (principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc L n)
    (integerUnitsModPrincipalUnitsSuccMap L n)
    (by
      intro g x
      exact
        principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc_galoisGroup_of_isIntegralClosure
          K L n g x)
    (by
      intro g x
      exact integerUnitsModPrincipalUnitsSuccMap_galoisGroup_of_isIntegralClosure K L n g x)
    (integerUnitsModPrincipalUnitsSuccMap_eq_one_iff_exists L n)
    (principalUnitsSuccQuotToIntegerUnitsModPrincipalUnitsSucc_injective L n)
    (by
      intro x
      exact integerUnitsModPrincipalUnitsSuccMap_surjective L n x)
    σ hgen

theorem

integerUnitsModPrincipalUnitsSucc_herbrandQuotient_eq_one_of_isIntegralClosure

L669 ↗

CyclicCohomology.integerUnitsModPrincipalUnitsSucc_herbrandQuotient_eq_one_of_isIntegralClosure

Documentation

If the graded quotient and the previous finite quotient both have Herbrand quotient 1, the next finite quotient has Herbrand quotient 1.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

theorem integerUnitsModPrincipalUnitsSucc_herbrandQuotient_eq_one_of_isIntegralClosure
    (K L : Type) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Fintype (Gal(L/K))] (n : Nat) (σ : Gal(L/K))
    (hgen : ∀ g : Gal(L / K), g ∈ Subgroup.zpowers σ)
    (hA0 :
      letI := galoisGroupPrincipalUnitsSuccQuotMulDistribMulActionOfIsIntegralClosure K L n
      Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandH0
        (Gal(L / K)) (PrincipalUnitsSuccQuot L n)))
    (hAm :
      letI := galoisGroupPrincipalUnitsSuccQuotMulDistribMulActionOfIsIntegralClosure K L n
      Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandHMinusOne
        (Gal(L / K)) (PrincipalUnitsSuccQuot L n) σ))
    (hB0 :
      letI := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure
        K L (n + 1)
      Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandH0
        (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L (n + 1))))
    (hBm :
      letI := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure
        K L (n + 1)
      Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandHMinusOne
        (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L (n + 1)) σ))
    (hC0 :
      letI := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure
        K L n
      Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandH0
        (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L n)))
    (hCm :
      letI := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure
        K L n
      Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandHMinusOne
        (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L n) σ))
    (hA :
      letI := galoisGroupPrincipalUnitsSuccQuotMulDistribMulActionOfIsIntegralClosure K L n
      letI : Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandH0
          (Gal(L / K)) (PrincipalUnitsSuccQuot L n)) := hA0
      letI : Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandHMinusOne
          (Gal(L / K)) (PrincipalUnitsSuccQuot L n) σ) := hAm
      CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandQuotient
        (G := Gal(L / K)) (A := PrincipalUnitsSuccQuot L n) σ = 1)
    (hC :
      letI := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure K L n
      letI : Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandH0
          (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L n)) := hC0
      letI : Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandHMinusOne
          (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L n) σ) := hCm
      CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandQuotient
        (G := Gal(L / K)) (A := IntegerUnitsModPrincipalUnitsAtLevel L n) σ = 1) :
    letI := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure
      K L (n + 1)
    letI : Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandH0
        (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L (n + 1))) := hB0
    letI : Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandHMinusOne
        (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L (n + 1)) σ) := hBm
    CyclicCohomology.ProfiniteCohomology.Herbrand.herbrandQuotient
      (G := Gal(L / K)) (A := IntegerUnitsModPrincipalUnitsAtLevel L (n + 1)) σ = 1 := by
  let := galoisGroupPrincipalUnitsSuccQuotMulDistribMulActionOfIsIntegralClosure K L n
  let := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure
    K L (n + 1)
  let := galoisGroupIntegerUnitsModPrincipalUnitsMulDistribMulActionOfIsIntegralClosure K L n
  let : Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandH0
      (Gal(L / K)) (PrincipalUnitsSuccQuot L n)) := hA0
  let : Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandHMinusOne
      (Gal(L / K)) (PrincipalUnitsSuccQuot L n) σ) := hAm
  let : Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandH0
      (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L (n + 1))) := hB0
  let : Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandHMinusOne
      (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L (n + 1)) σ) := hBm
  let : Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandH0
      (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L n)) := hC0
  let : Finite (CyclicCohomology.ProfiniteCohomology.Herbrand.HerbrandHMinusOne
      (Gal(L / K)) (IntegerUnitsModPrincipalUnitsAtLevel L n) σ) := hCm
  rw [integerUnitsModPrincipalUnitsSucc_herbrandQuotient_exact_multiplicative_of_isIntegralClosure
    K L n σ hgen hA0 hAm hB0 hBm hC0 hCm, hA, hC, one_mul]

Module documentation

Declarations