Pointwise instances on Subgroup
and AddSubgroup
s #
This file provides the actions
Subgroup.pointwiseMulAction
AddSubgroup.pointwiseMulAction
which matches the action of Set.mulActionSet
.
These actions are available in the Pointwise
locale.
Implementation notes #
The pointwise section of this file is almost identical to
the file Mathlib.Algebra.Group.Submonoid.Pointwise
.
Where possible, try to keep them in sync.
For subgroups generated by a single element, see the simpler zpow_induction_left
.
For additive subgroups generated by a single element, see the simpler
zsmul_induction_left
.
For subgroups generated by a single element, see the simpler zpow_induction_right
.
For additive subgroups generated by a single element, see the simpler
zsmul_induction_right
.
An induction principle for closure membership. If p
holds for 1
and all elements of
k
and their inverse, and is preserved under multiplication, then p
holds for all elements of
the closure of k
.
An induction principle for additive closure membership. If p
holds for 0
and all
elements of k
and their negation, and is preserved under addition, then p
holds for all
elements of the additive closure of k
.
An induction principle for elements of ⨆ i, S i
.
If C
holds for 1
and all elements of S i
for all i
, and is preserved under multiplication,
then it holds for all elements of the supremum of S
.
An induction principle for elements of ⨆ i, S i
.
If C
holds for 0
and all elements of S i
for all i
, and is preserved under addition,
then it holds for all elements of the supremum of S
.
A dependent version of Subgroup.iSup_induction
.
A dependent version of AddSubgroup.iSup_induction
.
The carrier of H ⊔ N
is just ↑H * ↑N
(pointwise set product)
when H
is a subgroup of the normalizer of N
in G
.
The carrier of H ⊔ N
is just ↑H + ↑N
(pointwise set addition)
when H
is a subgroup of the normalizer of N
in G
.
The carrier of N ⊔ H
is just ↑N * ↑H
(pointwise set product) when
H
is a subgroup of the normalizer of N
in G
.
The carrier of N ⊔ H
is just ↑N + ↑H
(pointwise set addition)
when H
is a subgroup of the normalizer of N
in G
.
The carrier of H ⊔ N
is just ↑H + ↑N
(pointwise set addition)
when N
is normal.
The carrier of N ⊔ H
is just ↑N + ↑H
(pointwise set addition)
when N
is normal.
Pointwise action #
The action on a subgroup corresponding to applying the action to every element.
This is available as an instance in the Pointwise
locale.
Equations
- Subgroup.pointwiseMulAction = { smul := fun (a : α) (S : Subgroup G) => Subgroup.map ((MulDistribMulAction.toMonoidEnd α G) a) S, one_smul := ⋯, mul_smul := ⋯ }
Instances For
Applying a MulDistribMulAction
results in an isomorphic subgroup
Equations
- Subgroup.equivSMul a H = (MulDistribMulAction.toMulEquiv G a).subgroupMap H
Instances For
Alias of Subgroup.Normal.conj_smul_eq_self
.