Lattice structure of subgroups #
We prove subgroups of a group form a complete lattice.
There are also theorems about the subgroups generated by an element or a subset of a group, defined both inductively and as the infimum of the set of subgroups containing a given element/subset.
Special thanks goes to Amelia Livingston and Yury Kudryashov for their help and inspiration.
Main definitions #
Notation used here:
G
is aGroup
k
is a set of elements of typeG
Definitions in the file:
CompleteLattice (Subgroup G)
: the subgroups ofG
form a complete latticeSubgroup.closure k
: the minimal subgroup that includes the setk
Subgroup.gi
:closure
forms a Galois insertion with the coercion to set
Implementation notes #
Subgroup inclusion is denoted ≤
rather than ⊆
, although ∈
is defined as
membership of a subgroup's underlying set.
Tags #
subgroup, subgroups
Conversion to/from Additive
/Multiplicative
#
Additive subgroup of an additive group Additive G
are isomorphic to subgroup of G
.
Equations
Instances For
Additive subgroups of an additive group A
are isomorphic to subgroups of Multiplicative A
.
Equations
Instances For
Subgroups of an additive group Multiplicative A
are isomorphic to additive subgroups of A
.
Equations
Instances For
The AddSubgroup G
of the AddGroup G
.
Equations
The top subgroup is isomorphic to the group.
This is the group version of Submonoid.topEquiv
.
Equations
Instances For
The top additive subgroup is isomorphic to the additive group.
This is the additive group version of AddSubmonoid.topEquiv
.
Equations
Instances For
The trivial AddSubgroup
{0}
of an AddGroup
G
.
Equations
Equations
A subgroup is either the trivial subgroup or nontrivial.
A subgroup is either the trivial subgroup or nontrivial.
A subgroup is either the trivial subgroup or contains a nonzero element.
The inf of two AddSubgroup
s is their intersection.
Equations
Subgroups of a group form a complete lattice.
Equations
The AddSubgroup
s of an AddGroup
form a complete lattice.
Equations
Equations
Equations
The AddSubgroup
generated by a set includes the set.
Alias of AddSubgroup.notMem_of_notMem_closure
.
Alias of Subgroup.notMem_of_notMem_closure
.
An induction principle for closure membership. If p
holds for 1
and all elements of k
, and
is preserved under multiplication and inverse, then p
holds for all elements of the closure
of k
.
See also Subgroup.closure_induction_left
and Subgroup.closure_induction_right
for versions that
only require showing p
is preserved by multiplication by elements in k
.
An induction principle for additive closure membership. If p
holds for 0
and all elements of k
, and is preserved under addition and inverses, then p
holds for all elements of the additive closure of k
.
See also AddSubgroup.closure_induction_left
and AddSubgroup.closure_induction_left
for
versions that only require showing p
is preserved by addition by elements in k
.
An induction principle for closure membership for predicates with two arguments.
An induction principle for additive closure membership, for predicates with two arguments.
Additive closure of an additive subgroup K
equals K