Documentation

TauCeti.RepresentationTheory.Homological.ContCohomology.Corestriction.IndexTwo.EvensConj

The conjugate class at index two, in every degree #

Let U be an open subgroup of index two in a profinite group G. On Hⁿ(U, 𝔽₂) the composite res ∘ cor of corestriction and restriction is 1 + s for either element s of the nontrivial coset of U, so res ∘ cor - id is the conjugation action of that coset, and it is defined without choosing s. This file defines it in every degree, on Mathlib's canonical continuous cohomology with trivial 𝔽₂ coefficients, as OpenSubgroup.evensConj. It is the conjugate class Ξ± ↦ s Β· Ξ± in the identities of the index-two Evens norm, such as res N(Ξ±) = Ξ± ⌣ (s Β· Ξ±).

Its basic laws follow from cor ∘ res = [G : U] = 2 (TauCeti.trivialF2ResMap_comp_trivialF2CorMap) alone: it is an involution, it fixes every class restricted from G, and corestriction does not see it. In degree one it is the explicit conjugation TauCeti.ContCohomology.evensConj1 read through the degree-one comparison TauCeti.ContCohomology.explicitH1AddEquivContinuousCohomology, and so it is conjugation by every element outside U (TauCeti.ContCohomology.evensConj1_eq_explicitConj1).

Main definitions #

Main results #

References #

source
noncomputable def OpenSubgroup.evensConj {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : OpenSubgroup G) (hU : (↑U).index = 2) (n : β„•) :
continuousCohomology n (TauCeti.trivialF2 β†₯↑U) ⟢ continuousCohomology n (TauCeti.trivialF2 β†₯↑U)

