Subgroups #
This file defines multiplicative and additive subgroups as an extension of submonoids, in a bundled
form (unbundled subgroups are in Deprecated/Subgroups.lean
).
Special thanks goes to Amelia Livingston and Yury Kudryashov for their help and inspiration.
Main definitions #
Notation used here:
G N
areGroup
sA
is anAddGroup
H K
areSubgroup
s ofG
orAddSubgroup
s ofA
x
is an element of typeG
or typeA
f g : N →* G
are group homomorphismss k
are sets of elements of typeG
Definitions in the file:
Subgroup G
: the type of subgroups of a groupG
AddSubgroup A
: the type of subgroups of an additive groupA
Subgroup.subtype
: the natural group homomorphism from a subgroup of groupG
toG
Implementation notes #
Subgroup inclusion is denoted ≤
rather than ⊆
, although ∈
is defined as
membership of a subgroup's underlying set.
Tags #
subgroup, subgroups
SubgroupClass S G
states S
is a type of subsets s ⊆ G
that are subgroups of G
.
Instances
AddSubgroupClass S G
states S
is a type of subsets s ⊆ G
that are
additive subgroups of G
.
Instances
A subgroup of a group inherits an inverse.
Alias of InvMemClass.coe_inv
.
A subgroup of a group inherits a division
An additive subgroup of an AddGroup
inherits a subtraction.
An additive subgroup of an AddGroup
inherits an integer scaling.
A subgroup of a group inherits an integer power.
A subgroup of a group inherits a group structure.
Equations
- SubgroupClass.toGroup H = Function.Injective.group (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
An additive subgroup of an AddGroup
inherits an AddGroup
structure.
Equations
- AddSubgroupClass.toAddGroup H = Function.Injective.addGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
A subgroup of a CommGroup
is a CommGroup
.
Equations
- SubgroupClass.toCommGroup H = Function.Injective.commGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
An additive subgroup of an AddCommGroup
is an AddCommGroup
.
Equations
- AddSubgroupClass.toAddCommGroup H = Function.Injective.addCommGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
The natural group hom from a subgroup of group G
to G
.
Equations
- ↑H = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The natural group hom from an additive subgroup of AddGroup
G
to G
.
Equations
- ↑H = { toFun := Subtype.val, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The inclusion homomorphism from a subgroup H
contained in K
to K
.
Equations
- SubgroupClass.inclusion h = MonoidHom.mk' (fun (x : ↥H) => ⟨↑x, ⋯⟩) ⋯
Instances For
The inclusion homomorphism from an additive subgroup H
contained in K
to K
.
Equations
- AddSubgroupClass.inclusion h = AddMonoidHom.mk' (fun (x : ↥H) => ⟨↑x, ⋯⟩) ⋯
Instances For
A subgroup of a group G
is a subset containing 1, closed under multiplication
and closed under multiplicative inverse.
G
is closed under inverses
Instances For
An additive subgroup of an additive group G
is a subset containing 0, closed
under addition and additive inverse.
G
is closed under negation
Instances For
Equations
- AddSubgroup.instSetLike = { coe := fun (s : AddSubgroup G) => s.carrier, coe_injective' := ⋯ }
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Copy of an additive subgroup with a new carrier
equal to the old one.
Useful to fix definitional equalities
Equations
- K.copy s hs = { carrier := s, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
Instances For
Two AddSubgroup
s are equal if they have the same elements.
An AddSubgroup
contains the group's 0.
An AddSubgroup
is closed under addition.
An AddSubgroup
is closed under inverse.
An AddSubgroup
is closed under subtraction.
Construct a subgroup from a nonempty set that is closed under division.
Equations
- Subgroup.ofDiv s hsn hs = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
Instances For
Construct a subgroup from a nonempty set that is closed under subtraction
Equations
- AddSubgroup.ofSub s hsn hs = { carrier := s, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
Instances For
An AddSubgroup
of an AddGroup
inherits an addition.
Equations
- H.add = H.add
An AddSubgroup
of an AddGroup
inherits a zero.
Equations
- H.zero = H.zero
An AddSubgroup
of an AddGroup
inherits an inverse.
An AddSubgroup
of an AddGroup
inherits a subtraction.
An AddSubgroup
of an AddGroup
inherits a natural scaling.
An AddSubgroup
of an AddGroup
inherits an integer scaling.
A subgroup of a group inherits a group structure.
Equations
- H.toGroup = Function.Injective.group (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
An AddSubgroup
of an AddGroup
inherits an AddGroup
structure.
Equations
- H.toAddGroup = Function.Injective.addGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
A subgroup of a CommGroup
is a CommGroup
.
Equations
- H.toCommGroup = Function.Injective.commGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
An AddSubgroup
of an AddCommGroup
is an AddCommGroup
.
Equations
- H.toAddCommGroup = Function.Injective.addCommGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
The natural group hom from an AddSubgroup
of AddGroup
G
to G
.
Equations
- H.subtype = { toFun := Subtype.val, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The inclusion homomorphism from a subgroup H
contained in K
to K
.
Equations
- Subgroup.inclusion h = MonoidHom.mk' (fun (x : ↥H) => ⟨↑x, ⋯⟩) ⋯
Instances For
The inclusion homomorphism from an additive subgroup H
contained in K
to K
.
Equations
- AddSubgroup.inclusion h = AddMonoidHom.mk' (fun (x : ↥H) => ⟨↑x, ⋯⟩) ⋯
Instances For
An AddSubgroup is normal if whenever n ∈ H
, then g + n - g ∈ H
for every g : G
N
is closed under additive conjugation
Instances
Equations
- ⋯ = ⋯
Commutativity of a subgroup
- is_comm : Std.Commutative fun (x1 x2 : ↥H) => x1 * x2
*
is commutative onH
Instances
Commutativity of an additive subgroup
- is_comm : Std.Commutative fun (x1 x2 : ↥H) => x1 + x2
+
is commutative onH
Instances
A commutative subgroup is commutative.
Equations
A commutative subgroup is commutative.
Equations
A subgroup of a commutative group is commutative.
Equations
- ⋯ = ⋯