First cohomology tensor comparison and prime-to-index descent

Let N be an open normal subgroup of G, let p be prime to [G : N], and let A be a finite ZMod p-module with the discrete topology on which N acts trivially. This file constructs the canonical comparison (available for any topological group acting trivially on a discrete A)

H¹(N, ZMod p) ⊗ A ≃ H¹(N, A).

The map evaluates a continuous character and scales its value by the tensor's second factor. It intertwines inverse conjugation on H¹(N, ZMod p) and the coefficient action on A with conjugation on H¹(N, A). Restriction and the prime-to-p coprime-descent theorem therefore give

dim H¹(G, A) = dim (H¹(N, ZMod p) ⊗ A)^G.

The final form is stated using the quotient representation of G/N, so it can be consumed by representation-theoretic invariant-dimension results.

Main definitions

• TauCeti.h1TensorEquiv: the canonical linear equivalence in first cohomology.
• TauCeti.h1TensorConj: the diagonal conjugation map on its source.
• TauCeti.h1ConjRepresentation: the induced G/N-representation on H¹(N, ZMod p).
• TauCeti.h1CoprimeTensorInvariantsEquiv: coprime descent followed by the tensor comparison.

Main results

• TauCeti.h1TensorEquiv_conj: the comparison is G-equivariant.
• TauCeti.finrank_H1_eq_finrank_tensorInvariants: the tensor-invariant dimension formula.
• TauCeti.finrank_H1_eq_finrank_representationInvariants: the same formula for the formal quotient representation.

References

• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., proof of (7.3.1).
• J. S. Milne, Arithmetic Duality Theorems, I, proof of Theorem 2.8.

theorem TauCeti.continuousSMulTrivialZMod {n : ℕ} {H : Type u_1} [Monoid H] [TopologicalSpace H] : ContinuousSMul H (ZMod n)

noncomputable def TauCeti.h1TensorEquiv {p : ℕ} {H : Type uG} [Group H] [TopologicalSpace H] {A : Type uA} [AddCommGroup A] [Module (ZMod p) A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction H A] [ContinuousSMul H A] [DiscreteTopology A] (htriv : ∀ (h : H) (a : A), h • a = a) [Fact (Nat.Prime p)] [Module.Finite (ZMod p) A] : TensorProduct (ZMod p) (ContCohomology.H1 H (ZMod p)) A ≃ₗ[ZMod p] ContCohomology.H1 H A

The first-cohomology tensor comparison. If H acts trivially on a finite ZMod p-module A with the discrete topology, evaluation identifies H¹(H, ZMod p) ⊗ A with H¹(H, A). The map is canonical even though a basis is used to prove its bijectivity.

@[simp]

theorem TauCeti.h1TensorEquiv_tmul_apply {p : ℕ} {H : Type uG} [Group H] [TopologicalSpace H] {A : Type uA} [AddCommGroup A] [Module (ZMod p) A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction H A] [ContinuousSMul H A] [DiscreteTopology A] (htriv : ∀ (h : H) (a : A), h • a = a) [Fact (Nat.Prime p)] [Module.Finite (ZMod p) A] (x : ContCohomology.H1 H (ZMod p)) (a : A) (h : H) : (Additive.toMul ((ContCohomology.H1EquivOfSmulEqSelf htriv) ((h1TensorEquiv htriv) (x ⊗ₜ[ZMod p] a)))) h = Multiplicative.ofAdd (Multiplicative.toAdd ((Additive.toMul ((h1EquivContinuousZModDual ⋯) x)) h) • a)

On a pure tensor, h1TensorEquiv is pointwise evaluation followed by scalar multiplication.

theorem TauCeti.H1EquivOfSmulEqSelf_explicitConj1_apply {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] {A : Type uA} [AddCommGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] [ContinuousSMul G A] (hN : ∀ (n : ↥N) (a : A), ↑n • a = a) (g : G) (x : ContCohomology.H1 (↥N) A) (n : ↥N) : (Additive.toMul ((ContCohomology.H1EquivOfSmulEqSelf hN) ((ContCohomology.explicitConj1 N g) x))) n = Multiplicative.ofAdd (g • Multiplicative.toAdd ((Additive.toMul ((ContCohomology.H1EquivOfSmulEqSelf hN) x)) ((N.inverseConjugationHom g) n)))

Under the continuous-homomorphism description of H¹, conjugation sends a character c to n ↦ g • c(g⁻¹ng).

noncomputable def TauCeti.h1TensorConj {p : ℕ} {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] {A : Type uA} [AddCommGroup A] [Module (ZMod p) A] [DistribMulAction G A] (g : G) : TensorProduct (ZMod p) (ContCohomology.H1 (↥N) (ZMod p)) A →ₗ[ZMod p] TensorProduct (ZMod p) (ContCohomology.H1 (↥N) (ZMod p)) A

