NYLL
Module

MixedTwoCocycle.lean

Nyll.GaloisCohomology.Kummer.MixedTwoCocycle
2 declarations indexed from sourceView source ↗

Module documentation

Killing mixed subgroup entries of a two-cocycle

A vanishing first cohomology group supplies primitives for the conjugation cocycles of a relative representative. A coset section then turns these primitives into one global cochain.

Imports5
Imported by2

Declarations

theorem

exists_conjugation_primitive

L31 ↗
ClassFieldTower.Cohomology.exists_conjugation_primitive
Source context 6 commands

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

open CategoryTheory
open Rep
open groupCohomology
namespace ClassFieldTower.Cohomology
noncomputable section
variable {k G : Type} [CommRing k] [Group G]
Lean source · statement
theorem exists_conjugation_primitive
    (A : Rep k G) (S : Subgroup G) [S.Normal]
    [Subsingleton (groupCohomology (res S.subtype A) 1)]
    (z : cocycles₂ A) (hz : ∀ n m : S, z ((n : G), (m : G)) = 0)
    (g : G) : ∃ b : A, ∀ n : S,
      A.ρ (n : G) b - b = z ((n : G), g) - z (g, g⁻¹ * (n : G) * g)
theorem

exists_mixedTwoCocycle_correction

L45 ↗
ClassFieldTower.Cohomology.exists_mixedTwoCocycle_correction
Documentation

A relative cocycle admits a global cochain which kills all entries having at least one argument in the subgroup when the subgroup H¹ vanishes.

Source context 6 commands

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

open CategoryTheory
open Rep
open groupCohomology
namespace ClassFieldTower.Cohomology
noncomputable section
variable {k G : Type} [CommRing k] [Group G]
Lean source · statement
theorem exists_mixedTwoCocycle_correction
    (A : Rep k G) (S : Subgroup G) [S.Normal]
    [Subsingleton (groupCohomology (res S.subtype A) 1)]
    (z : cocycles₂ A) (hz : ∀ n m : S, z ((n : G), (m : G)) = 0) :
    ∃ B : G → A,
      (∀ n : S, B n = 0) ∧
      (∀ (n : S) (g : G), d₁₂ A B ((n : G), g) = z ((n : G), g)) ∧
      (∀ (g : G) (n : S), d₁₂ A B (g, (n : G)) = z (g, (n : G)))

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