Module

QuotientTwoCocycle.lean

Nyll.GaloisCohomology.Kummer.QuotientTwoCocycle

5 declarations indexed from sourceView source ↗

Module documentation

Descent of mixed-zero two-cocycles to a quotient group

The descended cocycle takes values in the actual subgroup invariants. Together with relative normalization, this proves exactness in degree two when subgroup H¹ vanishes.

Imports9

Nyll.GaloisCohomology.Kummer.RelativeTwoCocycle
Nyll.GaloisCohomology.Kummer.MixedTwoCocycle
Mathlib.RepresentationTheory.Rep.Basic
Mathlib.RepresentationTheory.Rep.Res
Mathlib.RepresentationTheory.Invariants
Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Mathlib.GroupTheory.QuotientGroup.Defs
Mathlib.Tactic.Abel

Imported by2

theorem

mixedTwoCocycle_second_right

L35 ↗

ClassFieldTower.Cohomology.mixedTwoCocycle_second_right

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 mixedTwoCocycle_second_right
    (A : Rep k G) (S : Subgroup G) (z : cocycles₂ A)
    (hr : ∀ (g : G) (n : S), z (g, (n : G)) = 0)
    (g h : G) (n : S) : z (g, h * (n : G)) = z (g, h)

theorem

mixedTwoCocycle_first_right

L43 ↗

ClassFieldTower.Cohomology.mixedTwoCocycle_first_right

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 mixedTwoCocycle_first_right
    (A : Rep k G) (S : Subgroup G) [S.Normal] (z : cocycles₂ A)
    (hl : ∀ (n : S) (g : G), z ((n : G), g) = 0)
    (hr : ∀ (g : G) (n : S), z (g, (n : G)) = 0)
    (g h : G) (n : S) : z (g * (n : G), h) = z (g, h)

theorem

mixedTwoCocycle_invariant

L58 ↗

ClassFieldTower.Cohomology.mixedTwoCocycle_invariant

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 mixedTwoCocycle_invariant
    (A : Rep k G) (S : Subgroup G) [S.Normal] (z : cocycles₂ A)
    (hl : ∀ (n : S) (g : G), z ((n : G), g) = 0)
    (hr : ∀ (g : G) (n : S), z (g, (n : G)) = 0)
    (g h : G) (n : S) : A.ρ (n : G) (z (g, h)) = z (g, h)

theorem

exists_quotientTwoCocycle_of_mixed_zero

L75 ↗

ClassFieldTower.Cohomology.exists_quotientTwoCocycle_of_mixed_zero

Documentation

A cocycle vanishing on mixed subgroup arguments descends to quotient cohomology, with coefficients in the subgroup invariants.

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_quotientTwoCocycle_of_mixed_zero
    (A : Rep k G) (S : Subgroup G) [S.Normal] (z : cocycles₂ A)
    (hl : ∀ (n : S) (g : G), z ((n : G), g) = 0)
    (hr : ∀ (g : G) (n : S), z (g, (n : G)) = 0) :
    ∃ w : cocycles₂ (A.quotientToInvariants S),
      mapCocycles₂ (QuotientGroup.mk' S)
        (ofHom (A.ρ.quotientToInvariants_lift S)) w = z

theorem

degreeTwo_restriction_ker_le_inflation_range

L122 ↗

ClassFieldTower.Cohomology.degreeTwo_restriction_ker_le_inflation_range

Documentation

The restriction kernel in degree two is the inflation image whenever the subgroup H¹ vanishes. This constructs the quotient class from a cocycle.

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 degreeTwo_restriction_ker_le_inflation_range
    (A : Rep k G) (S : Subgroup G) [S.Normal]
    [Subsingleton (groupCohomology (res S.subtype A) 1)] :
    (groupCohomology.map S.subtype (𝟙 (res S.subtype A)) 2).hom.ker ≤
      (groupCohomology.map (A := A.quotientToInvariants S) (B := A) (QuotientGroup.mk' S)
        (ofHom (A.ρ.quotientToInvariants_lift S)) 2).hom.range

Module documentation

Descent of mixed-zero two-cocycles to a quotient group

Declarations

mixedTwoCocycle_second_right

mixedTwoCocycle_first_right

mixedTwoCocycle_invariant

exists_quotientTwoCocycle_of_mixed_zero

degreeTwo_restriction_ker_le_inflation_range