Short exact sequences of discrete modules, and the low-degree connecting maps

A short exact sequence 0 → A → B → C → 0 of discrete G-modules induces short exact sequences of continuous cochains

0 → Cⁿ(G, A) → Cⁿ(G, B) → Cⁿ(G, C) → 0,

and hence connecting homomorphisms δ⁰ : H⁰(G, C) → H¹(G, A) and δ¹ : H¹(G, C) → H²(G, A) on the explicit low-degree complex of TauCeti/RepresentationTheory/Homological/ContCohomology/LowDegree.lean. This file builds both.

Discreteness of the coefficients is used twice, once at each of the two ends of the sequence. Discreteness of C gives surjectivity on cochains: a continuous cochain into C is locally constant, so composing it with any set-theoretic section of B → C is still continuous (TauCeti.exists_continuous_lift). Discreteness of B gives exactness in the middle: every function out of B is continuous, so the retraction onto the image of incl is continuous, and a continuous cochain into B that the projection kills retracts to a continuous cochain into A (TauCeti.ContCohomology.DiscreteShortExact.exists_continuous_incl_comp_eq, whence C1_map_incl_eq_inf_ker). Cocycle conditions descend along incl because an injection into a discrete space reflects continuity (TauCeti.continuous_of_injective_comp). Discreteness of A and of B is also what makes incl and proj continuous. For general topological coefficients neither argument applies, since a set-theoretic section need not be continuous and a continuous cochain need not be locally constant; the cochain sequence can still be exact when suitable continuous lifts exist. Nothing below is asserted in that more general setting.

The sequence is carried by a structure rather than by loose hypotheses because every statement here is about the same sequence and has to name the same two coefficient maps.

Main definitions

• TauCeti.ContCohomology.DiscreteShortExact: a short exact sequence of discrete G-modules.
• TauCeti.ContCohomology.DiscreteShortExact.toShortComplex: the sequence as a short complex of canonical topological coefficient representations.
• TauCeti.ContCohomology.DiscreteShortExact.restrict: the same sequence over a subgroup.
• TauCeti.ContCohomology.DiscreteShortExact.ofAddSubgroup: the sequence 0 → N → B → B ⧸ N → 0 of a G-stable additive subgroup N of a discrete G-module B.
• TauCeti.ContCohomology.DiscreteShortExact.dual: the dual sequence 0 → Hom(C, N) → Hom(B, N) → Hom(A, N) → 0 of internal homs with the conjugation action, whenever homomorphisms A →+ N extend to B, as they do for a sequence killed by a prime p and for a sequence killed by n when N is an injective ℤ/nℤ-module; its maps are precomposition with the projection and the inclusion, which evalPairing_dual_incl and evalPairing_dual_proj record as compatibilities of the evaluation pairings.
• TauCeti.ContCohomology.DiscreteShortExact.inclDistribMulActionHom and TauCeti.ContCohomology.DiscreteShortExact.projDistribMulActionHom: the inclusion and projection bundled as equivariant additive homomorphisms, suitable as inputs to explicitCoeff0. TauCeti.ContCohomology.DiscreteShortExact.ofDiscreteModuleMap_inclDistribMulActionHom and TauCeti.ContCohomology.DiscreteShortExact.ofDiscreteModuleMap_projDistribMulActionHom identify their canonical coefficient maps with those of the raw homomorphisms.
• TauCeti.ContCohomology.DiscreteShortExact.explicitDelta0 and TauCeti.ContCohomology.DiscreteShortExact.explicitDelta1: the connecting homomorphisms H⁰(G, C) → H¹(G, A) and H¹(G, C) → H²(G, A).

Main statements

• TauCeti.ContCohomology.DiscreteShortExact.compLeft_incl_injective, C1_map_incl_eq_inf_ker and C1_map_proj_eq_C1: exactness of 0 → C¹(X, A) → C¹(X, B) → C¹(X, C) → 0 at its left, middle and right nodes, with C2_map_incl_eq_inf_ker and C2_map_proj_eq_C2 the degree-2 instances of the last two.
• TauCeti.ContCohomology.DiscreteShortExact.mem_Z1_of_incl_comp_mem_Z1 and mem_Z2_of_incl_comp_mem_Z2: the continuous cocycles descend along the inclusion, which is what turns a cochain produced by a diagram chase back into a cocycle on A.
• TauCeti.ContCohomology.DiscreteShortExact.explicitDelta0_apply and explicitDelta1_apply: the two connecting maps evaluated on representatives, in the shape of Mathlib's discrete groupCohomology.δ₀_apply and δ₁_apply. They hold for an arbitrary preimage and an arbitrary representing cocycle, so they are also the public form of the well-definedness of the two maps. Their cocycle hypotheses are discharged by TauCeti.ContCohomology.DiscreteShortExact.mem_Z1_of_incl_comp_eq_d0 and mem_Z2_of_incl_comp_eq_d1, which need no cocycle input of their own.

