Pairings with a coinduced module

Let U be an open subgroup of a topological group G and let μ : M →+ N →+ P be a G-equivariant biadditive pairing of G-modules, where P is discrete with continuous U-action. Pairing an element of M with every value of a coinduced function gives a natural pairing

M × Coind_U^G N → Coind_U^G P,
    (m, f) ↦ (g ↦ μ (g • m) (f g)).

The translate g • m is forced by equivariance. The resulting function is U-equivariant, hence locally constant because U is open and the stabilizers of P are open; no topology on M or N is needed, so the construction applies to an arbitrary topological representation M. Evaluation at 1 recovers μ, and the coinduced pairing commutes with the trace:

ev (m ⋆ f) = μ m (ev f),      tr (m ⋆ f) = μ m (tr f).

These two identities are the coefficient-level input to the projection formula for corestriction and cup products.

A U-equivariant biadditive pairing μ : A →+ B →+ C of U-modules also induces the pointwise pairing of the coinduced modules,

Coind_U^G A × Coind_U^G B → Coind_U^G C,
    (f, f') ↦ (g ↦ μ (f g) (f' g)),

which is G-equivariant for the right-translation action and commutes with evaluation at 1. Followed by the trace, the pointwise pairing is the pairing through which the internal hom out of a coinduced module is identified with a coinduced module, and the coefficient pairing along which Shapiro's isomorphism is multiplicative.

Main definitions

• TauCeti.DiscreteCoind.pairing: the biadditive pairing with a coinduced module.
• TauCeti.DiscreteCoind.pointwisePairing: the pointwise pairing of two coinduced modules.

Main results

• TauCeti.DiscreteCoind.eval_pairing: evaluation at 1 commutes with the pairing.
• TauCeti.DiscreteCoind.trace_pairing: the coinduced trace commutes with the pairing.
• TauCeti.DiscreteCoind.pointwisePairing_smul, TauCeti.DiscreteCoind.eval_pointwisePairing: the pointwise pairing is G-equivariant and commutes with evaluation at 1.

References

• K. S. Brown, Cohomology of Groups, GTM 87, Springer (1982), Chapter V, §3, (3.8).
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Springer (2008), Chapter I, §5, (1.5.3)(iv).

def TauCeti.DiscreteCoind.pairing {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] (U : Subgroup G) (hU : IsOpen ↑U) {M N P : Type u} [AddCommGroup M] [DistribMulAction G M] [AddCommGroup N] [DistribMulAction G N] [AddCommGroup P] [TopologicalSpace P] [DiscreteTopology P] [DistribMulAction G P] [ContinuousSMul (↥U) P] (μ : M →+ N →+ P) (hμ : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n) : M →+ DiscreteCoind G U N →+ DiscreteCoind G U P

Pairing an element of a G-module with a coinduced function, pointwise after translating the first argument: pairing μ m f g = μ (g • m) (f g).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.DiscreteCoind.pairing_apply {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] (U : Subgroup G) (hU : IsOpen ↑U) {M N P : Type u} [AddCommGroup M] [DistribMulAction G M] [AddCommGroup N] [DistribMulAction G N] [AddCommGroup P] [TopologicalSpace P] [DiscreteTopology P] [DistribMulAction G P] [ContinuousSMul (↥U) P] (μ : M →+ N →+ P) (hμ : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n) (m : M) (f : DiscreteCoind G U N) (g : G) : (((pairing U hU μ hμ) m) f) g = (μ (g • m)) (f g)

theorem TauCeti.DiscreteCoind.pairing_smul {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] (U : Subgroup G) (hU : IsOpen ↑U) {M N P : Type u} [AddCommGroup M] [DistribMulAction G M] [AddCommGroup N] [DistribMulAction G N] [AddCommGroup P] [TopologicalSpace P] [DiscreteTopology P] [DistribMulAction G P] [ContinuousSMul (↥U) P] (μ : M →+ N →+ P) (hμ : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n) (g : G) (m : M) (f : DiscreteCoind G U N) : ((pairing U hU μ hμ) (g • m)) (g • f) = g • ((pairing U hU μ hμ) m) f

The pairing with a coinduced module is G-equivariant.

theorem TauCeti.DiscreteCoind.eval_pairing {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] (U : Subgroup G) (hU : IsOpen ↑U) {M N P : Type u} [AddCommGroup M] [DistribMulAction G M] [AddCommGroup N] [DistribMulAction G N] [AddCommGroup P] [TopologicalSpace P] [DiscreteTopology P] [DistribMulAction G P] [ContinuousSMul (↥U) P] (μ : M →+ N →+ P) (hμ : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n) (m : M) (f : DiscreteCoind G U N) : (eval G U P) (((pairing U hU μ hμ) m) f) = (μ m) ((eval G U N) f)

