NYLL
Module

AbsoluteMuPTopRep.lean

Nyll.GaloisCohomology.Kummer.AbsoluteMuPTopRep
28 declarations indexed from sourceView source ↗

Module documentation

The natural absolute-Galois representation on mu_p

For an arbitrary characteristic-zero field, the p-th roots of unity in its algebraic closure form a discrete ZMod p-module with the natural (generally nontrivial) absolute-Galois action. This file constructs that coefficient TopRep without assuming that the base field contains the roots of unity. It also constructs the usual root quotient attached to a base-field unit as a continuous twisted one-cocycle for this action.

Imports6
Imported by4

Declarations

def

absoluteGaloisGroupContinuousMulEquiv

L37 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteGaloisGroupContinuousMulEquiv
Documentation

Unfold the public absolute-Galois-group wrapper to the Galois group on which the canonical field action is defined.

Source context 6 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
def absoluteGaloisGroupContinuousMulEquiv :
    Field.absoluteGaloisGroup K ≃ₜ* Gal(AlgebraicClosure K/K)
abbrev

AbsoluteMuP

L44 ↗
ClassFieldTower.Martinet.Shafarevich.AbsoluteMuP
Documentation

The additive presentation of the discrete group of p-th roots of unity in an algebraic closure. No choice of a primitive root is made.

Source context 6 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
abbrev AbsoluteMuP
theorem

absoluteMuP_nsmul_eq_zero

L49 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteMuP_nsmul_eq_zero
Documentation

Every element of AbsoluteMuP K p is killed by p.

Source context 7 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
omit [Fact p.Prime] in
Lean source · statement
theorem absoluteMuP_nsmul_eq_zero (x : AbsoluteMuP K p) : p • x = 0
instance

absoluteMuPModule

L55 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteMuPModule
Documentation

The intrinsic ZMod p-module structure on mu_p.

Source context 6 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
instance absoluteMuPModule : Module (ZMod p) (AbsoluteMuP K p)
instance

absoluteMuPContinuousSMul

L61 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteMuPContinuousSMul
Documentation

The intrinsic scalar action is continuous for the discrete topology on mu_p.

Source context 6 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
instance absoluteMuPContinuousSMul : ContinuousSMul (ZMod p) (AbsoluteMuP K p)
def

absoluteMuPActionAddHom

L65 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteMuPActionAddHom
Documentation

The natural action of an absolute Galois element on mu_p, as an additive homomorphism.

Source context 6 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
Lean source · full declaration
def absoluteMuPActionAddHom (sigma : Field.absoluteGaloisGroup K) :
    AbsoluteMuP K p →+ AbsoluteMuP K p where
  toFun x := Additive.ofMul
    ⟨absoluteGaloisGroupContinuousMulEquiv K sigma • x.toMul.1,
      smul_mem_nthRootsSubgroup (AlgebraicClosure K) p
        (absoluteGaloisGroupContinuousMulEquiv K sigma) x.toMul.property⟩
  map_zero' := by
    apply Additive.toMul.injective
    apply Subtype.ext
    change (absoluteGaloisGroupContinuousMulEquiv K sigma) •
      (1 : (AlgebraicClosure K)ˣ) = 1
    exact smul_one _
  map_add' x y := by
    apply Additive.toMul.injective
    apply Subtype.ext
    change (absoluteGaloisGroupContinuousMulEquiv K sigma) •
      (x.toMul.1 * y.toMul.1) =
        ((absoluteGaloisGroupContinuousMulEquiv K sigma) • x.toMul.1) *
          ((absoluteGaloisGroupContinuousMulEquiv K sigma) • y.toMul.1)
    exact smul_mul' _ _ _
theorem

absoluteMuPActionAddHom_apply_coe

L88 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteMuPActionAddHom_apply_coe
Source context 7 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
omit [Fact p.Prime] in
Lean source · statement
theorem absoluteMuPActionAddHom_apply_coe
    (sigma : Field.absoluteGaloisGroup K) (x : AbsoluteMuP K p) :
    (absoluteMuPActionAddHom K p sigma x).toMul.1 =
    (absoluteGaloisGroupContinuousMulEquiv K sigma) • x.toMul.1
def

absoluteMuPActionContinuousLinearMap

L96 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteMuPActionContinuousLinearMap
Documentation

The natural Galois action on mu_p; the scalar action of ZMod p is intrinsic, so every Galois action map is automatically linear.

Source context 6 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
Lean source · full declaration
def absoluteMuPActionContinuousLinearMap (sigma : Field.absoluteGaloisGroup K) :
    AbsoluteMuP K p →L[ZMod p] AbsoluteMuP K p where
  toLinearMap := (absoluteMuPActionAddHom K p sigma).toZModLinearMap p
  cont := continuous_of_discreteTopology
theorem

absoluteMuPActionContinuousLinearMap_apply

L103 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteMuPActionContinuousLinearMap_apply
Source context 7 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
omit [Fact p.Prime] in
Lean source · statement
theorem absoluteMuPActionContinuousLinearMap_apply
    (sigma : Field.absoluteGaloisGroup K) (x : AbsoluteMuP K p) :
    absoluteMuPActionContinuousLinearMap K p sigma x =
      absoluteMuPActionAddHom K p sigma x
