Topology of additive fixed points

The fixed points of a subgroup carry the subspace topology from the coefficient space. This file proves continuity of restricted biadditive pairings and supplies the continuous quotient actions used by invariant coefficients. Continuity of the inclusion into the ambient coefficient space follows from Mathlib's generic continuous_subtype_val, for additive monoids as well as groups.

For a normal subgroup H, the algebraic G ⧸ H-action on the fixed points of H is supplied by TauCeti/GroupTheory/GroupAction/FixedPoints.lean. If the coefficients are discrete and H is open, the quotient is discrete, so its action is continuous without a continuity assumption on the ambient action. For an arbitrary normal H, a continuous ambient action also descends to a continuous quotient action on discrete fixed points. The latter uses only the quotient topology, with no compatibility assumption on the topology and group structure of G.

The fixed points of open normal subgroups form a directed family, growing as the subgroup shrinks. Together with quotient-action continuity, this gives the coefficient system used in finite-quotient descriptions of continuous cohomology.

Pairings and quotient-action continuity have both additive-submonoid and additive-subgroup forms. The subgroup forms retain the coefficient groups' additive inverses and match the subgroup carrier used by group cohomology.

Main results

• Subgroup.continuous_fixedPointsAddSubmonoidPairing and Subgroup.continuous_fixedPointsPairing: restriction of a jointly continuous equivariant biadditive pairing remains jointly continuous.
• TauCeti.directed_fixedPoints_addSubmonoid and TauCeti.directed_fixedPoints_addSubgroup: fixed points of open normal subgroups form a directed family.
• TauCeti.continuousSMulQuotientFixedPointsAddSubmonoid and TauCeti.continuousSMulQuotientFixedPoints: quotient actions on discrete fixed points of open normal subgroups are continuous.
• TauCeti.continuousSMulQuotientFixedPointsAddSubmonoidOfContinuousSMul and TauCeti.continuousSMulQuotientFixedPointsOfContinuousSMul: quotient actions on discrete fixed points of arbitrary normal subgroups are continuous when the ambient action is continuous.
• TauCeti.continuous_fixedPoints_addSubgroup_subtype: the inclusion of the fixed-point additive subgroup into the ambient coefficient group is continuous.

theorem Subgroup.continuous_fixedPointsAddSubmonoidPairing {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [TopologicalSpace M] [DistribMulAction G M] {N : Type u_3} [AddMonoid N] [TopologicalSpace N] [DistribMulAction G N] {P : Type u_4} [AddCommMonoid P] [TopologicalSpace P] [DistribMulAction G P] (H : Subgroup G) (μ : M →+ N →+ P) (hequiv : ∀ (h : ↥H) (m : M) (n : N), (μ (↑h • m)) (↑h • n) = ↑h • (μ m) n) (hμ : Continuous fun (p : M × N) => (μ p.1) p.2) : Continuous fun (p : ↥(FixedPoints.addSubmonoid (↥H) M) × ↥(FixedPoints.addSubmonoid (↥H) N)) => ((H.fixedPointsAddSubmonoidPairing μ hequiv) p.1) p.2

Restricting a jointly continuous H-equivariant pairing to invariant coefficients remains jointly continuous.

theorem Subgroup.continuous_fixedPointsPairing {G : Type u_1} [Group G] {M : Type u_2} [AddGroup M] [TopologicalSpace M] [DistribMulAction G M] {N : Type u_3} [AddGroup N] [TopologicalSpace N] [DistribMulAction G N] {P : Type u_4} [AddCommGroup P] [TopologicalSpace P] [DistribMulAction G P] (H : Subgroup G) (μ : M →+ N →+ P) (hequiv : ∀ (h : ↥H) (m : M) (n : N), (μ (↑h • m)) (↑h • n) = ↑h • (μ m) n) (hμ : Continuous fun (p : M × N) => (μ p.1) p.2) : Continuous fun (p : ↥(FixedPoints.addSubgroup (↥H) M) × ↥(FixedPoints.addSubgroup (↥H) N)) => ((H.fixedPointsPairing μ hequiv) p.1) p.2

Restricting a jointly continuous H-equivariant pairing to the fixed-point additive subgroups remains jointly continuous.

theorem TauCeti.directed_fixedPoints_addSubmonoid (G : Type u_1) [Group G] [TopologicalSpace G] (M : Type u_2) [AddMonoid M] [DistribMulAction G M] : Directed (fun (x1 x2 : AddSubmonoid M) => x1 ≤ x2) fun (U : OpenNormalSubgroup G) => FixedPoints.addSubmonoid (↥↑U.toOpenSubgroup) M

The finite-level fixed-point additive submonoids form a directed family: the open normal subgroups are closed under intersection, and the fixed points grow as the subgroup shrinks.

instance TauCeti.continuousSMulQuotientFixedPointsAddSubmonoid (G : Type u_1) [Group G] [TopologicalSpace G] (M : Type u_2) [AddMonoid M] [DistribMulAction G M] [TopologicalSpace M] [DiscreteTopology M] [SeparatelyContinuousMul G] (U : OpenNormalSubgroup G) : ContinuousSMul (G ⧸ ↑U.toOpenSubgroup) ↥(FixedPoints.addSubmonoid (↥↑U.toOpenSubgroup) M)

For an open normal subgroup U, the action of the discrete quotient on the fixed-point additive submonoid is continuous.

theorem TauCeti.directed_fixedPoints_addSubgroup (G : Type u_1) [Group G] [TopologicalSpace G] (M : Type u_2) [AddGroup M] [DistribMulAction G M] : Directed (fun (x1 x2 : AddSubgroup M) => x1 ≤ x2) fun (U : OpenNormalSubgroup G) => FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) M

