Complements #
In this file we define the complement of a subgroup.
Main definitions #
IsComplement S T
whereS
andT
are subsets ofG
states that everyg : G
can be written uniquely as a products * t
fors ∈ S
,t ∈ T
.leftTransversals T
whereT
is a subset ofG
is the set of all left-complements ofT
, i.e. the set of allS : Set G
that contain exactly one element of each left coset ofT
.rightTransversals S
whereS
is a subset ofG
is the set of all right-complements ofS
, i.e. the set of allT : Set G
that contain exactly one element of each right coset ofS
.transferTransversal H g
is a specificleftTransversal
ofH
that is used in the computation of the transfer homomorphism evaluated at an elementg : G
.
Main results #
isComplement'_of_coprime
: Subgroups of coprime order are complements.
H
and K
are complements if (+) : H × K → G
is a bijection
Instances For
Instances For
Instances For
Instances For
Instances For
The equivalence G ≃ S × T
, such that the inverse is (*) : S × T → G
Instances For
A left transversal is in bijection with left cosets.
Instances For
A left transversal is in bijection with left cosets.
Instances For
A left transversal can be viewed as a function mapping each element of the group to the chosen representative from that left coset.
Instances For
A left transversal can be viewed as a function mapping each element of the group to the chosen representative from that left coset.
Instances For
A right transversal is in bijection with right cosets.
Instances For
A right transversal is in bijection with right cosets.
Instances For
A right transversal can be viewed as a function mapping each element of the group to the chosen representative from that right coset.
Instances For
A right transversal can be viewed as a function mapping each element of the group to the chosen representative from that right coset.
Instances For
Partition G ⧸ H
into orbits of the action of g : G
.
Instances For
The transfer transversal as a function. Given a ⟨g⟩
-orbit q₀, g • q₀, ..., g ^ (m - 1) • q₀
in G ⧸ H
, an element g ^ k • q₀
is mapped to g ^ k • g₀
for a fixed choice of
representative g₀
of q₀
.
Instances For
The transfer transversal. Contains elements of the form g ^ k • g₀
for fixed choices
of representatives g₀
of fixed choices of representatives q₀
of ⟨g⟩
-orbits in G ⧸ H
.