Implementation notes

Continuity of incl and of proj is not carried as data: A and B are discrete, so every map out of them is continuous. Exactness in the middle is Mathlib's Function.Exact, which is ∀ b, proj b = 0 ↔ b ∈ Set.range incl.

The cochain maps are Mathlib's AddMonoidHom.compLeft, postcomposition on a function space; the statements of exactness are therefore about the image and kernel of that homomorphism restricted to the cochain subgroup C¹ X -, which is C¹(G, -) at X = G and C²(G, -) at X = G × G. The compatible-pair pullback, which moves the group as well as the coefficients, is a different map and is not used here.

Both connecting maps are built from a variable preimage first, and the independence of the choice is a theorem rather than a definitional accident; only then is the map defined by choosing a preimage with Function.surjInv. The cochain-level constructions this passes through are private, including the retraction used on the kernel of the projection, since they depend on choices the mathematical statements must not mention; the public interface to them is explicitDelta0_apply and explicitDelta1_apply, which hold with whatever preimage a computation has in hand.

The cochain sequences are stated for a topological monoid G. The two connecting maps ask in addition that the coefficients be discrete G-modules with a continuous action: [ContinuousSMul G A] and [ContinuousSMul G B] for δ⁰, and also [ContinuousSMul G C] for δ¹. Without it B¹ ≤ Z¹ and B² ≤ Z² fail and the quotients H1 and H2 cannot be formed. δ¹ asks moreover for a continuous multiplication on G, which is what carries continuity through d¹. Restricting the sequence to a subgroup (DiscreteShortExact.restrict) and the dual sequence (DiscreteShortExact.dual, whose conjugation action needs inverses) ask G to be a group. Profiniteness plays no part here.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.3.2): the long exact cohomology sequence of a short exact sequence of discrete G-modules, whose degree-≤ 2 connecting maps are the ones built here.

Cochain lifting

The canonical set-theoretic lift of a cochain along a surjection, from which the connecting maps below are built. Its continuity is TauCeti.exists_continuous_lift's argument.

structure TauCeti.ContCohomology.DiscreteShortExact (G : Type u) [Monoid G] (A : Type vA) [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] (B : Type vB) [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] (C : Type vC) [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] : Type (max (max vA vB) vC)

A short exact sequence 0 → A → B → C → 0 of discrete G-modules.

Discreteness of the three modules is what makes the continuous cochain sequences exact: discreteness of C makes arbitrary set-theoretic lifts of continuous cochains continuous, and discreteness of B makes the retraction onto the image of the inclusion continuous, which is what retracts a continuous cochain killed by the projection. Continuity of the two maps is a further consequence of it, not data.

• incl : A →+ B

  The inclusion A → B.

• proj : B →+ C

  The projection B → C.

• incl_equivariant (g : G) (a : A) : self.incl (g • a) = g • self.incl a

  The inclusion is G-equivariant.

• proj_equivariant (g : G) (b : B) : self.proj (g • b) = g • self.proj b

  The projection is G-equivariant.

• incl_injective : Function.Injective ⇑self.incl

  Exactness on the left.

• proj_surjective : Function.Surjective ⇑self.proj

  Exactness on the right.

• exact : Function.Exact ⇑self.incl ⇑self.proj

  Exactness in the middle: proj b = 0 exactly when b comes from A.

theorem TauCeti.ContCohomology.DiscreteShortExact.ext {G : Type u} [Monoid G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] {S T : DiscreteShortExact G A B C} (hincl : S.incl = T.incl) (hproj : S.proj = T.proj) : S = T

Two short exact sequences with the same inclusion and projection are equal.

