NYLL
Module

Theorem6Dot1FormalHilbert90.lean

Nyll.Yamaguchi26AbfaithfulGalois.Theorem6Dot1FormalHilbert90
19 declarations indexed from sourceView source ↗

Module documentation

Definition 6.1: orientations and formal Hilbert 90

This module constructs the twisted coefficient representations from a continuous p-adic orientation and states formal Hilbert 90 using mathlib's continuous first cohomology and its functorial reduction map. Explicit continuous cocycles are retained only for the lifting statements; mathlib's continuous low-degree API does not yet expose them as functions.

Imports12
Imported by7

Declarations

abbrev

Orientation

L41 ↗
Yamaguchi26AbfaithfulGalois.Orientation
Documentation

A continuous ℓ-orientation of a topological group.

Source context 6 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
open ProCGroups.FiniteStepSolvableQuotients
open scoped commutatorElement
universe u
Lean source · statement
abbrev Orientation (ℓ : ℕ) [Fact ℓ.Prime]
    (G : Type u) [Group G] [TopologicalSpace G]
def

finiteOrientationUnits

L48 ↗
Yamaguchi26AbfaithfulGalois.finiteOrientationUnits
Documentation

The orientation restricted to a subgroup and reduced modulo ℓ ^ n. This is a homomorphism into units, so it gives the prescribed coefficient action without a separately postulated action.

Source context 6 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
open ProCGroups.FiniteStepSolvableQuotients
open scoped commutatorElement
universe u
Lean source · statement
def finiteOrientationUnits {ℓ : ℕ} [Fact ℓ.Prime]
    {G : Type u} [Group G] [TopologicalSpace G]
    (θ : Orientation ℓ G) (H : Subgroup G) (n : ℕ) :
    H →* (ZMod (ℓ ^ n))ˣ
def

finiteOrientationTopRep

L57 ↗
Yamaguchi26AbfaithfulGalois.finiteOrientationTopRep
Documentation

The actual discrete ℤ/ℓⁿℤ coefficient representation for the orientation, viewed as an integer module so reduction has a common base ring.

Source context 6 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
open ProCGroups.FiniteStepSolvableQuotients
open scoped commutatorElement
universe u
Lean source · statement
def finiteOrientationTopRep {ℓ : ℕ} [Fact ℓ.Prime]
    {G : Type u} [Group G] [TopologicalSpace G]
    (θ : Orientation ℓ G) (H : Subgroup G) (n : ℕ) : TopRep.{u} ℤ H
theorem

finiteOrientationTopRep_action

L77 ↗
Yamaguchi26AbfaithfulGalois.finiteOrientationTopRep_action
Documentation

The twisted coefficient action evaluated on a residue class.

Source context 6 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
open ProCGroups.FiniteStepSolvableQuotients
open scoped commutatorElement
universe u
Lean source · statement
theorem finiteOrientationTopRep_action {ℓ : ℕ} [Fact ℓ.Prime]
    {G : Type u} [Group G] [TopologicalSpace G]
    (θ : Orientation ℓ G) (H : Subgroup G) (n : ℕ)
    (g : H) (a : ULift.{u} (ZMod (ℓ ^ n))) :
    (finiteOrientationTopRep θ H n).ρ g a =
      ULift.up (PadicInt.toZModPow n (θ (g : G) : PadicInt ℓ) * a.down)
def

finiteOrientationReduction

L85 ↗
Yamaguchi26AbfaithfulGalois.finiteOrientationReduction
Documentation

The natural reduction morphism between twisted coefficient objects.

Source context 6 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
open ProCGroups.FiniteStepSolvableQuotients
open scoped commutatorElement
universe u
Lean source · statement
def finiteOrientationReduction {ℓ : ℕ} [Fact ℓ.Prime]
    {G : Type u} [Group G] [TopologicalSpace G]
    (θ : Orientation ℓ G) (H : Subgroup G) (n : ℕ) (hn : 1 ≤ n) :
    TopRep.res (ContinuousMonoidHom.id H) (finiteOrientationTopRep θ H n) ⟶
      finiteOrientationTopRep θ H 1
structure

FiniteCocycle

L119 ↗
Yamaguchi26AbfaithfulGalois.FiniteCocycle
Documentation

