Exactness of discrete coinduction

Coinduction from a closed subgroup of a profinite group takes a short exact sequence of discrete modules to a short exact sequence. This packages the injectivity, middle exactness, and surjectivity of TauCeti.coindMap in the coefficient format used by continuous cohomology. This is the exact coefficient sequence used in the coinduced proof of Shapiro's lemma (Ribes–Zalesskii, Profinite Groups, Theorem 6.10.5).

noncomputable def TauCeti.ContCohomology.DiscreteShortExact.coind {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : Subgroup G) (hU : IsClosed ↑U) {A : Type u_2} {B : Type u_3} {C : Type u_4} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction (↥U) A] [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction (↥U) B] [ContinuousSMul (↥U) B] [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction (↥U) C] (S : DiscreteShortExact (↥U) A B C) : DiscreteShortExact G (DiscreteCoind G U A) (DiscreteCoind G U B) (DiscreteCoind G U C)

The short exact sequence obtained by applying discrete coinduction from a closed subgroup to each term and map of a short exact sequence.

Equations

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

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.coind_incl_apply {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : Subgroup G) (hU : IsClosed ↑U) {A : Type u_2} {B : Type u_3} {C : Type u_4} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction (↥U) A] [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction (↥U) B] [ContinuousSMul (↥U) B] [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction (↥U) C] (S : DiscreteShortExact (↥U) A B C) (a : DiscreteCoind G U A) (g : G) : ((coind U hU S).incl a) g = S.incl (a g)

Coinduction applies the inclusion of a short exact sequence pointwise.

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.coind_proj_apply {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : Subgroup G) (hU : IsClosed ↑U) {A : Type u_2} {B : Type u_3} {C : Type u_4} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction (↥U) A] [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction (↥U) B] [ContinuousSMul (↥U) B] [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction (↥U) C] (S : DiscreteShortExact (↥U) A B C) (b : DiscreteCoind G U B) (g : G) : ((coind U hU S).proj b) g = S.proj (b g)

Coinduction applies the projection of a short exact sequence pointwise.