Module

ClassFormationPGroupH1.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.ClassFormationPGroupH1

4 declarations indexed from sourceView source ↗

Module documentation

Degree-one vanishing for finite p-extensions of a class formation

The cyclic class-field axiom already supplies H¹ = 0 through cyclic Tate periodicity. This file propagates that source result to every finite p-extension by induction on its quotient order.

The induction works with cocycles on the ambient closed subgroups. After subtracting a primitive on a maximal subgroup, the cocycle descends to the cyclic quotient. This avoids introducing intermediate-field representation comparisons or assuming a higher-degree class-formation theorem.

Imports4

Imported by2

theorem

cyclicClassFormationH1Primitive

L41 ↗

ClassFieldTower.Cohomology.cyclicClassFormationH1Primitive

Documentation

The cyclic class-field axiom produces an invariant primitive for a cocycle on the base subgroup vanishing on the top-field subgroup.

Source context 8 commands

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

open CategoryTheory groupCohomology
namespace ClassFieldTower.Cohomology
open ClassFormation CyclicCohomology
noncomputable section
variable {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (A : Rep ℤ G) (hcf : SatisfiesClassFieldAxiom A)
include hcf
omit [IsTopologicalGroup G] in

Lean source · statement

theorem cyclicClassFormationH1Primitive
    (K : FiniteAbstractField G) (L : FiniteGaloisSubextension K.field)
    (hcyc : IsCyclic L.extensionQuotient)
    (z : cocycles₁ (Rep.res K.field.toSubgroup.subtype A))
    (hz : ∀ n : extensionSubgroup K.field L.field L.below, z n.1 = 0) :
    ∃ a : A, (∀ l : L.field.toSubgroup, A.ρ l.1 a = a) ∧
      ∀ k : K.field.toSubgroup, A.ρ k.1 a - a = z k

theorem

subgroup_card_lt_of_ne_top

L79 ↗

ClassFieldTower.Cohomology.subgroup_card_lt_of_ne_top

Documentation

A proper subgroup of a finite group has strictly smaller order.

Source context 8 commands

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

open CategoryTheory groupCohomology
namespace ClassFieldTower.Cohomology
open ClassFormation CyclicCohomology
noncomputable section
variable {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (A : Rep ℤ G) (hcf : SatisfiesClassFieldAxiom A)
include hcf
omit hcf in

Lean source · statement

theorem subgroup_card_lt_of_ne_top
    {Q : Type} [Group Q] [Finite Q] (S : Subgroup Q) (hS : S ≠ ⊤) :
    Nat.card S < Nat.card Q

theorem

pClassFormationH1Primitive

L97 ↗

ClassFieldTower.Cohomology.pClassFormationH1Primitive

Documentation

Produce an invariant primitive in every finite p-extension by restricting to a maximal subgroup and then descending to its cyclic quotient.

Source context 7 commands

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

open CategoryTheory groupCohomology
namespace ClassFieldTower.Cohomology
open ClassFormation CyclicCohomology
noncomputable section
variable {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (A : Rep ℤ G) (hcf : SatisfiesClassFieldAxiom A)
include hcf

Lean source · statement

theorem pClassFormationH1Primitive
    {p : ℕ} [Fact p.Prime]
    (K : FiniteAbstractField G) (L : FiniteGaloisSubextension K.field)
    (hP : IsPGroup p L.extensionQuotient)
    (z : cocycles₁ (Rep.res K.field.toSubgroup.subtype A))
    (hz : ∀ n : extensionSubgroup K.field L.field L.below, z n.1 = 0) :
    ∃ a : A, (∀ l : L.field.toSubgroup, A.ρ l.1 a = a) ∧
      ∀ k : K.field.toSubgroup, A.ρ k.1 a - a = z k

theorem

pClassFormationH1_subsingleton

L172 ↗

ClassFieldTower.Cohomology.pClassFormationH1_subsingleton

Documentation

The cyclic class-field axiom implies degree-one vanishing for the actual fixed representation of every finite p-extension.

Source context 7 commands

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

open CategoryTheory groupCohomology
namespace ClassFieldTower.Cohomology
open ClassFormation CyclicCohomology
noncomputable section
variable {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (A : Rep ℤ G) (hcf : SatisfiesClassFieldAxiom A)
include hcf

Lean source · statement

theorem pClassFormationH1_subsingleton
    {p : ℕ} [Fact p.Prime]
    (K : FiniteAbstractField G) (L : FiniteGaloisSubextension K.field)
    (hP : IsPGroup p L.extensionQuotient) :
    Subsingleton (H1 (extensionFixedRepresentation A K.field L.field L.below L.normal))

Module documentation

Degree-one vanishing for finite p-extensions of a class formation

Declarations

cyclicClassFormationH1Primitive

subgroup_card_lt_of_ne_top

pClassFormationH1Primitive

pClassFormationH1_subsingleton