Subgroups #
This file defines multiplicative and additive subgroups as an extension of submonoids, in a bundled
form (unbundled subgroups are in Deprecated/Subgroups.lean
).
We prove subgroups of a group form a complete lattice, and results about images and preimages of subgroups under group homomorphisms. The bundled subgroups use bundled monoid homomorphisms.
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 N
areGroup
s -
A
is anAddGroup
-
H K
areSubgroup
s ofG
orAddSubgroup
s ofA
-
x
is an element of typeG
or typeA
-
f g : N →* G
are group homomorphisms -
s 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
-
CompleteLattice (Subgroup G)
: the subgroups ofG
form a complete lattice -
Subgroup.closure k
: the minimal subgroup that includes the setk
-
Subgroup.subtype
: the natural group homomorphism from a subgroup of groupG
toG
-
Subgroup.gi
:closure
forms a Galois insertion with the coercion to set -
Subgroup.comap H f
: the preimage of a subgroupH
along the group homomorphismf
is also a subgroup -
Subgroup.map f H
: the image of a subgroupH
along the group homomorphismf
is also a subgroup -
Subgroup.prod H K
: the product of subgroupsH
,K
of groupsG
,N
respectively,H × K
is a subgroup ofG × N
-
MonoidHom.range f
: the range of the group homomorphismf
is a subgroup -
MonoidHom.ker f
: the kernel of a group homomorphismf
is the subgroup of elementsx : G
such thatf x = 1
-
MonoidHom.eq_locus f g
: given group homomorphismsf
,g
, the elements ofG
such thatf x = g x
form a subgroup ofG
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
Equations
- (_ : motive x) = (_ : motive x)
Instances For
Alias of InvMemClass.coe_inv
.
An additive subgroup of an AddGroup
inherits a subtraction.
A subgroup of a group inherits a division
An additive subgroup of an AddGroup
inherits an integer scaling.
A subgroup of a group inherits an integer power.
An additive subgroup of an AddGroup
inherits an AddGroup
structure.
Equations
- One or more equations did not get rendered due to their size.
A subgroup of a group inherits a group structure.
Equations
- One or more equations did not get rendered due to their size.
An additive subgroup of an AddCommGroup
is an AddCommGroup
.
Equations
- One or more equations did not get rendered due to their size.
A subgroup of a CommGroup
is a CommGroup
.
Equations
- One or more equations did not get rendered due to their size.
An additive subgroup of an AddOrderedCommGroup
is an AddOrderedCommGroup
.
Equations
- One or more equations did not get rendered due to their size.
A subgroup of an OrderedCommGroup
is an OrderedCommGroup
.
Equations
- One or more equations did not get rendered due to their size.
An additive subgroup of a LinearOrderedAddCommGroup
is a
LinearOrderedAddCommGroup
.
Equations
- One or more equations did not get rendered due to their size.
A subgroup of a LinearOrderedCommGroup
is a LinearOrderedCommGroup
.
Equations
- One or more equations did not get rendered due to their size.
The natural group hom from an additive subgroup of AddGroup
G
to G
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The natural group hom from a subgroup of group G
to G
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inclusion homomorphism from an additive subgroup H
contained in K
to K
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inclusion homomorphism from a subgroup H
contained in K
to K
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A subgroup of a group G
is a subset containing 1, closed under multiplication
and closed under multiplicative inverse.
Instances For
An additive subgroup of an additive group G
is a subset containing 0, closed
under addition and additive inverse.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : AddSubgroupClass (AddSubgroup G) G) = (_ : AddSubgroupClass (AddSubgroup G) G)
Equations
- (_ : SubgroupClass (Subgroup G) G) = (_ : SubgroupClass (Subgroup G) G)
Conversion to/from Additive
/Multiplicative
#
Subgroups of a group G
are isomorphic to additive subgroups of Additive G
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Additive subgroup of an additive group Additive G
are isomorphic to subgroup of G
.
Equations
- AddSubgroup.toSubgroup' = OrderIso.symm Subgroup.toAddSubgroup
Instances For
Additive subgroups of an additive group A
are isomorphic to subgroups of Multiplicative A
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Subgroups of an additive group Multiplicative A
are isomorphic to additive subgroups of A
.
Equations
- Subgroup.toAddSubgroup' = OrderIso.symm AddSubgroup.toSubgroup
Instances For
Copy of an additive subgroup with a new carrier
equal to the old one.
Useful to fix definitional equalities
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- (_ : motive hsn) = (_ : motive hsn)
Instances For
Construct a subgroup from a nonempty set that is closed under subtraction
Equations
- One or more equations did not get rendered due to their size.
Instances For
Construct a subgroup from a nonempty set that is closed under division.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An AddSubgroup
of an AddGroup
inherits an addition.
Equations
- AddSubgroup.add H = AddSubmonoid.add H.toAddSubmonoid
A subgroup of a group inherits a multiplication.
Equations
- Subgroup.mul H = Submonoid.mul H.toSubmonoid
An AddSubgroup
of an AddGroup
inherits a zero.
Equations
- AddSubgroup.zero H = AddSubmonoid.zero H.toAddSubmonoid
A subgroup of a group inherits a 1.
Equations
- Subgroup.one H = Submonoid.one H.toSubmonoid
An AddSubgroup
of an AddGroup
inherits an inverse.
Equations
- AddSubgroup.neg H = { neg := fun (a : ↥H) => { val := -↑a, property := (_ : -↑a ∈ H) } }
An AddSubgroup
of an AddGroup
inherits a subtraction.
Equations
- AddSubgroup.sub H = { sub := fun (a b : ↥H) => { val := ↑a - ↑b, property := (_ : ↑a - ↑b ∈ H) } }
An AddSubgroup
of an AddGroup
inherits a natural scaling.
An AddSubgroup
of an AddGroup
inherits an integer scaling.
An AddSubgroup
of an AddGroup
inherits an AddGroup
structure.
Equations
- One or more equations did not get rendered due to their size.
An AddSubgroup
of an AddCommGroup
is an AddCommGroup
.
Equations
- One or more equations did not get rendered due to their size.
An AddSubgroup
of an AddOrderedCommGroup
is an AddOrderedCommGroup
.
Equations
- One or more equations did not get rendered due to their size.
A subgroup of an OrderedCommGroup
is an OrderedCommGroup
.
Equations
- One or more equations did not get rendered due to their size.
An AddSubgroup
of a LinearOrderedAddCommGroup
is a
LinearOrderedAddCommGroup
.
Equations
- One or more equations did not get rendered due to their size.
A subgroup of a LinearOrderedCommGroup
is a LinearOrderedCommGroup
.
Equations
- One or more equations did not get rendered due to their size.
The natural group hom from an AddSubgroup
of AddGroup
G
to G
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inclusion homomorphism from an additive subgroup H
contained in K
to K
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The AddSubgroup G
of the AddGroup G
.
The top additive subgroup is isomorphic to the additive group.
This is the additive group version of AddSubmonoid.topEquiv
.
Equations
- AddSubgroup.topEquiv = AddSubmonoid.topEquiv
Instances For
The top subgroup is isomorphic to the group.
This is the group version of Submonoid.topEquiv
.
Equations
- Subgroup.topEquiv = Submonoid.topEquiv
Instances For
The trivial AddSubgroup
{0}
of an AddGroup
G
.
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inf of two AddSubgroup
s is their intersection.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
The AddSubgroup
s of an AddGroup
form a complete lattice.
Equations
- One or more equations did not get rendered due to their size.
Subgroups of a group form a complete lattice.
Equations
- One or more equations did not get rendered due to their size.
Equations
- AddSubgroup.instUniqueAddSubgroup = { toInhabited := { default := ⊥ }, uniq := (_ : ∀ (a : AddSubgroup G), a = default) }
Equations
- (_ : Nontrivial (AddSubgroup G)) = (_ : Nontrivial (AddSubgroup G))
Equations
- (_ : Nontrivial (Subgroup G)) = (_ : Nontrivial (Subgroup G))
The AddSubgroup
generated by a set
Equations
- AddSubgroup.closure k = sInf {K : AddSubgroup G | k ⊆ ↑K}
Instances For
The AddSubgroup
generated by a set includes the set.
The subgroup generated by a set includes the set.
An additive subgroup K
includes closure k
if and only if it includes 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
.
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
.
Equations
- (_ : motive x) = (_ : motive x)
Instances For
A dependent version of AddSubgroup.closure_induction
.
A dependent version of Subgroup.closure_induction
.
An induction principle for additive closure membership, for predicates with two arguments.
An induction principle for closure membership for predicates with two arguments.
If all the elements of a set s
commute, then closure s
is an additive
commutative group.
Equations
- AddSubgroup.closureAddCommGroupOfComm hcomm = let src := AddSubgroup.toAddGroup (AddSubgroup.closure k); AddCommGroup.mk (_ : ∀ (x y : ↥(AddSubgroup.closure k)), x + y = y + x)
Instances For
If all the elements of a set s
commute, then closure s
is a commutative group.
Equations
- Subgroup.closureCommGroupOfComm hcomm = let src := Subgroup.toGroup (Subgroup.closure k); CommGroup.mk (_ : ∀ (x y : ↥(Subgroup.closure k)), x * y = y * x)
Instances For
closure
forms a Galois insertion with the coercion to set.
Equations
- One or more equations did not get rendered due to their size.
Instances For
closure
forms a Galois insertion with the coercion to set.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Additive closure of an additive subgroup K
equals K
Closure of a subgroup K
equals K
.
The AddSubgroup
generated by an element of an AddGroup
equals the set of
natural number multiples of the element.
The subgroup generated by an element of a group equals the set of integer number powers of the element.
Equations
- (_ : motive x) = (_ : motive x)
Instances For
The preimage of an AddSubgroup
along an AddMonoid
homomorphism
is an AddSubgroup
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The image of an AddSubgroup
along an AddMonoid
homomorphism
is an AddSubgroup
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
For any subgroups H
and K
, view H ⊓ K
as a subgroup of K
.
Equations
Instances For
For any subgroups H
and K
, view H ⊓ K
as a subgroup of K
.
Equations
- Subgroup.subgroupOf H K = Subgroup.comap (Subgroup.subtype K) H
Instances For
If H ≤ K
, then H
as a subgroup of K
is isomorphic to H
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If H ≤ K
, then H
as a subgroup of K
is isomorphic to H
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given AddSubgroup
s H
, K
of AddGroup
s A
, B
respectively, H × K
as an AddSubgroup
of A × B
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Product of additive subgroups is isomorphic to their product as additive groups
Equations
- One or more equations did not get rendered due to their size.
Instances For
A version of Set.pi
for AddSubmonoid
s. Given an index set I
and a family
of submodules s : Π i, AddSubmonoid f i
, pi I s
is the AddSubmonoid
of dependent functions
f : Π i, f i
such that f i
belongs to pi I s
whenever i ∈ I
. -/
Equations
- One or more equations did not get rendered due to their size.
Instances For
A version of Set.pi
for submonoids. Given an index set I
and a family of submodules
s : Π i, Submonoid f i
, pi I s
is the submonoid of dependent functions f : Π i, f i
such that
f i
belongs to Pi I s
whenever i ∈ I
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A version of Set.pi
for AddSubgroup
s. Given an index set I
and a family
of submodules s : Π i, AddSubgroup f i
, pi I s
is the AddSubgroup
of dependent functions
f : Π i, f i
such that f i
belongs to pi I s
whenever i ∈ I
. -/
Equations
- One or more equations did not get rendered due to their size.
Instances For
A version of Set.pi
for subgroups. Given an index set I
and a family of submodules
s : Π i, Subgroup f i
, pi I s
is the subgroup of dependent functions f : Π i, f i
such that
f i
belongs to pi I s
whenever i ∈ I
.
Equations
- One or more equations did not get rendered due to their size.
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
- (_ : AddSubgroup.Normal H) = (_ : AddSubgroup.Normal H)
Equations
- (_ : Subgroup.Normal H) = (_ : Subgroup.Normal H)
A subgroup is characteristic if it is fixed by all automorphisms.
Several equivalent conditions are provided by lemmas of the form Characteristic.iff...
- fixed : ∀ (ϕ : G ≃* G), Subgroup.comap (MulEquiv.toMonoidHom ϕ) H = H
H
is fixed by all automorphisms
Instances
Equations
- (_ : Subgroup.Normal H) = (_ : Subgroup.Normal H)
An AddSubgroup
is characteristic if it is fixed by all automorphisms.
Several equivalent conditions are provided by lemmas of the form Characteristic.iff...
- fixed : ∀ (ϕ : A ≃+ A), AddSubgroup.comap (AddEquiv.toAddMonoidHom ϕ) H = H
H
is fixed by all automorphisms
Instances
Equations
- (_ : AddSubgroup.Normal H) = (_ : AddSubgroup.Normal H)
Equations
- (_ : AddSubgroup.Characteristic ⊥) = (_ : AddSubgroup.Characteristic ⊥)
Equations
- (_ : Subgroup.Characteristic ⊥) = (_ : Subgroup.Characteristic ⊥)
Equations
- (_ : AddSubgroup.Characteristic ⊤) = (_ : AddSubgroup.Characteristic ⊤)
Equations
- (_ : Subgroup.Characteristic ⊤) = (_ : Subgroup.Characteristic ⊤)
The center of an additive group G
is the set of elements that commute with
everything in G
Equations
- One or more equations did not get rendered due to their size.
Instances For
The center of a group G
is the set of elements that commute with everything in G
Equations
- One or more equations did not get rendered due to their size.
Instances For
For a group with zero, the center of the units is the same as the units of the center.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Subgroup.decidableMemCenter z = decidable_of_iff' (∀ (g : G), g * z = z * g) (_ : z ∈ Subgroup.center G ↔ ∀ (g : G), g * z = z * g)
Equations
- (_ : AddSubgroup.Characteristic (AddSubgroup.center G)) = (_ : AddSubgroup.Characteristic (AddSubgroup.center G))
Equations
- (_ : Subgroup.Characteristic (Subgroup.center G)) = (_ : Subgroup.Characteristic (Subgroup.center G))
A group is commutative if the center is the whole group
Equations
- Group.commGroupOfCenterEqTop h = let src := inst; CommGroup.mk (_ : let src := inst; ∀ (x y : G), x * y = y * x)
Instances For
The normalizer
of H
is the largest subgroup of G
inside which H
is normal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The normalizer
of H
is the largest subgroup of G
inside which H
is normal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The setNormalizer
of S
is the subgroup of G
whose elements satisfy
g+S-g=S
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The setNormalizer
of S
is the subgroup of G
whose elements satisfy g*S*g⁻¹=S
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- (_ : AddSubgroup.Normal (AddSubgroup.addSubgroupOf H (AddSubgroup.normalizer H))) = (_ : AddSubgroup.Normal (AddSubgroup.addSubgroupOf H (AddSubgroup.normalizer H)))
Equations
- (_ : Subgroup.Normal (Subgroup.subgroupOf H (Subgroup.normalizer H))) = (_ : Subgroup.Normal (Subgroup.subgroupOf H (Subgroup.normalizer H)))
The preimage of the normalizer is contained in the normalizer of the preimage.
The image of the normalizer is contained in the normalizer of the image.
The image of the normalizer is contained in the normalizer of the image.
Every proper subgroup H
of G
is a proper normal subgroup of the normalizer of H
in G
.
Equations
- NormalizerCondition G = ∀ H < ⊤, H < Subgroup.normalizer H
Instances For
Alternative phrasing of the normalizer condition: Only the full group is self-normalizing. This may be easier to work with, as it avoids inequalities and negations.
In a group that satisfies the normalizer condition, every maximal subgroup is normal
The centralizer
of H
is the additive subgroup of g : G
commuting with every h : H
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The centralizer
of H
is the subgroup of g : G
commuting with every h : H
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- (_ : AddSubgroup.Characteristic (AddSubgroup.centralizer ↑H)) = (_ : AddSubgroup.Characteristic (AddSubgroup.centralizer ↑H))
Equations
- (_ : Subgroup.Characteristic (Subgroup.centralizer ↑H)) = (_ : Subgroup.Characteristic (Subgroup.centralizer ↑H))
Commutativity of a subgroup
- is_comm : Std.Commutative fun (x x_1 : ↥H) => x * x_1
*
is commutative onH
Instances
Commutativity of an additive subgroup
- is_comm : Std.Commutative fun (x x_1 : ↥H) => x + x_1
+
is commutative onH
Instances
A commutative subgroup is commutative.
Equations
- AddSubgroup.IsCommutative.addCommGroup H = let src := AddSubgroup.toAddGroup H; AddCommGroup.mk (_ : ∀ (a b : ↥H), a + b = b + a)
A commutative subgroup is commutative.
Equations
- Subgroup.IsCommutative.commGroup H = let src := Subgroup.toGroup H; CommGroup.mk (_ : ∀ (a b : ↥H), a * b = b * a)
Equations
- (_ : Subgroup.IsCommutative (Subgroup.center G)) = (_ : Subgroup.IsCommutative (Subgroup.center G))
Equations
- (_ : AddSubgroup.IsCommutative (AddSubgroup.map f H)) = (_ : AddSubgroup.IsCommutative (AddSubgroup.map f H))
Equations
- (_ : Subgroup.IsCommutative (Subgroup.map f H)) = (_ : Subgroup.IsCommutative (Subgroup.map f H))
Equations
- (_ : AddSubgroup.IsCommutative (AddSubgroup.addSubgroupOf H K)) = (_ : AddSubgroup.IsCommutative (AddSubgroup.comap (AddSubgroup.subtype K) H))
Equations
- (_ : Subgroup.IsCommutative (Subgroup.subgroupOf H K)) = (_ : Subgroup.IsCommutative (Subgroup.comap (Subgroup.subtype K) H))
Given a set s
, conjugatesOfSet s
is the set of all conjugates of
the elements of s
.
Equations
- Group.conjugatesOfSet s = ⋃ a ∈ s, conjugatesOf a
Instances For
The set of conjugates of s
is closed under conjugation.
The normal closure of a set s
is the subgroup closure of all the conjugates of
elements of s
. It is the smallest normal subgroup containing s
.
Equations
Instances For
The normal closure of s
is a normal subgroup.
Equations
- (_ : Subgroup.Normal (Subgroup.normalClosure s)) = (_ : Subgroup.Normal (Subgroup.normalClosure s))
The normal closure of s
is the smallest normal subgroup containing s
.
The normal core of a subgroup H
is the largest normal subgroup of G
contained in H
,
as shown by Subgroup.normalCore_eq_iSup
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- (_ : Subgroup.Normal (Subgroup.normalCore H)) = (_ : Subgroup.Normal (Subgroup.normalCore H))
The range of an AddMonoidHom
from an AddGroup
is an AddSubgroup
.
Equations
- AddMonoidHom.range f = AddSubgroup.copy (AddSubgroup.map f ⊤) (Set.range ⇑f) (_ : Set.range ⇑f = ⇑f '' Set.univ)
Instances For
The range of a monoid homomorphism from a group is a subgroup.
Equations
- MonoidHom.range f = Subgroup.copy (Subgroup.map f ⊤) (Set.range ⇑f) (_ : Set.range ⇑f = ⇑f '' Set.univ)
Instances For
The canonical surjective AddGroup
homomorphism G →+ f(G)
induced by a group
homomorphism G →+ N
.
Equations
- AddMonoidHom.rangeRestrict f = AddMonoidHom.codRestrict f (AddMonoidHom.range f) (_ : ∀ (x : G), ∃ (y : G), f y = f x)
Instances For
The canonical surjective group homomorphism G →* f(G)
induced by a group
homomorphism G →* N
.
Equations
- MonoidHom.rangeRestrict f = MonoidHom.codRestrict f (MonoidHom.range f) (_ : ∀ (x : G), ∃ (y : G), f y = f x)
Instances For
Equations
- (_ : motive x) = (_ : motive x)
Instances For
The range of a surjective AddMonoid
homomorphism is the whole of the codomain.
The range of a surjective monoid homomorphism is the whole of the codomain.
Computable alternative to AddMonoidHom.ofInjective
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Computable alternative to MonoidHom.ofInjective
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The range of an injective additive group homomorphism is isomorphic to its domain.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The range of an injective group homomorphism is isomorphic to its domain.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The additive kernel of an AddMonoid
homomorphism is the AddSubgroup
of elements
such that f x = 0
Equations
- AddMonoidHom.ker f = let src := AddMonoidHom.mker f; { toAddSubmonoid := src, neg_mem' := (_ : ∀ {x : G}, f x = 0 → f (-x) = 0) }
Instances For
The multiplicative kernel of a monoid homomorphism is the subgroup of elements x : G
such that
f x = 1
Equations
- MonoidHom.ker f = let src := MonoidHom.mker f; { toSubmonoid := src, inv_mem' := (_ : ∀ {x : G}, f x = 1 → f x⁻¹ = 1) }
Instances For
Equations
- AddMonoidHom.decidableMemKer f x = decidable_of_iff (f x = 0) (_ : x ∈ AddMonoidHom.ker f ↔ f x = 0)
Equations
- MonoidHom.decidableMemKer f x = decidable_of_iff (f x = 1) (_ : x ∈ MonoidHom.ker f ↔ f x = 1)
Equations
- (_ : AddSubgroup.Normal (AddMonoidHom.ker f)) = (_ : AddSubgroup.Normal (AddMonoidHom.ker f))
Equations
- (_ : Subgroup.Normal (MonoidHom.ker f)) = (_ : Subgroup.Normal (MonoidHom.ker f))
The additive subgroup of elements x : G
such that f x = g x
Equations
- AddMonoidHom.eqLocus f g = let src := AddMonoidHom.eqLocusM f g; { toAddSubmonoid := src, neg_mem' := (_ : ∀ {x : G}, f x = g x → f (-x) = g (-x)) }
Instances For
The subgroup of elements x : G
such that f x = g x
Equations
- MonoidHom.eqLocus f g = let src := MonoidHom.eqLocusM f g; { toSubmonoid := src, inv_mem' := (_ : ∀ {x : G}, f x = g x → f x⁻¹ = g x⁻¹) }
Instances For
The image under an AddMonoid
hom of the AddSubgroup
generated by a set equals
the AddSubgroup
generated by the image of the set.
The image under a monoid homomorphism of the subgroup generated by a set equals the subgroup generated by the image of the set.
Given f(A) = f(B)
, ker f ≤ A
, and ker f ≤ B
, deduce that A = B
.
Given f(A) = f(B)
, ker f ≤ A
, and ker f ≤ B
, deduce that A = B
.
An additive subgroup is isomorphic to its image under an injective function. If you
have an isomorphism, use AddEquiv.addSubgroupMap
for better definitional equalities.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A subgroup is isomorphic to its image under an injective function. If you have an isomorphism,
use MulEquiv.subgroupMap
for better definitional equalities.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The preimage of the normalizer is equal to the normalizer of the preimage of a surjective function.
The preimage of the normalizer is equal to the normalizer of the preimage of a surjective function.
The image of the normalizer is equal to the normalizer of the image of an isomorphism.
The image of the normalizer is equal to the normalizer of the image of a bijective function.
The image of the normalizer is equal to the normalizer of the image of a bijective function.
Auxiliary definition used to define liftOfRightInverse
Equations
- One or more equations did not get rendered due to their size.
Instances For
Auxiliary definition used to define liftOfRightInverse
Equations
- One or more equations did not get rendered due to their size.
Instances For
liftOfRightInverse f f_inv hf g hg
is the unique additive group homomorphism φ
- such that
φ.comp f = g
(AddMonoidHom.liftOfRightInverse_comp
), - where
f : G₁ →+ G₂
has a RightInversef_inv
(hf
), - and
g : G₂ →+ G₃
satisfieshg : f.ker ≤ g.ker
. SeeAddMonoidHom.eq_liftOfRightInverse
for the uniqueness lemma.
G₁.
| \
f | \ g
| \
v \⌟
G₂----> G₃
∃!φ
Equations
- One or more equations did not get rendered due to their size.
Instances For
liftOfRightInverse f hf g hg
is the unique group homomorphism φ
- such that
φ.comp f = g
(MonoidHom.liftOfRightInverse_comp
), - where
f : G₁ →+* G₂
has a RightInversef_inv
(hf
), - and
g : G₂ →+* G₃
satisfieshg : f.ker ≤ g.ker
.
See MonoidHom.eq_liftOfRightInverse
for the uniqueness lemma.
G₁.
| \
f | \ g
| \
v \⌟
G₂----> G₃
∃!φ
Equations
- One or more equations did not get rendered due to their size.
Instances For
A non-computable version of AddMonoidHom.liftOfRightInverse
for when no
computable right inverse is available.
Equations
- AddMonoidHom.liftOfSurjective f hf = AddMonoidHom.liftOfRightInverse f (Function.surjInv hf) (_ : Function.RightInverse (Function.surjInv hf) ⇑f)
Instances For
A non-computable version of MonoidHom.liftOfRightInverse
for when no computable right
inverse is available, that uses Function.surjInv
.
Equations
- MonoidHom.liftOfSurjective f hf = MonoidHom.liftOfRightInverse f (Function.surjInv hf) (_ : Function.RightInverse (Function.surjInv hf) ⇑f)
Instances For
Equations
- (_ : AddSubgroup.Normal (AddSubgroup.comap f H)) = (_ : AddSubgroup.Normal (AddSubgroup.comap f H))
Equations
- (_ : Subgroup.Normal (Subgroup.comap f H)) = (_ : Subgroup.Normal (Subgroup.comap f H))
Equations
- (_ : AddSubgroup.Normal (AddSubgroup.addSubgroupOf N H)) = (_ : AddSubgroup.Normal (AddSubgroup.comap (AddSubgroup.subtype H) N))
Equations
- (_ : Subgroup.Normal (Subgroup.subgroupOf N H)) = (_ : Subgroup.Normal (Subgroup.comap (Subgroup.subtype H) N))
the AddMonoidHom
from the preimage of an
additive subgroup to itself.
Equations
- AddMonoidHom.addSubgroupComap f H' = AddMonoidHom.addSubmonoidComap f H'.toAddSubmonoid
Instances For
The MonoidHom
from the preimage of a subgroup to itself.
Equations
- MonoidHom.subgroupComap f H' = MonoidHom.submonoidComap f H'.toSubmonoid
Instances For
the AddMonoidHom
from an additive subgroup to its image
Equations
- AddMonoidHom.addSubgroupMap f H = AddMonoidHom.addSubmonoidMap f H.toAddSubmonoid
Instances For
The MonoidHom
from a subgroup to its image.
Equations
- MonoidHom.subgroupMap f H = MonoidHom.submonoidMap f H.toSubmonoid
Instances For
Makes the identity additive isomorphism from a proof two subgroups of an additive group are equal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An additive subgroup is isomorphic to its image under an isomorphism. If you only
have an injective map, use AddSubgroup.equiv_map_of_injective
.
Equations
- AddEquiv.addSubgroupMap e H = AddEquiv.addSubmonoidMap e H.toAddSubmonoid
Instances For
A subgroup is isomorphic to its image under an isomorphism. If you only have an injective map,
use Subgroup.equiv_map_of_injective
.
Equations
- MulEquiv.subgroupMap e H = MulEquiv.submonoidMap e H.toSubmonoid
Instances For
Equations
- (_ : IsModularLattice (AddSubgroup C)) = (_ : IsModularLattice (AddSubgroup C))
Equations
- (_ : IsModularLattice (Subgroup C)) = (_ : IsModularLattice (Subgroup C))
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Subgroup.Normal (Subgroup.subgroupOf (Subgroup.prod H₁ H₂) (Subgroup.prod K₁ K₂))) = (_ : Subgroup.Normal (Subgroup.subgroupOf (Subgroup.prod H₁ H₂) (Subgroup.prod K₁ K₂)))
Equations
- (_ : AddSubgroup.Normal (AddSubgroup.prod H K)) = (_ : AddSubgroup.Normal (AddSubgroup.prod H K))
Equations
- (_ : Subgroup.Normal (Subgroup.prod H K)) = (_ : Subgroup.Normal (Subgroup.prod H K))
Equations
- (_ : AddSubgroup.Normal (H ⊓ K)) = (_ : AddSubgroup.Normal (H ⊓ K))
Equations
- (_ : Subgroup.Normal (H ⊓ K)) = (_ : Subgroup.Normal (H ⊓ K))
Elements of disjoint, normal subgroups commute.
Elements of disjoint, normal subgroups commute.
The conjugacy classes that are not trivial.
Equations
- ConjClasses.noncenter G = {x : ConjClasses G | Set.Nontrivial (ConjClasses.carrier x)}