The diagonal action on H¹(N, ZMod p) ⊗ A: conjugation on the character factor and the given action on the coefficient factor.

@[simp]

theorem TauCeti.h1TensorConj_tmul {p : ℕ} {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] {A : Type uA} [AddCommGroup A] [Module (ZMod p) A] [DistribMulAction G A] (g : G) (x : ContCohomology.H1 (↥N) (ZMod p)) (a : A) : (h1TensorConj g) (x ⊗ₜ[ZMod p] a) = (ContCohomology.explicitConj1 N g) x ⊗ₜ[ZMod p] (g • a)

The diagonal conjugation map acts on a pure tensor by conjugating the first factor and applying the coefficient action to the second.

theorem TauCeti.h1TensorEquiv_conj_tmul {p : ℕ} {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] {A : Type uA} [AddCommGroup A] [Module (ZMod p) A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] [ContinuousSMul G A] [DiscreteTopology A] (hN : ∀ (n : ↥N) (a : A), ↑n • a = a) [Fact (Nat.Prime p)] [Module.Finite (ZMod p) A] (g : G) (x : ContCohomology.H1 (↥N) (ZMod p)) (a : A) : (h1TensorEquiv hN) ((ContCohomology.explicitConj1 N g) x ⊗ₜ[ZMod p] (g • a)) = (ContCohomology.explicitConj1 N g) ((h1TensorEquiv hN) (x ⊗ₜ[ZMod p] a))

Equivariance of h1TensorEquiv on pure tensors.

theorem TauCeti.h1TensorEquiv_conj {p : ℕ} {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] {A : Type uA} [AddCommGroup A] [Module (ZMod p) A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] [ContinuousSMul G A] [DiscreteTopology A] (hN : ∀ (n : ↥N) (a : A), ↑n • a = a) [Fact (Nat.Prime p)] [Module.Finite (ZMod p) A] (g : G) (z : TensorProduct (ZMod p) (ContCohomology.H1 (↥N) (ZMod p)) A) : (h1TensorEquiv hN) ((h1TensorConj g) z) = (ContCohomology.explicitConj1 N g) ((h1TensorEquiv hN) z)

The first-cohomology tensor comparison is equivariant for the diagonal conjugation and coefficient action.

def TauCeti.h1TensorConjInvariants {p : ℕ} {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] {A : Type uA} [AddCommGroup A] [Module (ZMod p) A] [DistribMulAction G A] : Submodule (ZMod p) (TensorProduct (ZMod p) (ContCohomology.H1 (↥N) (ZMod p)) A)

The subspace fixed by every diagonal conjugation map on H¹(N, ZMod p) ⊗ A. When N acts trivially on A, the diagonal action factors through G/N, and this is the invariant subspace of the induced quotient representation.

@[simp]

theorem TauCeti.mem_h1TensorConjInvariants_iff {p : ℕ} {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] {A : Type uA} [AddCommGroup A] [Module (ZMod p) A] [DistribMulAction G A] {z : TensorProduct (ZMod p) (ContCohomology.H1 (↥N) (ZMod p)) A} : z ∈ h1TensorConjInvariants ↔ ∀ (g : G), (h1TensorConj g) z = z

Membership in h1TensorConjInvariants means being fixed by every diagonal conjugation map.

noncomputable def TauCeti.h1TensorInvariantsEquiv {p : ℕ} {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] {A : Type uA} [AddCommGroup A] [Module (ZMod p) A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] [ContinuousSMul G A] [DiscreteTopology A] (hN : ∀ (n : ↥N) (a : A), ↑n • a = a) [Fact (Nat.Prime p)] [Module.Finite (ZMod p) A] : ↥h1TensorConjInvariants ≃ₗ[ZMod p] ↥((AddSubgroup.toZModSubmodule p) (ContCohomology.H1ConjInvariants G A N))

Equivariance restricts h1TensorEquiv to the invariant subspaces.

@[simp]

theorem TauCeti.h1TensorInvariantsEquiv_apply {p : ℕ} {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] {A : Type uA} [AddCommGroup A] [Module (ZMod p) A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] [ContinuousSMul G A] [DiscreteTopology A] (hN : ∀ (n : ↥N) (a : A), ↑n • a = a) [Fact (Nat.Prime p)] [Module.Finite (ZMod p) A] (z : ↥h1TensorConjInvariants) : ↑((h1TensorInvariantsEquiv hN) z) = (h1TensorEquiv hN) ↑z

The forward map of h1TensorInvariantsEquiv is h1TensorEquiv on underlying elements.

@[simp]

theorem TauCeti.h1TensorInvariantsEquiv_symm_apply {p : ℕ} {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] {A : Type uA} [AddCommGroup A] [Module (ZMod p) A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] [ContinuousSMul G A] [DiscreteTopology A] (hN : ∀ (n : ↥N) (a : A), ↑n • a = a) [Fact (Nat.Prime p)] [Module.Finite (ZMod p) A] (x : ↥((AddSubgroup.toZModSubmodule p) (ContCohomology.H1ConjInvariants G A N))) : ↑((h1TensorInvariantsEquiv hN).symm x) = (h1TensorEquiv hN).symm ↑x

