Module

Instances.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.ClassFormation.LocalBlocks.Family.Instances

6 declarations indexed from sourceView source ↗

Module documentation

Finite families of local idele blocks

This file combines the local induced-module calculation over a finite family of places. It is the finite-support part of the localized class formation.

Imports2

Imported by4

structure

LocalPlaceDatum

L36 ↗

LocalClassFieldTheory.LocalPlaceDatum

Documentation

A chosen extension w of a nontrivial base absolute value. These are exactly the concrete inputs needed to form one local block.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u v w
variable (K : Type u) (L : Type v)
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · full declaration

structure LocalPlaceDatum where
  /-- The base absolute value. -/
  base : AbsoluteValue K ℝ
  /-- Nontriviality of the base absolute value. -/
  base_isNontrivial : base.IsNontrivial
  /-- A chosen extension of the base absolute value to `L`. -/
  extension : AbsoluteValueExtension base L

abbrev

LocalBlockFamily

L47 ↗

LocalClassFieldTheory.LocalBlockFamily

Documentation

Product of the local blocks attached to a family of chosen places.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u v w
variable (K : Type u) (L : Type v)
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
variable {K L}

Lean source · statement

abbrev LocalBlockFamily {ι : Type w}
    (d : ι → LocalPlaceDatum K L)

def

localBlockFamilyLocalAction

L57 ↗

LocalClassFieldTheory.localBlockFamilyLocalAction

Documentation

Canonical componentwise decomposition-group action for a local-block family.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u v w
variable (K : Type u) (L : Type v)
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
variable {K L}

Lean source · statement

def localBlockFamilyLocalAction
    {ι : Type w} (d : ι → LocalPlaceDatum K L) :
    ∀ i, MulDistribMulAction
      (absoluteValueDecompositionGroup K (d i).extension.1)
      (LocalizedCompletion
        (d i).base (d i).extension)ˣ

def

localBlockFamilyBlockAction

L70 ↗

LocalClassFieldTheory.localBlockFamilyBlockAction

Documentation

Canonical induced action on every local block in a family.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u v w
variable (K : Type u) (L : Type v)
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
variable {K L}

Lean source · statement

def localBlockFamilyBlockAction
    {ι : Type w} (d : ι → LocalPlaceDatum K L) :
    ∀ i, MulDistribMulAction (L ≃ₐ[K] L)
      (LocalPlaceBlock
        (d i).base (d i).base_isNontrivial
        (d i).extension)

def

localBlockFamilyCohomologyAction

L84 ↗

LocalClassFieldTheory.localBlockFamilyCohomologyAction

Documentation

Canonical componentwise action on the product of a local-block family.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u v w
variable (K : Type u) (L : Type v)
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
variable {K L}

Lean source · statement

def localBlockFamilyCohomologyAction
    {ι : Type w} (d : ι → LocalPlaceDatum K L) :
    MulDistribMulAction (L ≃ₐ[K] L)
      (LocalBlockFamily d)

def

localBlockFamilyDecompositionFintype

L99 ↗

LocalClassFieldTheory.localBlockFamilyDecompositionFintype

Documentation

Canonical finite structures on the decomposition groups in a local-block family.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
universe u v w
variable (K : Type u) (L : Type v)
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
variable {K L}

Lean source · statement

def localBlockFamilyDecompositionFintype
    {ι : Type w} (d : ι → LocalPlaceDatum K L) :
    ∀ i, Fintype
      (absoluteValueDecompositionGroup K
        (d i).extension.1)

Module documentation

Finite families of local idele blocks

Declarations

LocalPlaceDatum

LocalBlockFamily

localBlockFamilyLocalAction

localBlockFamilyBlockAction

localBlockFamilyCohomologyAction

localBlockFamilyDecompositionFintype