The additive fixed points of a subgroup #
Mathlib's Mathlib/GroupTheory/GroupAction/SubMulAction.lean and
Mathlib/GroupTheory/GroupAction/OfQuotient.lean put a MulAction G (fixedPoints H α) and a
MulAction (G ⧸ H) (fixedPoints H α) on the fixed points of a normal subgroup H, and refine the
latter to a MulDistribMulAction on FixedPoints.subgroup H α. This file is the additive
counterpart of that refinement: for a distributive action on an additive monoid it upgrades both of
Mathlib's MulActions to DistribMulActions on FixedPoints.addSubmonoid H M, records the
coercion lemmas that characterise the two actions on the AddSubgroup carrier, computes the fixed
points of ⊥ and ⊤, and supplies the inclusion and map API for additive fixed points.
Nothing here is specific to topology or cohomology. The topology of these actions and pairings is
developed in TauCeti/Topology/Algebra/GroupAction/FixedPoints.lean.
Main results #
TauCeti.fixedPoints_botandTauCeti.fixedPoints_top: the fixed points of the trivial subgroup are everything and those of⊤are those of the whole group, with theirAddSubgroupcorollaries and the trivial-action and subsingleton-coefficient edge cases.TauCeti.distribMulActionFixedPointsAddSubmonoidandTauCeti.distribMulActionQuotientFixedPointsAddSubmonoid: the distributiveG- andG ⧸ H-actions on the fixed points of a normalH, with theirAddSubgroupforms and the coercion lemmasTauCeti.coe_smul_fixedPoints_addSubgroupandTauCeti.coe_quotient_smul_fixedPoints_addSubgroup; a trivialG-action onMgives a trivialG ⧸ H-action onM ^ H(TauCeti.quotient_smul_fixedPoints_addSubgroup_eq_of_smul_eq).TauCeti.fixedPointsInclusion,TauCeti.fixedPointsDistribMulActionInclusion, andTauCeti.fixedPointsDistribMulActionSubtype: the additive and equivariant inclusions between fixed points and into the ambient additive monoid, with their functoriality laws.TauCeti.fixedPointsMapandTauCeti.fixedPointsQuotientMap: functoriality of fixed points in the additive monoid, additively and as a quotient-equivariant map.Subgroup.fixedPointsAddSubmonoidPairingandSubgroup.fixedPointsPairing: the pairings induced on the fixed points of an equivariant biadditive pairing, with a commutative target, for additive monoids and additive groups respectively.
The trivial subgroup fixes every point.
The points fixed by the subgroup ⊤ are the points fixed by the whole group.
M ^ H is stable under the G-action for normal H, and the action is distributive: this
adds smul_zero and smul_add to Mathlib's MulAction G (fixedPoints H M), which has no
multiplicative analogue upstream.
Equations
- TauCeti.distribMulActionFixedPointsAddSubmonoid = { toMulAction := inferInstance, smul_zero := ⋯, smul_add := ⋯ }
H acts trivially on M ^ H, so the distributive G-action descends to G ⧸ H: this is the
additive counterpart of Mathlib's MulDistribMulAction (G ⧸ H) (FixedPoints.submonoid H α).
Equations
- TauCeti.distribMulActionQuotientFixedPointsAddSubmonoid = { toMulAction := inferInstance, smul_zero := ⋯, smul_add := ⋯ }
The G-action on the fixed-point additive submonoid is the one on M.
The G ⧸ H-action on the fixed-point additive submonoid is induced by the G-action.
The trivial subgroup fixes everything.
The invariants of the whole group, reached through the subgroup ⊤.
If the G-action on M is trivial, every element is fixed by every subgroup.
The fixed-point subgroup of a subsingleton additive group is zero.
The distributive G-action on the invariants of a normal subgroup, on the AddSubgroup
carrier.
Equations
- TauCeti.distribMulActionFixedPointsAddSubgroup = { smul := TauCeti.distribMulActionFixedPointsAddSubgroup._aux_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }
The distributive G ⧸ H-action on the invariants of a normal subgroup H, on the
AddSubgroup carrier.
Equations
- TauCeti.distribMulActionQuotientFixedPointsAddSubgroup = { smul := TauCeti.distribMulActionQuotientFixedPointsAddSubgroup._aux_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }
The G-action on M ^ H is the one on M. Mathlib's coe_smul_fixedPoints_of_normal is
stated for the carrier ↥(fixedPoints H M) and so does not fire on FixedPoints.addSubgroup.
The G ⧸ H-action on M ^ H is the G-action through the quotient map. Mathlib's
coe_quotient_smul_fixedPoints is stated for the carrier ↥(fixedPoints H M) and so does not fire
on FixedPoints.addSubgroup.
If G acts trivially on M, then G ⧸ H acts trivially on M ^ H.
For K ≤ H, the fixed points of H include into the fixed points of K. This is stated on
additive submonoids so that it applies before additive inverses are available.
Equations
Instances For
The fixed-point inclusion does not move an element of M.
The fixed-point inclusions are injective.
The fixed-point inclusion is G-equivariant.
For normal H and K, fixed-point inclusion is a G-equivariant additive map.
Equations
- TauCeti.fixedPointsDistribMulActionInclusion h = { toFun := (↑(TauCeti.fixedPointsInclusion h)).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The G-equivariant inclusion of the fixed points of a normal subgroup into M.
Equations
- TauCeti.fixedPointsDistribMulActionSubtype H = { toFun := (↑(FixedPoints.addSubmonoid (↥H) M).subtype).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The equivariant fixed-point inclusion does not move an element of M.
The equivariant fixed-point subtype map does not move an element of M.
The fixed-point inclusion is equivariant along Mathlib's canonical quotient homomorphism
G ⧸ K →* G ⧸ H.
The fixed-point inclusions are functorial in the subgroup: the identity inclusion is the identity.
The fixed-point inclusions are functorial in the subgroup: they compose.
A G-equivariant additive map restricts to the fixed points of any subgroup.
Equations
- TauCeti.fixedPointsMap f H = { toFun := fun (m : ↥(FixedPoints.addSubmonoid (↥H) M)) => ⟨f ↑m, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The restricted map is the original map on underlying elements.
Restriction to fixed points preserves the identity map.
Restriction to fixed points preserves composition.
Restriction to the fixed points is equivariant for the G-actions of a normal subgroup.
Restriction to the fixed points is equivariant for the G ⧸ H-actions.
For normal H, restriction to the fixed points is a G ⧸ H-equivariant additive map.
Equations
- TauCeti.fixedPointsQuotientMap f H = { toFun := (↑(TauCeti.fixedPointsMap f H)).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The quotient-equivariant map is the original map on underlying elements.
Quotient-equivariant restriction to fixed points preserves the identity map.
Quotient-equivariant restriction to fixed points preserves composition.
Restriction to the fixed points commutes with the fixed-point inclusions.
An H-equivariant biadditive pairing of additive monoids restricts to the fixed points of
H.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The pairing on fixed points is the original pairing on underlying elements.
For a normal subgroup, the pairing on fixed points is equivariant for the quotient action.
An H-equivariant biadditive pairing restricts to the fixed-point additive subgroups.
The subgroup carrier retains the additive inverses of the coefficients.
Equations
- H.fixedPointsPairing μ hequiv = H.fixedPointsAddSubmonoidPairing μ hequiv
Instances For
The pairing on fixed-point additive subgroups preserves the underlying coefficients.
For a normal subgroup, the pairing on fixed-point additive subgroups is quotient-equivariant.