theorem TauCeti.ContCohomology.DiscreteShortExact.ext_iff {G : Type u} [Monoid G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] {S T : DiscreteShortExact G A B C} : S = T ↔ S.incl = T.incl ∧ S.proj = T.proj

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.proj_incl {G : Type u} [Monoid G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (a : A) : S.proj (S.incl a) = 0

The composite A → B → C vanishes.

def TauCeti.ContCohomology.DiscreteShortExact.inclDistribMulActionHom {G : Type u} [Monoid G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) : A →+[G] B

The inclusion of a short exact sequence, bundled as an equivariant additive homomorphism.

Equations

• S.inclDistribMulActionHom = { toFun := (↑S.incl).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

def TauCeti.ContCohomology.DiscreteShortExact.projDistribMulActionHom {G : Type u} [Monoid G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) : B →+[G] C

The projection of a short exact sequence, bundled as an equivariant additive homomorphism.

Equations

• S.projDistribMulActionHom = { toFun := (↑S.proj).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.inclDistribMulActionHom_apply {G : Type u} [Monoid G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (a : A) : S.inclDistribMulActionHom a = S.incl a

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.projDistribMulActionHom_apply {G : Type u} [Monoid G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (b : B) : S.projDistribMulActionHom b = S.proj b

theorem TauCeti.ContCohomology.DiscreteShortExact.inclDistribMulActionHom_injective {G : Type u} [Monoid G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) : Function.Injective ⇑S.inclDistribMulActionHom

The bundled inclusion is injective, as incl is.

theorem TauCeti.ContCohomology.DiscreteShortExact.projDistribMulActionHom_surjective {G : Type u} [Monoid G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) : Function.Surjective ⇑S.projDistribMulActionHom

The bundled projection is surjective, as proj is.

theorem TauCeti.ContCohomology.DiscreteShortExact.exists_incl_eq {G : Type u} [Monoid G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) {b : B} (hb : S.proj b = 0) : ∃ (a : A), S.incl a = b

An element of B killed by the projection comes from A.

theorem TauCeti.ContCohomology.DiscreteShortExact.nsmul_eq_zero_left {G : Type u} [Monoid G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) {n : ℕ} (hB : ∀ (b : B), n • b = 0) (a : A) : n • a = 0

A natural number killing the middle term of a short exact sequence kills its sub-object.

theorem TauCeti.ContCohomology.DiscreteShortExact.nsmul_eq_zero_right {G : Type u} [Monoid G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) {n : ℕ} (hB : ∀ (b : B), n • b = 0) (c : C) : n • c = 0

A natural number killing the middle term of a short exact sequence kills its quotient.

theorem TauCeti.ContCohomology.DiscreteShortExact.ofDiscreteModuleMap_inclDistribMulActionHom {G : Type u} [Monoid G] {A : Type w} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type w} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type w} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) : ofDiscreteModuleMap S.inclDistribMulActionHom.toAddMonoidHom.toIntLinearMap ⋯ = ofDiscreteModuleMap S.incl.toIntLinearMap ⋯

The canonical coefficient map of the bundled inclusion is that of the raw inclusion: the explicit comparison lemmas are stated for S.inclDistribMulActionHom, the canonical long exact sequence for S.incl.

theorem TauCeti.ContCohomology.DiscreteShortExact.ofDiscreteModuleMap_projDistribMulActionHom {G : Type u} [Monoid G] {A : Type w} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type w} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type w} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) : ofDiscreteModuleMap S.projDistribMulActionHom.toAddMonoidHom.toIntLinearMap ⋯ = ofDiscreteModuleMap S.proj.toIntLinearMap ⋯

The canonical coefficient map of the bundled projection is that of the raw projection: the explicit comparison lemmas are stated for S.projDistribMulActionHom, the canonical long exact sequence for S.proj.

def TauCeti.ContCohomology.DiscreteShortExact.ofAddSubgroup {G : Type u} [Monoid G] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] (N : AddSubgroup B) (hN : ∀ (g : G), ∀ x ∈ N, g • x ∈ N) : DiscreteShortExact G (↥N) B (B ⧸ N)

The short exact sequence 0 → N → B → B ⧸ N → 0 of a G-stable additive subgroup N of a discrete G-module B. The subgroup carries the subspace topology and the restricted action AddSubgroup.restrictDistribMulAction; the quotient carries the quotient topology, which is discrete, and the quotient action AddSubgroup.quotientDistribMulAction.