The conjugation of the nontrivial coset on Hⁿ(U, 𝔽₂), for an open subgroup U of index two, defined choice-free as res ∘ cor - id. At index two res ∘ cor is 1 + s for every s βˆ‰ U, so this is conjugation by any such s, while depending on U alone; in degree one this identification is evensConj_explicitH1AddEquivContinuousCohomology.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem OpenSubgroup.evensConj_def {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : OpenSubgroup G) (hU : (↑U).index = 2) (n : β„•) :
    U.evensConj hU n = CategoryTheory.CategoryStruct.comp (TauCeti.trivialF2CorMap G ↑U β‹― n) (TauCeti.trivialF2ResMap G (↑U) n) - CategoryTheory.CategoryStruct.id (continuousCohomology n (TauCeti.trivialF2 β†₯↑U))

    The definition of evensConj as corestriction followed by restriction, minus the identity.

    source
    theorem OpenSubgroup.trivialF2CorMap_comp_trivialF2ResMap {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : OpenSubgroup G) (hU : (↑U).index = 2) (n : β„•) :
    CategoryTheory.CategoryStruct.comp (TauCeti.trivialF2CorMap G ↑U β‹― n) (TauCeti.trivialF2ResMap G (↑U) n) = CategoryTheory.CategoryStruct.id (continuousCohomology n (TauCeti.trivialF2 β†₯↑U)) + U.evensConj hU n

    res ∘ cor = id + evensConj on Hⁿ(U, 𝔽₂) at index two, the definition of evensConj solved for res ∘ cor.

    source
    @[simp]
    theorem OpenSubgroup.trivialF2ResMap_trivialF2CorMap {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : OpenSubgroup G) (hU : (↑U).index = 2) (n : β„•) (y : ↑(continuousCohomology n (TauCeti.trivialF2 β†₯↑U)).toModuleCat) :
    (CategoryTheory.ConcreteCategory.hom (TauCeti.trivialF2ResMap G (↑U) n)) ((CategoryTheory.ConcreteCategory.hom (TauCeti.trivialF2CorMap G ↑U β‹― n)) y) = y + (CategoryTheory.ConcreteCategory.hom (U.evensConj hU n)) y

    res (cor y) = y + evensConj y for every class y ∈ Hⁿ(U, 𝔽₂), at index two.

    source
    theorem OpenSubgroup.evensConj_comp_evensConj {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : OpenSubgroup G) (hU : (↑U).index = 2) (n : β„•) :
    CategoryTheory.CategoryStruct.comp (U.evensConj hU n) (U.evensConj hU n) = CategoryTheory.CategoryStruct.id (continuousCohomology n (TauCeti.trivialF2 β†₯↑U))

    evensConj is an involution: conjugating twice by the nontrivial coset is the identity.

    source
    @[simp]
    theorem OpenSubgroup.evensConj_evensConj {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : OpenSubgroup G) (hU : (↑U).index = 2) (n : β„•) (y : ↑(continuousCohomology n (TauCeti.trivialF2 β†₯↑U)).toModuleCat) :
    (CategoryTheory.ConcreteCategory.hom (U.evensConj hU n)) ((CategoryTheory.ConcreteCategory.hom (U.evensConj hU n)) y) = y

    evensConj (evensConj y) = y for every class y ∈ Hⁿ(U, 𝔽₂).

    source
    theorem OpenSubgroup.trivialF2ResMap_comp_evensConj {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : OpenSubgroup G) (hU : (↑U).index = 2) (n : β„•) :
    CategoryTheory.CategoryStruct.comp (TauCeti.trivialF2ResMap G (↑U) n) (U.evensConj hU n) = TauCeti.trivialF2ResMap G (↑U) n

    evensConj fixes restricted classes: restriction from G followed by evensConj is restriction.

    source
    @[simp]
    theorem OpenSubgroup.evensConj_trivialF2ResMap {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : OpenSubgroup G) (hU : (↑U).index = 2) (n : β„•) (x : ↑(continuousCohomology n (TauCeti.trivialF2 G)).toModuleCat) :
    (CategoryTheory.ConcreteCategory.hom (U.evensConj hU n)) ((CategoryTheory.ConcreteCategory.hom (TauCeti.trivialF2ResMap G (↑U) n)) x) = (CategoryTheory.ConcreteCategory.hom (TauCeti.trivialF2ResMap G (↑U) n)) x

    evensConj (res x) = res x for every class x ∈ Hⁿ(G, 𝔽₂).

    source
    theorem OpenSubgroup.evensConj_comp_trivialF2CorMap {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : OpenSubgroup G) (hU : (↑U).index = 2) (n : β„•) :
    CategoryTheory.CategoryStruct.comp (U.evensConj hU n) (TauCeti.trivialF2CorMap G ↑U β‹― n) = TauCeti.trivialF2CorMap G ↑U β‹― n

    Corestriction is invariant under evensConj: evensConj followed by corestriction to G is corestriction.

    source
    @[simp]
    theorem OpenSubgroup.trivialF2CorMap_evensConj {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : OpenSubgroup G) (hU : (↑U).index = 2) (n : β„•) (y : ↑(continuousCohomology n (TauCeti.trivialF2 β†₯↑U)).toModuleCat) :
    (CategoryTheory.ConcreteCategory.hom (TauCeti.trivialF2CorMap G ↑U β‹― n)) ((CategoryTheory.ConcreteCategory.hom (U.evensConj hU n)) y) = (CategoryTheory.ConcreteCategory.hom (TauCeti.trivialF2CorMap G ↑U β‹― n)) y

    cor (evensConj y) = cor y for every class y ∈ Hⁿ(U, 𝔽₂).

    source
    theorem OpenSubgroup.evensConj_explicitH1AddEquivContinuousCohomology {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : OpenSubgroup G) (hU : (↑U).index = 2) (x : TauCeti.ContCohomology.H1 β†₯↑U ↑(TauCeti.trivialF2 G)) :
    (CategoryTheory.ConcreteCategory.hom (U.evensConj hU 1)) ((TopModuleCat.Hom.hom (CategoryTheory.eqToHom β‹―)) ((TauCeti.ContCohomology.explicitH1AddEquivContinuousCohomology β†₯↑U ↑(TauCeti.trivialF2 G)) x)) = (TopModuleCat.Hom.hom (CategoryTheory.eqToHom β‹―)) ((TauCeti.ContCohomology.explicitH1AddEquivContinuousCohomology β†₯↑U ↑(TauCeti.trivialF2 G)) ((TauCeti.ContCohomology.evensConj1 G (↑(TauCeti.trivialF2 G)) (↑U) hU β‹―) x))

    In degree one, evensConj is the explicit conjugation evensConj1. A class of HΒΉ(U, 𝔽₂) presented by an explicit cocycle valued in the carrier of trivialF2 G is sent to the class of its image under TauCeti.ContCohomology.evensConj1, both read in continuous cohomology through the identification of the coefficient object with trivialF2 U. Hence evensConj in degree one is conjugation by every element outside U (TauCeti.ContCohomology.evensConj1_eq_explicitConj1).