def

absoluteMuPContRepresentation

L112 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteMuPContRepresentation
Documentation

The natural continuous representation of the absolute Galois group on mu_p. Here "continuous representation" is Mathlib's ContRepresentation: the coefficient module is a topological module and each action map is continuous.

Source context 6 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
Lean source · full declaration
def absoluteMuPContRepresentation :
    ContRepresentation (ZMod p) (Field.absoluteGaloisGroup K) (AbsoluteMuP K p) where
  toMonoidHom :=
  { toFun := absoluteMuPActionContinuousLinearMap K p
    map_one' := by
      apply ContinuousLinearMap.ext
      intro x
      apply Additive.toMul.injective
      apply Subtype.ext
      change (absoluteGaloisGroupContinuousMulEquiv K 1) • x.toMul.1 = x.toMul.1
      rw [map_one, one_smul]
    map_mul' := by
      intro sigma tau
      apply ContinuousLinearMap.ext
      intro x
      apply Additive.toMul.injective
      apply Subtype.ext
      change (absoluteGaloisGroupContinuousMulEquiv K (sigma * tau)) • x.toMul.1 =
        (absoluteGaloisGroupContinuousMulEquiv K sigma) •
          ((absoluteGaloisGroupContinuousMulEquiv K tau) • x.toMul.1)
      rw [map_mul, mul_smul] }
def

absoluteMuPTopRep

L135 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteMuPTopRep
Documentation

The natural Tate-dual coefficient object mu_p in TopRep.

Source context 6 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
def absoluteMuPTopRep :
    TopRep (ZMod p) (Field.absoluteGaloisGroup K)
abbrev

primePNat

L141 ↗
ClassFieldTower.Martinet.Shafarevich.primePNat
Source context 7 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
variable [CharZero K]
Lean source · statement
abbrev primePNat : ℕ+
abbrev

AbsoluteRadicalDatum

L144 ↗
ClassFieldTower.Martinet.Shafarevich.AbsoluteRadicalDatum
Source context 7 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
variable [CharZero K]
Lean source · statement
abbrev AbsoluteRadicalDatum
def

absoluteKummerChosenRoot

L149 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteKummerChosenRoot
Documentation

The chosen algebraic-closure root used to form the Kummer cocycle of a base-field unit.

Source context 7 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
variable [CharZero K]
Lean source · statement
def absoluteKummerChosenRoot (a : Kˣ) : (AlgebraicClosure K)ˣ
theorem

absoluteKummerChosenRoot_pow

L156 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteKummerChosenRoot_pow
Documentation

The chosen absolute Kummer root has the prescribed p-th power.

Source context 8 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
variable [CharZero K]
omit [CharZero K] in
Lean source · statement
theorem absoluteKummerChosenRoot_pow (a : Kˣ) :
    absoluteKummerChosenRoot K p a ^ p =
      Units.map (algebraMap K (AlgebraicClosure K)).toMonoidHom a
def

absoluteKummerMuPRootCocycle

L168 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteKummerMuPRootCocycle
Documentation

The usual quotient sigma(beta) / beta, valued in the natural Galois module mu_p. Unlike the character-valued API, this construction does not assume mu_p lies in K.

Source context 7 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
variable [CharZero K]
Lean source · statement
def absoluteKummerMuPRootCocycle (a : Kˣ)
    (sigma : Field.absoluteGaloisGroup K) : AbsoluteMuP K p
theorem

absoluteKummerMuPRootCocycle_apply_coe

L180 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteKummerMuPRootCocycle_apply_coe
Documentation

Evaluation of the root cocycle in the ambient unit group.

Source context 8 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
variable [CharZero K]
omit [CharZero K] in
Lean source · statement
theorem absoluteKummerMuPRootCocycle_apply_coe
    (a : Kˣ) (sigma : Field.absoluteGaloisGroup K) :
    (absoluteKummerMuPRootCocycle K p a sigma).toMul.1 =
      absoluteGaloisGroupContinuousMulEquiv K sigma •
          absoluteKummerChosenRoot K p a /
        absoluteKummerChosenRoot K p a
theorem

absoluteKummerMuPRootCocycle_mul

L191 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteKummerMuPRootCocycle_mul
Documentation

The root quotient satisfies the twisted additive cocycle identity for the natural action on mu_p.

Source context 8 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
variable [CharZero K]
omit [CharZero K] in
Lean source · statement
theorem absoluteKummerMuPRootCocycle_mul
    (a : Kˣ) (sigma tau : Field.absoluteGaloisGroup K) :
    absoluteKummerMuPRootCocycle K p a (sigma * tau) =
      absoluteMuPActionContinuousLinearMap K p sigma
          (absoluteKummerMuPRootCocycle K p a tau) +
        absoluteKummerMuPRootCocycle K p a sigma
theorem

absoluteKummerMuPRootCocycle_isLocallyConstant

L205 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteKummerMuPRootCocycle_isLocallyConstant
Documentation