The finite-level invariants form a directed family: the open normal subgroups are closed under intersection, and the invariants grow as the subgroup shrinks. The corresponding cohomology tower is filtered for this reason.

instance TauCeti.continuousSMulQuotientFixedPoints (G : Type u_1) [Group G] [TopologicalSpace G] (M : Type u_2) [AddGroup M] [DistribMulAction G M] [SeparatelyContinuousMul G] [TopologicalSpace M] [DiscreteTopology M] (U : OpenNormalSubgroup G) : ContinuousSMul (G ⧸ ↑U.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) M)

For an open normal subgroup U the action of the discrete quotient group G ⧸ U on the invariant coefficients M ^ U is continuous.

theorem TauCeti.continuous_fixedPoints_addSubgroup_subtype (G : Type u_1) [Group G] (M : Type u_2) [AddGroup M] [DistribMulAction G M] [TopologicalSpace M] (H : Subgroup G) : Continuous ⇑(FixedPoints.addSubgroup (↥H) M).subtype

The inclusion M ^ H ↪ M of the invariants is continuous for the subspace topology.

instance TauCeti.continuousSMulQuotientFixedPointsAddSubmonoidOfContinuousSMul (G : Type u_1) [Group G] [TopologicalSpace G] (M : Type u_2) [AddMonoid M] [DistribMulAction G M] [TopologicalSpace M] [DiscreteTopology M] [ContinuousSMul G M] (H : Subgroup G) [H.Normal] : ContinuousSMul (G ⧸ H) ↥(FixedPoints.addSubmonoid (↥H) M)

For an arbitrary normal subgroup H, the action of G ⧸ H on the invariants M ^ H of a discrete module is continuous. Unlike TauCeti.continuousSMulQuotientFixedPoints, which reads the continuity off the discreteness of G ⧸ H for open H and needs no continuity of the G-action, this deduces it from continuity of the G-action: the invariants are discrete, so continuity is continuity in the group variable alone, and there it is the continuity of the G-action read through the quotient map. No compatibility of the topology of G with its group structure is needed, since G ⧸ H carries the quotient topology.

instance TauCeti.continuousSMulQuotientFixedPointsOfContinuousSMul (G : Type u_3) [Group G] [TopologicalSpace G] (M : Type u_4) [AddGroup M] [DistribMulAction G M] [TopologicalSpace M] [DiscreteTopology M] [ContinuousSMul G M] (H : Subgroup G) [H.Normal] : ContinuousSMul (G ⧸ H) ↥(FixedPoints.addSubgroup (↥H) M)

For an arbitrary normal subgroup H, the quotient acts continuously on the fixed-point additive subgroup of a discrete module with continuous G-action.