A continuous crossed homomorphism with coefficients in ℤ/ℓⁿℤ, twisted by the restriction of an orientation.

Source context 6 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
open ProCGroups.FiniteStepSolvableQuotients
open scoped commutatorElement
universe u
Lean source · full declaration
structure FiniteCocycle {ℓ : ℕ} [Fact ℓ.Prime]
    {G : Type u} [Group G] [TopologicalSpace G]
    (θ : Orientation ℓ G) (H : Subgroup G) (n : ℕ) where
  /-- The cocycle values in the finite coefficient ring. -/
  toFun : H → ZMod (ℓ ^ n)
  /-- Continuity of the cocycle value function. -/
  continuous_toFun : Continuous toFun
  /-- The crossed-homomorphism identity for the reduced orientation action. -/
  cocycle : ∀ x y : H,
    toFun (x * y) = toFun x +
      PadicInt.toZModPow n (θ (x : G) : PadicInt ℓ) * toFun y
structure

PadicCocycle

L132 ↗
Yamaguchi26AbfaithfulGalois.PadicCocycle
Documentation

A continuous crossed homomorphism with p-adic integer coefficients.

Source context 6 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
open ProCGroups.FiniteStepSolvableQuotients
open scoped commutatorElement
universe u
Lean source · full declaration
structure PadicCocycle {ℓ : ℕ} [Fact ℓ.Prime]
    {G : Type u} [Group G] [TopologicalSpace G]
    (θ : Orientation ℓ G) (H : Subgroup G) where
  /-- The cocycle values in the p-adic coefficient ring. -/
  toFun : H → PadicInt ℓ
  /-- Continuity of the cocycle value function. -/
  continuous_toFun : Continuous toFun
  /-- The crossed-homomorphism identity for the orientation action. -/
  cocycle : ∀ x y : H,
    toFun (x * y) = toFun x + (θ (x : G) : PadicInt ℓ) * toFun y
def

HasH1ReductionSurjective

L145 ↗
Yamaguchi26AbfaithfulGalois.HasH1ReductionSurjective
Documentation

Surjectivity of the actual mathlib map on continuous first cohomology induced by reduction of the twisted coefficient representation.

Source context 6 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
open ProCGroups.FiniteStepSolvableQuotients
open scoped commutatorElement
universe u
Lean source · statement
def HasH1ReductionSurjective {ℓ : ℕ} [Fact ℓ.Prime]
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (θ : Orientation ℓ G) (H : Subgroup G) (n : ℕ) (hn : 1 ≤ n) : Prop
def

FormalHilbert90

L153 ↗
Yamaguchi26AbfaithfulGalois.FormalHilbert90
Documentation

Formal Hilbert 90 at every open subgroup, for the given orientation.

Source context 6 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
open ProCGroups.FiniteStepSolvableQuotients
open scoped commutatorElement
universe u
Lean source · statement
def FormalHilbert90 {ℓ : ℕ} [Fact ℓ.Prime]
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (θ : Orientation ℓ G) : Prop
def

RelativeFormalHilbert90

L160 ↗
Yamaguchi26AbfaithfulGalois.RelativeFormalHilbert90
Documentation

The relative lifting condition H_ℓ used in the earlier manuscript.

Source context 6 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
open ProCGroups.FiniteStepSolvableQuotients
open scoped commutatorElement
universe u
Lean source · statement
def RelativeFormalHilbert90 {ℓ : ℕ} [Fact ℓ.Prime]
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (D : Subgroup G) (θ : Orientation ℓ G) : Prop
abbrev

PrimaryAbelianization

L171 ↗
Yamaguchi26AbfaithfulGalois.PrimaryAbelianization
Documentation

The ℓ-primary factor of the topological abelianization of D. For a profinite abelian group this maximal pro-ℓ quotient is its usual ℓ-primary component. Mathlib's CommGroup.primaryComponent is instead the subgroup of elements of finite ℓ-power order.

Source context 6 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
open ProCGroups.FiniteStepSolvableQuotients
open scoped commutatorElement
universe u
Lean source · statement
abbrev PrimaryAbelianization (ℓ : ℕ) [Fact ℓ.Prime]
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (D : Subgroup G)
abbrev

GroupPrimaryAbelianization

L179 ↗
Yamaguchi26AbfaithfulGalois.GroupPrimaryAbelianization
Documentation