The inverse of h1TensorInvariantsEquiv is the inverse of h1TensorEquiv on underlying elements.

noncomputable def TauCeti.h1CoprimeTensorInvariantsEquiv {p : ℕ} {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] {A : Type uA} [AddCommGroup A] [Module (ZMod p) A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] [ContinuousSMul G A] [DiscreteTopology A] (hN : ∀ (n : ↥N) (a : A), ↑n • a = a) [Fact (Nat.Prime p)] [Module.Finite (ZMod p) A] (hopen : IsOpen ↑N) (hcop : N.index.Coprime p) : ContCohomology.H1 G A ≃ₗ[ZMod p] ↥h1TensorConjInvariants

Coprime descent followed by the tensor comparison.

@[simp]

theorem TauCeti.h1CoprimeTensorInvariantsEquiv_apply {p : ℕ} {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] {A : Type uA} [AddCommGroup A] [Module (ZMod p) A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] [ContinuousSMul G A] [DiscreteTopology A] (hN : ∀ (n : ↥N) (a : A), ↑n • a = a) [Fact (Nat.Prime p)] [Module.Finite (ZMod p) A] (hopen : IsOpen ↑N) (hcop : N.index.Coprime p) (x : ContCohomology.H1 G A) : ↑((h1CoprimeTensorInvariantsEquiv hN hopen hcop) x) = (h1TensorEquiv hN).symm ↑((ContCohomology.explicitResConj1 G A N) x)

The forward map of h1CoprimeTensorInvariantsEquiv is restriction to N followed by the inverse tensor comparison.

theorem TauCeti.finrank_H1_eq_finrank_tensorInvariants {p : ℕ} {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] {A : Type uA} [AddCommGroup A] [Module (ZMod p) A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] [ContinuousSMul G A] [DiscreteTopology A] (hN : ∀ (n : ↥N) (a : A), ↑n • a = a) [Fact (Nat.Prime p)] [Module.Finite (ZMod p) A] (hopen : IsOpen ↑N) (hcop : N.index.Coprime p) : Module.finrank (ZMod p) (ContCohomology.H1 G A) = Module.finrank (ZMod p) ↥h1TensorConjInvariants

The first-cohomology tensor-invariant dimension formula. For an open normal subgroup of index prime to p acting trivially on A, the dimension of H¹(G, A) is the dimension of the invariants in H¹(N, ZMod p) ⊗ A.

noncomputable def TauCeti.h1ConjRepresentation {p : ℕ} {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] : Representation (ZMod p) (G ⧸ N) (ContCohomology.H1 (↥N) (ZMod p))

Conjugation makes H¹(N, ZMod p) a G/N-representation. Inner conjugation by an element of N is trivial on cohomology, so the ambient G-action factors through the quotient.

@[simp]

theorem TauCeti.h1ConjRepresentation_quotient_mk_apply {p : ℕ} {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] (g : G) (x : ContCohomology.H1 (↥N) (ZMod p)) : (h1ConjRepresentation ↑g) x = (ContCohomology.explicitConj1 N g) x

The quotient representation evaluated on the class of g is conjugation by g.

theorem TauCeti.h1TensorConjInvariants_eq_representationInvariants {p : ℕ} {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] {A : Type uA} [AddCommGroup A] [Module (ZMod p) A] [DistribMulAction G A] (ρ : Representation (ZMod p) (G ⧸ N) A) (hρ : ∀ (g : G) (a : A), (ρ ↑g) a = g • a) : h1TensorConjInvariants = (h1ConjRepresentation.tprod ρ).invariants

The fixed subspace defined through h1TensorConj is the usual invariant subspace of the tensor product of the quotient representations.

theorem TauCeti.finrank_H1_eq_finrank_representationInvariants {p : ℕ} {G : Type uG} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] {A : Type uA} [AddCommGroup A] [Module (ZMod p) A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] [ContinuousSMul G A] [DiscreteTopology A] (hN : ∀ (n : ↥N) (a : A), ↑n • a = a) [Fact (Nat.Prime p)] [Module.Finite (ZMod p) A] (hopen : IsOpen ↑N) (hcop : N.index.Coprime p) (ρ : Representation (ZMod p) (G ⧸ N) A) (hρ : ∀ (g : G) (a : A), (ρ ↑g) a = g • a) : Module.finrank (ZMod p) (ContCohomology.H1 G A) = Module.finrank (ZMod p) ↥(h1ConjRepresentation.tprod ρ).invariants

The representation-theoretic first-cohomology dimension formula. This is the form consumed by finrankTensorInvariantsK0: the right side is the invariant dimension of the tensor of the quotient representation H¹(N, ZMod p) with A.