Evaluation at 1 commutes with the pairing with a coinduced module.

theorem TauCeti.DiscreteCoind.trace_pairing {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] (U : Subgroup G) (hU : IsOpen ↑U) {M N P : Type u} [AddCommGroup M] [DistribMulAction G M] [AddCommGroup N] [DistribMulAction G N] [AddCommGroup P] [TopologicalSpace P] [DiscreteTopology P] [DistribMulAction G P] [ContinuousSMul (↥U) P] (μ : M →+ N →+ P) (hμ : ∀ (g : G) (m : M) (n : N), (μ (g • m)) (g • n) = g • (μ m) n) [U.FiniteIndex] (m : M) (f : DiscreteCoind G U N) : (trace G U P) (((pairing U hU μ hμ) m) f) = (μ m) ((trace G U N) f)

The coinduced trace commutes with the pairing: tr (g ↦ μ (g • m) (f g)) = μ m (tr f). This is the coefficient identity behind the projection formula in cohomology.

def TauCeti.DiscreteCoind.pointwisePairing {G : Type u} [Group G] [TopologicalSpace G] (U : Subgroup G) {A : Type v} {B : Type w} {C : Type x} [AddCommGroup A] [DistribMulAction (↥U) A] [AddCommGroup B] [DistribMulAction (↥U) B] [AddCommGroup C] [DistribMulAction (↥U) C] (μ : A →+ B →+ C) (hμ : ∀ (u : ↥U) (a : A) (b : B), (μ (u • a)) (u • b) = u • (μ a) b) : DiscreteCoind G U A →+ DiscreteCoind G U B →+ DiscreteCoind G U C

The pointwise pairing of two coinduced modules: a U-equivariant biadditive pairing μ : A →+ B →+ C of U-modules pairs coinduced functions value by value, pointwisePairing U μ hμ f f' g = μ (f g) (f' g).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.DiscreteCoind.pointwisePairing_apply {G : Type u} [Group G] [TopologicalSpace G] (U : Subgroup G) {A : Type v} {B : Type w} {C : Type x} [AddCommGroup A] [DistribMulAction (↥U) A] [AddCommGroup B] [DistribMulAction (↥U) B] [AddCommGroup C] [DistribMulAction (↥U) C] (μ : A →+ B →+ C) (hμ : ∀ (u : ↥U) (a : A) (b : B), (μ (u • a)) (u • b) = u • (μ a) b) (f : DiscreteCoind G U A) (f' : DiscreteCoind G U B) (g : G) : (((pointwisePairing U μ hμ) f) f') g = (μ (f g)) (f' g)

theorem TauCeti.DiscreteCoind.pointwisePairing_smul {G : Type u} [Group G] [TopologicalSpace G] (U : Subgroup G) {A : Type v} {B : Type w} {C : Type x} [AddCommGroup A] [DistribMulAction (↥U) A] [AddCommGroup B] [DistribMulAction (↥U) B] [AddCommGroup C] [DistribMulAction (↥U) C] (μ : A →+ B →+ C) (hμ : ∀ (u : ↥U) (a : A) (b : B), (μ (u • a)) (u • b) = u • (μ a) b) [ContinuousMul G] (g : G) (f : DiscreteCoind G U A) (f' : DiscreteCoind G U B) : ((pointwisePairing U μ hμ) (g • f)) (g • f') = g • ((pointwisePairing U μ hμ) f) f'

The pointwise pairing of coinduced modules is G-equivariant.

theorem TauCeti.DiscreteCoind.eval_pointwisePairing {G : Type u} [Group G] [TopologicalSpace G] (U : Subgroup G) {A : Type v} {B : Type w} {C : Type x} [AddCommGroup A] [DistribMulAction (↥U) A] [AddCommGroup B] [DistribMulAction (↥U) B] [AddCommGroup C] [DistribMulAction (↥U) C] (μ : A →+ B →+ C) (hμ : ∀ (u : ↥U) (a : A) (b : B), (μ (u • a)) (u • b) = u • (μ a) b) (f : DiscreteCoind G U A) (f' : DiscreteCoind G U B) : (eval G U C) (((pointwisePairing U μ hμ) f) f') = (μ ((eval G U A) f)) ((eval G U B) f')

Evaluation at 1 commutes with the pointwise pairing of coinduced modules.