Subgroups #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 Naregroups -
Ais anadd_group -
H Karesubgroups ofGoradd_subgroups ofA -
xis an element of typeGor typeA -
f g : N →* Gare group homomorphisms -
s kare sets of elements of typeG
Definitions in the file:
-
subgroup G: the type of subgroups of a groupG -
add_subgroup A: the type of subgroups of an additive groupA -
complete_lattice (subgroup G): the subgroups ofGform a complete lattice -
subgroup.closure k: the minimal subgroup that includes the setk -
subgroup.subtype: the natural group homomorphism from a subgroup of groupGtoG -
subgroup.gi:closureforms a Galois insertion with the coercion to set -
subgroup.comap H f: the preimage of a subgroupHalong the group homomorphismfis also a subgroup -
subgroup.map f H: the image of a subgroupHalong the group homomorphismfis also a subgroup -
subgroup.prod H K: the product of subgroupsH,Kof groupsG,Nrespectively,H × Kis a subgroup ofG × N -
monoid_hom.range f: the range of the group homomorphismfis a subgroup -
monoid_hom.ker f: the kernel of a group homomorphismfis the subgroup of elementsx : Gsuch thatf x = 1 -
monoid_hom.eq_locus f g: given group homomorphismsf,g, the elements ofGsuch thatf x = g xform 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
@[class]
inv_mem_class S G states S is a type of subsets s ⊆ G closed under inverses.
Instances of this typeclass
@[class]
neg_mem_class S G states S is a type of subsets s ⊆ G closed under negation.
Instances of this typeclass
@[class]
- to_submonoid_class : submonoid_class S G
- to_inv_mem_class : inv_mem_class S G
subgroup_class S G states S is a type of subsets s ⊆ G that are subgroups of G.
Instances of this typeclass
@[class]
- to_add_submonoid_class : add_submonoid_class S G
- to_neg_mem_class : neg_mem_class S G
add_subgroup_class S G states S is a type of subsets s ⊆ G that are
additive subgroups of G.
@[simp]
theorem
neg_mem_iff
{S : Type u_1}
{G : Type u_2}
[has_involutive_neg G]
[set_like S G]
[neg_mem_class S G]
{H : S}
{x : G} :
@[simp]
theorem
inv_mem_iff
{S : Type u_1}
{G : Type u_2}
[has_involutive_inv G]
[set_like S G]
[inv_mem_class S G]
{H : S}
{x : G} :
@[protected, instance]
def
add_subgroup_class.has_neg
{M : Type u_4}
{S : Type u_5}
[sub_neg_monoid M]
[set_like S M]
[hSM : add_subgroup_class S M]
{H : S} :
An additive subgroup of a add_group inherits an inverse.
@[protected, instance]
def
subgroup_class.has_inv
{M : Type u_4}
{S : Type u_5}
[div_inv_monoid M]
[set_like S M]
[hSM : subgroup_class S M]
{H : S} :
A subgroup of a group inherits an inverse.
@[protected, instance]
def
subgroup_class.has_div
{M : Type u_4}
{S : Type u_5}
[div_inv_monoid M]
[set_like S M]
[hSM : subgroup_class S M]
{H : S} :
A subgroup of a group inherits a division
@[protected, instance]
def
add_subgroup_class.has_sub
{M : Type u_4}
{S : Type u_5}
[sub_neg_monoid M]
[set_like S M]
[hSM : add_subgroup_class S M]
{H : S} :
An additive subgroup of an add_group inherits a subtraction.
@[protected, instance]
def
add_subgroup_class.has_zsmul
{M : Type u_1}
{S : Type u_2}
[sub_neg_monoid M]
[set_like S M]
[add_subgroup_class S M]
{H : S} :
An additive subgroup of an add_group inherits an integer scaling.
@[protected, instance]
def
subgroup_class.has_zpow
{M : Type u_4}
{S : Type u_5}
[div_inv_monoid M]
[set_like S M]
[hSM : subgroup_class S M]
{H : S} :
A subgroup of a group inherits an integer power.
@[simp, norm_cast]
theorem
add_subgroup_class.coe_neg
{M : Type u_4}
{S : Type u_5}
[sub_neg_monoid M]
[set_like S M]
[hSM : add_subgroup_class S M]
{H : S}
(x : ↥H) :
@[simp, norm_cast]
theorem
subgroup_class.coe_inv
{M : Type u_4}
{S : Type u_5}
[div_inv_monoid M]
[set_like S M]
[hSM : subgroup_class S M]
{H : S}
(x : ↥H) :
@[simp, norm_cast]
theorem
subgroup_class.coe_div
{M : Type u_4}
{S : Type u_5}
[div_inv_monoid M]
[set_like S M]
[hSM : subgroup_class S M]
{H : S}
(x y : ↥H) :
@[simp, norm_cast]
theorem
add_subgroup_class.coe_sub
{M : Type u_4}
{S : Type u_5}
[sub_neg_monoid M]
[set_like S M]
[hSM : add_subgroup_class S M]
{H : S}
(x y : ↥H) :
@[protected, instance]
def
subgroup_class.to_group
{G : Type u_1}
[group G]
{S : Type u_5}
(H : S)
[set_like S G]
[hSG : subgroup_class S G] :
A subgroup of a group inherits a group structure.
Equations
- subgroup_class.to_group H = function.injective.group coe _ _ _ _ _ _ _
@[protected, instance]
def
add_subgroup_class.to_add_group
{G : Type u_1}
[add_group G]
{S : Type u_5}
(H : S)
[set_like S G]
[hSG : add_subgroup_class S G] :
An additive subgroup of an add_group inherits an add_group structure.
Equations
- add_subgroup_class.to_add_group H = function.injective.add_group coe _ _ _ _ _ _ _
@[protected, instance]
def
subgroup_class.to_comm_group
{S : Type u_5}
(H : S)
{G : Type u_1}
[comm_group G]
[set_like S G]
[subgroup_class S G] :
A subgroup of a comm_group is a comm_group.
Equations
- subgroup_class.to_comm_group H = function.injective.comm_group coe _ _ _ _ _ _ _
@[protected, instance]
def
add_subgroup_class.to_add_comm_group
{S : Type u_5}
(H : S)
{G : Type u_1}
[add_comm_group G]
[set_like S G]
[add_subgroup_class S G] :
An additive subgroup of an add_comm_group is an add_comm_group.
Equations
- add_subgroup_class.to_add_comm_group H = function.injective.add_comm_group coe _ _ _ _ _ _ _
@[protected, instance]
def
add_subgroup_class.to_ordered_add_comm_group
{S : Type u_5}
(H : S)
{G : Type u_1}
[ordered_add_comm_group G]
[set_like S G]
[add_subgroup_class S G] :
An additive subgroup of an add_ordered_comm_group is an add_ordered_comm_group.
Equations
@[protected, instance]
def
subgroup_class.to_ordered_comm_group
{S : Type u_5}
(H : S)
{G : Type u_1}
[ordered_comm_group G]
[set_like S G]
[subgroup_class S G] :
A subgroup of an ordered_comm_group is an ordered_comm_group.
Equations
@[protected, instance]
def
add_subgroup_class.to_linear_ordered_add_comm_group
{S : Type u_5}
(H : S)
{G : Type u_1}
[linear_ordered_add_comm_group G]
[set_like S G]
[add_subgroup_class S G] :
An additive subgroup of a linear_ordered_add_comm_group is a
linear_ordered_add_comm_group.
Equations
@[protected, instance]
def
subgroup_class.to_linear_ordered_comm_group
{S : Type u_5}
(H : S)
{G : Type u_1}
[linear_ordered_comm_group G]
[set_like S G]
[subgroup_class S G] :
A subgroup of a linear_ordered_comm_group is a linear_ordered_comm_group.
Equations
- subgroup_class.to_linear_ordered_comm_group H = function.injective.linear_ordered_comm_group coe _ _ _ _ _ _ _ _ _
@[protected]
def
add_subgroup_class.subtype
{G : Type u_1}
[add_group G]
{S : Type u_5}
(H : S)
[set_like S G]
[hSG : add_subgroup_class S G] :
The natural group hom from an additive subgroup of add_group G to G.
Equations
- add_subgroup_class.subtype H = {to_fun := coe coe_to_lift, map_zero' := _, map_add' := _}
@[protected]
def
subgroup_class.subtype
{G : Type u_1}
[group G]
{S : Type u_5}
(H : S)
[set_like S G]
[hSG : subgroup_class S G] :
The natural group hom from a subgroup of group G to G.
Equations
- subgroup_class.subtype H = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _}
@[simp]
theorem
add_subgroup_class.coe_subtype
{G : Type u_1}
[add_group G]
{S : Type u_5}
(H : S)
[set_like S G]
[hSG : add_subgroup_class S G] :
@[simp]
theorem
subgroup_class.coe_subtype
{G : Type u_1}
[group G]
{S : Type u_5}
(H : S)
[set_like S G]
[hSG : subgroup_class S G] :
def
add_subgroup_class.inclusion
{G : Type u_1}
[add_group G]
{S : Type u_5}
[set_like S G]
[hSG : add_subgroup_class S G]
{H K : S}
(h : H ≤ K) :
The inclusion homomorphism from a additive subgroup H contained in K to K.
Equations
- add_subgroup_class.inclusion h = add_monoid_hom.mk' (λ (x : ↥H), ⟨↑x, _⟩) _
def
subgroup_class.inclusion
{G : Type u_1}
[group G]
{S : Type u_5}
[set_like S G]
[hSG : subgroup_class S G]
{H K : S}
(h : H ≤ K) :
The inclusion homomorphism from a subgroup H contained in K to K.
Equations
- subgroup_class.inclusion h = monoid_hom.mk' (λ (x : ↥H), ⟨↑x, _⟩) _
@[simp]
theorem
add_subgroup_class.inclusion_self
{G : Type u_1}
[add_group G]
{S : Type u_5}
{H : S}
[set_like S G]
[hSG : add_subgroup_class S G]
(x : ↥H) :
@[simp]
theorem
subgroup_class.inclusion_self
{G : Type u_1}
[group G]
{S : Type u_5}
{H : S}
[set_like S G]
[hSG : subgroup_class S G]
(x : ↥H) :
⇑(subgroup_class.inclusion le_rfl) x = x
@[simp]
theorem
add_subgroup_class.inclusion_mk
{G : Type u_1}
[add_group G]
{S : Type u_5}
{H K : S}
[set_like S G]
[hSG : add_subgroup_class S G]
{h : H ≤ K}
(x : G)
(hx : x ∈ H) :
⇑(add_subgroup_class.inclusion h) ⟨x, hx⟩ = ⟨x, _⟩
@[simp]
theorem
subgroup_class.inclusion_mk
{G : Type u_1}
[group G]
{S : Type u_5}
{H K : S}
[set_like S G]
[hSG : subgroup_class S G]
{h : H ≤ K}
(x : G)
(hx : x ∈ H) :
⇑(subgroup_class.inclusion h) ⟨x, hx⟩ = ⟨x, _⟩
@[simp]
theorem
subgroup_class.inclusion_inclusion
{G : Type u_1}
[group G]
{S : Type u_5}
{H K : S}
[set_like S G]
[hSG : subgroup_class S G]
{L : S}
(hHK : H ≤ K)
(hKL : K ≤ L)
(x : ↥H) :
⇑(subgroup_class.inclusion hKL) (⇑(subgroup_class.inclusion hHK) x) = ⇑(subgroup_class.inclusion _) x
@[simp]
theorem
add_subgroup_class.coe_inclusion
{G : Type u_1}
[add_group G]
{S : Type u_5}
[set_like S G]
[hSG : add_subgroup_class S G]
{H K : S}
{h : H ≤ K}
(a : ↥H) :
↑(⇑(add_subgroup_class.inclusion h) a) = ↑a
@[simp]
theorem
subgroup_class.coe_inclusion
{G : Type u_1}
[group G]
{S : Type u_5}
[set_like S G]
[hSG : subgroup_class S G]
{H K : S}
{h : H ≤ K}
(a : ↥H) :
↑(⇑(subgroup_class.inclusion h) a) = ↑a
@[simp]
theorem
add_subgroup_class.subtype_comp_inclusion
{G : Type u_1}
[add_group G]
{S : Type u_5}
[set_like S G]
[hSG : add_subgroup_class S G]
{H K : S}
(hH : H ≤ K) :
@[simp]
theorem
subgroup_class.subtype_comp_inclusion
{G : Type u_1}
[group G]
{S : Type u_5}
[set_like S G]
[hSG : subgroup_class S G]
{H K : S}
(hH : H ≤ K) :
- carrier : set G
- mul_mem' : ∀ {a b : G}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
- one_mem' : 1 ∈ self.carrier
- inv_mem' : ∀ {x : G}, x ∈ self.carrier → x⁻¹ ∈ self.carrier
A subgroup of a group G is a subset containing 1, closed under multiplication
and closed under multiplicative inverse.
Instances for subgroup
- subgroup.has_sizeof_inst
- subgroup.set_like
- subgroup.subgroup_class
- subgroup.has_top
- subgroup.has_bot
- subgroup.inhabited
- subgroup.has_inf
- subgroup.has_Inf
- subgroup.complete_lattice
- subgroup.unique
- subgroup.nontrivial
- subgroup.is_modular_lattice
- subgroup.pointwise_central_scalar
- quotient_group.subgroup.has_quotient
- subgroup.commutator
- is_simple_group.subgroup.is_simple_order
- open_subgroup.has_coe_subgroup
- sylow.subgroup.has_coe
- carrier : set G
- add_mem' : ∀ {a b : G}, a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
- zero_mem' : 0 ∈ self.carrier
- neg_mem' : ∀ {x : G}, x ∈ self.carrier → -x ∈ self.carrier
An additive subgroup of an additive group G is a subset containing 0, closed
under addition and additive inverse.
Instances for add_subgroup
- add_subgroup.has_sizeof_inst
- add_subgroup.set_like
- add_subgroup.add_subgroup_class
- add_subgroup.has_top
- add_subgroup.has_bot
- add_subgroup.inhabited
- add_subgroup.has_inf
- add_subgroup.has_Inf
- add_subgroup.complete_lattice
- add_subgroup.unique
- add_subgroup.nontrivial
- add_subgroup.is_modular_lattice
- add_subgroup.pointwise_central_scalar
- quotient_add_group.subgroup.has_quotient
- is_simple_add_group.subgroup.is_simple_order
- open_add_subgroup.has_coe_add_subgroup
Reinterpret an add_subgroup as an add_submonoid.
@[protected, instance]
Equations
- subgroup.set_like = {coe := subgroup.carrier _inst_1, coe_injective' := _}
@[protected, instance]
Equations
- add_subgroup.set_like = {coe := add_subgroup.carrier _inst_1, coe_injective' := _}
@[protected, instance]
@[protected, instance]
@[simp]
See Note [custom simps projection]
Equations
- subgroup.simps.coe S = ↑S
See Note [custom simps projection]
Equations
@[simp]
theorem
add_subgroup.coe_to_add_submonoid
{G : Type u_1}
[add_group G]
(K : add_subgroup G) :
↑(K.to_add_submonoid) = ↑K
@[simp]
theorem
subgroup.coe_to_submonoid
{G : Type u_1}
[group G]
(K : subgroup G) :
↑(K.to_submonoid) = ↑K
@[simp]
theorem
subgroup.mem_to_submonoid
{G : Type u_1}
[group G]
(K : subgroup G)
(x : G) :
x ∈ K.to_submonoid ↔ x ∈ K
@[simp]
theorem
add_subgroup.mem_to_add_submonoid
{G : Type u_1}
[add_group G]
(K : add_subgroup G)
(x : G) :
x ∈ K.to_add_submonoid ↔ x ∈ K
@[simp]
theorem
add_subgroup.to_add_submonoid_eq
{G : Type u_1}
[add_group G]
{p q : add_subgroup G} :
p.to_add_submonoid = q.to_add_submonoid ↔ p = q
@[simp]
theorem
subgroup.to_submonoid_eq
{G : Type u_1}
[group G]
{p q : subgroup G} :
p.to_submonoid = q.to_submonoid ↔ p = q
@[simp]
theorem
add_subgroup.to_add_submonoid_le
{G : Type u_1}
[add_group G]
{p q : add_subgroup G} :
p.to_add_submonoid ≤ q.to_add_submonoid ↔ p ≤ q
@[simp]
theorem
subgroup.to_submonoid_le
{G : Type u_1}
[group G]
{p q : subgroup G} :
p.to_submonoid ≤ q.to_submonoid ↔ p ≤ q
Conversion to/from additive/multiplicative #
Supgroups of a group G are isomorphic to additive subgroups of additive G.
Equations
- subgroup.to_add_subgroup = {to_equiv := {to_fun := λ (S : subgroup G), {carrier := (⇑submonoid.to_add_submonoid S.to_submonoid).carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}, inv_fun := λ (S : add_subgroup (additive G)), {carrier := (⇑add_submonoid.to_submonoid' S.to_add_submonoid).carrier, mul_mem' := _, one_mem' := _, inv_mem' := _}, left_inv := _, right_inv := _}, map_rel_iff' := _}
@[simp]
@[simp]
theorem
subgroup.to_add_subgroup_symm_apply_coe
{G : Type u_1}
[group G]
(S : add_subgroup (additive G)) :
@[reducible]
Additive subgroup of an additive group additive G are isomorphic to subgroup of G.
def
add_subgroup.to_subgroup
{A : Type u_3}
[add_group A] :
add_subgroup A ≃o subgroup (multiplicative A)
Additive supgroups of an additive group A are isomorphic to subgroups of multiplicative A.
Equations
- add_subgroup.to_subgroup = {to_equiv := {to_fun := λ (S : add_subgroup A), {carrier := (⇑add_submonoid.to_submonoid S.to_add_submonoid).carrier, mul_mem' := _, one_mem' := _, inv_mem' := _}, inv_fun := λ (S : subgroup (multiplicative A)), {carrier := (⇑submonoid.to_add_submonoid' S.to_submonoid).carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}, left_inv := _, right_inv := _}, map_rel_iff' := _}
@[simp]
@[simp]
theorem
add_subgroup.to_subgroup_symm_apply_coe
{A : Type u_3}
[add_group A]
(S : subgroup (multiplicative A)) :
@[reducible]
def
subgroup.to_add_subgroup'
{A : Type u_3}
[add_group A] :
subgroup (multiplicative A) ≃o add_subgroup A
Subgroups of an additive group multiplicative A are isomorphic to additive subgroups of A.
@[protected]
Copy of a subgroup with a new carrier equal to the old one. Useful to fix definitional
equalities.
@[protected]
Copy of an additive subgroup with a new carrier equal to the old one.
Useful to fix definitional equalities
theorem
add_subgroup.copy_eq
{G : Type u_1}
[add_group G]
(K : add_subgroup G)
(s : set G)
(hs : s = ↑K) :
@[ext]
theorem
add_subgroup.ext
{G : Type u_1}
[add_group G]
{H K : add_subgroup G}
(h : ∀ (x : G), x ∈ H ↔ x ∈ K) :
H = K
Two add_subgroups are equal if they have the same elements.
@[protected]
An add_subgroup contains the group's 0.
@[protected]
An add_subgroup is closed under addition.
@[protected]
An add_subgroup is closed under inverse.
@[protected]
theorem
add_subgroup.sub_mem
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
{x y : G}
(hx : x ∈ H)
(hy : y ∈ H) :
An add_subgroup is closed under subtraction.
@[protected]
@[protected]
@[protected]
theorem
add_subgroup.add_mem_cancel_right
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
{x y : G}
(h : x ∈ H) :
@[protected]
theorem
add_subgroup.add_mem_cancel_left
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
{x y : G}
(h : x ∈ H) :
@[protected]
theorem
add_subgroup.nsmul_mem
{G : Type u_1}
[add_group G]
(K : add_subgroup G)
{x : G}
(hx : x ∈ K)
(n : ℕ) :
@[protected]
theorem
add_subgroup.zsmul_mem
{G : Type u_1}
[add_group G]
(K : add_subgroup G)
{x : G}
(hx : x ∈ K)
(n : ℤ) :
@[protected, instance]
An add_subgroup of an add_group inherits a natural scaling.
@[protected, instance]
An add_subgroup of an add_group inherits an integer scaling.
@[simp, norm_cast]
@[simp, norm_cast]
theorem
add_subgroup.coe_mk
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
(x : G)
(hx : x ∈ H) :
@[simp]
theorem
add_subgroup.mk_eq_zero_iff
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
{g : G}
{h : g ∈ H} :
@[protected, instance]
An add_subgroup of an add_group inherits an add_group structure.
Equations
- H.to_add_group = function.injective.add_group coe _ _ _ _ _ _ _
@[protected, instance]
An add_subgroup of an add_comm_group is an add_comm_group.
Equations
- H.to_add_comm_group = function.injective.add_comm_group coe _ _ _ _ _ _ _
@[protected, instance]
A subgroup of a comm_group is a comm_group.
Equations
- H.to_comm_group = function.injective.comm_group coe _ _ _ _ _ _ _
@[protected, instance]
def
add_subgroup.to_ordered_add_comm_group
{G : Type u_1}
[ordered_add_comm_group G]
(H : add_subgroup G) :
An add_subgroup of an add_ordered_comm_group is an add_ordered_comm_group.
Equations
- H.to_ordered_add_comm_group = function.injective.ordered_add_comm_group coe _ _ _ _ _ _ _
@[protected, instance]
A subgroup of an ordered_comm_group is an ordered_comm_group.
Equations
- H.to_ordered_comm_group = function.injective.ordered_comm_group coe _ _ _ _ _ _ _
@[protected, instance]
def
subgroup.to_linear_ordered_comm_group
{G : Type u_1}
[linear_ordered_comm_group G]
(H : subgroup G) :
A subgroup of a linear_ordered_comm_group is a linear_ordered_comm_group.
Equations
- H.to_linear_ordered_comm_group = function.injective.linear_ordered_comm_group coe _ _ _ _ _ _ _ _ _
@[protected, instance]
def
add_subgroup.to_linear_ordered_add_comm_group
{G : Type u_1}
[linear_ordered_add_comm_group G]
(H : add_subgroup G) :
An add_subgroup of a linear_ordered_add_comm_group is a
linear_ordered_add_comm_group.
Equations
- H.to_linear_ordered_add_comm_group = function.injective.linear_ordered_add_comm_group coe _ _ _ _ _ _ _ _ _
@[protected]
The natural group hom from an add_subgroup of add_group G to G.
@[simp]
The inclusion homomorphism from a additive subgroup H contained in K to K.
Equations
- add_subgroup.inclusion h = add_monoid_hom.mk' (λ (x : ↥H), ⟨↑x, _⟩) _
The inclusion homomorphism from a subgroup H contained in K to K.
Equations
- subgroup.inclusion h = monoid_hom.mk' (λ (x : ↥H), ⟨↑x, _⟩) _
@[simp]
theorem
add_subgroup.coe_inclusion
{G : Type u_1}
[add_group G]
{H K : add_subgroup G}
{h : H ≤ K}
(a : ↥H) :
↑(⇑(add_subgroup.inclusion h) a) = ↑a
theorem
add_subgroup.inclusion_injective
{G : Type u_1}
[add_group G]
{H K : add_subgroup G}
(h : H ≤ K) :
@[simp]
theorem
add_subgroup.subtype_comp_inclusion
{G : Type u_1}
[add_group G]
{H K : add_subgroup G}
(hH : H ≤ K) :
K.subtype.comp (add_subgroup.inclusion hH) = H.subtype
@[protected, instance]
The add_subgroup G of the add_group G.
@[simp]
@[simp]
theorem
subgroup.top_equiv_symm_apply_coe
{G : Type u_1}
[group G]
(x : G) :
↑(⇑(subgroup.top_equiv.symm) x) = x
The top subgroup is isomorphic to the group.
This is the group version of submonoid.top_equiv.
Equations
@[simp]
theorem
add_subgroup.top_equiv_symm_apply_coe
{G : Type u_1}
[add_group G]
(x : G) :
↑(⇑(add_subgroup.top_equiv.symm) x) = x
The top additive subgroup is isomorphic to the additive group.
This is the additive group version of add_submonoid.top_equiv.
Equations
@[simp]
@[protected, instance]
The trivial add_subgroup {0} of an add_group G.
@[protected, instance]
Equations
@[protected, instance]
Equations
- add_subgroup.has_bot.bot.unique = {to_inhabited := {default := 0}, uniq := _}
@[protected, instance]
Equations
- subgroup.has_bot.bot.unique = {to_inhabited := {default := 1}, uniq := _}
@[simp]
@[simp]
theorem
subgroup.eq_bot_of_subsingleton
{G : Type u_1}
[group G]
(H : subgroup G)
[subsingleton ↥H] :
theorem
add_subgroup.eq_bot_of_subsingleton
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
[subsingleton ↥H] :
theorem
add_subgroup.nontrivial_iff_exists_ne_zero
{G : Type u_1}
[add_group G]
(H : add_subgroup G) :
theorem
subgroup.bot_or_nontrivial
{G : Type u_1}
[group G]
(H : subgroup G) :
H = ⊥ ∨ nontrivial ↥H
A subgroup is either the trivial subgroup or nontrivial.
theorem
add_subgroup.bot_or_nontrivial
{G : Type u_1}
[add_group G]
(H : add_subgroup G) :
H = ⊥ ∨ nontrivial ↥H
A subgroup is either the trivial subgroup or nontrivial.
@[protected, instance]
The inf of two subgroups is their intersection.
Equations
- subgroup.has_inf = {inf := λ (H₁ H₂ : subgroup G), {carrier := (H₁.to_submonoid ⊓ H₂.to_submonoid).carrier, mul_mem' := _, one_mem' := _, inv_mem' := _}}
@[protected, instance]
The inf of two add_subgroupss is their intersection.
Equations
- add_subgroup.has_inf = {inf := λ (H₁ H₂ : add_subgroup G), {carrier := (H₁.to_add_submonoid ⊓ H₂.to_add_submonoid).carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}}
@[protected, instance]
Equations
- add_subgroup.has_Inf = {Inf := λ (s : set (add_subgroup G)), {carrier := ((⨅ (S : add_subgroup G) (H : S ∈ s), S.to_add_submonoid).copy (⋂ (S : add_subgroup G) (H : S ∈ s), ↑S) _).carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}}
@[protected, instance]
@[simp, norm_cast]
theorem
add_subgroup.coe_Inf
{G : Type u_1}
[add_group G]
(H : set (add_subgroup G)) :
↑(has_Inf.Inf H) = ⋂ (s : add_subgroup G) (H : s ∈ H), ↑s
@[simp]
theorem
add_subgroup.mem_Inf
{G : Type u_1}
[add_group G]
{S : set (add_subgroup G)}
{x : G} :
x ∈ has_Inf.Inf S ↔ ∀ (p : add_subgroup G), p ∈ S → x ∈ p
@[protected, instance]
Subgroups of a group form a complete lattice.
Equations
- subgroup.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Inf (subgroup G) subgroup.complete_lattice._proof_1), le := complete_lattice.le (complete_lattice_of_Inf (subgroup G) subgroup.complete_lattice._proof_1), lt := complete_lattice.lt (complete_lattice_of_Inf (subgroup G) subgroup.complete_lattice._proof_1), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf subgroup.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (subgroup G) subgroup.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (complete_lattice_of_Inf (subgroup G) subgroup.complete_lattice._proof_1), Inf_le := _, le_Inf := _, top := ⊤, bot := ⊥, le_top := _, bot_le := _}
@[protected, instance]
The add_subgroups of an add_group form a complete lattice.
Equations
- add_subgroup.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Inf (add_subgroup G) add_subgroup.complete_lattice._proof_1), le := complete_lattice.le (complete_lattice_of_Inf (add_subgroup G) add_subgroup.complete_lattice._proof_1), lt := complete_lattice.lt (complete_lattice_of_Inf (add_subgroup G) add_subgroup.complete_lattice._proof_1), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf add_subgroup.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (add_subgroup G) add_subgroup.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (complete_lattice_of_Inf (add_subgroup G) add_subgroup.complete_lattice._proof_1), Inf_le := _, le_Inf := _, top := ⊤, bot := ⊥, le_top := _, bot_le := _}
theorem
add_subgroup.add_mem_sup
{G : Type u_1}
[add_group G]
{S T : add_subgroup G}
{x y : G}
(hx : x ∈ S)
(hy : y ∈ T) :
theorem
add_subgroup.mem_Sup_of_mem
{G : Type u_1}
[add_group G]
{S : set (add_subgroup G)}
{s : add_subgroup G}
(hs : s ∈ S)
{x : G} :
x ∈ s → x ∈ has_Sup.Sup S
@[simp]
theorem
subgroup.subsingleton_iff
{G : Type u_1}
[group G] :
subsingleton (subgroup G) ↔ subsingleton G
@[simp]
@[simp]
@[simp]
theorem
add_subgroup.nontrivial_iff
{G : Type u_1}
[add_group G] :
nontrivial (add_subgroup G) ↔ nontrivial G
@[protected, instance]
Equations
- add_subgroup.unique = {to_inhabited := {default := ⊥}, uniq := _}
@[protected, instance]
Equations
- subgroup.unique = {to_inhabited := {default := ⊥}, uniq := _}
@[protected, instance]
@[protected, instance]
The add_subgroup generated by a set
Equations
- add_subgroup.closure k = has_Inf.Inf {K : add_subgroup G | k ⊆ ↑K}
Instances for ↥add_subgroup.closure
The subgroup generated by a set.
Equations
- subgroup.closure k = has_Inf.Inf {K : subgroup G | k ⊆ ↑K}
Instances for ↥subgroup.closure
theorem
add_subgroup.mem_closure
{G : Type u_1}
[add_group G]
{k : set G}
{x : G} :
x ∈ add_subgroup.closure k ↔ ∀ (K : add_subgroup G), k ⊆ ↑K → x ∈ K
@[simp]
The subgroup generated by a set includes the set.
@[simp]
theorem
add_subgroup.subset_closure
{G : Type u_1}
[add_group G]
{k : set G} :
k ⊆ ↑(add_subgroup.closure k)
The add_subgroup generated by a set includes the set.
theorem
add_subgroup.not_mem_of_not_mem_closure
{G : Type u_1}
[add_group G]
{k : set G}
{P : G}
(hP : P ∉ add_subgroup.closure k) :
P ∉ k
theorem
subgroup.not_mem_of_not_mem_closure
{G : Type u_1}
[group G]
{k : set G}
{P : G}
(hP : P ∉ subgroup.closure k) :
P ∉ k
@[simp]
theorem
add_subgroup.closure_le
{G : Type u_1}
[add_group G]
(K : add_subgroup G)
{k : set G} :
add_subgroup.closure k ≤ K ↔ k ⊆ ↑K
An additive subgroup K includes closure k if and only if it includes k
theorem
subgroup.closure_eq_of_le
{G : Type u_1}
[group G]
(K : subgroup G)
{k : set G}
(h₁ : k ⊆ ↑K)
(h₂ : K ≤ subgroup.closure k) :
subgroup.closure k = K
theorem
add_subgroup.closure_eq_of_le
{G : Type u_1}
[add_group G]
(K : add_subgroup G)
{k : set G}
(h₁ : k ⊆ ↑K)
(h₂ : K ≤ add_subgroup.closure k) :
theorem
subgroup.closure_induction
{G : Type u_1}
[group G]
{k : set G}
{p : G → Prop}
{x : G}
(h : x ∈ subgroup.closure k)
(Hk : ∀ (x : G), x ∈ k → p x)
(H1 : p 1)
(Hmul : ∀ (x y : G), p x → p y → p (x * y))
(Hinv : ∀ (x : G), p x → p x⁻¹) :
p x
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.
theorem
add_subgroup.closure_induction
{G : Type u_1}
[add_group G]
{k : set G}
{p : G → Prop}
{x : G}
(h : x ∈ add_subgroup.closure k)
(Hk : ∀ (x : G), x ∈ k → p x)
(H1 : p 0)
(Hmul : ∀ (x y : G), p x → p y → p (x + y))
(Hinv : ∀ (x : G), p x → p (-x)) :
p x
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.
theorem
subgroup.closure_induction'
{G : Type u_1}
[group G]
{k : set G}
{p : Π (x : G), x ∈ subgroup.closure k → Prop}
(Hs : ∀ (x : G) (h : x ∈ k), p x _)
(H1 : p 1 _)
(Hmul : ∀ (x : G) (hx : x ∈ subgroup.closure k) (y : G) (hy : y ∈ subgroup.closure k), p x hx → p y hy → p (x * y) _)
(Hinv : ∀ (x : G) (hx : x ∈ subgroup.closure k), p x hx → p x⁻¹ _)
{x : G}
(hx : x ∈ subgroup.closure k) :
p x hx
A dependent version of subgroup.closure_induction.
theorem
add_subgroup.closure_induction'
{G : Type u_1}
[add_group G]
{k : set G}
{p : Π (x : G), x ∈ add_subgroup.closure k → Prop}
(Hs : ∀ (x : G) (h : x ∈ k), p x _)
(H1 : p 0 _)
(Hmul : ∀ (x : G) (hx : x ∈ add_subgroup.closure k) (y : G) (hy : y ∈ add_subgroup.closure k), p x hx → p y hy → p (x + y) _)
(Hinv : ∀ (x : G) (hx : x ∈ add_subgroup.closure k), p x hx → p (-x) _)
{x : G}
(hx : x ∈ add_subgroup.closure k) :
p x hx
A dependent version of add_subgroup.closure_induction.
theorem
add_subgroup.closure_induction₂
{G : Type u_1}
[add_group G]
{k : set G}
{p : G → G → Prop}
{x y : G}
(hx : x ∈ add_subgroup.closure k)
(hy : y ∈ add_subgroup.closure k)
(Hk : ∀ (x : G), x ∈ k → ∀ (y : G), y ∈ k → p x y)
(H1_left : ∀ (x : G), p 0 x)
(H1_right : ∀ (x : G), p x 0)
(Hmul_left : ∀ (x₁ x₂ y : G), p x₁ y → p x₂ y → p (x₁ + x₂) y)
(Hmul_right : ∀ (x y₁ y₂ : G), p x y₁ → p x y₂ → p x (y₁ + y₂))
(Hinv_left : ∀ (x y : G), p x y → p (-x) y)
(Hinv_right : ∀ (x y : G), p x y → p x (-y)) :
p x y
An induction principle for additive closure membership, for predicates with two arguments.
theorem
subgroup.closure_induction₂
{G : Type u_1}
[group G]
{k : set G}
{p : G → G → Prop}
{x y : G}
(hx : x ∈ subgroup.closure k)
(hy : y ∈ subgroup.closure k)
(Hk : ∀ (x : G), x ∈ k → ∀ (y : G), y ∈ k → p x y)
(H1_left : ∀ (x : G), p 1 x)
(H1_right : ∀ (x : G), p x 1)
(Hmul_left : ∀ (x₁ x₂ y : G), p x₁ y → p x₂ y → p (x₁ * x₂) y)
(Hmul_right : ∀ (x y₁ y₂ : G), p x y₁ → p x y₂ → p x (y₁ * y₂))
(Hinv_left : ∀ (x y : G), p x y → p x⁻¹ y)
(Hinv_right : ∀ (x y : G), p x y → p x y⁻¹) :
p x y
An induction principle for closure membership for predicates with two arguments.
@[simp]
theorem
subgroup.closure_closure_coe_preimage
{G : Type u_1}
[group G]
{k : set G} :
subgroup.closure (coe ⁻¹' k) = ⊤
@[simp]
theorem
add_subgroup.closure_closure_coe_preimage
{G : Type u_1}
[add_group G]
{k : set G} :
add_subgroup.closure (coe ⁻¹' k) = ⊤
def
subgroup.closure_comm_group_of_comm
{G : Type u_1}
[group G]
{k : set G}
(hcomm : ∀ (x : G), x ∈ k → ∀ (y : G), y ∈ k → x * y = y * x) :
If all the elements of a set s commute, then closure s is a commutative group.
Equations
- subgroup.closure_comm_group_of_comm hcomm = {mul := group.mul (subgroup.closure k).to_group, mul_assoc := _, one := group.one (subgroup.closure k).to_group, one_mul := _, mul_one := _, npow := group.npow (subgroup.closure k).to_group, npow_zero' := _, npow_succ' := _, inv := group.inv (subgroup.closure k).to_group, div := group.div (subgroup.closure k).to_group, div_eq_mul_inv := _, zpow := group.zpow (subgroup.closure k).to_group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}
def
add_subgroup.closure_add_comm_group_of_comm
{G : Type u_1}
[add_group G]
{k : set G}
(hcomm : ∀ (x : G), x ∈ k → ∀ (y : G), y ∈ k → x + y = y + x) :
If all the elements of a set s commute, then closure s is an additive
commutative group.
Equations
- add_subgroup.closure_add_comm_group_of_comm hcomm = {add := add_group.add (add_subgroup.closure k).to_add_group, add_assoc := _, zero := add_group.zero (add_subgroup.closure k).to_add_group, zero_add := _, add_zero := _, nsmul := add_group.nsmul (add_subgroup.closure k).to_add_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg (add_subgroup.closure k).to_add_group, sub := add_group.sub (add_subgroup.closure k).to_add_group, sub_eq_add_neg := _, zsmul := add_group.zsmul (add_subgroup.closure k).to_add_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
@[protected]
closure forms a Galois insertion with the coercion to set.
Equations
- add_subgroup.gi G = {choice := λ (s : set G) (_x : ↑(add_subgroup.closure s) ≤ s), add_subgroup.closure s, gc := _, le_l_u := _, choice_eq := _}
@[protected]
closure forms a Galois insertion with the coercion to set.
Equations
- subgroup.gi G = {choice := λ (s : set G) (_x : ↑(subgroup.closure s) ≤ s), subgroup.closure s, gc := _, le_l_u := _, choice_eq := _}
@[simp]
Closure of a subgroup K equals K.
@[simp]
Additive closure of an additive subgroup K equals K
@[simp]
@[simp]
@[simp]
theorem
subgroup.closure_union
{G : Type u_1}
[group G]
(s t : set G) :
subgroup.closure (s ∪ t) = subgroup.closure s ⊔ subgroup.closure t
theorem
subgroup.closure_Union
{G : Type u_1}
[group G]
{ι : Sort u_2}
(s : ι → set G) :
subgroup.closure (⋃ (i : ι), s i) = ⨆ (i : ι), subgroup.closure (s i)
theorem
add_subgroup.closure_Union
{G : Type u_1}
[add_group G]
{ι : Sort u_2}
(s : ι → set G) :
add_subgroup.closure (⋃ (i : ι), s i) = ⨆ (i : ι), add_subgroup.closure (s i)
theorem
subgroup.closure_eq_bot_iff
(G : Type u_1)
[group G]
(S : set G) :
subgroup.closure S = ⊥ ↔ S ⊆ {1}
theorem
add_subgroup.closure_eq_bot_iff
(G : Type u_1)
[add_group G]
(S : set G) :
add_subgroup.closure S = ⊥ ↔ S ⊆ {0}
theorem
add_subgroup.supr_eq_closure
{G : Type u_1}
[add_group G]
{ι : Sort u_2}
(p : ι → add_subgroup G) :
The add_subgroup generated by an element of an add_group equals the set of
natural number multiples of the element.
theorem
add_subgroup.closure_singleton_zero
{G : Type u_1}
[add_group G] :
add_subgroup.closure {0} = ⊥
theorem
add_subgroup.closure_eq_top_of_mclosure_eq_top
{G : Type u_1}
[add_group G]
{S : set G}
(h : add_submonoid.closure S = ⊤) :
theorem
subgroup.closure_eq_top_of_mclosure_eq_top
{G : Type u_1}
[group G]
{S : set G}
(h : submonoid.closure S = ⊤) :
theorem
add_subgroup.mem_Sup_of_directed_on
{G : Type u_1}
[add_group G]
{K : set (add_subgroup G)}
(Kne : K.nonempty)
(hK : directed_on has_le.le K)
{x : G} :
x ∈ has_Sup.Sup K ↔ ∃ (s : add_subgroup G) (H : s ∈ K), x ∈ s
def
add_subgroup.comap
{G : Type u_1}
[add_group G]
{N : Type u_2}
[add_group N]
(f : G →+ N)
(H : add_subgroup N) :
The preimage of an add_subgroup along an add_monoid homomorphism
is an add_subgroup.
Equations
Instances for add_subgroup.comap
@[simp]
theorem
add_subgroup.coe_comap
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(K : add_subgroup N)
(f : G →+ N) :
@[simp]
theorem
add_subgroup.mem_comap
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{K : add_subgroup N}
{f : G →+ N}
{x : G} :
x ∈ add_subgroup.comap f K ↔ ⇑f x ∈ K
theorem
subgroup.comap_mono
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{f : G →* N}
{K K' : subgroup N} :
K ≤ K' → subgroup.comap f K ≤ subgroup.comap f K'
theorem
add_subgroup.comap_mono
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{f : G →+ N}
{K K' : add_subgroup N} :
K ≤ K' → add_subgroup.comap f K ≤ add_subgroup.comap f K'
theorem
add_subgroup.comap_comap
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{P : Type u_5}
[add_group P]
(K : add_subgroup P)
(g : N →+ P)
(f : G →+ N) :
add_subgroup.comap f (add_subgroup.comap g K) = add_subgroup.comap (g.comp f) K
theorem
subgroup.comap_comap
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{P : Type u_5}
[group P]
(K : subgroup P)
(g : N →* P)
(f : G →* N) :
subgroup.comap f (subgroup.comap g K) = subgroup.comap (g.comp f) K
@[simp]
theorem
subgroup.comap_id
{N : Type u_4}
[group N]
(K : subgroup N) :
subgroup.comap (monoid_hom.id N) K = K
@[simp]
theorem
add_subgroup.comap_id
{N : Type u_4}
[add_group N]
(K : add_subgroup N) :
add_subgroup.comap (add_monoid_hom.id N) K = K
def
add_subgroup.map
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(f : G →+ N)
(H : add_subgroup G) :
The image of an add_subgroup along an add_monoid homomorphism
is an add_subgroup.
Equations
Instances for add_subgroup.map
@[simp]
theorem
add_subgroup.coe_map
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(f : G →+ N)
(K : add_subgroup G) :
theorem
add_subgroup.mem_map_of_mem
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(f : G →+ N)
{K : add_subgroup G}
{x : G}
(hx : x ∈ K) :
⇑f x ∈ add_subgroup.map f K
theorem
add_subgroup.apply_coe_mem_map
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(f : G →+ N)
(K : add_subgroup G)
(x : ↥K) :
⇑f ↑x ∈ add_subgroup.map f K
theorem
add_subgroup.map_mono
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{f : G →+ N}
{K K' : add_subgroup G} :
K ≤ K' → add_subgroup.map f K ≤ add_subgroup.map f K'
theorem
subgroup.map_mono
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{f : G →* N}
{K K' : subgroup G} :
K ≤ K' → subgroup.map f K ≤ subgroup.map f K'
@[simp]
theorem
add_subgroup.map_id
{G : Type u_1}
[add_group G]
(K : add_subgroup G) :
add_subgroup.map (add_monoid_hom.id G) K = K
@[simp]
theorem
subgroup.map_id
{G : Type u_1}
[group G]
(K : subgroup G) :
subgroup.map (monoid_hom.id G) K = K
theorem
add_subgroup.map_map
{G : Type u_1}
[add_group G]
(K : add_subgroup G)
{N : Type u_4}
[add_group N]
{P : Type u_5}
[add_group P]
(g : N →+ P)
(f : G →+ N) :
add_subgroup.map g (add_subgroup.map f K) = add_subgroup.map (g.comp f) K
theorem
subgroup.map_map
{G : Type u_1}
[group G]
(K : subgroup G)
{N : Type u_4}
[group N]
{P : Type u_5}
[group P]
(g : N →* P)
(f : G →* N) :
subgroup.map g (subgroup.map f K) = subgroup.map (g.comp f) K
@[simp]
theorem
subgroup.map_one_eq_bot
{G : Type u_1}
[group G]
(K : subgroup G)
{N : Type u_4}
[group N] :
subgroup.map 1 K = ⊥
@[simp]
theorem
add_subgroup.map_zero_eq_bot
{G : Type u_1}
[add_group G]
(K : add_subgroup G)
{N : Type u_4}
[add_group N] :
add_subgroup.map 0 K = ⊥
theorem
subgroup.mem_map_equiv
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{f : G ≃* N}
{K : subgroup G}
{x : N} :
x ∈ subgroup.map f.to_monoid_hom K ↔ ⇑(f.symm) x ∈ K
theorem
add_subgroup.mem_map_equiv
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{f : G ≃+ N}
{K : add_subgroup G}
{x : N} :
x ∈ add_subgroup.map f.to_add_monoid_hom K ↔ ⇑(f.symm) x ∈ K
theorem
subgroup.mem_map_iff_mem
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{f : G →* N}
(hf : function.injective ⇑f)
{K : subgroup G}
{x : G} :
⇑f x ∈ subgroup.map f K ↔ x ∈ K
theorem
add_subgroup.mem_map_iff_mem
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{f : G →+ N}
(hf : function.injective ⇑f)
{K : add_subgroup G}
{x : G} :
⇑f x ∈ add_subgroup.map f K ↔ x ∈ K
theorem
add_subgroup.map_equiv_eq_comap_symm
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(f : G ≃+ N)
(K : add_subgroup G) :
theorem
add_subgroup.comap_equiv_eq_map_symm
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(f : N ≃+ G)
(K : add_subgroup G) :
theorem
add_subgroup.map_symm_eq_iff_map_eq
{G : Type u_1}
[add_group G]
(K : add_subgroup G)
{N : Type u_4}
[add_group N]
{H : add_subgroup N}
{e : G ≃+ N} :
add_subgroup.map ↑(e.symm) H = K ↔ add_subgroup.map ↑e K = H
theorem
add_subgroup.map_le_iff_le_comap
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{f : G →+ N}
{K : add_subgroup G}
{H : add_subgroup N} :
add_subgroup.map f K ≤ H ↔ K ≤ add_subgroup.comap f H
theorem
subgroup.map_le_iff_le_comap
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{f : G →* N}
{K : subgroup G}
{H : subgroup N} :
subgroup.map f K ≤ H ↔ K ≤ subgroup.comap f H
theorem
add_subgroup.map_sup
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(H K : add_subgroup G)
(f : G →+ N) :
add_subgroup.map f (H ⊔ K) = add_subgroup.map f H ⊔ add_subgroup.map f K
theorem
subgroup.map_sup
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
(H K : subgroup G)
(f : G →* N) :
subgroup.map f (H ⊔ K) = subgroup.map f H ⊔ subgroup.map f K
theorem
add_subgroup.map_supr
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{ι : Sort u_2}
(f : G →+ N)
(s : ι → add_subgroup G) :
add_subgroup.map f (supr s) = ⨆ (i : ι), add_subgroup.map f (s i)
theorem
add_subgroup.comap_sup_comap_le
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(H K : add_subgroup N)
(f : G →+ N) :
add_subgroup.comap f H ⊔ add_subgroup.comap f K ≤ add_subgroup.comap f (H ⊔ K)
theorem
subgroup.comap_sup_comap_le
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
(H K : subgroup N)
(f : G →* N) :
subgroup.comap f H ⊔ subgroup.comap f K ≤ subgroup.comap f (H ⊔ K)
theorem
add_subgroup.supr_comap_le
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{ι : Sort u_2}
(f : G →+ N)
(s : ι → add_subgroup N) :
(⨆ (i : ι), add_subgroup.comap f (s i)) ≤ add_subgroup.comap f (supr s)
theorem
add_subgroup.comap_inf
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(H K : add_subgroup N)
(f : G →+ N) :
add_subgroup.comap f (H ⊓ K) = add_subgroup.comap f H ⊓ add_subgroup.comap f K
theorem
subgroup.comap_inf
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
(H K : subgroup N)
(f : G →* N) :
subgroup.comap f (H ⊓ K) = subgroup.comap f H ⊓ subgroup.comap f K
theorem
add_subgroup.comap_infi
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{ι : Sort u_2}
(f : G →+ N)
(s : ι → add_subgroup N) :
add_subgroup.comap f (infi s) = ⨅ (i : ι), add_subgroup.comap f (s i)
theorem
add_subgroup.map_inf_le
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(H K : add_subgroup G)
(f : G →+ N) :
add_subgroup.map f (H ⊓ K) ≤ add_subgroup.map f H ⊓ add_subgroup.map f K
theorem
subgroup.map_inf_le
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
(H K : subgroup G)
(f : G →* N) :
subgroup.map f (H ⊓ K) ≤ subgroup.map f H ⊓ subgroup.map f K
theorem
subgroup.map_inf_eq
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
(H K : subgroup G)
(f : G →* N)
(hf : function.injective ⇑f) :
subgroup.map f (H ⊓ K) = subgroup.map f H ⊓ subgroup.map f K
theorem
add_subgroup.map_inf_eq
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(H K : add_subgroup G)
(f : G →+ N)
(hf : function.injective ⇑f) :
add_subgroup.map f (H ⊓ K) = add_subgroup.map f H ⊓ add_subgroup.map f K
@[simp]
theorem
subgroup.map_top_of_surjective
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
(f : G →* N)
(h : function.surjective ⇑f) :
subgroup.map f ⊤ = ⊤
@[simp]
theorem
add_subgroup.map_top_of_surjective
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(f : G →+ N)
(h : function.surjective ⇑f) :
add_subgroup.map f ⊤ = ⊤
For any subgroups H and K, view H ⊓ K as a subgroup of K.
Equations
- H.add_subgroup_of K = add_subgroup.comap K.subtype H
Instances for add_subgroup.add_subgroup_of
For any subgroups H and K, view H ⊓ K as a subgroup of K.
Equations
- H.subgroup_of K = subgroup.comap K.subtype H
Instances for subgroup.subgroup_of
@[simp]
theorem
subgroup.subgroup_of_equiv_of_le_apply_coe
{G : Type u_1}
[group G]
{H K : subgroup G}
(h : H ≤ K)
(g : ↥(H.subgroup_of K)) :
def
subgroup.subgroup_of_equiv_of_le
{G : Type u_1}
[group G]
{H K : subgroup G}
(h : H ≤ K) :
↥(H.subgroup_of K) ≃* ↥H
If H ≤ K, then H as a subgroup of K is isomorphic to H.
@[simp]
theorem
add_subgroup.add_subgroup_of_equiv_of_le_apply_coe
{G : Type u_1}
[add_group G]
{H K : add_subgroup G}
(h : H ≤ K)
(g : ↥(H.add_subgroup_of K)) :
@[simp]
theorem
add_subgroup.add_subgroup_of_equiv_of_le_symm_apply_coe_coe
{G : Type u_1}
[add_group G]
{H K : add_subgroup G}
(h : H ≤ K)
(g : ↥H) :
def
add_subgroup.add_subgroup_of_equiv_of_le
{G : Type u_1}
[add_group G]
{H K : add_subgroup G}
(h : H ≤ K) :
↥(H.add_subgroup_of K) ≃+ ↥H
If H ≤ K, then H as a subgroup of K is isomorphic to H.
@[simp]
theorem
subgroup.comap_subtype
{G : Type u_1}
[group G]
(H K : subgroup G) :
subgroup.comap K.subtype H = H.subgroup_of K
@[simp]
theorem
add_subgroup.comap_subtype
{G : Type u_1}
[add_group G]
(H K : add_subgroup G) :
add_subgroup.comap K.subtype H = H.add_subgroup_of K
@[simp]
theorem
add_subgroup.comap_inclusion_add_subgroup_of
{G : Type u_1}
[add_group G]
{K₁ K₂ : add_subgroup G}
(h : K₁ ≤ K₂)
(H : add_subgroup G) :
add_subgroup.comap (add_subgroup.inclusion h) (H.add_subgroup_of K₂) = H.add_subgroup_of K₁
@[simp]
theorem
subgroup.comap_inclusion_subgroup_of
{G : Type u_1}
[group G]
{K₁ K₂ : subgroup G}
(h : K₁ ≤ K₂)
(H : subgroup G) :
subgroup.comap (subgroup.inclusion h) (H.subgroup_of K₂) = H.subgroup_of K₁
theorem
add_subgroup.mem_add_subgroup_of
{G : Type u_1}
[add_group G]
{H K : add_subgroup G}
{h : ↥K} :
h ∈ H.add_subgroup_of K ↔ ↑h ∈ H
@[simp]
theorem
add_subgroup.add_subgroup_of_map_subtype
{G : Type u_1}
[add_group G]
(H K : add_subgroup G) :
add_subgroup.map K.subtype (H.add_subgroup_of K) = H ⊓ K
@[simp]
theorem
subgroup.subgroup_of_map_subtype
{G : Type u_1}
[group G]
(H K : subgroup G) :
subgroup.map K.subtype (H.subgroup_of K) = H ⊓ K
@[simp]
theorem
add_subgroup.bot_add_subgroup_of
{G : Type u_1}
[add_group G]
(H : add_subgroup G) :
⊥.add_subgroup_of H = ⊥
@[simp]
@[simp]
@[simp]
theorem
add_subgroup.top_add_subgroup_of
{G : Type u_1}
[add_group G]
(H : add_subgroup G) :
⊤.add_subgroup_of H = ⊤
theorem
add_subgroup.add_subgroup_of_bot_eq_bot
{G : Type u_1}
[add_group G]
(H : add_subgroup G) :
H.add_subgroup_of ⊥ = ⊥
theorem
subgroup.subgroup_of_bot_eq_bot
{G : Type u_1}
[group G]
(H : subgroup G) :
H.subgroup_of ⊥ = ⊥
theorem
add_subgroup.add_subgroup_of_bot_eq_top
{G : Type u_1}
[add_group G]
(H : add_subgroup G) :
H.add_subgroup_of ⊥ = ⊤
theorem
subgroup.subgroup_of_bot_eq_top
{G : Type u_1}
[group G]
(H : subgroup G) :
H.subgroup_of ⊥ = ⊤
@[simp]
@[simp]
theorem
add_subgroup.add_subgroup_of_self
{G : Type u_1}
[add_group G]
(H : add_subgroup G) :
H.add_subgroup_of H = ⊤
@[simp]
theorem
add_subgroup.add_subgroup_of_inj
{G : Type u_1}
[add_group G]
{H₁ H₂ K : add_subgroup G} :
H₁.add_subgroup_of K = H₂.add_subgroup_of K ↔ H₁ ⊓ K = H₂ ⊓ K
@[simp]
theorem
subgroup.subgroup_of_inj
{G : Type u_1}
[group G]
{H₁ H₂ K : subgroup G} :
H₁.subgroup_of K = H₂.subgroup_of K ↔ H₁ ⊓ K = H₂ ⊓ K
@[simp]
theorem
add_subgroup.inf_add_subgroup_of_right
{G : Type u_1}
[add_group G]
(H K : add_subgroup G) :
(H ⊓ K).add_subgroup_of K = H.add_subgroup_of K
@[simp]
theorem
subgroup.inf_subgroup_of_right
{G : Type u_1}
[group G]
(H K : subgroup G) :
(H ⊓ K).subgroup_of K = H.subgroup_of K
@[simp]
theorem
add_subgroup.inf_add_subgroup_of_left
{G : Type u_1}
[add_group G]
(H K : add_subgroup G) :
(K ⊓ H).add_subgroup_of K = H.add_subgroup_of K
@[simp]
theorem
subgroup.inf_subgroup_of_left
{G : Type u_1}
[group G]
(H K : subgroup G) :
(K ⊓ H).subgroup_of K = H.subgroup_of K
@[simp]
theorem
subgroup.subgroup_of_eq_bot
{G : Type u_1}
[group G]
{H K : subgroup G} :
H.subgroup_of K = ⊥ ↔ disjoint H K
@[simp]
theorem
add_subgroup.add_subgroup_of_eq_bot
{G : Type u_1}
[add_group G]
{H K : add_subgroup G} :
H.add_subgroup_of K = ⊥ ↔ disjoint H K
@[simp]
theorem
add_subgroup.add_subgroup_of_eq_top
{G : Type u_1}
[add_group G]
{H K : add_subgroup G} :
H.add_subgroup_of K = ⊤ ↔ K ≤ H
@[simp]
theorem
subgroup.subgroup_of_eq_top
{G : Type u_1}
[group G]
{H K : subgroup G} :
H.subgroup_of K = ⊤ ↔ K ≤ H
def
add_subgroup.prod
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(H : add_subgroup G)
(K : add_subgroup N) :
add_subgroup (G × N)
Given add_subgroups H, K of add_groups A, B respectively, H × K
as an add_subgroup of A × B.
Equations
Instances for add_subgroup.prod
theorem
add_subgroup.coe_prod
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(H : add_subgroup G)
(K : add_subgroup N) :
theorem
add_subgroup.prod_mono_right
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(K : add_subgroup G) :
monotone (λ (t : add_subgroup N), K.prod t)
theorem
add_subgroup.prod_mono_left
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(H : add_subgroup N) :
monotone (λ (K : add_subgroup G), K.prod H)
theorem
add_subgroup.prod_top
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(K : add_subgroup G) :
K.prod ⊤ = add_subgroup.comap (add_monoid_hom.fst G N) K
theorem
subgroup.prod_top
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
(K : subgroup G) :
K.prod ⊤ = subgroup.comap (monoid_hom.fst G N) K
theorem
add_subgroup.top_prod
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(H : add_subgroup N) :
⊤.prod H = add_subgroup.comap (add_monoid_hom.snd G N) H
theorem
subgroup.top_prod
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
(H : subgroup N) :
⊤.prod H = subgroup.comap (monoid_hom.snd G N) H
theorem
add_subgroup.le_prod_iff
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{H : add_subgroup G}
{K : add_subgroup N}
{J : add_subgroup (G × N)} :
J ≤ H.prod K ↔ add_subgroup.map (add_monoid_hom.fst G N) J ≤ H ∧ add_subgroup.map (add_monoid_hom.snd G N) J ≤ K
theorem
subgroup.le_prod_iff
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{H : subgroup G}
{K : subgroup N}
{J : subgroup (G × N)} :
J ≤ H.prod K ↔ subgroup.map (monoid_hom.fst G N) J ≤ H ∧ subgroup.map (monoid_hom.snd G N) J ≤ K
theorem
subgroup.prod_le_iff
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{H : subgroup G}
{K : subgroup N}
{J : subgroup (G × N)} :
H.prod K ≤ J ↔ subgroup.map (monoid_hom.inl G N) H ≤ J ∧ subgroup.map (monoid_hom.inr G N) K ≤ J
theorem
add_subgroup.prod_le_iff
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{H : add_subgroup G}
{K : add_subgroup N}
{J : add_subgroup (G × N)} :
H.prod K ≤ J ↔ add_subgroup.map (add_monoid_hom.inl G N) H ≤ J ∧ add_subgroup.map (add_monoid_hom.inr G N) K ≤ J
def
add_subgroup.prod_equiv
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(H : add_subgroup G)
(K : add_subgroup N) :
Product of additive subgroups is isomorphic to their product as additive groups
def
add_submonoid.pi
{η : Type u_6}
{f : η → Type u_7}
[Π (i : η), add_zero_class (f i)]
(I : set η)
(s : Π (i : η), add_submonoid (f i)) :
add_submonoid (Π (i : η), f i)
A version of set.pi for add_submonoids. Given an index set I and a family
of submodules s : Π i, add_submonoid f i, pi I s is the add_submonoid of dependent functions
f : Π i, f i such that f i belongs to pi I s whenever i ∈ I. -/
def
submonoid.pi
{η : Type u_6}
{f : η → Type u_7}
[Π (i : η), mul_one_class (f i)]
(I : set η)
(s : Π (i : η), submonoid (f i)) :
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.
def
add_subgroup.pi
{η : Type u_6}
{f : η → Type u_7}
[Π (i : η), add_group (f i)]
(I : set η)
(H : Π (i : η), add_subgroup (f i)) :
add_subgroup (Π (i : η), f i)
A version of set.pi for add_subgroups. Given an index set I and a family
of submodules s : Π i, add_subgroup f i, pi I s is the add_subgroup of dependent functions
f : Π i, f i such that f i belongs to pi I s whenever i ∈ I. -/
Equations
- add_subgroup.pi I H = {carrier := (add_submonoid.pi I (λ (i : η), (H i).to_add_submonoid)).carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}
def
subgroup.pi
{η : Type u_6}
{f : η → Type u_7}
[Π (i : η), group (f i)]
(I : set η)
(H : Π (i : η), subgroup (f i)) :
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
- subgroup.pi I H = {carrier := (submonoid.pi I (λ (i : η), (H i).to_submonoid)).carrier, mul_mem' := _, one_mem' := _, inv_mem' := _}
theorem
add_subgroup.coe_pi
{η : Type u_6}
{f : η → Type u_7}
[Π (i : η), add_group (f i)]
(I : set η)
(H : Π (i : η), add_subgroup (f i)) :
↑(add_subgroup.pi I H) = I.pi (λ (i : η), ↑(H i))
theorem
add_subgroup.pi_empty
{η : Type u_6}
{f : η → Type u_7}
[Π (i : η), add_group (f i)]
(H : Π (i : η), add_subgroup (f i)) :
add_subgroup.pi ∅ H = ⊤
theorem
add_subgroup.le_pi_iff
{η : Type u_6}
{f : η → Type u_7}
[Π (i : η), add_group (f i)]
{I : set η}
{H : Π (i : η), add_subgroup (f i)}
{J : add_subgroup (Π (i : η), f i)} :
J ≤ add_subgroup.pi I H ↔ ∀ (i : η), i ∈ I → add_subgroup.map (pi.eval_add_monoid_hom f i) J ≤ H i
@[simp]
theorem
subgroup.mul_single_mem_pi
{η : Type u_6}
{f : η → Type u_7}
[Π (i : η), group (f i)]
[decidable_eq η]
{I : set η}
{H : Π (i : η), subgroup (f i)}
(i : η)
(x : f i) :
pi.mul_single i x ∈ subgroup.pi I H ↔ i ∈ I → x ∈ H i
@[simp]
theorem
add_subgroup.single_mem_pi
{η : Type u_6}
{f : η → Type u_7}
[Π (i : η), add_group (f i)]
[decidable_eq η]
{I : set η}
{H : Π (i : η), add_subgroup (f i)}
(i : η)
(x : f i) :
@[class]
A subgroup is normal if whenever n ∈ H, then g * n * g⁻¹ ∈ H for every g : G
Instances of this typeclass
- subgroup.normal_of_comm
- subgroup.normal_of_characteristic
- subgroup.normal_in_normalizer
- monoid_hom.normal_ker
- subgroup.normal_comap
- subgroup.normal_subgroup_of
- subgroup.normal_closure_normal
- subgroup.normal_core_normal
- subgroup.prod_subgroup_of_prod_normal
- subgroup.prod_normal
- subgroup.normal_inf_normal
- conj_act.normal_of_characteristic_of_normal
- subgroup.sup_normal
- quotient_group.map_normal
- subgroup.commutator_normal
- commutator.normal
- principal_ideals.normal
- upper_central_series_step.subgroup.normal
- upper_central_series.subgroup.normal
- lower_central_series.subgroup.normal
- alternating_group.normal
@[class]
An add_subgroup is normal if whenever n ∈ H, then g + n - g ∈ H for every g : G
Instances of this typeclass
- add_subgroup.normal_of_comm
- add_subgroup.normal_of_characteristic
- add_subgroup.normal_in_normalizer
- add_monoid_hom.normal_ker
- add_subgroup.normal_comap
- add_subgroup.normal_add_subgroup_of
- add_subgroup.sum_add_subgroup_of_sum_normal
- add_subgroup.sum_normal
- add_subgroup.normal_inf_normal
- quotient_add_group.map_normal
@[protected, instance]
@[protected, instance]
theorem
add_subgroup.normal.mem_comm
{G : Type u_1}
[add_group G]
{H : add_subgroup G}
(nH : H.normal)
{a b : G}
(h : a + b ∈ H) :
@[class]
- fixed : ∀ (ϕ : G ≃* G), subgroup.comap ϕ.to_monoid_hom H = H
A subgroup is characteristic if it is fixed by all automorphisms.
Several equivalent conditions are provided by lemmas of the form characteristic.iff...
@[protected, instance]
def
subgroup.normal_of_characteristic
{G : Type u_1}
[group G]
(H : subgroup G)
[h : H.characteristic] :
H.normal
@[class]
- fixed : ∀ (ϕ : A ≃+ A), add_subgroup.comap ϕ.to_add_monoid_hom H = H
A add_subgroup is characteristic if it is fixed by all automorphisms.
Several equivalent conditions are provided by lemmas of the form characteristic.iff...
@[protected, instance]
def
add_subgroup.normal_of_characteristic
{A : Type u_3}
[add_group A]
(H : add_subgroup A)
[h : H.characteristic] :
H.normal
theorem
add_subgroup.characteristic_iff_comap_eq
{G : Type u_1}
[add_group G]
{H : add_subgroup G} :
H.characteristic ↔ ∀ (ϕ : G ≃+ G), add_subgroup.comap ϕ.to_add_monoid_hom H = H
theorem
subgroup.characteristic_iff_comap_eq
{G : Type u_1}
[group G]
{H : subgroup G} :
H.characteristic ↔ ∀ (ϕ : G ≃* G), subgroup.comap ϕ.to_monoid_hom H = H
theorem
add_subgroup.characteristic_iff_comap_le
{G : Type u_1}
[add_group G]
{H : add_subgroup G} :
H.characteristic ↔ ∀ (ϕ : G ≃+ G), add_subgroup.comap ϕ.to_add_monoid_hom H ≤ H
theorem
subgroup.characteristic_iff_comap_le
{G : Type u_1}
[group G]
{H : subgroup G} :
H.characteristic ↔ ∀ (ϕ : G ≃* G), subgroup.comap ϕ.to_monoid_hom H ≤ H
theorem
add_subgroup.characteristic_iff_le_comap
{G : Type u_1}
[add_group G]
{H : add_subgroup G} :
H.characteristic ↔ ∀ (ϕ : G ≃+ G), H ≤ add_subgroup.comap ϕ.to_add_monoid_hom H
theorem
subgroup.characteristic_iff_le_comap
{G : Type u_1}
[group G]
{H : subgroup G} :
H.characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ subgroup.comap ϕ.to_monoid_hom H
theorem
subgroup.characteristic_iff_map_eq
{G : Type u_1}
[group G]
{H : subgroup G} :
H.characteristic ↔ ∀ (ϕ : G ≃* G), subgroup.map ϕ.to_monoid_hom H = H
theorem
add_subgroup.characteristic_iff_map_eq
{G : Type u_1}
[add_group G]
{H : add_subgroup G} :
H.characteristic ↔ ∀ (ϕ : G ≃+ G), add_subgroup.map ϕ.to_add_monoid_hom H = H
theorem
subgroup.characteristic_iff_map_le
{G : Type u_1}
[group G]
{H : subgroup G} :
H.characteristic ↔ ∀ (ϕ : G ≃* G), subgroup.map ϕ.to_monoid_hom H ≤ H
theorem
add_subgroup.characteristic_iff_map_le
{G : Type u_1}
[add_group G]
{H : add_subgroup G} :
H.characteristic ↔ ∀ (ϕ : G ≃+ G), add_subgroup.map ϕ.to_add_monoid_hom H ≤ H
theorem
add_subgroup.characteristic_iff_le_map
{G : Type u_1}
[add_group G]
{H : add_subgroup G} :
H.characteristic ↔ ∀ (ϕ : G ≃+ G), H ≤ add_subgroup.map ϕ.to_add_monoid_hom H
theorem
subgroup.characteristic_iff_le_map
{G : Type u_1}
[group G]
{H : subgroup G} :
H.characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ subgroup.map ϕ.to_monoid_hom H
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
The center of an additive group G is the set of elements that commute with
everything in G
Equations
- add_subgroup.center G = {carrier := set.add_center G (add_zero_class.to_has_add G), add_mem' := _, zero_mem' := _, neg_mem' := _}
Instances for add_subgroup.center
The center of a group G is the set of elements that commute with everything in G
Equations
- subgroup.center G = {carrier := set.center G (mul_one_class.to_has_mul G), mul_mem' := _, one_mem' := _, inv_mem' := _}
Instances for subgroup.center
Instances for ↥subgroup.center
@[simp]
@[simp]
@[protected, instance]
def
subgroup.decidable_mem_center
{G : Type u_1}
[group G]
(z : G)
[decidable (∀ (g : G), g * z = z * g)] :
decidable (z ∈ subgroup.center G)
Equations
- subgroup.decidable_mem_center z = decidable_of_iff' (∀ (g : G), g * z = z * g) subgroup.mem_center_iff
@[protected, instance]
@[protected, instance]
A group is commutative if the center is the whole group
Equations
- group.comm_group_of_center_eq_top h = {mul := group.mul _inst_1, mul_assoc := _, one := group.one _inst_1, one_mul := _, mul_one := _, npow := group.npow _inst_1, npow_zero' := _, npow_succ' := _, inv := group.inv _inst_1, div := group.div _inst_1, div_eq_mul_inv := _, zpow := group.zpow _inst_1, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}
The normalizer of H is the largest subgroup of G inside which H is normal.
The set_normalizer of S is the subgroup of G whose elements satisfy g*S*g⁻¹=S
The set_normalizer of S is the subgroup of G whose elements satisfy
g+S-g=S.
theorem
add_subgroup.mem_normalizer_iff''
{G : Type u_1}
[add_group G]
{H : add_subgroup G}
{g : G} :
theorem
add_subgroup.mem_normalizer_iff'
{G : Type u_1}
[add_group G]
{H : add_subgroup G}
{g : G} :
theorem
add_subgroup.le_normalizer
{G : Type u_1}
[add_group G]
{H : add_subgroup G} :
H ≤ H.normalizer
@[protected, instance]
def
add_subgroup.normal_in_normalizer
{G : Type u_1}
[add_group G]
{H : add_subgroup G} :
(H.add_subgroup_of H.normalizer).normal
@[protected, instance]
def
subgroup.normal_in_normalizer
{G : Type u_1}
[group G]
{H : subgroup G} :
(H.subgroup_of H.normalizer).normal
theorem
add_subgroup.normalizer_eq_top
{G : Type u_1}
[add_group G]
{H : add_subgroup G} :
H.normalizer = ⊤ ↔ H.normal
theorem
subgroup.normalizer_eq_top
{G : Type u_1}
[group G]
{H : subgroup G} :
H.normalizer = ⊤ ↔ H.normal
theorem
subgroup.le_normalizer_of_normal
{G : Type u_1}
[group G]
{H K : subgroup G}
[hK : (H.subgroup_of K).normal]
(HK : H ≤ K) :
K ≤ H.normalizer
theorem
add_subgroup.le_normalizer_of_normal
{G : Type u_1}
[add_group G]
{H K : add_subgroup G}
[hK : (H.add_subgroup_of K).normal]
(HK : H ≤ K) :
K ≤ H.normalizer
theorem
subgroup.le_normalizer_comap
{G : Type u_1}
[group G]
{H : subgroup G}
{N : Type u_4}
[group N]
(f : N →* G) :
subgroup.comap f H.normalizer ≤ (subgroup.comap f H).normalizer
The preimage of the normalizer is contained in the normalizer of the preimage.
theorem
add_subgroup.le_normalizer_comap
{G : Type u_1}
[add_group G]
{H : add_subgroup G}
{N : Type u_4}
[add_group N]
(f : N →+ G) :
The preimage of the normalizer is contained in the normalizer of the preimage.
theorem
subgroup.le_normalizer_map
{G : Type u_1}
[group G]
{H : subgroup G}
{N : Type u_4}
[group N]
(f : G →* N) :
subgroup.map f H.normalizer ≤ (subgroup.map f H).normalizer
The image of the normalizer is contained in the normalizer of the image.
theorem
add_subgroup.le_normalizer_map
{G : Type u_1}
[add_group G]
{H : add_subgroup G}
{N : Type u_4}
[add_group N]
(f : G →+ N) :
add_subgroup.map f H.normalizer ≤ (add_subgroup.map f H).normalizer
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
- normalizer_condition G = ∀ (H : subgroup G), H < ⊤ → H < H.normalizer
theorem
normalizer_condition_iff_only_full_group_self_normalizing
{G : Type u_1}
[group G] :
normalizer_condition G ↔ ∀ (H : subgroup G), H.normalizer = H → H = ⊤
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.
theorem
subgroup.normalizer_condition.normal_of_coatom
{G : Type u_1}
[group G]
(H : subgroup G)
(hnc : normalizer_condition G)
(hmax : is_coatom H) :
H.normal
In a group that satisifes the normalizer condition, every maximal subgroup is normal
The centralizer of H is the subgroup of g : G commuting with every h : H.
Equations
- subgroup.centralizer s = {carrier := s.centralizer (mul_one_class.to_has_mul G), mul_mem' := _, one_mem' := _, inv_mem' := _}
Instances for subgroup.centralizer
The centralizer of H is the additive subgroup of g : G commuting with
every h : H.
Equations
- add_subgroup.centralizer s = {carrier := s.add_centralizer (add_zero_class.to_has_add G), add_mem' := _, zero_mem' := _, neg_mem' := _}
Instances for add_subgroup.centralizer
theorem
subgroup.le_centralizer_iff
{G : Type u_1}
[group G]
{H K : subgroup G} :
H ≤ subgroup.centralizer ↑K ↔ K ≤ subgroup.centralizer ↑H
@[simp]
theorem
add_subgroup.centralizer_eq_top_iff_subset
{G : Type u_1}
[add_group G]
{s : set G} :
add_subgroup.centralizer s = ⊤ ↔ s ⊆ ↑(add_subgroup.center G)
@[simp]
theorem
subgroup.centralizer_eq_top_iff_subset
{G : Type u_1}
[group G]
{s : set G} :
subgroup.centralizer s = ⊤ ↔ s ⊆ ↑(subgroup.center G)
@[protected, instance]
def
add_subgroup.subgroup.centralizer.characteristic
{G : Type u_1}
[add_group G]
{H : add_subgroup G}
[hH : H.characteristic] :
@[protected, instance]
def
subgroup.subgroup.centralizer.characteristic
{G : Type u_1}
[group G]
{H : subgroup G}
[hH : H.characteristic] :
@[class]
- is_comm : is_commutative ↥H has_mul.mul
Commutivity of a subgroup
Instances of this typeclass
@[class]
- is_comm : is_commutative ↥H has_add.add
Commutivity of an additive subgroup
Instances of this typeclass
@[protected, instance]
def
add_subgroup.is_commutative.add_comm_group
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
[h : H.is_commutative] :
A commutative subgroup is commutative.
Equations
- add_subgroup.is_commutative.add_comm_group H = {add := add_group.add H.to_add_group, add_assoc := _, zero := add_group.zero H.to_add_group, zero_add := _, add_zero := _, nsmul := add_group.nsmul H.to_add_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg H.to_add_group, sub := add_group.sub H.to_add_group, sub_eq_add_neg := _, zsmul := add_group.zsmul H.to_add_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
@[protected, instance]
def
subgroup.is_commutative.comm_group
{G : Type u_1}
[group G]
(H : subgroup G)
[h : H.is_commutative] :
A commutative subgroup is commutative.
Equations
- subgroup.is_commutative.comm_group H = {mul := group.mul H.to_group, mul_assoc := _, one := group.one H.to_group, one_mul := _, mul_one := _, npow := group.npow H.to_group, npow_zero' := _, npow_succ' := _, inv := group.inv H.to_group, div := group.div H.to_group, div_eq_mul_inv := _, zpow := group.zpow H.to_group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}
@[protected, instance]
@[protected, instance]
def
add_subgroup.map_is_commutative
{G : Type u_1}
{G' : Type u_2}
[add_group G]
[add_group G']
(H : add_subgroup G)
(f : G →+ G')
[H.is_commutative] :
@[protected, instance]
def
subgroup.map_is_commutative
{G : Type u_1}
{G' : Type u_2}
[group G]
[group G']
(H : subgroup G)
(f : G →* G')
[H.is_commutative] :
(subgroup.map f H).is_commutative
theorem
subgroup.comap_injective_is_commutative
{G : Type u_1}
{G' : Type u_2}
[group G]
[group G']
(H : subgroup G)
{f : G' →* G}
(hf : function.injective ⇑f)
[H.is_commutative] :
(subgroup.comap f H).is_commutative
theorem
add_subgroup.comap_injective_is_commutative
{G : Type u_1}
{G' : Type u_2}
[add_group G]
[add_group G']
(H : add_subgroup G)
{f : G' →+ G}
(hf : function.injective ⇑f)
[H.is_commutative] :
@[protected, instance]
def
subgroup.subgroup_of_is_commutative
{G : Type u_1}
[group G]
(H : subgroup G)
{K : subgroup G}
[H.is_commutative] :
(H.subgroup_of K).is_commutative
@[protected, instance]
def
add_subgroup.add_subgroup_of_is_commutative
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
{K : add_subgroup G}
[H.is_commutative] :
theorem
add_subgroup.le_centralizer_iff_is_commutative
{G : Type u_1}
[add_group G]
{K : add_subgroup G} :
theorem
add_subgroup.le_centralizer
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
[h : H.is_commutative] :
Given a set s, conjugates_of_set s is the set of all conjugates of
the elements of s.
Equations
- group.conjugates_of_set s = ⋃ (a : G) (H : a ∈ s), conjugates_of a
theorem
group.conjugates_subset_normal
{G : Type u_1}
[group G]
{N : subgroup G}
[tn : N.normal]
{a : G}
(h : a ∈ N) :
conjugates_of a ⊆ ↑N
theorem
group.conj_mem_conjugates_of_set
{G : Type u_1}
[group G]
{s : set G}
{x c : G} :
x ∈ group.conjugates_of_set s → c * x * c⁻¹ ∈ group.conjugates_of_set s
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 subgroup.normal_closure
theorem
subgroup.subset_normal_closure
{G : Type u_1}
[group G]
{s : set G} :
s ⊆ ↑(subgroup.normal_closure s)
@[protected, instance]
The normal closure of s is a normal subgroup.
@[simp]
@[simp]
@[simp]
The normal core of a subgroup H is the largest normal subgroup of G contained in H,
as shown by subgroup.normal_core_eq_supr.
Equations
Instances for subgroup.normal_core
@[protected, instance]
theorem
subgroup.normal_le_normal_core
{G : Type u_1}
[group G]
{H N : subgroup G}
[hN : N.normal] :
N ≤ H.normal_core ↔ N ≤ H
theorem
subgroup.normal_core_mono
{G : Type u_1}
[group G]
{H K : subgroup G}
(h : H ≤ K) :
H.normal_core ≤ K.normal_core
@[simp]
theorem
subgroup.normal_core_eq_self
{G : Type u_1}
[group G]
(H : subgroup G)
[H.normal] :
H.normal_core = H
@[simp]
The range of an add_monoid_hom from an add_group is an add_subgroup.
Instances for ↥add_monoid_hom.range
The range of a monoid homomorphism from a group is a subgroup.
Instances for monoid_hom.range
Instances for ↥monoid_hom.range
@[simp]
theorem
add_monoid_hom.restrict_range
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(K : add_subgroup G)
(f : G →+ N) :
(f.restrict K).range = add_subgroup.map f K
The canonical surjective group homomorphism G →* f(G) induced by a group
homomorphism G →* N.
Equations
- f.range_restrict = f.cod_restrict f.range _
def
add_monoid_hom.range_restrict
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(f : G →+ N) :
The canonical surjective add_group homomorphism G →+ f(G) induced by a group
homomorphism G →+ N.
Equations
- f.range_restrict = f.cod_restrict f.range _
theorem
add_monoid_hom.range_top_of_surjective
{G : Type u_1}
[add_group G]
{N : Type u_2}
[add_group N]
(f : G →+ N)
(hf : function.surjective ⇑f) :
The range of a surjective add_monoid homomorphism is the whole of the codomain.
@[simp]
@[simp]
theorem
add_subgroup.inclusion_range
{G : Type u_1}
[add_group G]
{H K : add_subgroup G}
(h_le : H ≤ K) :
(add_subgroup.inclusion h_le).range = H.add_subgroup_of K
@[simp]
theorem
subgroup.inclusion_range
{G : Type u_1}
[group G]
{H K : subgroup G}
(h_le : H ≤ K) :
(subgroup.inclusion h_le).range = H.subgroup_of K
theorem
monoid_hom.subgroup_of_range_eq_of_le
{G₁ : Type u_1}
{G₂ : Type u_2}
[group G₁]
[group G₂]
{K : subgroup G₂}
(f : G₁ →* G₂)
(h : f.range ≤ K) :
f.range.subgroup_of K = (f.cod_restrict K _).range
theorem
add_monoid_hom.add_subgroup_of_range_eq_of_le
{G₁ : Type u_1}
{G₂ : Type u_2}
[add_group G₁]
[add_group G₂]
{K : add_subgroup G₂}
(f : G₁ →+ G₂)
(h : f.range ≤ K) :
f.range.add_subgroup_of K = (f.cod_restrict K _).range
def
monoid_hom.of_left_inverse
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{f : G →* N}
{g : N →* G}
(h : function.left_inverse ⇑g ⇑f) :
Computable alternative to monoid_hom.of_injective.
def
add_monoid_hom.of_left_inverse
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{f : G →+ N}
{g : N →+ G}
(h : function.left_inverse ⇑g ⇑f) :
Computable alternative to add_monoid_hom.of_injective.
noncomputable
def
monoid_hom.of_injective
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{f : G →* N}
(hf : function.injective ⇑f) :
The range of an injective group homomorphism is isomorphic to its domain.
Equations
- monoid_hom.of_injective hf = mul_equiv.of_bijective (f.cod_restrict f.range monoid_hom.of_injective._proof_3) _
noncomputable
def
add_monoid_hom.of_injective
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{f : G →+ N}
(hf : function.injective ⇑f) :
The range of an injective additive group homomorphism is isomorphic to its domain.
Equations
- add_monoid_hom.of_injective hf = add_equiv.of_bijective (f.cod_restrict f.range add_monoid_hom.of_injective._proof_3) _
theorem
monoid_hom.of_injective_apply
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{f : G →* N}
(hf : function.injective ⇑f)
{x : G} :
↑(⇑(monoid_hom.of_injective hf) x) = ⇑f x
theorem
add_monoid_hom.of_injective_apply
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{f : G →+ N}
(hf : function.injective ⇑f)
{x : G} :
↑(⇑(add_monoid_hom.of_injective hf) x) = ⇑f x
def
monoid_hom.ker
{G : Type u_1}
[group G]
{M : Type u_6}
[mul_one_class M]
(f : G →* M) :
subgroup G
The multiplicative kernel of a monoid homomorphism is the subgroup of elements x : G such that
f x = 1
Equations
Instances for monoid_hom.ker
def
add_monoid_hom.ker
{G : Type u_1}
[add_group G]
{M : Type u_6}
[add_zero_class M]
(f : G →+ M) :
The additive kernel of an add_monoid homomorphism is the add_subgroup of elements
such that f x = 0
Equations
Instances for add_monoid_hom.ker
@[simp]
theorem
add_monoid_hom.ker_to_hom_add_units
{G : Type u_1}
[add_group G]
{M : Type u_2}
[add_monoid M]
(f : G →+ M) :
f.to_hom_add_units.ker = f.ker
@[protected, instance]
def
monoid_hom.decidable_mem_ker
{G : Type u_1}
[group G]
{M : Type u_6}
[mul_one_class M]
[decidable_eq M]
(f : G →* M) :
decidable_pred (λ (_x : G), _x ∈ f.ker)
Equations
- f.decidable_mem_ker = λ (x : G), decidable_of_iff (⇑f x = 1) _
@[protected, instance]
def
add_monoid_hom.decidable_mem_ker
{G : Type u_1}
[add_group G]
{M : Type u_6}
[add_zero_class M]
[decidable_eq M]
(f : G →+ M) :
decidable_pred (λ (_x : G), _x ∈ f.ker)
Equations
- f.decidable_mem_ker = λ (x : G), decidable_of_iff (⇑f x = 0) _
@[simp]
theorem
add_monoid_hom.ker_restrict
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(K : add_subgroup G)
(f : G →+ N) :
(f.restrict K).ker = f.ker.add_subgroup_of K
@[simp]
@[simp]
@[simp]
theorem
monoid_hom.ker_eq_bot_iff
{G : Type u_1}
[group G]
{M : Type u_6}
[mul_one_class M]
(f : G →* M) :
theorem
add_monoid_hom.ker_eq_bot_iff
{G : Type u_1}
[add_group G]
{M : Type u_6}
[add_zero_class M]
(f : G →+ M) :
@[simp]
@[simp]
theorem
subgroup.ker_inclusion
{G : Type u_1}
[group G]
{H K : subgroup G}
(h : H ≤ K) :
(subgroup.inclusion h).ker = ⊥
@[simp]
theorem
add_subgroup.ker_inclusion
{G : Type u_1}
[add_group G]
{H K : add_subgroup G}
(h : H ≤ K) :
(add_subgroup.inclusion h).ker = ⊥
theorem
add_monoid_hom.sum_map_comap_sum
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{G' : Type u_2}
{N' : Type u_3}
[add_group G']
[add_group N']
(f : G →+ N)
(g : G' →+ N')
(S : add_subgroup N)
(S' : add_subgroup N') :
add_subgroup.comap (f.prod_map g) (S.prod S') = (add_subgroup.comap f S).prod (add_subgroup.comap g S')
theorem
monoid_hom.prod_map_comap_prod
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{G' : Type u_2}
{N' : Type u_3}
[group G']
[group N']
(f : G →* N)
(g : G' →* N')
(S : subgroup N)
(S' : subgroup N') :
subgroup.comap (f.prod_map g) (S.prod S') = (subgroup.comap f S).prod (subgroup.comap g S')
@[protected, instance]
@[protected, instance]
def
add_monoid_hom.normal_ker
{G : Type u_1}
[add_group G]
{M : Type u_6}
[add_zero_class M]
(f : G →+ M) :
theorem
add_monoid_hom.eq_of_eq_on_dense
{G : Type u_1}
[add_group G]
{M : Type u_6}
[add_monoid M]
{s : set G}
(hs : add_subgroup.closure s = ⊤)
{f g : G →+ M}
(h : set.eq_on ⇑f ⇑g s) :
f = g
theorem
add_monoid_hom.closure_preimage_le
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(f : G →+ N)
(s : set N) :
add_subgroup.closure (⇑f ⁻¹' s) ≤ add_subgroup.comap f (add_subgroup.closure s)
theorem
monoid_hom.closure_preimage_le
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
(f : G →* N)
(s : set N) :
subgroup.closure (⇑f ⁻¹' s) ≤ subgroup.comap f (subgroup.closure s)
theorem
add_monoid_hom.map_closure
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(f : G →+ N)
(s : set G) :
add_subgroup.map f (add_subgroup.closure s) = add_subgroup.closure (⇑f '' s)
The image under an add_monoid hom of the add_subgroup generated by a set equals
the add_subgroup generated by the image of the set.
theorem
monoid_hom.map_closure
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
(f : G →* N)
(s : set G) :
subgroup.map f (subgroup.closure s) = subgroup.closure (⇑f '' s)
The image under a monoid homomorphism of the subgroup generated by a set equals the subgroup generated by the image of the set.
theorem
subgroup.normal.map
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{H : subgroup G}
(h : H.normal)
(f : G →* N)
(hf : function.surjective ⇑f) :
(subgroup.map f H).normal
theorem
add_subgroup.normal.map
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{H : add_subgroup G}
(h : H.normal)
(f : G →+ N)
(hf : function.surjective ⇑f) :
(add_subgroup.map f H).normal
theorem
add_subgroup.map_eq_bot_iff
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(H : add_subgroup G)
{f : G →+ N} :
theorem
add_subgroup.map_eq_bot_iff_of_injective
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(H : add_subgroup G)
{f : G →+ N}
(hf : function.injective ⇑f) :
theorem
add_subgroup.map_le_range
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(f : G →+ N)
(H : add_subgroup G) :
add_subgroup.map f H ≤ f.range
theorem
subgroup.map_subtype_le
{G : Type u_1}
[group G]
{H : subgroup G}
(K : subgroup ↥H) :
subgroup.map H.subtype K ≤ H
theorem
add_subgroup.map_subtype_le
{G : Type u_1}
[add_group G]
{H : add_subgroup G}
(K : add_subgroup ↥H) :
add_subgroup.map H.subtype K ≤ H
theorem
add_subgroup.ker_le_comap
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(f : G →+ N)
(H : add_subgroup N) :
f.ker ≤ add_subgroup.comap f H
theorem
add_subgroup.map_comap_le
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(f : G →+ N)
(H : add_subgroup N) :
add_subgroup.map f (add_subgroup.comap f H) ≤ H
theorem
subgroup.map_comap_le
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
(f : G →* N)
(H : subgroup N) :
subgroup.map f (subgroup.comap f H) ≤ H
theorem
subgroup.le_comap_map
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
(f : G →* N)
(H : subgroup G) :
H ≤ subgroup.comap f (subgroup.map f H)
theorem
add_subgroup.le_comap_map
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(f : G →+ N)
(H : add_subgroup G) :
H ≤ add_subgroup.comap f (add_subgroup.map f H)
theorem
add_subgroup.map_comap_eq
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(f : G →+ N)
(H : add_subgroup N) :
add_subgroup.map f (add_subgroup.comap f H) = f.range ⊓ H
theorem
subgroup.map_comap_eq
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
(f : G →* N)
(H : subgroup N) :
subgroup.map f (subgroup.comap f H) = f.range ⊓ H
theorem
add_subgroup.comap_map_eq
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(f : G →+ N)
(H : add_subgroup G) :
add_subgroup.comap f (add_subgroup.map f H) = H ⊔ f.ker
theorem
subgroup.comap_map_eq
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
(f : G →* N)
(H : subgroup G) :
subgroup.comap f (subgroup.map f H) = H ⊔ f.ker
theorem
add_subgroup.map_comap_eq_self
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{f : G →+ N}
{H : add_subgroup N}
(h : H ≤ f.range) :
add_subgroup.map f (add_subgroup.comap f H) = H
theorem
subgroup.map_comap_eq_self
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{f : G →* N}
{H : subgroup N}
(h : H ≤ f.range) :
subgroup.map f (subgroup.comap f H) = H
theorem
add_subgroup.map_comap_eq_self_of_surjective
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{f : G →+ N}
(h : function.surjective ⇑f)
(H : add_subgroup N) :
add_subgroup.map f (add_subgroup.comap f H) = H
theorem
subgroup.map_comap_eq_self_of_surjective
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{f : G →* N}
(h : function.surjective ⇑f)
(H : subgroup N) :
subgroup.map f (subgroup.comap f H) = H
theorem
subgroup.comap_le_comap_of_le_range
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{f : G →* N}
{K L : subgroup N}
(hf : K ≤ f.range) :
subgroup.comap f K ≤ subgroup.comap f L ↔ K ≤ L
theorem
add_subgroup.comap_le_comap_of_le_range
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{f : G →+ N}
{K L : add_subgroup N}
(hf : K ≤ f.range) :
add_subgroup.comap f K ≤ add_subgroup.comap f L ↔ K ≤ L
theorem
subgroup.comap_le_comap_of_surjective
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{f : G →* N}
{K L : subgroup N}
(hf : function.surjective ⇑f) :
subgroup.comap f K ≤ subgroup.comap f L ↔ K ≤ L
theorem
add_subgroup.comap_le_comap_of_surjective
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{f : G →+ N}
{K L : add_subgroup N}
(hf : function.surjective ⇑f) :
add_subgroup.comap f K ≤ add_subgroup.comap f L ↔ K ≤ L
theorem
subgroup.comap_lt_comap_of_surjective
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{f : G →* N}
{K L : subgroup N}
(hf : function.surjective ⇑f) :
subgroup.comap f K < subgroup.comap f L ↔ K < L
theorem
add_subgroup.comap_lt_comap_of_surjective
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{f : G →+ N}
{K L : add_subgroup N}
(hf : function.surjective ⇑f) :
add_subgroup.comap f K < add_subgroup.comap f L ↔ K < L
theorem
subgroup.comap_injective
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{f : G →* N}
(h : function.surjective ⇑f) :
theorem
add_subgroup.comap_injective
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{f : G →+ N}
(h : function.surjective ⇑f) :
theorem
subgroup.comap_map_eq_self
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{f : G →* N}
{H : subgroup G}
(h : f.ker ≤ H) :
subgroup.comap f (subgroup.map f H) = H
theorem
add_subgroup.comap_map_eq_self
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{f : G →+ N}
{H : add_subgroup G}
(h : f.ker ≤ H) :
add_subgroup.comap f (add_subgroup.map f H) = H
theorem
subgroup.comap_map_eq_self_of_injective
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{f : G →* N}
(h : function.injective ⇑f)
(H : subgroup G) :
subgroup.comap f (subgroup.map f H) = H
theorem
add_subgroup.comap_map_eq_self_of_injective
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{f : G →+ N}
(h : function.injective ⇑f)
(H : add_subgroup G) :
add_subgroup.comap f (add_subgroup.map f H) = H
theorem
add_subgroup.map_le_map_iff
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{f : G →+ N}
{H K : add_subgroup G} :
add_subgroup.map f H ≤ add_subgroup.map f K ↔ H ≤ K ⊔ f.ker
theorem
subgroup.map_le_map_iff
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{f : G →* N}
{H K : subgroup G} :
subgroup.map f H ≤ subgroup.map f K ↔ H ≤ K ⊔ f.ker
theorem
add_subgroup.map_le_map_iff'
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{f : G →+ N}
{H K : add_subgroup G} :
add_subgroup.map f H ≤ add_subgroup.map f K ↔ H ⊔ f.ker ≤ K ⊔ f.ker
theorem
add_subgroup.map_eq_map_iff
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{f : G →+ N}
{H K : add_subgroup G} :
add_subgroup.map f H = add_subgroup.map f K ↔ H ⊔ f.ker = K ⊔ f.ker
theorem
subgroup.map_eq_range_iff
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{f : G →* N}
{H : subgroup G} :
subgroup.map f H = f.range ↔ codisjoint H f.ker
theorem
add_subgroup.map_eq_range_iff
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{f : G →+ N}
{H : add_subgroup G} :
add_subgroup.map f H = f.range ↔ codisjoint H f.ker
theorem
subgroup.map_le_map_iff_of_injective
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{f : G →* N}
(hf : function.injective ⇑f)
{H K : subgroup G} :
subgroup.map f H ≤ subgroup.map f K ↔ H ≤ K
theorem
add_subgroup.map_le_map_iff_of_injective
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{f : G →+ N}
(hf : function.injective ⇑f)
{H K : add_subgroup G} :
add_subgroup.map f H ≤ add_subgroup.map f K ↔ H ≤ K
@[simp]
theorem
add_subgroup.map_subtype_le_map_subtype
{G : Type u_1}
[add_group G]
{G' : add_subgroup G}
{H K : add_subgroup ↥G'} :
add_subgroup.map G'.subtype H ≤ add_subgroup.map G'.subtype K ↔ H ≤ K
@[simp]
theorem
subgroup.map_subtype_le_map_subtype
{G : Type u_1}
[group G]
{G' : subgroup G}
{H K : subgroup ↥G'} :
subgroup.map G'.subtype H ≤ subgroup.map G'.subtype K ↔ H ≤ K
theorem
add_subgroup.map_injective
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{f : G →+ N}
(h : function.injective ⇑f) :
theorem
subgroup.map_injective
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{f : G →* N}
(h : function.injective ⇑f) :
theorem
subgroup.map_eq_comap_of_inverse
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{f : G →* N}
{g : N →* G}
(hl : function.left_inverse ⇑g ⇑f)
(hr : function.right_inverse ⇑g ⇑f)
(H : subgroup G) :
subgroup.map f H = subgroup.comap g H
theorem
add_subgroup.map_eq_comap_of_inverse
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{f : G →+ N}
{g : N →+ G}
(hl : function.left_inverse ⇑g ⇑f)
(hr : function.right_inverse ⇑g ⇑f)
(H : add_subgroup G) :
add_subgroup.map f H = add_subgroup.comap g H
theorem
add_subgroup.map_injective_of_ker_le
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(f : G →+ N)
{H K : add_subgroup G}
(hH : f.ker ≤ H)
(hK : f.ker ≤ K)
(hf : add_subgroup.map f H = add_subgroup.map f K) :
H = K
Given f(A) = f(B), ker f ≤ A, and ker f ≤ B, deduce that A = B.
theorem
add_subgroup.closure_preimage_eq_top
{G : Type u_1}
[add_group G]
(s : set G) :
add_subgroup.closure (⇑((add_subgroup.closure s).subtype) ⁻¹' s) = ⊤
theorem
subgroup.closure_preimage_eq_top
{G : Type u_1}
[group G]
(s : set G) :
subgroup.closure (⇑((subgroup.closure s).subtype) ⁻¹' s) = ⊤
theorem
subgroup.comap_sup_eq_of_le_range
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
(f : G →* N)
{H K : subgroup N}
(hH : H ≤ f.range)
(hK : K ≤ f.range) :
subgroup.comap f H ⊔ subgroup.comap f K = subgroup.comap f (H ⊔ K)
theorem
add_subgroup.comap_sup_eq_of_le_range
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(f : G →+ N)
{H K : add_subgroup N}
(hH : H ≤ f.range)
(hK : K ≤ f.range) :
add_subgroup.comap f H ⊔ add_subgroup.comap f K = add_subgroup.comap f (H ⊔ K)
theorem
add_subgroup.comap_sup_eq
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(f : G →+ N)
(H K : add_subgroup N)
(hf : function.surjective ⇑f) :
add_subgroup.comap f H ⊔ add_subgroup.comap f K = add_subgroup.comap f (H ⊔ K)
theorem
subgroup.comap_sup_eq
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
(f : G →* N)
(H K : subgroup N)
(hf : function.surjective ⇑f) :
subgroup.comap f H ⊔ subgroup.comap f K = subgroup.comap f (H ⊔ K)
theorem
subgroup.sup_subgroup_of_eq
{G : Type u_1}
[group G]
{H K L : subgroup G}
(hH : H ≤ L)
(hK : K ≤ L) :
H.subgroup_of L ⊔ K.subgroup_of L = (H ⊔ K).subgroup_of L
theorem
add_subgroup.sup_add_subgroup_of_eq
{G : Type u_1}
[add_group G]
{H K L : add_subgroup G}
(hH : H ≤ L)
(hK : K ≤ L) :
H.add_subgroup_of L ⊔ K.add_subgroup_of L = (H ⊔ K).add_subgroup_of L
theorem
subgroup.codisjoint_subgroup_of_sup
{G : Type u_1}
[group G]
(H K : subgroup G) :
codisjoint (H.subgroup_of (H ⊔ K)) (K.subgroup_of (H ⊔ K))
theorem
add_subgroup.codisjoint_add_subgroup_of_sup
{G : Type u_1}
[add_group G]
(H K : add_subgroup G) :
codisjoint (H.add_subgroup_of (H ⊔ K)) (K.add_subgroup_of (H ⊔ K))
noncomputable
def
subgroup.equiv_map_of_injective
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
(H : subgroup G)
(f : G →* N)
(hf : function.injective ⇑f) :
↥H ≃* ↥(subgroup.map f H)
A subgroup is isomorphic to its image under an injective function. If you have an isomorphism,
use mul_equiv.subgroup_map for better definitional equalities.
noncomputable
def
add_subgroup.equiv_map_of_injective
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(H : add_subgroup G)
(f : G →+ N)
(hf : function.injective ⇑f) :
↥H ≃+ ↥(add_subgroup.map f H)
An additive subgroup is isomorphic to its image under an injective function. If you
have an isomorphism, use add_equiv.add_subgroup_map for better definitional equalities.
@[simp]
theorem
add_subgroup.coe_equiv_map_of_injective_apply
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(H : add_subgroup G)
(f : G →+ N)
(hf : function.injective ⇑f)
(h : ↥H) :
theorem
add_subgroup.comap_normalizer_eq_of_surjective
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(H : add_subgroup G)
{f : N →+ G}
(hf : function.surjective ⇑f) :
The preimage of the normalizer is equal to the normalizer of the preimage of a surjective function.
theorem
subgroup.comap_normalizer_eq_of_surjective
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
(H : subgroup G)
{f : N →* G}
(hf : function.surjective ⇑f) :
subgroup.comap f H.normalizer = (subgroup.comap f H).normalizer
The preimage of the normalizer is equal to the normalizer of the preimage of a surjective function.
theorem
subgroup.comap_normalizer_eq_of_injective_of_le_range
{G : Type u_1}
[group G]
{N : Type u_2}
[group N]
(H : subgroup G)
{f : N →* G}
(hf : function.injective ⇑f)
(h : H.normalizer ≤ f.range) :
subgroup.comap f H.normalizer = (subgroup.comap f H).normalizer
theorem
add_subgroup.comap_normalizer_eq_of_injective_of_le_range
{G : Type u_1}
[add_group G]
{N : Type u_2}
[add_group N]
(H : add_subgroup G)
{f : N →+ G}
(hf : function.injective ⇑f)
(h : H.normalizer ≤ f.range) :
theorem
add_subgroup.add_subgroup_of_normalizer_eq
{G : Type u_1}
[add_group G]
{H N : add_subgroup G}
(h : H.normalizer ≤ N) :
H.normalizer.add_subgroup_of N = (H.add_subgroup_of N).normalizer
theorem
subgroup.subgroup_of_normalizer_eq
{G : Type u_1}
[group G]
{H N : subgroup G}
(h : H.normalizer ≤ N) :
H.normalizer.subgroup_of N = (H.subgroup_of N).normalizer
theorem
add_subgroup.map_equiv_normalizer_eq
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(H : add_subgroup G)
(f : G ≃+ N) :
The image of the normalizer is equal to the normalizer of the image of an isomorphism.
theorem
subgroup.map_normalizer_eq_of_bijective
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
(H : subgroup G)
{f : G →* N}
(hf : function.bijective ⇑f) :
subgroup.map f H.normalizer = (subgroup.map f H).normalizer
The image of the normalizer is equal to the normalizer of the image of a bijective function.
theorem
add_subgroup.map_normalizer_eq_of_bijective
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(H : add_subgroup G)
{f : G →+ N}
(hf : function.bijective ⇑f) :
add_subgroup.map f H.normalizer = (add_subgroup.map f H).normalizer
The image of the normalizer is equal to the normalizer of the image of a bijective function.
def
add_monoid_hom.lift_of_right_inverse_aux
{G₁ : Type u_4}
{G₂ : Type u_5}
{G₃ : Type u_6}
[add_group G₁]
[add_group G₂]
[add_group G₃]
(f : G₁ →+ G₂)
(f_inv : G₂ → G₁)
(hf : function.right_inverse f_inv ⇑f)
(g : G₁ →+ G₃)
(hg : f.ker ≤ g.ker) :
G₂ →+ G₃
Auxiliary definition used to define lift_of_right_inverse
@[simp]
theorem
monoid_hom.lift_of_right_inverse_aux_comp_apply
{G₁ : Type u_4}
{G₂ : Type u_5}
{G₃ : Type u_6}
[group G₁]
[group G₂]
[group G₃]
(f : G₁ →* G₂)
(f_inv : G₂ → G₁)
(hf : function.right_inverse f_inv ⇑f)
(g : G₁ →* G₃)
(hg : f.ker ≤ g.ker)
(x : G₁) :
⇑(f.lift_of_right_inverse_aux f_inv hf g hg) (⇑f x) = ⇑g x
@[simp]
theorem
add_monoid_hom.lift_of_right_inverse_aux_comp_apply
{G₁ : Type u_4}
{G₂ : Type u_5}
{G₃ : Type u_6}
[add_group G₁]
[add_group G₂]
[add_group G₃]
(f : G₁ →+ G₂)
(f_inv : G₂ → G₁)
(hf : function.right_inverse f_inv ⇑f)
(g : G₁ →+ G₃)
(hg : f.ker ≤ g.ker)
(x : G₁) :
⇑(f.lift_of_right_inverse_aux f_inv hf g hg) (⇑f x) = ⇑g x
def
add_monoid_hom.lift_of_right_inverse
{G₁ : Type u_4}
{G₂ : Type u_5}
{G₃ : Type u_6}
[add_group G₁]
[add_group G₂]
[add_group G₃]
(f : G₁ →+ G₂)
(f_inv : G₂ → G₁)
(hf : function.right_inverse f_inv ⇑f) :
lift_of_right_inverse f f_inv hf g hg is the unique additive group homomorphism φ
- such that
φ.comp f = g(add_monoid_hom.lift_of_right_inverse_comp), - where
f : G₁ →+ G₂has a right_inversef_inv(hf), - and
g : G₂ →+ G₃satisfieshg : f.ker ≤ g.ker.
See add_monoid_hom.eq_lift_of_right_inverse for the uniqueness lemma.
G₁.
| \
f | \ g
| \
v \⌟
G₂----> G₃
∃!φ
def
monoid_hom.lift_of_right_inverse
{G₁ : Type u_4}
{G₂ : Type u_5}
{G₃ : Type u_6}
[group G₁]
[group G₂]
[group G₃]
(f : G₁ →* G₂)
(f_inv : G₂ → G₁)
(hf : function.right_inverse f_inv ⇑f) :
lift_of_right_inverse f hf g hg is the unique group homomorphism φ
- such that
φ.comp f = g(monoid_hom.lift_of_right_inverse_comp), - where
f : G₁ →+* G₂has a right_inversef_inv(hf), - and
g : G₂ →+* G₃satisfieshg : f.ker ≤ g.ker.
See monoid_hom.eq_lift_of_right_inverse for the uniqueness lemma.
G₁.
| \
f | \ g
| \
v \⌟
G₂----> G₃
∃!φ
@[simp, reducible]
noncomputable
def
add_monoid_hom.lift_of_surjective
{G₁ : Type u_4}
{G₂ : Type u_5}
{G₃ : Type u_6}
[add_group G₁]
[add_group G₂]
[add_group G₃]
(f : G₁ →+ G₂)
(hf : function.surjective ⇑f) :
A non-computable version of add_monoid_hom.lift_of_right_inverse for when no
computable right inverse is available.
@[simp, reducible]
noncomputable
def
monoid_hom.lift_of_surjective
{G₁ : Type u_4}
{G₂ : Type u_5}
{G₃ : Type u_6}
[group G₁]
[group G₂]
[group G₃]
(f : G₁ →* G₂)
(hf : function.surjective ⇑f) :
A non-computable version of monoid_hom.lift_of_right_inverse for when no computable right
inverse is available, that uses function.surj_inv.
@[simp]
@[simp]
theorem
add_monoid_hom.eq_lift_of_right_inverse
{G₁ : Type u_4}
{G₂ : Type u_5}
{G₃ : Type u_6}
[add_group G₁]
[add_group G₂]
[add_group G₃]
(f : G₁ →+ G₂)
(f_inv : G₂ → G₁)
(hf : function.right_inverse f_inv ⇑f)
(g : G₁ →+ G₃)
(hg : f.ker ≤ g.ker)
(h : G₂ →+ G₃)
(hh : h.comp f = g) :
h = ⇑(f.lift_of_right_inverse f_inv hf) ⟨g, hg⟩
theorem
monoid_hom.eq_lift_of_right_inverse
{G₁ : Type u_4}
{G₂ : Type u_5}
{G₃ : Type u_6}
[group G₁]
[group G₂]
[group G₃]
(f : G₁ →* G₂)
(f_inv : G₂ → G₁)
(hf : function.right_inverse f_inv ⇑f)
(g : G₁ →* G₃)
(hg : f.ker ≤ g.ker)
(h : G₂ →* G₃)
(hh : h.comp f = g) :
h = ⇑(f.lift_of_right_inverse f_inv hf) ⟨g, hg⟩
theorem
add_subgroup.normal.comap
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{H : add_subgroup N}
(hH : H.normal)
(f : G →+ N) :
(add_subgroup.comap f H).normal
@[protected, instance]
def
add_subgroup.normal_comap
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{H : add_subgroup N}
[nH : H.normal]
(f : G →+ N) :
(add_subgroup.comap f H).normal
theorem
add_subgroup.normal.add_subgroup_of
{G : Type u_1}
[add_group G]
{H : add_subgroup G}
(hH : H.normal)
(K : add_subgroup G) :
(H.add_subgroup_of K).normal
theorem
subgroup.normal.subgroup_of
{G : Type u_1}
[group G]
{H : subgroup G}
(hH : H.normal)
(K : subgroup G) :
(H.subgroup_of K).normal
@[protected, instance]
def
add_subgroup.normal_add_subgroup_of
{G : Type u_1}
[add_group G]
{H N : add_subgroup G}
[N.normal] :
(N.add_subgroup_of H).normal
@[protected, instance]
def
subgroup.normal_subgroup_of
{G : Type u_1}
[group G]
{H N : subgroup G}
[N.normal] :
(N.subgroup_of H).normal
@[simp]
theorem
add_monoid_hom.add_subgroup_comap_apply_coe
{G : Type u_1}
{G' : Type u_2}
[add_group G]
[add_group G']
(f : G →+ G')
(H' : add_subgroup G')
(x : ↥(add_submonoid.comap f H'.to_add_submonoid)) :
def
monoid_hom.subgroup_comap
{G : Type u_1}
{G' : Type u_2}
[group G]
[group G']
(f : G →* G')
(H' : subgroup G') :
↥(subgroup.comap f H') →* ↥H'
The monoid_hom from the preimage of a subgroup to itself.
Equations
- f.subgroup_comap H' = f.submonoid_comap H'.to_submonoid
def
add_monoid_hom.add_subgroup_comap
{G : Type u_1}
{G' : Type u_2}
[add_group G]
[add_group G']
(f : G →+ G')
(H' : add_subgroup G') :
↥(add_subgroup.comap f H') →+ ↥H'
the add_monoid_hom from the preimage of an additive subgroup to itself.
Equations
@[simp]
theorem
monoid_hom.subgroup_comap_apply_coe
{G : Type u_1}
{G' : Type u_2}
[group G]
[group G']
(f : G →* G')
(H' : subgroup G')
(x : ↥(submonoid.comap f H'.to_submonoid)) :
def
monoid_hom.subgroup_map
{G : Type u_1}
{G' : Type u_2}
[group G]
[group G']
(f : G →* G')
(H : subgroup G) :
↥H →* ↥(subgroup.map f H)
The monoid_hom from a subgroup to its image.
Equations
- f.subgroup_map H = f.submonoid_map H.to_submonoid
@[simp]
theorem
add_monoid_hom.add_subgroup_map_apply_coe
{G : Type u_1}
{G' : Type u_2}
[add_group G]
[add_group G']
(f : G →+ G')
(H : add_subgroup G)
(x : ↥(H.to_add_submonoid)) :
def
add_monoid_hom.add_subgroup_map
{G : Type u_1}
{G' : Type u_2}
[add_group G]
[add_group G']
(f : G →+ G')
(H : add_subgroup G) :
↥H →+ ↥(add_subgroup.map f H)
the add_monoid_hom from an additive subgroup to its image
Equations
theorem
add_monoid_hom.add_subgroup_map_surjective
{G : Type u_1}
{G' : Type u_2}
[add_group G]
[add_group G']
(f : G →+ G')
(H : add_subgroup G) :
Makes the identity isomorphism from a proof two subgroups of a multiplicative group are equal.
Equations
- mul_equiv.subgroup_congr h = {to_fun := (equiv.set_congr _).to_fun, inv_fun := (equiv.set_congr _).inv_fun, left_inv := _, right_inv := _, map_mul' := _}
Makes the identity additive isomorphism from a proof two subgroups of an additive group are equal.
Equations
- add_equiv.add_subgroup_congr h = {to_fun := (equiv.set_congr _).to_fun, inv_fun := (equiv.set_congr _).inv_fun, left_inv := _, right_inv := _, map_add' := _}
def
mul_equiv.subgroup_map
{G : Type u_1}
{G' : Type u_2}
[group G]
[group G']
(e : G ≃* G')
(H : subgroup G) :
↥H ≃* ↥(subgroup.map ↑e H)
A subgroup is isomorphic to its image under an isomorphism. If you only have an injective map,
use subgroup.equiv_map_of_injective.
Equations
- e.subgroup_map H = e.submonoid_map H.to_submonoid
def
add_equiv.add_subgroup_map
{G : Type u_1}
{G' : Type u_2}
[add_group G]
[add_group G']
(e : G ≃+ G')
(H : add_subgroup G) :
↥H ≃+ ↥(add_subgroup.map ↑e H)
An additive subgroup is isomorphic to its image under an an isomorphism. If you only
have an injective map, use add_subgroup.equiv_map_of_injective.
Equations
@[simp]
theorem
add_equiv.coe_add_subgroup_map_apply
{G : Type u_1}
{G' : Type u_2}
[add_group G]
[add_group G']
(e : G ≃+ G')
(H : add_subgroup G)
(g : ↥H) :
@[simp]
theorem
add_equiv.add_subgroup_map_symm_apply
{G : Type u_1}
{G' : Type u_2}
[add_group G]
[add_group G']
(e : G ≃+ G')
(H : add_subgroup G)
(g : ↥(add_subgroup.map ↑e H)) :
@[simp]
theorem
add_subgroup.equiv_map_of_injective_coe_add_equiv
{G : Type u_1}
{G' : Type u_2}
[add_group G]
[add_group G']
(H : add_subgroup G)
(e : G ≃+ G') :
H.equiv_map_of_injective ↑e _ = e.add_subgroup_map H
@[simp]
theorem
subgroup.equiv_map_of_injective_coe_mul_equiv
{G : Type u_1}
{G' : Type u_2}
[group G]
[group G']
(H : subgroup G)
(e : G ≃* G') :
H.equiv_map_of_injective ↑e _ = e.subgroup_map H
@[protected, instance]
@[protected, instance]
@[protected, instance]
def
add_subgroup.sum_add_subgroup_of_sum_normal
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
{H₁ K₁ : add_subgroup G}
{H₂ K₂ : add_subgroup N}
[h₁ : (H₁.add_subgroup_of K₁).normal]
[h₂ : (H₂.add_subgroup_of K₂).normal] :
((H₁.prod H₂).add_subgroup_of (K₁.prod K₂)).normal
@[protected, instance]
def
subgroup.prod_subgroup_of_prod_normal
{G : Type u_1}
[group G]
{N : Type u_4}
[group N]
{H₁ K₁ : subgroup G}
{H₂ K₂ : subgroup N}
[h₁ : (H₁.subgroup_of K₁).normal]
[h₂ : (H₂.subgroup_of K₂).normal] :
((H₁.prod H₂).subgroup_of (K₁.prod K₂)).normal
@[protected, instance]
def
add_subgroup.sum_normal
{G : Type u_1}
[add_group G]
{N : Type u_4}
[add_group N]
(H : add_subgroup G)
(K : add_subgroup N)
[hH : H.normal]
[hK : K.normal] :
theorem
subgroup.inf_subgroup_of_inf_normal_of_right
{G : Type u_1}
[group G]
(A B' B : subgroup G)
(hB : B' ≤ B)
[hN : (B'.subgroup_of B).normal] :
((A ⊓ B').subgroup_of (A ⊓ B)).normal
theorem
add_subgroup.inf_add_subgroup_of_inf_normal_of_right
{G : Type u_1}
[add_group G]
(A B' B : add_subgroup G)
(hB : B' ≤ B)
[hN : (B'.add_subgroup_of B).normal] :
((A ⊓ B').add_subgroup_of (A ⊓ B)).normal
theorem
subgroup.inf_subgroup_of_inf_normal_of_left
{G : Type u_1}
[group G]
{A' A : subgroup G}
(B : subgroup G)
(hA : A' ≤ A)
[hN : (A'.subgroup_of A).normal] :
((A' ⊓ B).subgroup_of (A ⊓ B)).normal
theorem
add_subgroup.inf_add_subgroup_of_inf_normal_of_left
{G : Type u_1}
[add_group G]
{A' A : add_subgroup G}
(B : add_subgroup G)
(hA : A' ≤ A)
[hN : (A'.add_subgroup_of A).normal] :
((A' ⊓ B).add_subgroup_of (A ⊓ B)).normal
@[protected, instance]
def
add_subgroup.normal_inf_normal
{G : Type u_1}
[add_group G]
(H K : add_subgroup G)
[hH : H.normal]
[hK : K.normal] :
theorem
add_subgroup.add_subgroup_of_sup
{G : Type u_1}
[add_group G]
(A A' B : add_subgroup G)
(hA : A ≤ B)
(hA' : A' ≤ B) :
(A ⊔ A').add_subgroup_of B = A.add_subgroup_of B ⊔ A'.add_subgroup_of B
theorem
subgroup.subgroup_of_sup
{G : Type u_1}
[group G]
(A A' B : subgroup G)
(hA : A ≤ B)
(hA' : A' ≤ B) :
(A ⊔ A').subgroup_of B = A.subgroup_of B ⊔ A'.subgroup_of B
theorem
add_subgroup.subgroup_normal.mem_comm
{G : Type u_1}
[add_group G]
{H K : add_subgroup G}
(hK : H ≤ K)
[hN : (H.add_subgroup_of K).normal]
{a b : G}
(hb : b ∈ K)
(h : a + b ∈ H) :
theorem
add_subgroup.commute_of_normal_of_disjoint
{G : Type u_1}
[add_group G]
(H₁ H₂ : add_subgroup G)
(hH₁ : H₁.normal)
(hH₂ : H₂.normal)
(hdis : disjoint H₁ H₂)
(x y : G)
(hx : x ∈ H₁)
(hy : y ∈ H₂) :
add_commute x y
Elements of disjoint, normal subgroups commute.
theorem
add_subgroup.add_injective_of_disjoint
{G : Type u_1}
[add_group G]
{H₁ H₂ : add_subgroup G}
(h : disjoint H₁ H₂) :
theorem
is_conj.eq_of_left_mem_center
{M : Type u_5}
[monoid M]
{g h : M}
(H : is_conj g h)
(Hg : g ∈ set.center M) :
g = h
theorem
is_conj.eq_of_right_mem_center
{M : Type u_5}
[monoid M]
{g h : M}
(H : is_conj g h)
(Hh : h ∈ set.center M) :
g = h