Documentation

TauCeti.RepresentationTheory.Homological.ContCohomology.Nonabelian.Inflation

Inflation in continuous nonabelian first cohomology #

Let N be a normal subgroup of a topological group G acting on a topological group A. The quotient G ⧸ N, with the quotient topology, acts on the fixed points Aᴺ, and inflation

H¹(G ⧸ N, Aᴺ) → H¹(G, A)

is the map induced by the compatible pair formed by the projection G → G ⧸ N and the inclusion Aᴺ ↪ A. This file proves the nonabelian inflation–restriction sequence

1 → H¹(G ⧸ N, Aᴺ) → H¹(G, A) → H¹(N, A),

an exact sequence of pointed sets: inflation is injective, and a class restricts to the base point of H¹(N, A) exactly when it is inflated.

For G compact and A discrete this gives the reduction of H¹(G, A) to finite quotients: every class is inflated from G ⧸ U for an open normal subgroup U, and G ⧸ U is finite. Together with the injectivity of inflation, H¹(G, A) is the union of the injective images of the sets H¹(G ⧸ U, Aᵁ). For a profinite Galois group this is the reduction of continuous Galois cohomology to the cohomology of finite Galois extensions.

The key construction is TauCeti.NonabelianH1.Cocycle.descend: a cocycle trivial on N is constant on the cosets of N, takes values in Aᴺ, and so descends to a cocycle of G ⧸ N.

Main definitions #

Main results #

References #

source
theorem TauCeti.NonabelianH1.subgroupSubtype_quotientMk_smul {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] (N : Subgroup G) [N.Normal] (g : G) (a : ↥(FixedPoints.subgroup (↥N) A)) :
(ContinuousMonoidHom.subgroupSubtype (FixedPoints.subgroup (↥N) A)) (N.quotientMkContinuousMonoidHom g • a) = g • (ContinuousMonoidHom.subgroupSubtype (FixedPoints.subgroup (↥N) A)) a

The projection G → G ⧸ N and the inclusion Aᴺ ↪ A form a compatible pair.

source
def TauCeti.NonabelianH1.infl {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] (N : Subgroup G) [N.Normal] :
NonabelianH1 (G ⧸ N) ↥(FixedPoints.subgroup (↥N) A) → NonabelianH1 G A

Inflation H¹(G ⧸ N, Aᴺ) → H¹(G, A): the map induced by the projection G → G ⧸ N and the inclusion of the fixed points Aᴺ ↪ A.

Instances For
    source
    theorem TauCeti.NonabelianH1.infl_mk {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] (N : Subgroup G) [N.Normal] (f : Cocycle (G ⧸ N) ↥(FixedPoints.subgroup (↥N) A)) :
    infl N (mk f) = mk (Cocycle.map N.quotientMkContinuousMonoidHom (ContinuousMonoidHom.subgroupSubtype (FixedPoints.subgroup (↥N) A)) ⋯ f)

    Inflation composes a representing cocycle with the projection G → G ⧸ N.

    source
    @[simp]
    theorem TauCeti.NonabelianH1.infl_one {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] (N : Subgroup G) [N.Normal] :
    infl N 1 = 1

    Inflation preserves the base point.

    source
    theorem TauCeti.NonabelianH1.Cocycle.apply_mul_of_mem {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] {N : Subgroup G} {f : Cocycle G A} (hf : ∀ n ∈ N, f n = 1) (g : G) {n : G} (hn : n ∈ N) :
    f (g * n) = f g

    A cocycle trivial on N is constant on the cosets g * N.

    source
    theorem TauCeti.NonabelianH1.Cocycle.smul_apply_of_mem {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] {N : Subgroup G} [N.Normal] {f : Cocycle G A} (hf : ∀ n ∈ N, f n = 1) (g : G) {n : G} (hn : n ∈ N) :
    n • f g = f g

    A cocycle trivial on N takes values fixed by N.

    source
    def TauCeti.NonabelianH1.Cocycle.descend {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] (N : Subgroup G) [N.Normal] (f : Cocycle G A) (hf : ∀ n ∈ N, f n = 1) :
    Cocycle (G ⧸ N) ↥(FixedPoints.subgroup (↥N) A)

    The cocycle of G ⧸ N with values in Aᴺ induced by a cocycle f of G trivial on N: f is constant on the cosets of N and takes values in Aᴺ.

    Instances For
      source
      @[simp]
      theorem TauCeti.NonabelianH1.Cocycle.coe_descend_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] (N : Subgroup G) [N.Normal] {f : Cocycle G A} (hf : ∀ n ∈ N, f n = 1) (g : G) :
      ↑((descend N f hf) ↑g) = f g
      source
      @[simp]
      theorem TauCeti.NonabelianH1.Cocycle.map_descend {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] (N : Subgroup G) [N.Normal] {f : Cocycle G A} (hf : ∀ n ∈ N, f n = 1) :
      map N.quotientMkContinuousMonoidHom (ContinuousMonoidHom.subgroupSubtype (FixedPoints.subgroup (↥N) A)) ⋯ (descend N f hf) = f

      Inflating the descended cocycle recovers the original cocycle.

      source
      theorem TauCeti.NonabelianH1.infl_mk_descend {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] (N : Subgroup G) [N.Normal] (f : Cocycle G A) (hf : ∀ n ∈ N, f n = 1) :
      infl N (mk (Cocycle.descend N f hf)) = mk f

      The class of a cocycle trivial on N is the inflation of the class of its descent.

      source
      theorem TauCeti.NonabelianH1.infl_injective {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] (N : Subgroup G) [N.Normal] :
      Function.Injective (infl N)

      Inflation is injective: for every normal subgroup N of G, the map H¹(G ⧸ N, Aᴺ) → H¹(G, A) is injective. No continuity of the multiplication of A or of the action of G on A is needed.

      source
      @[simp]
      theorem TauCeti.NonabelianH1.res_infl {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] (N : Subgroup G) [N.Normal] (c : NonabelianH1 (G ⧸ N) ↥(FixedPoints.subgroup (↥N) A)) :
      res N (infl N c) = 1

      The restriction to N of an inflated class is the base point.

      source
      theorem TauCeti.NonabelianH1.res_eq_one_iff {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] (N : Subgroup G) [N.Normal] [ContinuousMul A] [ContinuousSMul G A] {c : NonabelianH1 G A} :
      res N c = 1 ↔ c ∈ Set.range (infl N)

      Inflation–restriction: a class restricts to the base point of H¹(N, A) exactly when it is inflated from H¹(G ⧸ N, Aᴺ).

      source
      theorem TauCeti.NonabelianH1.exists_mem_range_infl {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [Group A] [TopologicalSpace A] [MulDistribMulAction G A] [IsTopologicalGroup G] [CompactSpace G] [DiscreteTopology A] (c : NonabelianH1 G A) :
      ∃ (U : OpenNormalSubgroup G), c ∈ Set.range (infl ↑U.toOpenSubgroup)

      Reduction to finite quotients: for G compact and A discrete, every class of H¹(G, A) is inflated from G ⧸ U for an open normal subgroup U. Such a quotient is finite (Subgroup.quotient_finite_of_isOpen).