The root quotient is locally constant on the Krull-topological absolute Galois group.

Source context 7 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
variable [CharZero K]
Lean source · statement
theorem absoluteKummerMuPRootCocycle_isLocallyConstant (a : Kˣ) :
    IsLocallyConstant (absoluteKummerMuPRootCocycle K p a)
theorem

absoluteKummerMuPRootCocycle_continuous

L237 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteKummerMuPRootCocycle_continuous
Documentation

The absolute Kummer root quotient is continuous with its natural, nontrivial coefficient action.

Source context 7 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
variable [CharZero K]
Lean source · statement
theorem absoluteKummerMuPRootCocycle_continuous (a : Kˣ) :
    Continuous (absoluteKummerMuPRootCocycle K p a)
def

absoluteKummerMuPRootCocycleContinuousMap

L242 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteKummerMuPRootCocycleContinuousMap
Documentation

The root quotient packaged as a continuous map.

Source context 7 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
variable [CharZero K]
Lean source · statement
def absoluteKummerMuPRootCocycleContinuousMap (a : Kˣ) :
    C(Field.absoluteGaloisGroup K, AbsoluteMuP K p)
def

absoluteKummerMuPHomogeneousOneCochain

L250 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteKummerMuPHomogeneousOneCochain
Documentation

The homogeneous one-cochain associated with the absolute Kummer root cocycle. Writing it as c(h) - c(g) makes continuity immediate and avoids imposing joint continuity on Mathlib's TopRep action.

Source context 7 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
variable [CharZero K]
Lean source · statement
def absoluteKummerMuPHomogeneousOneCochain (a : Kˣ) :
    (TopRep.homogeneousCochains (absoluteMuPTopRep K p)).X 1
theorem

absoluteKummerMuPHomogeneousOneCochain_apply

L282 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteKummerMuPHomogeneousOneCochain_apply
Source context 7 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
variable [CharZero K]
Lean source · statement
theorem absoluteKummerMuPHomogeneousOneCochain_apply
    (a : Kˣ) (g h : Field.absoluteGaloisGroup K) :
    (absoluteKummerMuPHomogeneousOneCochain K p a).1 g h =
      absoluteKummerMuPRootCocycle K p a h -
        absoluteKummerMuPRootCocycle K p a g
theorem

absoluteKummerMuPHomogeneousOneCochain_eq_action

L291 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteKummerMuPHomogeneousOneCochain_eq_action
Documentation

The difference presentation agrees with the usual homogeneousization g • c(g⁻¹h).

Source context 7 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
variable [CharZero K]
Lean source · statement
theorem absoluteKummerMuPHomogeneousOneCochain_eq_action
    (a : Kˣ) (g h : Field.absoluteGaloisGroup K) :
    (absoluteKummerMuPHomogeneousOneCochain K p a).1 g h =
      absoluteMuPActionContinuousLinearMap K p g
        (absoluteKummerMuPRootCocycle K p a (g⁻¹ * h))
theorem

absoluteKummerMuPHomogeneousOneCochain_mem_cycles

L303 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteKummerMuPHomogeneousOneCochain_mem_cycles
Documentation

The homogeneous Kummer one-cochain is killed by the next differential.

Source context 7 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
variable [CharZero K]
Lean source · statement
theorem absoluteKummerMuPHomogeneousOneCochain_mem_cycles (a : Kˣ) :
    ((TopRep.homogeneousCochains (absoluteMuPTopRep K p)).d 1 2).hom
      (absoluteKummerMuPHomogeneousOneCochain K p a) = 0
def

absoluteKummerMuPHomogeneousOneCocycle

L325 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteKummerMuPHomogeneousOneCocycle
Documentation

The absolute Kummer root quotient packaged as a homogeneous continuous one-cocycle.

Source context 7 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
variable [CharZero K]
Lean source · statement
def absoluteKummerMuPHomogeneousOneCocycle (a : Kˣ) :
    ContinuousCohomology.cocycles (absoluteMuPTopRep K p) 1
theorem

iCycles_absoluteKummerMuPHomogeneousOneCocycle

L333 ↗
ClassFieldTower.Martinet.Shafarevich.iCycles_absoluteKummerMuPHomogeneousOneCocycle
Source context 7 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
variable [CharZero K]
Lean source · statement
theorem iCycles_absoluteKummerMuPHomogeneousOneCocycle (a : Kˣ) :
    (TopRep.homogeneousCochains (absoluteMuPTopRep K p)).iCycles 1
        (absoluteKummerMuPHomogeneousOneCocycle K p a) =
      absoluteKummerMuPHomogeneousOneCochain K p a
def

absoluteKummerMuPH1Class

L344 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteKummerMuPH1Class
Documentation

The degree-one continuous cohomology class of the absolute Kummer root quotient with its natural Tate-dual coefficient action.

Source context 7 commands

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

open scoped Pointwise Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CategoryTheory KummerTheory TopRep ContRepresentation groupCohomology
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
variable [CharZero K]
Lean source · statement
def absoluteKummerMuPH1Class (a : Kˣ) :
    continuousCohomology 1 (absoluteMuPTopRep K p)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.