The ℓ-primary factor of the ambient group's abelianization.

Source context 6 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
open ProCGroups.FiniteStepSolvableQuotients
open scoped commutatorElement
universe u
Lean source · statement
abbrev GroupPrimaryAbelianization (ℓ : ℕ) [Fact ℓ.Prime]
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
def

abelianizationInclusion

L187 ↗
Yamaguchi26AbfaithfulGalois.abelianizationInclusion
Documentation

The map on topological abelianizations induced by the actual inclusion of D into G.

Source context 6 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
open ProCGroups.FiniteStepSolvableQuotients
open scoped commutatorElement
universe u
Lean source · statement
def abelianizationInclusion
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (D : Subgroup G) :
    TopologicalAbelianization D →ₜ* TopologicalAbelianization G
def

primaryInclusionMap

L196 ↗
Yamaguchi26AbfaithfulGalois.primaryInclusionMap
Documentation

The natural homomorphism on ℓ-primary abelianizations induced by inclusion.

Source context 6 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
open ProCGroups.FiniteStepSolvableQuotients
open scoped commutatorElement
universe u
Lean source · statement
def primaryInclusionMap (ℓ : ℕ) [Fact ℓ.Prime]
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] (D : Subgroup G) (hDclosed : IsClosed (D : Set G)) :
    PrimaryAbelianization ℓ D →ₜ* GroupPrimaryAbelianization ℓ G
def

primaryConjugationMap

L208 ↗
Yamaguchi26AbfaithfulGalois.primaryConjugationMap
Documentation

Conjugation by g induces the canonical map on the ℓ-primary factor.

Source context 6 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
open ProCGroups.FiniteStepSolvableQuotients
open scoped commutatorElement
universe u
Lean source · statement
def primaryConjugationMap (ℓ : ℕ) [Fact ℓ.Prime]
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (D : Subgroup G) [D.Normal] (hDclosed : IsClosed (D : Set G))
    [CompactSpace G] (g : G) :
    PrimaryAbelianization ℓ D →ₜ* PrimaryAbelianization ℓ D
def

primaryFixedSubgroup

L224 ↗
Yamaguchi26AbfaithfulGalois.primaryFixedSubgroup
Documentation

Elements of the ℓ-primary abelianization fixed by a subgroup.

Source context 6 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
open ProCGroups.FiniteStepSolvableQuotients
open scoped commutatorElement
universe u
Lean source · full declaration
def primaryFixedSubgroup (ℓ : ℕ) [Fact ℓ.Prime]
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] (D : Subgroup G) [D.Normal]
    (hDclosed : IsClosed (D : Set G)) (H : Subgroup G) :
    Subgroup (PrimaryAbelianization ℓ D) where
  carrier := {a | ∀ h : H, primaryConjugationMap ℓ D hDclosed (h : G) a = a}
  one_mem' := by intro h; exact map_one _
  mul_mem' := by
    intro x y hx hy h
    rw [map_mul, hx h, hy h]
  inv_mem' := by
    intro x hx h
    rw [map_inv, hx h]
abbrev

relativeDerived

L240 ↗
Yamaguchi26AbfaithfulGalois.relativeDerived
Documentation

The closed commutator subgroup [D,D], as a subgroup of the ambient group.

Source context 6 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
open ProCGroups.FiniteStepSolvableQuotients
open scoped commutatorElement
universe u
Lean source · statement
abbrev relativeDerived
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (D : Subgroup G) : Subgroup G
instance

relativeDerived_normal

L245 ↗
Yamaguchi26AbfaithfulGalois.relativeDerived_normal
Source context 6 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
open ProCGroups.FiniteStepSolvableQuotients
open scoped commutatorElement
universe u
Lean source · statement
instance relativeDerived_normal
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (D : Subgroup G) [D.Normal] : (relativeDerived D).Normal
abbrev

RelativeDerivedQuotient

L252 ↗
Yamaguchi26AbfaithfulGalois.RelativeDerivedQuotient
Documentation

The actual quotient G/[D,D].

Source context 6 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.Abelian ProCGroups.ProC
open ProCGroups.FiniteStepSolvableQuotients
open scoped commutatorElement
universe u
Lean source · statement
abbrev RelativeDerivedQuotient
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (D : Subgroup G) [D.Normal]

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