Equations

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

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.ofAddSubgroup_incl {G : Type u} [Monoid G] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] (N : AddSubgroup B) (hN : ∀ (g : G), ∀ x ∈ N, g • x ∈ N) : (ofAddSubgroup N hN).incl = N.subtype

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.ofAddSubgroup_proj {G : Type u} [Monoid G] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] (N : AddSubgroup B) (hN : ∀ (g : G), ∀ x ∈ N, g • x ∈ N) : (ofAddSubgroup N hN).proj = QuotientAddGroup.mk' N

def TauCeti.ContCohomology.DiscreteShortExact.restrict {G : Type u} [Group G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (T : Subgroup G) : DiscreteShortExact (↥T) A B C

A short exact sequence of discrete G-modules restricts to one of discrete T-modules, for any subgroup T ≤ G. The two maps are unchanged; the naturality of the connecting maps under restriction is stated against this sequence.

Equations

• S.restrict T = { incl := S.incl, proj := S.proj, incl_equivariant := ⋯, proj_equivariant := ⋯, incl_injective := ⋯, proj_surjective := ⋯, exact := ⋯ }

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.restrict_incl {G : Type u} [Group G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (T : Subgroup G) : (S.restrict T).incl = S.incl

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.restrict_proj {G : Type u} [Group G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (T : Subgroup G) : (S.restrict T).proj = S.proj

def TauCeti.ContCohomology.DiscreteShortExact.dual {G : Type u} [Group G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (N : Type vN) [AddCommGroup N] [DistribMulAction G N] (hsurj : Function.Surjective ⇑(InternalHom.precomp G S.inclDistribMulActionHom)) : DiscreteShortExact G (InternalHom G C N) (InternalHom G B N) (InternalHom G A N)

The dual short exact sequence. For a short exact sequence 0 → A → B → C → 0 of discrete G-modules and a G-module N such that every homomorphism A →+ N extends to B, that is, precomposition with the inclusion is surjective on internal homs, precomposition with the two maps gives the short exact sequence

0 → InternalHom G C N → InternalHom G B N → InternalHom G A N → 0

of internal homs with their conjugation actions. The extension hypothesis is the only input beyond the exactness of S: injectivity on the left is InternalHom.precomp_injective and exactness in the middle is InternalHom.exact_precomp, for every N. It holds for every N when B is killed by a prime p, since A embeds in B and Hom(-, N) is exact on 𝔽_p-vector spaces (InternalHom.precomp_surjective), and it holds when B is killed by n and N satisfies Baer's criterion over ℤ/nℤ, for instance N = ℤ/nℤ with any action when n ≠ 0 (InternalHom.precomp_surjective_of_baer); precomp_inclDistribMulActionHom_surjective and precomp_inclDistribMulActionHom_surjective_of_baer state the two cases for the inclusion of S. Evaluation identifies the two maps: evalPairing_dual_incl and evalPairing_dual_proj.

Equations

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

theorem TauCeti.ContCohomology.DiscreteShortExact.precomp_inclDistribMulActionHom_surjective {G : Type u} [Group G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (N : Type vN) [AddCommGroup N] [DistribMulAction G N] {p : ℕ} [Fact (Nat.Prime p)] (hB : ∀ (b : B), p • b = 0) : Function.Surjective ⇑(InternalHom.precomp G S.inclDistribMulActionHom)

The extension hypothesis of dual for a sequence killed by a prime. If B is killed by a prime p, precomposition with the inclusion of S is surjective on internal homs into any N.

theorem TauCeti.ContCohomology.DiscreteShortExact.precomp_inclDistribMulActionHom_surjective_of_baer {G : Type u} [Group G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (N : Type vN) [AddCommGroup N] [DistribMulAction G N] {n : ℕ} [Module (ZMod n) N] (hN : Module.Baer (ZMod n) N) (hB : ∀ (b : B), n • b = 0) : Function.Surjective ⇑(InternalHom.precomp G S.inclDistribMulActionHom)

The extension hypothesis of dual for a sequence killed by n and a Baer target. If B is killed by n and N satisfies Baer's criterion over ℤ/nℤ, precomposition with the inclusion of S is surjective on internal homs into N.

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.dual_incl {G : Type u} [Group G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (N : Type vN) [AddCommGroup N] [DistribMulAction G N] (hsurj : Function.Surjective ⇑(InternalHom.precomp G S.inclDistribMulActionHom)) : (S.dual N hsurj).incl = (InternalHom.precomp G S.projDistribMulActionHom).toAddMonoidHom

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.dual_proj {G : Type u} [Group G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (N : Type vN) [AddCommGroup N] [DistribMulAction G N] (hsurj : Function.Surjective ⇑(InternalHom.precomp G S.inclDistribMulActionHom)) : (S.dual N hsurj).proj = (InternalHom.precomp G S.inclDistribMulActionHom).toAddMonoidHom

theorem TauCeti.ContCohomology.DiscreteShortExact.evalPairing_dual_incl {G : Type u} [Group G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (N : Type vN) [AddCommGroup N] [DistribMulAction G N] (hsurj : Function.Surjective ⇑(InternalHom.precomp G S.inclDistribMulActionHom)) (φ : InternalHom G C N) (b : B) : ((InternalHom.evalPairing G) ((S.dual N hsurj).incl φ)) b = ((InternalHom.evalPairing G) φ) (S.proj b)

The inclusion of the dual sequence is precomposition with the projection: the evaluation pairings of InternalHom G C N with C and of InternalHom G B N with B are compatible along the two maps.

theorem TauCeti.ContCohomology.DiscreteShortExact.evalPairing_dual_proj {G : Type u} [Group G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (N : Type vN) [AddCommGroup N] [DistribMulAction G N] (hsurj : Function.Surjective ⇑(InternalHom.precomp G S.inclDistribMulActionHom)) (ψ : InternalHom G B N) (a : A) : ((InternalHom.evalPairing G) ((S.dual N hsurj).proj ψ)) a = ((InternalHom.evalPairing G) ψ) (S.incl a)

The projection of the dual sequence is precomposition with the inclusion: the evaluation pairings of InternalHom G B N with B and of InternalHom G A N with A are compatible along the two maps.

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.dual_inclDistribMulActionHom {G : Type u} [Group G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (N : Type vN) [AddCommGroup N] [DistribMulAction G N] (hsurj : Function.Surjective ⇑(InternalHom.precomp G S.inclDistribMulActionHom)) : (S.dual N hsurj).inclDistribMulActionHom = InternalHom.precomp G S.projDistribMulActionHom

The equivariant inclusion of the dual sequence is precomposition with the equivariant projection of the original sequence.

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.dual_projDistribMulActionHom {G : Type u} [Group G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (N : Type vN) [AddCommGroup N] [DistribMulAction G N] (hsurj : Function.Surjective ⇑(InternalHom.precomp G S.inclDistribMulActionHom)) : (S.dual N hsurj).projDistribMulActionHom = InternalHom.precomp G S.inclDistribMulActionHom

The equivariant projection of the dual sequence is precomposition with the equivariant inclusion of the original sequence.

theorem TauCeti.ContCohomology.DiscreteShortExact.dual_dual_incl_eval {G : Type u} [Group G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (N : Type vN) [AddCommGroup N] [DistribMulAction G N] (hsurj : Function.Surjective ⇑(InternalHom.precomp G S.inclDistribMulActionHom)) (hsurj' : Function.Surjective ⇑(InternalHom.precomp G (S.dual N hsurj).inclDistribMulActionHom)) (a : A) : ((S.dual N hsurj).dual N hsurj').incl ((InternalHom.eval G A N) a) = (InternalHom.eval G B N) (S.incl a)

Evaluation is a morphism from a sequence to its double dual, on the inclusions. The inclusion of the double dual sequence 0 → A^{∨∨} → B^{∨∨} → C^{∨∨} → 0 carries the evaluation class of a : A to the evaluation class of S.incl a.

theorem TauCeti.ContCohomology.DiscreteShortExact.dual_dual_proj_eval {G : Type u} [Group G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (N : Type vN) [AddCommGroup N] [DistribMulAction G N] (hsurj : Function.Surjective ⇑(InternalHom.precomp G S.inclDistribMulActionHom)) (hsurj' : Function.Surjective ⇑(InternalHom.precomp G (S.dual N hsurj).inclDistribMulActionHom)) (b : B) : ((S.dual N hsurj).dual N hsurj').proj ((InternalHom.eval G B N) b) = (InternalHom.eval G C N) (S.proj b)

Evaluation is a morphism from a sequence to its double dual, on the projections. The projection of the double dual sequence 0 → A^{∨∨} → B^{∨∨} → C^{∨∨} → 0 carries the evaluation class of b : B to the evaluation class of S.proj b.

theorem TauCeti.ContCohomology.DiscreteShortExact.compLeft_incl_injective {G : Type u} [Monoid G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (X : Type w) : Function.Injective ⇑(S.incl.compLeft X)

Exactness of 0 → C¹(X, A) → C¹(X, B) at the left node: postcomposition with the inclusion is injective on all cochains, hence in particular on the continuous ones C¹(X, A). The statement does not mention the cochain subgroups, so the degree-2 node is this theorem at X = G × G and needs no separate C² form.

theorem TauCeti.ContCohomology.DiscreteShortExact.exists_continuous_incl_comp_eq {G : Type u} [Monoid G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) {X : Type w} [TopologicalSpace X] {φ : X → B} (hφ : Continuous φ) (hzero : ∀ (x : X), S.proj (φ x) = 0) : ∃ (a : X → A), Continuous a ∧ ∀ (x : X), S.incl (a x) = φ x

A continuous cochain into B killed by the projection comes from a continuous cochain into A, obtained by retracting the cochain pointwise.

theorem TauCeti.ContCohomology.DiscreteShortExact.C1_map_incl_eq_inf_ker {G : Type u} [Monoid G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (X : Type w) [TopologicalSpace X] : AddSubgroup.map (S.incl.compLeft X) (C1 X A) = C1 X B ⊓ (S.proj.compLeft X).ker

Exactness of 0 → C¹(X, A) → C¹(X, B) → C¹(X, C) → 0 at the middle node: a continuous cochain into B is killed by the projection exactly when it is the image of a continuous cochain into A. Taking X = G this is degree 1, and taking X = G × G it is degree 2.

theorem TauCeti.ContCohomology.DiscreteShortExact.C1_map_proj_eq_C1 {G : Type u} [Monoid G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (X : Type w) [TopologicalSpace X] : AddSubgroup.map (S.proj.compLeft X) (C1 X B) = C1 X C

Exactness of C¹(X, B) → C¹(X, C) → 0 at the right node: every continuous cochain into C lifts, by TauCeti.exists_continuous_lift.

theorem TauCeti.ContCohomology.DiscreteShortExact.C2_map_incl_eq_inf_ker {G : Type u} [Monoid G] [TopologicalSpace G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) : AddSubgroup.map (S.incl.compLeft (G × G)) (C2 G A) = C2 G B ⊓ (S.proj.compLeft (G × G)).ker

Exactness of 0 → C²(G, A) → C²(G, B) → C²(G, C) → 0 in the middle: the degree-2 instance of TauCeti.ContCohomology.DiscreteShortExact.C1_map_incl_eq_inf_ker, at X = G × G.

theorem TauCeti.ContCohomology.DiscreteShortExact.C2_map_proj_eq_C2 {G : Type u} [Monoid G] [TopologicalSpace G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) : AddSubgroup.map (S.proj.compLeft (G × G)) (C2 G B) = C2 G C

Exactness of 0 → C²(G, A) → C²(G, B) → C²(G, C) → 0 on the right: the degree-2 instance of TauCeti.ContCohomology.DiscreteShortExact.C1_map_proj_eq_C1, at X = G × G.

theorem TauCeti.ContCohomology.DiscreteShortExact.mem_Z1_of_incl_comp_mem_Z1 {G : Type u} [Monoid G] [TopologicalSpace G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] {S : DiscreteShortExact G A B C} {a : G → A} {e : G → B} (hae : ∀ (g : G), S.incl (a g) = e g) (he : e ∈ Z1 G B) : a ∈ Z1 G A

A 1-cochain on A lying over a continuous 1-cocycle on B is one. Both halves of membership in Z¹ descend along the inclusion: it reflects continuity, the two modules being discrete, and it is injective, so the cocycle identity descends as well.

theorem TauCeti.ContCohomology.DiscreteShortExact.mem_Z2_of_incl_comp_mem_Z2 {G : Type u} [Monoid G] [TopologicalSpace G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] {S : DiscreteShortExact G A B C} {a : G × G → A} {z : G × G → B} (haz : ∀ (p : G × G), S.incl (a p) = z p) (hz : z ∈ Z2 G B) : a ∈ Z2 G A

A 2-cochain on A lying over a continuous 2-cocycle on B is one, the degree-2 counterpart of TauCeti.ContCohomology.DiscreteShortExact.mem_Z1_of_incl_comp_mem_Z1.

theorem TauCeti.ContCohomology.DiscreteShortExact.proj_d0_eq_zero {G : Type u} [Monoid G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] {S : DiscreteShortExact G A B C} {b : B} (hb : S.proj b ∈ H0 G C) (g : G) : S.proj ((d0 G B) b g) = 0

If the image of b in C is G-invariant then its coboundary d⁰ b is killed by the projection, hence — the sequence being exact in the middle — comes from A.

theorem TauCeti.ContCohomology.DiscreteShortExact.mem_Z1_of_incl_comp_eq_d0 {G : Type u} [Monoid G] [TopologicalSpace G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) {b : B} {a : G → A} (hab : ∀ (g : G), S.incl (a g) = g • b - b) : a ∈ Z1 G A

A cochain on A lying over a coboundary of B is a continuous 1-cocycle. No cocycle hypothesis is needed, a coboundary being a continuous cocycle already; this is the case e = d⁰ b of TauCeti.ContCohomology.DiscreteShortExact.mem_Z1_of_incl_comp_mem_Z1. It is what discharges the hypothesis ha of TauCeti.ContCohomology.DiscreteShortExact.explicitDelta0_apply, whose hab it takes verbatim.

noncomputable def TauCeti.ContCohomology.DiscreteShortExact.explicitDelta0 {G : Type u} [Monoid G] [TopologicalSpace G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) [ContinuousSMul G A] : ↥(H0 G C) →+ H1 G A

The connecting homomorphism δ⁰ : H⁰(G, C) → H¹(G, A). Choose a preimage in B of an invariant of C and take the class of the retraction of its coboundary.

Equations

• S.explicitDelta0 = AddMonoidHom.mk' (fun (c : ↥(TauCeti.ContCohomology.H0 G C)) => TauCeti.ContCohomology.DiscreteShortExact.delta0Class✝ S (Function.surjInv ⋯ ↑c) ⋯) ⋯

theorem TauCeti.ContCohomology.DiscreteShortExact.explicitDelta0_apply {G : Type u} [Monoid G] [TopologicalSpace G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) [ContinuousSMul G A] (c : ↥(H0 G C)) {b : B} (hb : S.proj b = ↑c) {a : G → A} (ha : a ∈ Z1 G A) (hab : ∀ (g : G), S.incl (a g) = g • b - b) : S.explicitDelta0 c = (H1pi G A) ⟨a, ha⟩

δ⁰ on representatives. For any preimage b of an invariant c and any continuous 1-cocycle a with incl ∘ a = d⁰ b, the class of a is δ⁰ c. This mirrors the shape of Mathlib's discrete groupCohomology.δ₀_apply. The hypothesis ha is discharged from hab by TauCeti.ContCohomology.DiscreteShortExact.mem_Z1_of_incl_comp_eq_d0.

theorem TauCeti.ContCohomology.DiscreteShortExact.proj_d1_eq_zero {G : Type u} [Monoid G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] {S : DiscreteShortExact G A B C} {e : G → B} {f : G → C} (he : ∀ (g : G), S.proj (e g) = f g) (hf : groupCohomology.IsCocycle₁ f) (p : G × G) : S.proj ((d1 G B) e p) = 0

If e lies over a 1-cocycle f on C then its coboundary d¹ e is killed by the projection, hence — the sequence being exact in the middle — comes from A.

theorem TauCeti.ContCohomology.DiscreteShortExact.mem_Z2_of_incl_comp_eq_d1 {G : Type u} [Monoid G] [TopologicalSpace G] [ContinuousMul G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) {e : G → B} (hc : Continuous e) {a : G × G → A} (hae : ∀ (g h : G), S.incl (a (g, h)) = g • e h - e (g * h) + e g) : a ∈ Z2 G A

A cochain on A lying over a coboundary of B is a continuous 2-cocycle. No cocycle hypothesis on e is needed, a continuous coboundary being a continuous cocycle already; this is the case z = d¹ e of TauCeti.ContCohomology.DiscreteShortExact.mem_Z2_of_incl_comp_mem_Z2. It is what discharges the hypothesis ha of TauCeti.ContCohomology.DiscreteShortExact.explicitDelta1_apply, whose hae it takes verbatim.

noncomputable def TauCeti.ContCohomology.DiscreteShortExact.explicitDelta1 {G : Type u} [Monoid G] [TopologicalSpace G] [ContinuousMul G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) [ContinuousSMul G A] [ContinuousSMul G C] : H1 G C →+ H2 G A

The connecting homomorphism δ¹ : H¹(G, C) → H²(G, A). Lift a continuous 1-cocycle on C to a continuous 1-cochain on B and take the class of the retraction of its d¹.

Equations

• S.explicitDelta1 = QuotientAddGroup.lift ((TauCeti.ContCohomology.B1 G C).addSubgroupOf (TauCeti.ContCohomology.Z1 G C)) (TauCeti.ContCohomology.DiscreteShortExact.delta1Hom✝ S) ⋯

theorem TauCeti.ContCohomology.DiscreteShortExact.explicitDelta1_apply {G : Type u} [Monoid G] [TopologicalSpace G] [ContinuousMul G] {A : Type vA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type vB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {C : Type vC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) [ContinuousSMul G A] [ContinuousSMul G C] (f : ↥(Z1 G C)) {e : G → B} (hc : Continuous e) (he : ∀ (g : G), S.proj (e g) = ↑f g) {a : G × G → A} (ha : a ∈ Z2 G A) (hae : ∀ (g h : G), S.incl (a (g, h)) = g • e h - e (g * h) + e g) : S.explicitDelta1 ((H1pi G C) f) = (H2pi G A) ⟨a, ha⟩

δ¹ on representatives. For any continuous lift e of a continuous 1-cocycle f on C and any continuous 2-cocycle a with incl ∘ a = d¹ e, the class of a is δ¹ of the class of f. This mirrors the shape of Mathlib's discrete groupCohomology.δ₁_apply. The hypothesis ha is discharged from hae by TauCeti.ContCohomology.DiscreteShortExact.mem_Z2_of_incl_comp_eq_d1.

noncomputable def TauCeti.ContCohomology.DiscreteShortExact.toShortComplex {G : Type u_1} [Monoid G] {A : Type uS} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type uS} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type uS} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) : CategoryTheory.ShortComplex (TopRep ℤ G)

A short exact sequence of discrete G-modules as a short complex of canonical coefficient objects in TopRep ℤ G.

Equations

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

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.toShortComplex_X₁ {G : Type u_1} [Monoid G] {A : Type uS} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type uS} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type uS} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) : S.toShortComplex.X₁ = ofDiscreteModule ℤ G A

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.toShortComplex_g {G : Type u_1} [Monoid G] {A : Type uS} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type uS} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type uS} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) : S.toShortComplex.g = ofDiscreteModuleMap S.proj.toIntLinearMap ⋯

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.toShortComplex_f {G : Type u_1} [Monoid G] {A : Type uS} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type uS} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type uS} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) : S.toShortComplex.f = ofDiscreteModuleMap S.incl.toIntLinearMap ⋯

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.toShortComplex_X₃ {G : Type u_1} [Monoid G] {A : Type uS} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type uS} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type uS} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) : S.toShortComplex.X₃ = ofDiscreteModule ℤ G C

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.toShortComplex_X₂ {G : Type u_1} [Monoid G] {A : Type uS} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type uS} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type uS} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) : S.toShortComplex.X₂ = ofDiscreteModule ℤ G B

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.toShortComplex_g_hom_apply {G : Type u_1} [Monoid G] {A : Type uS} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type uS} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type uS} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (b : B) : (TopRep.Hom.hom S.toShortComplex.g) b = S.proj b

The projection of the coefficient short complex is the given projection on elements.

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.toShortComplex_X₂_ρ_apply {G : Type u_1} [Monoid G] {A : Type uS} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type uS} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type uS} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (k : G) (b : B) : (S.toShortComplex.X₂.ρ k) b = k • b

The middle coefficient representation has the given action.

@[simp]

theorem TauCeti.ContCohomology.DiscreteShortExact.toShortComplex_X₃_ρ_apply {G : Type u_1} [Monoid G] {A : Type uS} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type uS} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] {C : Type uS} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] (S : DiscreteShortExact G A B C) (k : G) (c : C) : (S.toShortComplex.X₃.ρ k) c = k • c

The final coefficient representation has the given action.