Subgroups

We prove subgroups of a group form a complete lattice, and results about images and preimages of subgroups under group homomorphisms. The bundled subgroups use bundled monoid homomorphisms.

There are also theorems about the subgroups generated by an element or a subset of a group, defined both inductively and as the infimum of the set of subgroups containing a given element/subset.

Special thanks goes to Amelia Livingston and Yury Kudryashov for their help and inspiration.

Main definitions

Notation used here:

• G N are Groups

• A is an AddGroup

• H K are Subgroups of G or AddSubgroups of A

• x is an element of type G or type A

• f g : N →* G are group homomorphisms

• s k are sets of elements of type G

Definitions in the file:

• CompleteLattice (Subgroup G) : the subgroups of G form a complete lattice

• Subgroup.closure k : the minimal subgroup that includes the set k

• Subgroup.subtype : the natural group homomorphism from a subgroup of group G to G

• Subgroup.gi : closure forms a Galois insertion with the coercion to set

• Subgroup.comap H f : the preimage of a subgroup H along the group homomorphism f is also a subgroup

• Subgroup.map f H : the image of a subgroup H along the group homomorphism f is also a subgroup

• Subgroup.prod H K : the product of subgroups H, K of groups G, N respectively, H × K is a subgroup of G × N

• MonoidHom.range f : the range of the group homomorphism f is a subgroup

• MonoidHom.ker f : the kernel of a group homomorphism f is the subgroup of elements x : G such that f x = 1

• MonoidHom.eqLocus f g : given group homomorphisms f, g, the elements of G such that f x = g x form a subgroup of G

Implementation notes

Subgroup inclusion is denoted ≤ rather than ⊆, although ∈ is defined as membership of a subgroup's underlying set.

Tags

subgroup, subgroups

theorem sub_mem_comm_iff {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} [SetLike S G] [AddSubgroupClass S G] {a : G} {b : G} : a - b ∈ H ↔ b - a ∈ H

theorem div_mem_comm_iff {G : Type u_1} [Group G] {S : Type u_6} {H : S} [SetLike S G] [SubgroupClass S G] {a : G} {b : G} : a / b ∈ H ↔ b / a ∈ H

Conversion to/from Additive/Multiplicative

@[simp]

theorem Subgroup.toAddSubgroup_symm_apply_coe {G : Type u_1} [Group G] (S : AddSubgroup (Additive G)) : ↑((RelIso.symm Subgroup.toAddSubgroup) S) = ⇑Multiplicative.toAdd ⁻¹' ↑S

@[simp]

theorem Subgroup.toAddSubgroup_apply_coe {G : Type u_1} [Group G] (S : Subgroup G) : ↑(Subgroup.toAddSubgroup S) = ⇑Additive.toMul ⁻¹' ↑S

def Subgroup.toAddSubgroup {G : Type u_1} [Group G] : Subgroup G ≃o AddSubgroup (Additive G)

Subgroups of a group G are isomorphic to additive subgroups of Additive G.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev AddSubgroup.toSubgroup' {G : Type u_1} [Group G] : AddSubgroup (Additive G) ≃o Subgroup G

Additive subgroup of an additive group Additive G are isomorphic to subgroup of G.

Equations

• AddSubgroup.toSubgroup' = Subgroup.toAddSubgroup.symm

@[simp]

theorem AddSubgroup.toSubgroup_apply_coe {A : Type u_4} [AddGroup A] (S : AddSubgroup A) : ↑(AddSubgroup.toSubgroup S) = ⇑Multiplicative.toAdd ⁻¹' ↑S

@[simp]

theorem AddSubgroup.toSubgroup_symm_apply_coe {A : Type u_4} [AddGroup A] (S : Subgroup (Multiplicative A)) : ↑((RelIso.symm AddSubgroup.toSubgroup) S) = ⇑Additive.toMul ⁻¹' ↑S

def AddSubgroup.toSubgroup {A : Type u_4} [AddGroup A] : AddSubgroup A ≃o Subgroup (Multiplicative A)

Additive subgroups of an additive group A are isomorphic to subgroups of Multiplicative A.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Subgroup.toAddSubgroup' {A : Type u_4} [AddGroup A] : Subgroup (Multiplicative A) ≃o AddSubgroup A

Subgroups of an additive group Multiplicative A are isomorphic to additive subgroups of A.

Equations

• Subgroup.toAddSubgroup' = AddSubgroup.toSubgroup.symm

theorem AddSubgroup.sub_mem_comm_iff {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {a : G} {b : G} : a - b ∈ H ↔ b - a ∈ H

theorem Subgroup.div_mem_comm_iff {G : Type u_1} [Group G] (H : Subgroup G) {a : G} {b : G} : a / b ∈ H ↔ b / a ∈ H

theorem AddSubgroup.instTop.proof_1 {G : Type u_1} [AddGroup G] : ∀ {x : G}, x ∈ ⊤.carrier → -x ∈ Set.univ

instance AddSubgroup.instTop {G : Type u_1} [AddGroup G] : Top (AddSubgroup G)

The AddSubgroup G of the AddGroup G.

Equations

• AddSubgroup.instTop = { top := let __src := ⊤; { toAddSubmonoid := __src, neg_mem' := ⋯ } }

instance Subgroup.instTop {G : Type u_1} [Group G] : Top (Subgroup G)

The subgroup G of the group G.

Equations

• Subgroup.instTop = { top := let __src := ⊤; { toSubmonoid := __src, inv_mem' := ⋯ } }

def AddSubgroup.topEquiv {G : Type u_1} [AddGroup G] : ↥⊤ ≃+ G

The top additive subgroup is isomorphic to the additive group.

This is the additive group version of AddSubmonoid.topEquiv.

Equations

• AddSubgroup.topEquiv = AddSubmonoid.topEquiv

@[simp]

theorem AddSubgroup.topEquiv_apply {G : Type u_1} [AddGroup G] (x : ↥⊤) : AddSubgroup.topEquiv x = ↑x

@[simp]

theorem Subgroup.topEquiv_apply {G : Type u_1} [Group G] (x : ↥⊤) : Subgroup.topEquiv x = ↑x

@[simp]

theorem Subgroup.topEquiv_symm_apply_coe {G : Type u_1} [Group G] (x : G) : ↑(Subgroup.topEquiv.symm x) = x

@[simp]

theorem AddSubgroup.topEquiv_symm_apply_coe {G : Type u_1} [AddGroup G] (x : G) : ↑(AddSubgroup.topEquiv.symm x) = x

def Subgroup.topEquiv {G : Type u_1} [Group G] : ↥⊤ ≃* G

The top subgroup is isomorphic to the group.

This is the group version of Submonoid.topEquiv.

Equations

• Subgroup.topEquiv = Submonoid.topEquiv

instance AddSubgroup.instBot {G : Type u_1} [AddGroup G] : Bot (AddSubgroup G)

The trivial AddSubgroup {0} of an AddGroup G.

Equations

• AddSubgroup.instBot = { bot := let __src := ⊥; { toAddSubmonoid := __src, neg_mem' := ⋯ } }

theorem AddSubgroup.instBot.proof_1 {G : Type u_1} [AddGroup G] (a : G) : a ∈ ⊥.carrier → -a ∈ ⊥.carrier

instance Subgroup.instBot {G : Type u_1} [Group G] : Bot (Subgroup G)

The trivial subgroup {1} of a group G.

Equations

• Subgroup.instBot = { bot := let __src := ⊥; { toSubmonoid := __src, inv_mem' := ⋯ } }

instance AddSubgroup.instInhabited {G : Type u_1} [AddGroup G] : Inhabited (AddSubgroup G)

Equations

• AddSubgroup.instInhabited = { default := ⊥ }

instance Subgroup.instInhabited {G : Type u_1} [Group G] : Inhabited (Subgroup G)

Equations

• Subgroup.instInhabited = { default := ⊥ }

@[simp]

theorem AddSubgroup.mem_bot {G : Type u_1} [AddGroup G] {x : G} : x ∈ ⊥ ↔ x = 0

@[simp]

theorem Subgroup.mem_bot {G : Type u_1} [Group G] {x : G} : x ∈ ⊥ ↔ x = 1

@[simp]

theorem AddSubgroup.mem_top {G : Type u_1} [AddGroup G] (x : G) : x ∈ ⊤

@[simp]

theorem Subgroup.mem_top {G : Type u_1} [Group G] (x : G) : x ∈ ⊤

@[simp]

theorem AddSubgroup.coe_top {G : Type u_1} [AddGroup G] : ↑⊤ = Set.univ

@[simp]

theorem Subgroup.coe_top {G : Type u_1} [Group G] : ↑⊤ = Set.univ

@[simp]

theorem AddSubgroup.coe_bot {G : Type u_1} [AddGroup G] : ↑⊥ = {0}

@[simp]

theorem Subgroup.coe_bot {G : Type u_1} [Group G] : ↑⊥ = {1}

theorem AddSubgroup.instUniqueSubtypeMemBot.proof_1 {G : Type u_1} [AddGroup G] (g : ↥⊥) : g = default

instance AddSubgroup.instUniqueSubtypeMemBot {G : Type u_1} [AddGroup G] : Unique ↥⊥

Equations

• AddSubgroup.instUniqueSubtypeMemBot = { default := 0, uniq := ⋯ }

instance Subgroup.instUniqueSubtypeMemBot {G : Type u_1} [Group G] : Unique ↥⊥

Equations

• Subgroup.instUniqueSubtypeMemBot = { default := 1, uniq := ⋯ }

@[simp]

theorem AddSubgroup.top_toAddSubmonoid {G : Type u_1} [AddGroup G] : ⊤.toAddSubmonoid = ⊤

@[simp]

theorem Subgroup.top_toSubmonoid {G : Type u_1} [Group G] : ⊤.toSubmonoid = ⊤

@[simp]

theorem AddSubgroup.bot_toAddSubmonoid {G : Type u_1} [AddGroup G] : ⊥.toAddSubmonoid = ⊥

@[simp]

theorem Subgroup.bot_toSubmonoid {G : Type u_1} [Group G] : ⊥.toSubmonoid = ⊥

theorem AddSubgroup.eq_bot_iff_forall {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H = ⊥ ↔ ∀ x ∈ H, x = 0

theorem Subgroup.eq_bot_iff_forall {G : Type u_1} [Group G] (H : Subgroup G) : H = ⊥ ↔ ∀ x ∈ H, x = 1

theorem AddSubgroup.eq_bot_of_subsingleton {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Subsingleton ↥H] : H = ⊥

theorem Subgroup.eq_bot_of_subsingleton {G : Type u_1} [Group G] (H : Subgroup G) [Subsingleton ↥H] : H = ⊥

@[simp]

theorem AddSubgroup.coe_eq_univ {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : ↑H = Set.univ ↔ H = ⊤

@[simp]

theorem Subgroup.coe_eq_univ {G : Type u_1} [Group G] {H : Subgroup G} : ↑H = Set.univ ↔ H = ⊤

theorem AddSubgroup.coe_eq_singleton {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : (∃ (g : G), ↑H = {g}) ↔ H = ⊥

theorem Subgroup.coe_eq_singleton {G : Type u_1} [Group G] {H : Subgroup G} : (∃ (g : G), ↑H = {g}) ↔ H = ⊥

theorem AddSubgroup.nontrivial_iff_exists_ne_zero {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : Nontrivial ↥H ↔ ∃ x ∈ H, x ≠ 0

theorem Subgroup.nontrivial_iff_exists_ne_one {G : Type u_1} [Group G] (H : Subgroup G) : Nontrivial ↥H ↔ ∃ x ∈ H, x ≠ 1

theorem AddSubgroup.exists_ne_zero_of_nontrivial {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Nontrivial ↥H] : ∃ x ∈ H, x ≠ 0

theorem Subgroup.exists_ne_one_of_nontrivial {G : Type u_1} [Group G] (H : Subgroup G) [Nontrivial ↥H] : ∃ x ∈ H, x ≠ 1

theorem AddSubgroup.nontrivial_iff_ne_bot {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : Nontrivial ↥H ↔ H ≠ ⊥

theorem Subgroup.nontrivial_iff_ne_bot {G : Type u_1} [Group G] (H : Subgroup G) : Nontrivial ↥H ↔ H ≠ ⊥

theorem AddSubgroup.bot_or_nontrivial {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H = ⊥ ∨ Nontrivial ↥H

A subgroup is either the trivial subgroup or nontrivial.

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 AddSubgroup.bot_or_exists_ne_zero {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H = ⊥ ∨ ∃ x ∈ H, x ≠ 0

A subgroup is either the trivial subgroup or contains a nonzero element.

theorem Subgroup.bot_or_exists_ne_one {G : Type u_1} [Group G] (H : Subgroup G) : H = ⊥ ∨ ∃ x ∈ H, x ≠ 1

A subgroup is either the trivial subgroup or contains a non-identity element.

theorem AddSubgroup.ne_bot_iff_exists_ne_zero {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H ≠ ⊥ ↔ ∃ (a : ↥H), a ≠ 0

theorem Subgroup.ne_bot_iff_exists_ne_one {G : Type u_1} [Group G] {H : Subgroup G} : H ≠ ⊥ ↔ ∃ (a : ↥H), a ≠ 1

instance AddSubgroup.instInf {G : Type u_1} [AddGroup G] : Inf (AddSubgroup G)

The inf of two AddSubgroups is their intersection.

Equations

• AddSubgroup.instInf = { inf := fun (H₁ H₂ : AddSubgroup G) => let __src := H₁.toAddSubmonoid ⊓ H₂.toAddSubmonoid; { toAddSubmonoid := __src, neg_mem' := ⋯ } }

theorem AddSubgroup.instInf.proof_1 {G : Type u_1} [AddGroup G] (H₁ : AddSubgroup G) (H₂ : AddSubgroup G) : ∀ {x : G}, x ∈ (H₁.toAddSubmonoid ⊓ H₂.toAddSubmonoid).carrier → -x ∈ (H₁.toAddSubmonoid ⊓ H₂.toAddSubmonoid).carrier

instance Subgroup.instInf {G : Type u_1} [Group G] : Inf (Subgroup G)

The inf of two subgroups is their intersection.

Equations

• Subgroup.instInf = { inf := fun (H₁ H₂ : Subgroup G) => let __src := H₁.toSubmonoid ⊓ H₂.toSubmonoid; { toSubmonoid := __src, inv_mem' := ⋯ } }

@[simp]

theorem AddSubgroup.coe_inf {G : Type u_1} [AddGroup G] (p : AddSubgroup G) (p' : AddSubgroup G) : ↑(p ⊓ p') = ↑p ∩ ↑p'

@[simp]

theorem Subgroup.coe_inf {G : Type u_1} [Group G] (p : Subgroup G) (p' : Subgroup G) : ↑(p ⊓ p') = ↑p ∩ ↑p'

@[simp]

theorem AddSubgroup.mem_inf {G : Type u_1} [AddGroup G] {p : AddSubgroup G} {p' : AddSubgroup G} {x : G} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

@[simp]

theorem Subgroup.mem_inf {G : Type u_1} [Group G] {p : Subgroup G} {p' : Subgroup G} {x : G} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

instance AddSubgroup.instInfSet {G : Type u_1} [AddGroup G] : InfSet (AddSubgroup G)

Equations

• AddSubgroup.instInfSet = { sInf := fun (s : Set (AddSubgroup G)) => let __src := (⨅ S ∈ s, S.toAddSubmonoid).copy (⋂ S ∈ s, ↑S) ⋯; { toAddSubmonoid := __src, neg_mem' := ⋯ } }

theorem AddSubgroup.instInfSet.proof_2 {G : Type u_1} [AddGroup G] (s : Set (AddSubgroup G)) {x : G} (hx : x ∈ ((⨅ S ∈ s, S.toAddSubmonoid).copy (⋂ S ∈ s, ↑S) ⋯).carrier) : -x ∈ ⋂ x ∈ s, ↑x

theorem AddSubgroup.instInfSet.proof_1 {G : Type u_1} [AddGroup G] (s : Set (AddSubgroup G)) : ⋂ S ∈ s, ↑S = ↑(⨅ i ∈ s, i.toAddSubmonoid)

instance Subgroup.instInfSet {G : Type u_1} [Group G] : InfSet (Subgroup G)

Equations

• Subgroup.instInfSet = { sInf := fun (s : Set (Subgroup G)) => let __src := (⨅ S ∈ s, S.toSubmonoid).copy (⋂ S ∈ s, ↑S) ⋯; { toSubmonoid := __src, inv_mem' := ⋯ } }

@[simp]

theorem AddSubgroup.coe_sInf {G : Type u_1} [AddGroup G] (H : Set (AddSubgroup G)) : ↑(sInf H) = ⋂ s ∈ H, ↑s

@[simp]

theorem Subgroup.coe_sInf {G : Type u_1} [Group G] (H : Set (Subgroup G)) : ↑(sInf H) = ⋂ s ∈ H, ↑s

@[simp]

theorem AddSubgroup.mem_sInf {G : Type u_1} [AddGroup G] {S : Set (AddSubgroup G)} {x : G} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

@[simp]

theorem Subgroup.mem_sInf {G : Type u_1} [Group G] {S : Set (Subgroup G)} {x : G} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

theorem AddSubgroup.mem_iInf {G : Type u_1} [AddGroup G] {ι : Sort u_5} {S : ι → AddSubgroup G} {x : G} : x ∈ ⨅ (i : ι), S i ↔ ∀ (i : ι), x ∈ S i

theorem Subgroup.mem_iInf {G : Type u_1} [Group G] {ι : Sort u_5} {S : ι → Subgroup G} {x : G} : x ∈ ⨅ (i : ι), S i ↔ ∀ (i : ι), x ∈ S i

@[simp]

theorem AddSubgroup.coe_iInf {G : Type u_1} [AddGroup G] {ι : Sort u_5} {S : ι → AddSubgroup G} : ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)

@[simp]

theorem Subgroup.coe_iInf {G : Type u_1} [Group G] {ι : Sort u_5} {S : ι → Subgroup G} : ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)

theorem AddSubgroup.instCompleteLattice.proof_2 {G : Type u_1} [AddGroup G] (_a : AddSubgroup G) (_b : AddSubgroup G) (_x : G) (self : _x ∈ ↑_a.toAddSubmonoid ∧ _x ∈ ↑_b.toAddSubmonoid) : _x ∈ ↑_a.toAddSubmonoid

instance AddSubgroup.instCompleteLattice {G : Type u_1} [AddGroup G] : CompleteLattice (AddSubgroup G)

The AddSubgroups of an AddGroup form a complete lattice.

Equations

• AddSubgroup.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem AddSubgroup.instCompleteLattice.proof_7 {G : Type u_1} [AddGroup G] (s : Set (AddSubgroup G)) (a : AddSubgroup G) : a ∈ s → sInf s ≤ a

theorem AddSubgroup.instCompleteLattice.proof_5 {G : Type u_1} [AddGroup G] (s : Set (AddSubgroup G)) (a : AddSubgroup G) : a ∈ s → a ≤ sSup s

theorem AddSubgroup.instCompleteLattice.proof_8 {G : Type u_1} [AddGroup G] (s : Set (AddSubgroup G)) (a : AddSubgroup G) : (∀ b ∈ s, a ≤ b) → a ≤ sInf s

theorem AddSubgroup.instCompleteLattice.proof_4 {G : Type u_1} [AddGroup G] (_a : AddSubgroup G) (_b : AddSubgroup G) (_c : AddSubgroup G) (ha : _a ≤ _b) (hb : _a ≤ _c) (_x : G) (hx : _x ∈ _a) : _x ∈ ↑_b.toAddSubmonoid ∧ _x ∈ ↑_c.toAddSubmonoid

theorem AddSubgroup.instCompleteLattice.proof_6 {G : Type u_1} [AddGroup G] (s : Set (AddSubgroup G)) (a : AddSubgroup G) : (∀ b ∈ s, b ≤ a) → sSup s ≤ a

theorem AddSubgroup.instCompleteLattice.proof_1 {G : Type u_1} [AddGroup G] (_s : Set (AddSubgroup G)) : IsGLB _s (sInf _s)

theorem AddSubgroup.instCompleteLattice.proof_9 {G : Type u_1} [AddGroup G] (S : AddSubgroup G) (_x : G) (hx : _x ∈ ⊥) : _x ∈ S

theorem AddSubgroup.instCompleteLattice.proof_3 {G : Type u_1} [AddGroup G] (_a : AddSubgroup G) (_b : AddSubgroup G) (_x : G) (self : _x ∈ ↑_a.toAddSubmonoid ∧ _x ∈ ↑_b.toAddSubmonoid) : _x ∈ ↑_b.toAddSubmonoid

instance Subgroup.instCompleteLattice {G : Type u_1} [Group G] : CompleteLattice (Subgroup G)

Subgroups of a group form a complete lattice.

Equations

• Subgroup.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem AddSubgroup.mem_sup_left {G : Type u_1} [AddGroup G] {S : AddSubgroup G} {T : AddSubgroup G} {x : G} : x ∈ S → x ∈ S ⊔ T

theorem Subgroup.mem_sup_left {G : Type u_1} [Group G] {S : Subgroup G} {T : Subgroup G} {x : G} : x ∈ S → x ∈ S ⊔ T

theorem AddSubgroup.mem_sup_right {G : Type u_1} [AddGroup G] {S : AddSubgroup G} {T : AddSubgroup G} {x : G} : x ∈ T → x ∈ S ⊔ T

theorem Subgroup.mem_sup_right {G : Type u_1} [Group G] {S : Subgroup G} {T : Subgroup G} {x : G} : x ∈ T → x ∈ S ⊔ T

theorem AddSubgroup.add_mem_sup {G : Type u_1} [AddGroup G] {S : AddSubgroup G} {T : AddSubgroup G} {x : G} {y : G} (hx : x ∈ S) (hy : y ∈ T) : x + y ∈ S ⊔ T

theorem Subgroup.mul_mem_sup {G : Type u_1} [Group G] {S : Subgroup G} {T : Subgroup G} {x : G} {y : G} (hx : x ∈ S) (hy : y ∈ T) : x * y ∈ S ⊔ T

theorem AddSubgroup.mem_iSup_of_mem {G : Type u_1} [AddGroup G] {ι : Sort u_5} {S : ι → AddSubgroup G} (i : ι) {x : G} : x ∈ S i → x ∈ iSup S

theorem Subgroup.mem_iSup_of_mem {G : Type u_1} [Group G] {ι : Sort u_5} {S : ι → Subgroup G} (i : ι) {x : G} : x ∈ S i → x ∈ iSup S

theorem AddSubgroup.mem_sSup_of_mem {G : Type u_1} [AddGroup G] {S : Set (AddSubgroup G)} {s : AddSubgroup G} (hs : s ∈ S) {x : G} : x ∈ s → x ∈ sSup S

theorem Subgroup.mem_sSup_of_mem {G : Type u_1} [Group G] {S : Set (Subgroup G)} {s : Subgroup G} (hs : s ∈ S) {x : G} : x ∈ s → x ∈ sSup S

@[simp]

theorem AddSubgroup.subsingleton_iff {G : Type u_1} [AddGroup G] : Subsingleton (AddSubgroup G) ↔ Subsingleton G

@[simp]

theorem Subgroup.subsingleton_iff {G : Type u_1} [Group G] : Subsingleton (Subgroup G) ↔ Subsingleton G

@[simp]

theorem AddSubgroup.nontrivial_iff {G : Type u_1} [AddGroup G] : Nontrivial (AddSubgroup G) ↔ Nontrivial G

@[simp]

theorem Subgroup.nontrivial_iff {G : Type u_1} [Group G] : Nontrivial (Subgroup G) ↔ Nontrivial G

theorem AddSubgroup.instUniqueOfSubsingleton.proof_1 {G : Type u_1} [AddGroup G] [Subsingleton G] (a : AddSubgroup G) : a = default

instance AddSubgroup.instUniqueOfSubsingleton {G : Type u_1} [AddGroup G] [Subsingleton G] : Unique (AddSubgroup G)

Equations

• AddSubgroup.instUniqueOfSubsingleton = { default := ⊥, uniq := ⋯ }

instance Subgroup.instUniqueOfSubsingleton {G : Type u_1} [Group G] [Subsingleton G] : Unique (Subgroup G)

Equations

• Subgroup.instUniqueOfSubsingleton = { default := ⊥, uniq := ⋯ }

instance AddSubgroup.instNontrivial {G : Type u_1} [AddGroup G] [Nontrivial G] : Nontrivial (AddSubgroup G)

Equations

• ⋯ = ⋯

instance Subgroup.instNontrivial {G : Type u_1} [Group G] [Nontrivial G] : Nontrivial (Subgroup G)

Equations

• ⋯ = ⋯

theorem AddSubgroup.eq_top_iff' {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H = ⊤ ↔ ∀ (x : G), x ∈ H

theorem Subgroup.eq_top_iff' {G : Type u_1} [Group G] (H : Subgroup G) : H = ⊤ ↔ ∀ (x : G), x ∈ H

def AddSubgroup.closure {G : Type u_1} [AddGroup G] (k : Set G) : AddSubgroup G

The AddSubgroup generated by a set

Equations

• AddSubgroup.closure k = sInf {K : AddSubgroup G | k ⊆ ↑K}

def Subgroup.closure {G : Type u_1} [Group G] (k : Set G) : Subgroup G

The Subgroup generated by a set.

Equations

• Subgroup.closure k = sInf {K : Subgroup G | k ⊆ ↑K}

theorem AddSubgroup.mem_closure {G : Type u_1} [AddGroup G] {k : Set G} {x : G} : x ∈ AddSubgroup.closure k ↔ ∀ (K : AddSubgroup G), k ⊆ ↑K → x ∈ K

theorem Subgroup.mem_closure {G : Type u_1} [Group G] {k : Set G} {x : G} : x ∈ Subgroup.closure k ↔ ∀ (K : Subgroup G), k ⊆ ↑K → x ∈ K

@[simp]

theorem AddSubgroup.subset_closure {G : Type u_1} [AddGroup G] {k : Set G} : k ⊆ ↑(AddSubgroup.closure k)

The AddSubgroup generated by a set includes the set.

@[simp]

theorem Subgroup.subset_closure {G : Type u_1} [Group G] {k : Set G} : k ⊆ ↑(Subgroup.closure k)

The subgroup generated by a set includes the set.

theorem AddSubgroup.not_mem_of_not_mem_closure {G : Type u_1} [AddGroup G] {k : Set G} {P : G} (hP : P ∉ AddSubgroup.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 AddSubgroup.closure_le {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {k : Set G} : AddSubgroup.closure k ≤ K ↔ k ⊆ ↑K

An additive subgroup K includes closure k if and only if it includes k

@[simp]

theorem Subgroup.closure_le {G : Type u_1} [Group G] (K : Subgroup G) {k : Set G} : Subgroup.closure k ≤ K ↔ k ⊆ ↑K

A subgroup K includes closure k if and only if it includes k.

theorem AddSubgroup.closure_eq_of_le {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {k : Set G} (h₁ : k ⊆ ↑K) (h₂ : K ≤ AddSubgroup.closure k) : AddSubgroup.closure k = 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 AddSubgroup.closure_induction {G : Type u_1} [AddGroup G] {k : Set G} {p : (g : G) → g ∈ AddSubgroup.closure k → Prop} (mem : ∀ (x : G) (hx : x ∈ k), p x ⋯) (one : p 0 ⋯) (mul : ∀ (x y : G) (hx : x ∈ AddSubgroup.closure k) (hy : y ∈ AddSubgroup.closure k), p x hx → p y hy → p (x + y) ⋯) (inv : ∀ (x : G) (hx : x ∈ AddSubgroup.closure k), p x hx → p (-x) ⋯) {x : G} (hx : x ∈ AddSubgroup.closure k) : p x hx

An induction principle for additive closure membership. If p holds for 0 and all elements of k, and is preserved under addition and inverses, then p holds for all elements of the additive closure of k.

See also AddSubgroup.closure_induction_left and AddSubgroup.closure_induction_left for versions that only require showing p is preserved by addition by elements in k.

theorem Subgroup.closure_induction {G : Type u_1} [Group G] {k : Set G} {p : (g : G) → g ∈ Subgroup.closure k → Prop} (mem : ∀ (x : G) (hx : x ∈ k), p x ⋯) (one : p 1 ⋯) (mul : ∀ (x y : G) (hx : x ∈ Subgroup.closure k) (hy : y ∈ Subgroup.closure k), p x hx → p y hy → p (x * y) ⋯) (inv : ∀ (x : G) (hx : x ∈ Subgroup.closure k), p x hx → p x⁻¹ ⋯) {x : G} (hx : x ∈ Subgroup.closure k) : p x hx

An induction principle for closure membership. If p holds for 1 and all elements of k, and is preserved under multiplication and inverse, then p holds for all elements of the closure of k.

See also Subgroup.closure_induction_left and Subgroup.closure_induction_right for versions that only require showing p is preserved by multiplication by elements in k.

@[deprecated Subgroup.closure_induction]

theorem Subgroup.closure_induction' {G : Type u_1} [Group G] {k : Set G} {p : (g : G) → g ∈ Subgroup.closure k → Prop} (mem : ∀ (x : G) (hx : x ∈ k), p x ⋯) (one : p 1 ⋯) (mul : ∀ (x y : G) (hx : x ∈ Subgroup.closure k) (hy : y ∈ Subgroup.closure k), p x hx → p y hy → p (x * y) ⋯) (inv : ∀ (x : G) (hx : x ∈ Subgroup.closure k), p x hx → p x⁻¹ ⋯) {x : G} (hx : x ∈ Subgroup.closure k) : p x hx

Alias of Subgroup.closure_induction.

---

An induction principle for closure membership. If p holds for 1 and all elements of k, and is preserved under multiplication and inverse, then p holds for all elements of the closure of k.

See also Subgroup.closure_induction_left and Subgroup.closure_induction_right for versions that only require showing p is preserved by multiplication by elements in k.

theorem AddSubgroup.closure_induction₂ {G : Type u_1} [AddGroup G] {k : Set G} {p : (x y : G) → x ∈ AddSubgroup.closure k → y ∈ AddSubgroup.closure k → Prop} (mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯) (one_left : ∀ (x : G) (hx : x ∈ AddSubgroup.closure k), p 0 x ⋯ hx) (one_right : ∀ (x : G) (hx : x ∈ AddSubgroup.closure k), p x 0 hx ⋯) (mul_left : ∀ (x y z : G) (hx : x ∈ AddSubgroup.closure k) (hy : y ∈ AddSubgroup.closure k) (hz : z ∈ AddSubgroup.closure k), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) (mul_right : ∀ (y z x : G) (hy : y ∈ AddSubgroup.closure k) (hz : z ∈ AddSubgroup.closure k) (hx : x ∈ AddSubgroup.closure k), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯) (inv_left : ∀ (x y : G) (hx : x ∈ AddSubgroup.closure k) (hy : y ∈ AddSubgroup.closure k), p x y hx hy → p (-x) y ⋯ hy) (inv_right : ∀ (x y : G) (hx : x ∈ AddSubgroup.closure k) (hy : y ∈ AddSubgroup.closure k), p x y hx hy → p x (-y) hx ⋯) {x : G} {y : G} (hx : x ∈ AddSubgroup.closure k) (hy : y ∈ AddSubgroup.closure k) : p x y hx hy

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 : (x y : G) → x ∈ Subgroup.closure k → y ∈ Subgroup.closure k → Prop} (mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯) (one_left : ∀ (x : G) (hx : x ∈ Subgroup.closure k), p 1 x ⋯ hx) (one_right : ∀ (x : G) (hx : x ∈ Subgroup.closure k), p x 1 hx ⋯) (mul_left : ∀ (x y z : G) (hx : x ∈ Subgroup.closure k) (hy : y ∈ Subgroup.closure k) (hz : z ∈ Subgroup.closure k), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz) (mul_right : ∀ (y z x : G) (hy : y ∈ Subgroup.closure k) (hz : z ∈ Subgroup.closure k) (hx : x ∈ Subgroup.closure k), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯) (inv_left : ∀ (x y : G) (hx : x ∈ Subgroup.closure k) (hy : y ∈ Subgroup.closure k), p x y hx hy → p x⁻¹ y ⋯ hy) (inv_right : ∀ (x y : G) (hx : x ∈ Subgroup.closure k) (hy : y ∈ Subgroup.closure k), p x y hx hy → p x y⁻¹ hx ⋯) {x : G} {y : G} (hx : x ∈ Subgroup.closure k) (hy : y ∈ Subgroup.closure k) : p x y hx hy

An induction principle for closure membership for predicates with two arguments.

@[simp]

theorem AddSubgroup.closure_closure_coe_preimage {G : Type u_1} [AddGroup G] {k : Set G} : AddSubgroup.closure (Subtype.val ⁻¹' k) = ⊤

@[simp]

theorem Subgroup.closure_closure_coe_preimage {G : Type u_1} [Group G] {k : Set G} : Subgroup.closure (Subtype.val ⁻¹' k) = ⊤

def AddSubgroup.closureAddCommGroupOfComm {G : Type u_1} [AddGroup G] {k : Set G} (hcomm : ∀ x ∈ k, ∀ y ∈ k, x + y = y + x) : AddCommGroup ↥(AddSubgroup.closure k)

If all the elements of a set s commute, then closure s is an additive commutative group.

Equations

• AddSubgroup.closureAddCommGroupOfComm hcomm = AddCommGroup.mk ⋯

theorem AddSubgroup.closureAddCommGroupOfComm.proof_1 {G : Type u_1} [AddGroup G] {k : Set G} (hcomm : ∀ x ∈ k, ∀ y ∈ k, x + y = y + x) : ∀ (x x_1 : ↥(AddSubgroup.closure k)), x + x_1 = x_1 + x

def Subgroup.closureCommGroupOfComm {G : Type u_1} [Group G] {k : Set G} (hcomm : ∀ x ∈ k, ∀ y ∈ k, x * y = y * x) : CommGroup ↥(Subgroup.closure k)

If all the elements of a set s commute, then closure s is a commutative group.

Equations

• Subgroup.closureCommGroupOfComm hcomm = CommGroup.mk ⋯

theorem AddSubgroup.gi.proof_1 (G : Type u_1) [AddGroup G] (_s : AddSubgroup G) : ↑_s ⊆ ↑(AddSubgroup.closure ↑_s)

theorem AddSubgroup.gi.proof_2 (G : Type u_1) [AddGroup G] (_s : Set G) (_h : ↑(AddSubgroup.closure _s) ≤ _s) : (fun (s : Set G) (x : ↑(AddSubgroup.closure s) ≤ s) => AddSubgroup.closure s) _s _h = (fun (s : Set G) (x : ↑(AddSubgroup.closure s) ≤ s) => AddSubgroup.closure s) _s _h

def AddSubgroup.gi (G : Type u_1) [AddGroup G] : GaloisInsertion AddSubgroup.closure SetLike.coe

closure forms a Galois insertion with the coercion to set.

Equations

• AddSubgroup.gi G = { choice := fun (s : Set G) (x : ↑(AddSubgroup.closure s) ≤ s) => AddSubgroup.closure s, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

def Subgroup.gi (G : Type u_1) [Group G] : GaloisInsertion Subgroup.closure SetLike.coe

closure forms a Galois insertion with the coercion to set.

Equations

• Subgroup.gi G = { choice := fun (s : Set G) (x : ↑(Subgroup.closure s) ≤ s) => Subgroup.closure s, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

theorem AddSubgroup.closure_mono {G : Type u_1} [AddGroup G] ⦃h : Set G⦄ ⦃k : Set G⦄ (h' : h ⊆ k) : AddSubgroup.closure h ≤ AddSubgroup.closure k

Additive subgroup closure of a set is monotone in its argument: if h ⊆ k, then closure h ≤ closure k

theorem Subgroup.closure_mono {G : Type u_1} [Group G] ⦃h : Set G⦄ ⦃k : Set G⦄ (h' : h ⊆ k) : Subgroup.closure h ≤ Subgroup.closure k

Subgroup closure of a set is monotone in its argument: if h ⊆ k, then closure h ≤ closure k.

@[simp]

theorem AddSubgroup.closure_eq {G : Type u_1} [AddGroup G] (K : AddSubgroup G) : AddSubgroup.closure ↑K = K

Additive closure of an additive subgroup K equals K

@[simp]

theorem Subgroup.closure_eq {G : Type u_1} [Group G] (K : Subgroup G) : Subgroup.closure ↑K = K

Closure of a subgroup K equals K.

@[simp]

theorem AddSubgroup.closure_empty {G : Type u_1} [AddGroup G] : AddSubgroup.closure ∅ = ⊥

@[simp]

theorem Subgroup.closure_empty {G : Type u_1} [Group G] : Subgroup.closure ∅ = ⊥

@[simp]

theorem AddSubgroup.closure_univ {G : Type u_1} [AddGroup G] : AddSubgroup.closure Set.univ = ⊤

@[simp]

theorem Subgroup.closure_univ {G : Type u_1} [Group G] : Subgroup.closure Set.univ = ⊤

theorem AddSubgroup.closure_union {G : Type u_1} [AddGroup G] (s : Set G) (t : Set G) : AddSubgroup.closure (s ∪ t) = AddSubgroup.closure s ⊔ AddSubgroup.closure t

theorem Subgroup.closure_union {G : Type u_1} [Group G] (s : Set G) (t : Set G) : Subgroup.closure (s ∪ t) = Subgroup.closure s ⊔ Subgroup.closure t

theorem AddSubgroup.sup_eq_closure {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (H' : AddSubgroup G) : H ⊔ H' = AddSubgroup.closure (↑H ∪ ↑H')

theorem Subgroup.sup_eq_closure {G : Type u_1} [Group G] (H : Subgroup G) (H' : Subgroup G) : H ⊔ H' = Subgroup.closure (↑H ∪ ↑H')

theorem AddSubgroup.closure_iUnion {G : Type u_1} [AddGroup G] {ι : Sort u_5} (s : ι → Set G) : AddSubgroup.closure (⋃ (i : ι), s i) = ⨆ (i : ι), AddSubgroup.closure (s i)

theorem Subgroup.closure_iUnion {G : Type u_1} [Group G] {ι : Sort u_5} (s : ι → Set G) : Subgroup.closure (⋃ (i : ι), s i) = ⨆ (i : ι), Subgroup.closure (s i)

@[simp]

theorem AddSubgroup.closure_eq_bot_iff {G : Type u_1} [AddGroup G] {k : Set G} : AddSubgroup.closure k = ⊥ ↔ k ⊆ {0}

@[simp]

theorem Subgroup.closure_eq_bot_iff {G : Type u_1} [Group G] {k : Set G} : Subgroup.closure k = ⊥ ↔ k ⊆ {1}

theorem AddSubgroup.iSup_eq_closure {G : Type u_1} [AddGroup G] {ι : Sort u_5} (p : ι → AddSubgroup G) : ⨆ (i : ι), p i = AddSubgroup.closure (⋃ (i : ι), ↑(p i))

theorem Subgroup.iSup_eq_closure {G : Type u_1} [Group G] {ι : Sort u_5} (p : ι → Subgroup G) : ⨆ (i : ι), p i = Subgroup.closure (⋃ (i : ι), ↑(p i))

theorem AddSubgroup.mem_closure_singleton {G : Type u_1} [AddGroup G] {x : G} {y : G} : y ∈ AddSubgroup.closure {x} ↔ ∃ (n : ℤ), n • x = y

The AddSubgroup generated by an element of an AddGroup equals the set of natural number multiples of the element.

theorem Subgroup.mem_closure_singleton {G : Type u_1} [Group G] {x : G} {y : G} : y ∈ Subgroup.closure {x} ↔ ∃ (n : ℤ), x ^ n = y

The subgroup generated by an element of a group equals the set of integer number powers of the element.

theorem AddSubgroup.closure_singleton_zero {G : Type u_1} [AddGroup G] : AddSubgroup.closure {0} = ⊥

theorem Subgroup.closure_singleton_one {G : Type u_1} [Group G] : Subgroup.closure {1} = ⊥

@[simp]

theorem AddSubgroup.mem_closure_singleton_self {G : Type u_1} [AddGroup G] (x : G) : x ∈ AddSubgroup.closure {x}

@[simp]

theorem Subgroup.mem_closure_singleton_self {G : Type u_1} [Group G] (x : G) : x ∈ Subgroup.closure {x}

theorem AddSubgroup.le_closure_toAddSubmonoid {G : Type u_1} [AddGroup G] (S : Set G) : AddSubmonoid.closure S ≤ (AddSubgroup.closure S).toAddSubmonoid

theorem Subgroup.le_closure_toSubmonoid {G : Type u_1} [Group G] (S : Set G) : Submonoid.closure S ≤ (Subgroup.closure S).toSubmonoid

theorem AddSubgroup.closure_eq_top_of_mclosure_eq_top {G : Type u_1} [AddGroup G] {S : Set G} (h : AddSubmonoid.closure S = ⊤) : AddSubgroup.closure S = ⊤

theorem Subgroup.closure_eq_top_of_mclosure_eq_top {G : Type u_1} [Group G] {S : Set G} (h : Submonoid.closure S = ⊤) : Subgroup.closure S = ⊤

theorem AddSubgroup.mem_iSup_of_directed {G : Type u_1} [AddGroup G] {ι : Sort u_5} [hι : Nonempty ι] {K : ι → AddSubgroup G} (hK : Directed (fun (x1 x2 : AddSubgroup G) => x1 ≤ x2) K) {x : G} : x ∈ iSup K ↔ ∃ (i : ι), x ∈ K i

theorem Subgroup.mem_iSup_of_directed {G : Type u_1} [Group G] {ι : Sort u_5} [hι : Nonempty ι] {K : ι → Subgroup G} (hK : Directed (fun (x1 x2 : Subgroup G) => x1 ≤ x2) K) {x : G} : x ∈ iSup K ↔ ∃ (i : ι), x ∈ K i

theorem AddSubgroup.coe_iSup_of_directed {G : Type u_1} [AddGroup G] {ι : Sort u_5} [Nonempty ι] {S : ι → AddSubgroup G} (hS : Directed (fun (x1 x2 : AddSubgroup G) => x1 ≤ x2) S) : ↑(⨆ (i : ι), S i) = ⋃ (i : ι), ↑(S i)

theorem Subgroup.coe_iSup_of_directed {G : Type u_1} [Group G] {ι : Sort u_5} [Nonempty ι] {S : ι → Subgroup G} (hS : Directed (fun (x1 x2 : Subgroup G) => x1 ≤ x2) S) : ↑(⨆ (i : ι), S i) = ⋃ (i : ι), ↑(S i)

theorem AddSubgroup.mem_sSup_of_directedOn {G : Type u_1} [AddGroup G] {K : Set (AddSubgroup G)} (Kne : K.Nonempty) (hK : DirectedOn (fun (x1 x2 : AddSubgroup G) => x1 ≤ x2) K) {x : G} : x ∈ sSup K ↔ ∃ s ∈ K, x ∈ s

theorem Subgroup.mem_sSup_of_directedOn {G : Type u_1} [Group G] {K : Set (Subgroup G)} (Kne : K.Nonempty) (hK : DirectedOn (fun (x1 x2 : Subgroup G) => x1 ≤ x2) K) {x : G} : x ∈ sSup K ↔ ∃ s ∈ K, x ∈ s

theorem AddSubgroup.comap.proof_2 {G : Type u_1} [AddGroup G] {N : Type u_2} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) : ∀ {a b : G}, a ∈ (AddSubmonoid.comap f H.toAddSubmonoid).carrier → b ∈ (AddSubmonoid.comap f H.toAddSubmonoid).carrier → a + b ∈ (AddSubmonoid.comap f H.toAddSubmonoid).carrier

theorem AddSubgroup.comap.proof_3 {G : Type u_1} [AddGroup G] {N : Type u_2} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) : 0 ∈ (AddSubmonoid.comap f H.toAddSubmonoid).carrier

theorem AddSubgroup.comap.proof_1 {G : Type u_2} [AddGroup G] {N : Type u_1} [AddGroup N] : AddMonoidHomClass (G →+ N) G N

def AddSubgroup.comap {G : Type u_1} [AddGroup G] {N : Type u_7} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) : AddSubgroup G

The preimage of an AddSubgroup along an AddMonoid homomorphism is an AddSubgroup.

Equations

• AddSubgroup.comap f H = { carrier := ⇑f ⁻¹' ↑H, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

theorem AddSubgroup.comap.proof_4 {G : Type u_1} [AddGroup G] {N : Type u_2} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) {a : G} (ha : a ∈ { carrier := ⇑f ⁻¹' ↑H, add_mem' := ⋯, zero_mem' := ⋯ }.carrier) : f (-a) ∈ H

def Subgroup.comap {G : Type u_1} [Group G] {N : Type u_7} [Group N] (f : G →* N) (H : Subgroup N) : Subgroup G

The preimage of a subgroup along a monoid homomorphism is a subgroup.

Equations

• Subgroup.comap f H = { carrier := ⇑f ⁻¹' ↑H, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem AddSubgroup.coe_comap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (K : AddSubgroup N) (f : G →+ N) : ↑(AddSubgroup.comap f K) = ⇑f ⁻¹' ↑K

@[simp]

theorem Subgroup.coe_comap {G : Type u_1} [Group G] {N : Type u_5} [Group N] (K : Subgroup N) (f : G →* N) : ↑(Subgroup.comap f K) = ⇑f ⁻¹' ↑K

@[simp]

theorem Subgroup.toAddSubgroup_comap {G : Type u_1} [Group G] {G₂ : Type u_7} [Group G₂] (f : G →* G₂) (s : Subgroup G₂) : AddSubgroup.comap (MonoidHom.toAdditive f) (Subgroup.toAddSubgroup s) = Subgroup.toAddSubgroup (Subgroup.comap f s)

@[simp]

theorem AddSubgroup.toSubgroup_comap {A : Type u_7} {A₂ : Type u_8} [AddGroup A] [AddGroup A₂] (f : A →+ A₂) (s : AddSubgroup A₂) : Subgroup.comap (AddMonoidHom.toMultiplicative f) (AddSubgroup.toSubgroup s) = AddSubgroup.toSubgroup (AddSubgroup.comap f s)

@[simp]

theorem AddSubgroup.mem_comap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {K : AddSubgroup N} {f : G →+ N} {x : G} : x ∈ AddSubgroup.comap f K ↔ f x ∈ K

@[simp]

theorem Subgroup.mem_comap {G : Type u_1} [Group G] {N : Type u_5} [Group N] {K : Subgroup N} {f : G →* N} {x : G} : x ∈ Subgroup.comap f K ↔ f x ∈ K

theorem AddSubgroup.comap_mono {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K : AddSubgroup N} {K' : AddSubgroup N} : K ≤ K' → AddSubgroup.comap f K ≤ AddSubgroup.comap f K'

theorem Subgroup.comap_mono {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {K : Subgroup N} {K' : Subgroup N} : K ≤ K' → Subgroup.comap f K ≤ Subgroup.comap f K'

theorem AddSubgroup.comap_comap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {P : Type u_6} [AddGroup P] (K : AddSubgroup P) (g : N →+ P) (f : G →+ N) : AddSubgroup.comap f (AddSubgroup.comap g K) = AddSubgroup.comap (g.comp f) K

theorem Subgroup.comap_comap {G : Type u_1} [Group G] {N : Type u_5} [Group N] {P : Type u_6} [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 AddSubgroup.comap_id {N : Type u_5} [AddGroup N] (K : AddSubgroup N) : AddSubgroup.comap (AddMonoidHom.id N) K = K

@[simp]

theorem Subgroup.comap_id {N : Type u_5} [Group N] (K : Subgroup N) : Subgroup.comap (MonoidHom.id N) K = K

theorem AddSubgroup.map.proof_3 {G : Type u_2} [AddGroup G] {N : Type u_1} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) : 0 ∈ (AddSubmonoid.map f H.toAddSubmonoid).carrier

theorem AddSubgroup.map.proof_4 {G : Type u_2} [AddGroup G] {N : Type u_1} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) : ∀ {x : N}, x ∈ { carrier := ⇑f '' ↑H, add_mem' := ⋯, zero_mem' := ⋯ }.carrier → -x ∈ { carrier := ⇑f '' ↑H, add_mem' := ⋯, zero_mem' := ⋯ }.carrier

theorem AddSubgroup.map.proof_2 {G : Type u_2} [AddGroup G] {N : Type u_1} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) : ∀ {a b : N}, a ∈ (AddSubmonoid.map f H.toAddSubmonoid).carrier → b ∈ (AddSubmonoid.map f H.toAddSubmonoid).carrier → a + b ∈ (AddSubmonoid.map f H.toAddSubmonoid).carrier

def AddSubgroup.map {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) : AddSubgroup N

The image of an AddSubgroup along an AddMonoid homomorphism is an AddSubgroup.

Equations

• AddSubgroup.map f H = { carrier := ⇑f '' ↑H, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

theorem AddSubgroup.map.proof_1 {G : Type u_2} [AddGroup G] {N : Type u_1} [AddGroup N] : AddMonoidHomClass (G →+ N) G N

def Subgroup.map {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup G) : Subgroup N

The image of a subgroup along a monoid homomorphism is a subgroup.

Equations

• Subgroup.map f H = { carrier := ⇑f '' ↑H, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem AddSubgroup.coe_map {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (K : AddSubgroup G) : ↑(AddSubgroup.map f K) = ⇑f '' ↑K

@[simp]

theorem Subgroup.coe_map {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (K : Subgroup G) : ↑(Subgroup.map f K) = ⇑f '' ↑K

@[simp]

theorem AddSubgroup.mem_map {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K : AddSubgroup G} {y : N} : y ∈ AddSubgroup.map f K ↔ ∃ x ∈ K, f x = y

@[simp]

theorem Subgroup.mem_map {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {K : Subgroup G} {y : N} : y ∈ Subgroup.map f K ↔ ∃ x ∈ K, f x = y

theorem AddSubgroup.mem_map_of_mem {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) {K : AddSubgroup G} {x : G} (hx : x ∈ K) : f x ∈ AddSubgroup.map f K

theorem Subgroup.mem_map_of_mem {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) {K : Subgroup G} {x : G} (hx : x ∈ K) : f x ∈ Subgroup.map f K

theorem AddSubgroup.apply_coe_mem_map {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (K : AddSubgroup G) (x : ↥K) : f ↑x ∈ AddSubgroup.map f K

theorem Subgroup.apply_coe_mem_map {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (K : Subgroup G) (x : ↥K) : f ↑x ∈ Subgroup.map f K

theorem AddSubgroup.map_mono {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K : AddSubgroup G} {K' : AddSubgroup G} : K ≤ K' → AddSubgroup.map f K ≤ AddSubgroup.map f K'

theorem Subgroup.map_mono {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {K : Subgroup G} {K' : Subgroup G} : K ≤ K' → Subgroup.map f K ≤ Subgroup.map f K'

@[simp]

theorem AddSubgroup.map_id {G : Type u_1} [AddGroup G] (K : AddSubgroup G) : AddSubgroup.map (AddMonoidHom.id G) K = K

@[simp]

theorem Subgroup.map_id {G : Type u_1} [Group G] (K : Subgroup G) : Subgroup.map (MonoidHom.id G) K = K

theorem AddSubgroup.map_map {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {N : Type u_5} [AddGroup N] {P : Type u_6} [AddGroup P] (g : N →+ P) (f : G →+ N) : AddSubgroup.map g (AddSubgroup.map f K) = AddSubgroup.map (g.comp f) K

theorem Subgroup.map_map {G : Type u_1} [Group G] (K : Subgroup G) {N : Type u_5} [Group N] {P : Type u_6} [Group P] (g : N →* P) (f : G →* N) : Subgroup.map g (Subgroup.map f K) = Subgroup.map (g.comp f) K

@[simp]

theorem AddSubgroup.map_zero_eq_bot {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {N : Type u_5} [AddGroup N] : AddSubgroup.map 0 K = ⊥

@[simp]

theorem Subgroup.map_one_eq_bot {G : Type u_1} [Group G] (K : Subgroup G) {N : Type u_5} [Group N] : Subgroup.map 1 K = ⊥

theorem AddSubgroup.mem_map_equiv {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G ≃+ N} {K : AddSubgroup G} {x : N} : x ∈ AddSubgroup.map f.toAddMonoidHom K ↔ f.symm x ∈ K

theorem Subgroup.mem_map_equiv {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G ≃* N} {K : Subgroup G} {x : N} : x ∈ Subgroup.map f.toMonoidHom K ↔ f.symm x ∈ K

@[simp]

theorem AddSubgroup.mem_map_iff_mem {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective ⇑f) {K : AddSubgroup G} {x : G} : f x ∈ AddSubgroup.map f K ↔ x ∈ K

@[simp]

theorem Subgroup.mem_map_iff_mem {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (hf : Function.Injective ⇑f) {K : Subgroup G} {x : G} : f x ∈ Subgroup.map f K ↔ x ∈ K

theorem AddSubgroup.map_equiv_eq_comap_symm' {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G ≃+ N) (K : AddSubgroup G) : AddSubgroup.map f.toAddMonoidHom K = AddSubgroup.comap f.symm.toAddMonoidHom K

theorem Subgroup.map_equiv_eq_comap_symm' {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G ≃* N) (K : Subgroup G) : Subgroup.map f.toMonoidHom K = Subgroup.comap f.symm.toMonoidHom K

theorem AddSubgroup.map_equiv_eq_comap_symm {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G ≃+ N) (K : AddSubgroup G) : AddSubgroup.map (↑f) K = AddSubgroup.comap (↑f.symm) K

theorem Subgroup.map_equiv_eq_comap_symm {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G ≃* N) (K : Subgroup G) : Subgroup.map (↑f) K = Subgroup.comap (↑f.symm) K

theorem AddSubgroup.comap_equiv_eq_map_symm {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : N ≃+ G) (K : AddSubgroup G) : AddSubgroup.comap (↑f) K = AddSubgroup.map (↑f.symm) K

theorem Subgroup.comap_equiv_eq_map_symm {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : N ≃* G) (K : Subgroup G) : Subgroup.comap (↑f) K = Subgroup.map (↑f.symm) K

theorem AddSubgroup.comap_equiv_eq_map_symm' {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : N ≃+ G) (K : AddSubgroup G) : AddSubgroup.comap f.toAddMonoidHom K = AddSubgroup.map f.symm.toAddMonoidHom K

theorem Subgroup.comap_equiv_eq_map_symm' {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : N ≃* G) (K : Subgroup G) : Subgroup.comap f.toMonoidHom K = Subgroup.map f.symm.toMonoidHom K

theorem AddSubgroup.map_symm_eq_iff_map_eq {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {N : Type u_5} [AddGroup N] {H : AddSubgroup N} {e : G ≃+ N} : AddSubgroup.map (↑e.symm) H = K ↔ AddSubgroup.map (↑e) K = H

theorem Subgroup.map_symm_eq_iff_map_eq {G : Type u_1} [Group G] (K : Subgroup G) {N : Type u_5} [Group N] {H : Subgroup N} {e : G ≃* N} : Subgroup.map (↑e.symm) H = K ↔ Subgroup.map (↑e) K = H

theorem AddSubgroup.map_le_iff_le_comap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K : AddSubgroup G} {H : AddSubgroup N} : AddSubgroup.map f K ≤ H ↔ K ≤ AddSubgroup.comap f H

theorem Subgroup.map_le_iff_le_comap {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {K : Subgroup G} {H : Subgroup N} : Subgroup.map f K ≤ H ↔ K ≤ Subgroup.comap f H

theorem AddSubgroup.gc_map_comap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : GaloisConnection (AddSubgroup.map f) (AddSubgroup.comap f)

theorem Subgroup.gc_map_comap {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : GaloisConnection (Subgroup.map f) (Subgroup.comap f)

theorem AddSubgroup.map_sup {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (K : AddSubgroup G) (f : G →+ N) : AddSubgroup.map f (H ⊔ K) = AddSubgroup.map f H ⊔ AddSubgroup.map f K

theorem Subgroup.map_sup {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (K : Subgroup G) (f : G →* N) : Subgroup.map f (H ⊔ K) = Subgroup.map f H ⊔ Subgroup.map f K

theorem AddSubgroup.map_iSup {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {ι : Sort u_7} (f : G →+ N) (s : ι → AddSubgroup G) : AddSubgroup.map f (iSup s) = ⨆ (i : ι), AddSubgroup.map f (s i)

theorem Subgroup.map_iSup {G : Type u_1} [Group G] {N : Type u_5} [Group N] {ι : Sort u_7} (f : G →* N) (s : ι → Subgroup G) : Subgroup.map f (iSup s) = ⨆ (i : ι), Subgroup.map f (s i)

theorem AddSubgroup.map_inf {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (K : AddSubgroup G) (f : G →+ N) (hf : Function.Injective ⇑f) : AddSubgroup.map f (H ⊓ K) = AddSubgroup.map f H ⊓ AddSubgroup.map f K

theorem Subgroup.map_inf {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (K : Subgroup G) (f : G →* N) (hf : Function.Injective ⇑f) : Subgroup.map f (H ⊓ K) = Subgroup.map f H ⊓ Subgroup.map f K

theorem AddSubgroup.map_iInf {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {ι : Sort u_7} [Nonempty ι] (f : G →+ N) (hf : Function.Injective ⇑f) (s : ι → AddSubgroup G) : AddSubgroup.map f (iInf s) = ⨅ (i : ι), AddSubgroup.map f (s i)

theorem Subgroup.map_iInf {G : Type u_1} [Group G] {N : Type u_5} [Group N] {ι : Sort u_7} [Nonempty ι] (f : G →* N) (hf : Function.Injective ⇑f) (s : ι → Subgroup G) : Subgroup.map f (iInf s) = ⨅ (i : ι), Subgroup.map f (s i)

theorem AddSubgroup.comap_sup_comap_le {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup N) (K : AddSubgroup N) (f : G →+ N) : AddSubgroup.comap f H ⊔ AddSubgroup.comap f K ≤ AddSubgroup.comap f (H ⊔ K)

theorem Subgroup.comap_sup_comap_le {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup N) (K : Subgroup N) (f : G →* N) : Subgroup.comap f H ⊔ Subgroup.comap f K ≤ Subgroup.comap f (H ⊔ K)

theorem AddSubgroup.iSup_comap_le {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {ι : Sort u_7} (f : G →+ N) (s : ι → AddSubgroup N) : ⨆ (i : ι), AddSubgroup.comap f (s i) ≤ AddSubgroup.comap f (iSup s)

theorem Subgroup.iSup_comap_le {G : Type u_1} [Group G] {N : Type u_5} [Group N] {ι : Sort u_7} (f : G →* N) (s : ι → Subgroup N) : ⨆ (i : ι), Subgroup.comap f (s i) ≤ Subgroup.comap f (iSup s)

theorem AddSubgroup.comap_inf {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup N) (K : AddSubgroup N) (f : G →+ N) : AddSubgroup.comap f (H ⊓ K) = AddSubgroup.comap f H ⊓ AddSubgroup.comap f K

theorem Subgroup.comap_inf {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup N) (K : Subgroup N) (f : G →* N) : Subgroup.comap f (H ⊓ K) = Subgroup.comap f H ⊓ Subgroup.comap f K

theorem AddSubgroup.comap_iInf {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {ι : Sort u_7} (f : G →+ N) (s : ι → AddSubgroup N) : AddSubgroup.comap f (iInf s) = ⨅ (i : ι), AddSubgroup.comap f (s i)

theorem Subgroup.comap_iInf {G : Type u_1} [Group G] {N : Type u_5} [Group N] {ι : Sort u_7} (f : G →* N) (s : ι → Subgroup N) : Subgroup.comap f (iInf s) = ⨅ (i : ι), Subgroup.comap f (s i)

theorem AddSubgroup.map_inf_le {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (K : AddSubgroup G) (f : G →+ N) : AddSubgroup.map f (H ⊓ K) ≤ AddSubgroup.map f H ⊓ AddSubgroup.map f K

theorem Subgroup.map_inf_le {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (K : Subgroup G) (f : G →* N) : Subgroup.map f (H ⊓ K) ≤ Subgroup.map f H ⊓ Subgroup.map f K

theorem AddSubgroup.map_inf_eq {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (K : AddSubgroup G) (f : G →+ N) (hf : Function.Injective ⇑f) : AddSubgroup.map f (H ⊓ K) = AddSubgroup.map f H ⊓ AddSubgroup.map f K

theorem Subgroup.map_inf_eq {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (K : Subgroup G) (f : G →* N) (hf : Function.Injective ⇑f) : Subgroup.map f (H ⊓ K) = Subgroup.map f H ⊓ Subgroup.map f K

@[simp]

theorem AddSubgroup.map_bot {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : AddSubgroup.map f ⊥ = ⊥

@[simp]

theorem Subgroup.map_bot {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : Subgroup.map f ⊥ = ⊥

@[simp]

theorem AddSubgroup.map_top_of_surjective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (h : Function.Surjective ⇑f) : AddSubgroup.map f ⊤ = ⊤

@[simp]

theorem Subgroup.map_top_of_surjective {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (h : Function.Surjective ⇑f) : Subgroup.map f ⊤ = ⊤

@[simp]

theorem AddSubgroup.comap_top {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : AddSubgroup.comap f ⊤ = ⊤

@[simp]

theorem Subgroup.comap_top {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : Subgroup.comap f ⊤ = ⊤

def AddSubgroup.addSubgroupOf {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) : AddSubgroup ↥K

For any subgroups H and K, view H ⊓ K as a subgroup of K.

Equations

• H.addSubgroupOf K = AddSubgroup.comap K.subtype H

def Subgroup.subgroupOf {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) : Subgroup ↥K

For any subgroups H and K, view H ⊓ K as a subgroup of K.

Equations

• H.subgroupOf K = Subgroup.comap K.subtype H

theorem AddSubgroup.addSubgroupOfEquivOfLe.proof_1 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (g : ↥(H.addSubgroupOf K)) : ↑g ∈ H.addSubgroupOf K

theorem AddSubgroup.addSubgroupOfEquivOfLe.proof_3 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (g : ↥H) : ↑g ∈ H

theorem AddSubgroup.addSubgroupOfEquivOfLe.proof_2 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H ≤ K) (g : ↥H) : ↑g ∈ K

def AddSubgroup.addSubgroupOfEquivOfLe {G : Type u_7} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H ≤ K) : ↥(H.addSubgroupOf K) ≃+ ↥H

If H ≤ K, then H as a subgroup of K is isomorphic to H.

Equations

• AddSubgroup.addSubgroupOfEquivOfLe h = { toFun := fun (g : ↥(H.addSubgroupOf K)) => ⟨↑↑g, ⋯⟩, invFun := fun (g : ↥H) => ⟨⟨↑g, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

theorem AddSubgroup.addSubgroupOfEquivOfLe.proof_6 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H ≤ K) (_g : ↥(H.addSubgroupOf K)) (_h : ↥(H.addSubgroupOf K)) : { toFun := fun (g : ↥(H.addSubgroupOf K)) => ⟨↑↑g, ⋯⟩, invFun := fun (g : ↥H) => ⟨⟨↑g, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.toFun (_g + _h) = { toFun := fun (g : ↥(H.addSubgroupOf K)) => ⟨↑↑g, ⋯⟩, invFun := fun (g : ↥H) => ⟨⟨↑g, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.toFun (_g + _h)

theorem AddSubgroup.addSubgroupOfEquivOfLe.proof_5 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H ≤ K) (_g : ↥H) : (fun (g : ↥(H.addSubgroupOf K)) => ⟨↑↑g, ⋯⟩) ((fun (g : ↥H) => ⟨⟨↑g, ⋯⟩, ⋯⟩) _g) = _g

theorem AddSubgroup.addSubgroupOfEquivOfLe.proof_4 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H ≤ K) (_g : ↥(H.addSubgroupOf K)) : (fun (g : ↥H) => ⟨⟨↑g, ⋯⟩, ⋯⟩) ((fun (g : ↥(H.addSubgroupOf K)) => ⟨↑↑g, ⋯⟩) _g) = _g

@[simp]

theorem Subgroup.subgroupOfEquivOfLe_apply_coe {G : Type u_7} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H ≤ K) (g : ↥(H.subgroupOf K)) : ↑((Subgroup.subgroupOfEquivOfLe h) g) = ↑↑g

@[simp]

theorem AddSubgroup.addSubgroupOfEquivOfLe_apply_coe {G : Type u_7} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H ≤ K) (g : ↥(H.addSubgroupOf K)) : ↑((AddSubgroup.addSubgroupOfEquivOfLe h) g) = ↑↑g

@[simp]

theorem AddSubgroup.addSubgroupOfEquivOfLe_symm_apply_coe_coe {G : Type u_7} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H ≤ K) (g : ↥H) : ↑↑((AddSubgroup.addSubgroupOfEquivOfLe h).symm g) = ↑g

@[simp]

theorem Subgroup.subgroupOfEquivOfLe_symm_apply_coe_coe {G : Type u_7} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H ≤ K) (g : ↥H) : ↑↑((Subgroup.subgroupOfEquivOfLe h).symm g) = ↑g

def Subgroup.subgroupOfEquivOfLe {G : Type u_7} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H ≤ K) : ↥(H.subgroupOf K) ≃* ↥H

If H ≤ K, then H as a subgroup of K is isomorphic to H.

Equations

• Subgroup.subgroupOfEquivOfLe h = { toFun := fun (g : ↥(H.subgroupOf K)) => ⟨↑↑g, ⋯⟩, invFun := fun (g : ↥H) => ⟨⟨↑g, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

@[simp]

theorem AddSubgroup.comap_subtype {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) : AddSubgroup.comap K.subtype H = H.addSubgroupOf K

@[simp]

theorem Subgroup.comap_subtype {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) : Subgroup.comap K.subtype H = H.subgroupOf K

@[simp]

theorem AddSubgroup.comap_inclusion_addSubgroupOf {G : Type u_1} [AddGroup G] {K₁ : AddSubgroup G} {K₂ : AddSubgroup G} (h : K₁ ≤ K₂) (H : AddSubgroup G) : AddSubgroup.comap (AddSubgroup.inclusion h) (H.addSubgroupOf K₂) = H.addSubgroupOf K₁

@[simp]

theorem Subgroup.comap_inclusion_subgroupOf {G : Type u_1} [Group G] {K₁ : Subgroup G} {K₂ : Subgroup G} (h : K₁ ≤ K₂) (H : Subgroup G) : Subgroup.comap (Subgroup.inclusion h) (H.subgroupOf K₂) = H.subgroupOf K₁

theorem AddSubgroup.coe_addSubgroupOf {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) : ↑(H.addSubgroupOf K) = ⇑K.subtype ⁻¹' ↑H

theorem Subgroup.coe_subgroupOf {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) : ↑(H.subgroupOf K) = ⇑K.subtype ⁻¹' ↑H

theorem AddSubgroup.mem_addSubgroupOf {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} {h : ↥K} : h ∈ H.addSubgroupOf K ↔ ↑h ∈ H

theorem Subgroup.mem_subgroupOf {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {h : ↥K} : h ∈ H.subgroupOf K ↔ ↑h ∈ H

@[simp]

theorem AddSubgroup.addSubgroupOf_map_subtype {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) : AddSubgroup.map K.subtype (H.addSubgroupOf K) = H ⊓ K

@[simp]

theorem Subgroup.subgroupOf_map_subtype {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) : Subgroup.map K.subtype (H.subgroupOf K) = H ⊓ K

@[simp]

theorem AddSubgroup.bot_addSubgroupOf {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : ⊥.addSubgroupOf H = ⊥

@[simp]

theorem Subgroup.bot_subgroupOf {G : Type u_1} [Group G] (H : Subgroup G) : ⊥.subgroupOf H = ⊥

@[simp]

theorem AddSubgroup.top_addSubgroupOf {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : ⊤.addSubgroupOf H = ⊤

@[simp]

theorem Subgroup.top_subgroupOf {G : Type u_1} [Group G] (H : Subgroup G) : ⊤.subgroupOf H = ⊤

theorem AddSubgroup.addSubgroupOf_bot_eq_bot {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.addSubgroupOf ⊥ = ⊥

theorem Subgroup.subgroupOf_bot_eq_bot {G : Type u_1} [Group G] (H : Subgroup G) : H.subgroupOf ⊥ = ⊥

theorem AddSubgroup.addSubgroupOf_bot_eq_top {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.addSubgroupOf ⊥ = ⊤

theorem Subgroup.subgroupOf_bot_eq_top {G : Type u_1} [Group G] (H : Subgroup G) : H.subgroupOf ⊥ = ⊤

@[simp]

theorem AddSubgroup.addSubgroupOf_self {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.addSubgroupOf H = ⊤

@[simp]

theorem Subgroup.subgroupOf_self {G : Type u_1} [Group G] (H : Subgroup G) : H.subgroupOf H = ⊤

@[simp]

theorem AddSubgroup.addSubgroupOf_inj {G : Type u_1} [AddGroup G] {H₁ : AddSubgroup G} {H₂ : AddSubgroup G} {K : AddSubgroup G} : H₁.addSubgroupOf K = H₂.addSubgroupOf K ↔ H₁ ⊓ K = H₂ ⊓ K

@[simp]

theorem Subgroup.subgroupOf_inj {G : Type u_1} [Group G] {H₁ : Subgroup G} {H₂ : Subgroup G} {K : Subgroup G} : H₁.subgroupOf K = H₂.subgroupOf K ↔ H₁ ⊓ K = H₂ ⊓ K

@[simp]

theorem AddSubgroup.inf_addSubgroupOf_right {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) : (H ⊓ K).addSubgroupOf K = H.addSubgroupOf K

@[simp]

theorem Subgroup.inf_subgroupOf_right {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) : (H ⊓ K).subgroupOf K = H.subgroupOf K

@[simp]

theorem AddSubgroup.inf_addSubgroupOf_left {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) : (K ⊓ H).addSubgroupOf K = H.addSubgroupOf K

@[simp]

theorem Subgroup.inf_subgroupOf_left {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) : (K ⊓ H).subgroupOf K = H.subgroupOf K

@[simp]

theorem AddSubgroup.addSubgroupOf_eq_bot {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} : H.addSubgroupOf K = ⊥ ↔ Disjoint H K

@[simp]

theorem Subgroup.subgroupOf_eq_bot {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} : H.subgroupOf K = ⊥ ↔ Disjoint H K

@[simp]

theorem AddSubgroup.addSubgroupOf_eq_top {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} : H.addSubgroupOf K = ⊤ ↔ K ≤ H

@[simp]

theorem Subgroup.subgroupOf_eq_top {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} : H.subgroupOf K = ⊤ ↔ K ≤ H

def AddSubgroup.prod {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (K : AddSubgroup N) : AddSubgroup (G × N)

Given AddSubgroups H, K of AddGroups A, B respectively, H × K as an AddSubgroup of A × B.

Equations

• H.prod K = { toAddSubmonoid := H.prod K.toAddSubmonoid, neg_mem' := ⋯ }

theorem AddSubgroup.prod.proof_1 {G : Type u_1} [AddGroup G] {N : Type u_2} [AddGroup N] (H : AddSubgroup G) (K : AddSubgroup N) : ∀ {x : G × N}, x ∈ (H.prod K.toAddSubmonoid).carrier → (-x).1 ∈ ↑H.toAddSubmonoid ∧ (-x).2 ∈ ↑K.toAddSubmonoid

def Subgroup.prod {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (K : Subgroup N) : Subgroup (G × N)

Given Subgroups H, K of groups G, N respectively, H × K as a subgroup of G × N.

Equations

• H.prod K = { toSubmonoid := H.prod K.toSubmonoid, inv_mem' := ⋯ }

theorem AddSubgroup.coe_prod {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (K : AddSubgroup N) : ↑(H.prod K) = ↑H ×ˢ ↑K

theorem Subgroup.coe_prod {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (K : Subgroup N) : ↑(H.prod K) = ↑H ×ˢ ↑K

theorem AddSubgroup.mem_prod {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup G} {K : AddSubgroup N} {p : G × N} : p ∈ H.prod K ↔ p.1 ∈ H ∧ p.2 ∈ K

theorem Subgroup.mem_prod {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H : Subgroup G} {K : Subgroup N} {p : G × N} : p ∈ H.prod K ↔ p.1 ∈ H ∧ p.2 ∈ K

theorem AddSubgroup.prod_mono {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] : ((fun (x1 x2 : AddSubgroup G) => x1 ≤ x2) ⇒ (fun (x1 x2 : AddSubgroup N) => x1 ≤ x2) ⇒ fun (x1 x2 : AddSubgroup (G × N)) => x1 ≤ x2) AddSubgroup.prod AddSubgroup.prod

theorem Subgroup.prod_mono {G : Type u_1} [Group G] {N : Type u_5} [Group N] : ((fun (x1 x2 : Subgroup G) => x1 ≤ x2) ⇒ (fun (x1 x2 : Subgroup N) => x1 ≤ x2) ⇒ fun (x1 x2 : Subgroup (G × N)) => x1 ≤ x2) Subgroup.prod Subgroup.prod

theorem AddSubgroup.prod_mono_right {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (K : AddSubgroup G) : Monotone fun (t : AddSubgroup N) => K.prod t

theorem Subgroup.prod_mono_right {G : Type u_1} [Group G] {N : Type u_5} [Group N] (K : Subgroup G) : Monotone fun (t : Subgroup N) => K.prod t

theorem AddSubgroup.prod_mono_left {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup N) : Monotone fun (K : AddSubgroup G) => K.prod H

theorem Subgroup.prod_mono_left {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup N) : Monotone fun (K : Subgroup G) => K.prod H

theorem AddSubgroup.prod_top {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (K : AddSubgroup G) : K.prod ⊤ = AddSubgroup.comap (AddMonoidHom.fst G N) K

theorem Subgroup.prod_top {G : Type u_1} [Group G] {N : Type u_5} [Group N] (K : Subgroup G) : K.prod ⊤ = Subgroup.comap (MonoidHom.fst G N) K

theorem AddSubgroup.top_prod {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup N) : ⊤.prod H = AddSubgroup.comap (AddMonoidHom.snd G N) H

theorem Subgroup.top_prod {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup N) : ⊤.prod H = Subgroup.comap (MonoidHom.snd G N) H

@[simp]

theorem AddSubgroup.top_prod_top {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] : ⊤.prod ⊤ = ⊤

@[simp]

theorem Subgroup.top_prod_top {G : Type u_1} [Group G] {N : Type u_5} [Group N] : ⊤.prod ⊤ = ⊤

theorem AddSubgroup.bot_sum_bot {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] : ⊥.prod ⊥ = ⊥

theorem Subgroup.bot_prod_bot {G : Type u_1} [Group G] {N : Type u_5} [Group N] : ⊥.prod ⊥ = ⊥

theorem AddSubgroup.le_prod_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup G} {K : AddSubgroup N} {J : AddSubgroup (G × N)} : J ≤ H.prod K ↔ AddSubgroup.map (AddMonoidHom.fst G N) J ≤ H ∧ AddSubgroup.map (AddMonoidHom.snd G N) J ≤ K

theorem Subgroup.le_prod_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H : Subgroup G} {K : Subgroup N} {J : Subgroup (G × N)} : J ≤ H.prod K ↔ Subgroup.map (MonoidHom.fst G N) J ≤ H ∧ Subgroup.map (MonoidHom.snd G N) J ≤ K

theorem AddSubgroup.prod_le_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup G} {K : AddSubgroup N} {J : AddSubgroup (G × N)} : H.prod K ≤ J ↔ AddSubgroup.map (AddMonoidHom.inl G N) H ≤ J ∧ AddSubgroup.map (AddMonoidHom.inr G N) K ≤ J

theorem Subgroup.prod_le_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H : Subgroup G} {K : Subgroup N} {J : Subgroup (G × N)} : H.prod K ≤ J ↔ Subgroup.map (MonoidHom.inl G N) H ≤ J ∧ Subgroup.map (MonoidHom.inr G N) K ≤ J

@[simp]

theorem AddSubgroup.prod_eq_bot_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup G} {K : AddSubgroup N} : H.prod K = ⊥ ↔ H = ⊥ ∧ K = ⊥

@[simp]

theorem Subgroup.prod_eq_bot_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H : Subgroup G} {K : Subgroup N} : H.prod K = ⊥ ↔ H = ⊥ ∧ K = ⊥

theorem AddSubgroup.closure_prod {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {s : Set G} {t : Set N} (hs : 0 ∈ s) (ht : 0 ∈ t) : AddSubgroup.closure (s ×ˢ t) = (AddSubgroup.closure s).prod (AddSubgroup.closure t)

theorem Subgroup.closure_prod {G : Type u_1} [Group G] {N : Type u_5} [Group N] {s : Set G} {t : Set N} (hs : 1 ∈ s) (ht : 1 ∈ t) : Subgroup.closure (s ×ˢ t) = (Subgroup.closure s).prod (Subgroup.closure t)

theorem AddSubgroup.prodEquiv.proof_1 {G : Type u_1} [AddGroup G] {N : Type u_2} [AddGroup N] (H : AddSubgroup G) (K : AddSubgroup N) : ∀ (x x_1 : ↥(H.prod K)), (Equiv.Set.prod ↑H ↑K).toFun (x + x_1) = (Equiv.Set.prod ↑H ↑K).toFun (x + x_1)

def AddSubgroup.prodEquiv {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (K : AddSubgroup N) : ↥(H.prod K) ≃+ ↥H × ↥K

Product of additive subgroups is isomorphic to their product as additive groups

Equations

• H.prodEquiv K = { toEquiv := Equiv.Set.prod ↑H ↑K, map_add' := ⋯ }

def Subgroup.prodEquiv {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (K : Subgroup N) : ↥(H.prod K) ≃* ↥H × ↥K

Product of subgroups is isomorphic to their product as groups.

Equations

• H.prodEquiv K = { toEquiv := Equiv.Set.prod ↑H ↑K, map_mul' := ⋯ }

theorem AddSubmonoid.pi.proof_1 {η : Type u_1} {f : η → Type u_2} [(i : η) → AddZeroClass (f i)] (I : Set η) (s : (i : η) → AddSubmonoid (f i)) : ∀ {a b : (i : η) → f i}, (a ∈ I.pi fun (i : η) => (s i).carrier) → (b ∈ I.pi fun (i : η) => (s i).carrier) → ∀ i ∈ I, a i + b i ∈ s i

theorem AddSubmonoid.pi.proof_2 {η : Type u_1} {f : η → Type u_2} [(i : η) → AddZeroClass (f i)] (I : Set η) (s : (i : η) → AddSubmonoid (f i)) (i : η) : i ∈ I → 0 ∈ s i

def AddSubmonoid.pi {η : Type u_7} {f : η → Type u_8} [(i : η) → AddZeroClass (f i)] (I : Set η) (s : (i : η) → AddSubmonoid (f i)) : AddSubmonoid ((i : η) → f i)

A version of Set.pi for AddSubmonoids. Given an index set I and a family of submodules s : Π i, AddSubmonoid f i, pi I s is the AddSubmonoid of dependent functions f : Π i, f i such that f i belongs to pi I s whenever i ∈ I.

Equations

• AddSubmonoid.pi I s = { carrier := I.pi fun (i : η) => (s i).carrier, add_mem' := ⋯, zero_mem' := ⋯ }

def Submonoid.pi {η : Type u_7} {f : η → Type u_8} [(i : η) → MulOneClass (f i)] (I : Set η) (s : (i : η) → Submonoid (f i)) : Submonoid ((i : η) → 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.

Equations

• Submonoid.pi I s = { carrier := I.pi fun (i : η) => (s i).carrier, mul_mem' := ⋯, one_mem' := ⋯ }

theorem AddSubgroup.pi.proof_1 {η : Type u_1} {f : η → Type u_2} [(i : η) → AddGroup (f i)] (I : Set η) (H : (i : η) → AddSubgroup (f i)) : ∀ {x : (i : η) → f i}, x ∈ (AddSubmonoid.pi I fun (i : η) => (H i).toAddSubmonoid).carrier → ∀ i ∈ I, -x i ∈ H i

def AddSubgroup.pi {η : Type u_7} {f : η → Type u_8} [(i : η) → AddGroup (f i)] (I : Set η) (H : (i : η) → AddSubgroup (f i)) : AddSubgroup ((i : η) → f i)

A version of Set.pi for AddSubgroups. Given an index set I and a family of submodules s : Π i, AddSubgroup f i, pi I s is the AddSubgroup of dependent functions f : Π i, f i such that f i belongs to pi I s whenever i ∈ I.

Equations

• AddSubgroup.pi I H = { toAddSubmonoid := AddSubmonoid.pi I fun (i : η) => (H i).toAddSubmonoid, neg_mem' := ⋯ }

def Subgroup.pi {η : Type u_7} {f : η → Type u_8} [(i : η) → Group (f i)] (I : Set η) (H : (i : η) → Subgroup (f i)) : Subgroup ((i : η) → 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 = { toSubmonoid := Submonoid.pi I fun (i : η) => (H i).toSubmonoid, inv_mem' := ⋯ }

theorem AddSubgroup.coe_pi {η : Type u_7} {f : η → Type u_8} [(i : η) → AddGroup (f i)] (I : Set η) (H : (i : η) → AddSubgroup (f i)) : ↑(AddSubgroup.pi I H) = I.pi fun (i : η) => ↑(H i)

theorem Subgroup.coe_pi {η : Type u_7} {f : η → Type u_8} [(i : η) → Group (f i)] (I : Set η) (H : (i : η) → Subgroup (f i)) : ↑(Subgroup.pi I H) = I.pi fun (i : η) => ↑(H i)

theorem AddSubgroup.mem_pi {η : Type u_7} {f : η → Type u_8} [(i : η) → AddGroup (f i)] (I : Set η) {H : (i : η) → AddSubgroup (f i)} {p : (i : η) → f i} : p ∈ AddSubgroup.pi I H ↔ ∀ i ∈ I, p i ∈ H i

theorem Subgroup.mem_pi {η : Type u_7} {f : η → Type u_8} [(i : η) → Group (f i)] (I : Set η) {H : (i : η) → Subgroup (f i)} {p : (i : η) → f i} : p ∈ Subgroup.pi I H ↔ ∀ i ∈ I, p i ∈ H i

theorem AddSubgroup.pi_top {η : Type u_7} {f : η → Type u_8} [(i : η) → AddGroup (f i)] (I : Set η) : (AddSubgroup.pi I fun (i : η) => ⊤) = ⊤

theorem Subgroup.pi_top {η : Type u_7} {f : η → Type u_8} [(i : η) → Group (f i)] (I : Set η) : (Subgroup.pi I fun (i : η) => ⊤) = ⊤

theorem AddSubgroup.pi_empty {η : Type u_7} {f : η → Type u_8} [(i : η) → AddGroup (f i)] (H : (i : η) → AddSubgroup (f i)) : AddSubgroup.pi ∅ H = ⊤

theorem Subgroup.pi_empty {η : Type u_7} {f : η → Type u_8} [(i : η) → Group (f i)] (H : (i : η) → Subgroup (f i)) : Subgroup.pi ∅ H = ⊤

theorem AddSubgroup.pi_bot {η : Type u_7} {f : η → Type u_8} [(i : η) → AddGroup (f i)] : (AddSubgroup.pi Set.univ fun (i : η) => ⊥) = ⊥

theorem Subgroup.pi_bot {η : Type u_7} {f : η → Type u_8} [(i : η) → Group (f i)] : (Subgroup.pi Set.univ fun (i : η) => ⊥) = ⊥

theorem AddSubgroup.le_pi_iff {η : Type u_7} {f : η → Type u_8} [(i : η) → AddGroup (f i)] {I : Set η} {H : (i : η) → AddSubgroup (f i)} {J : AddSubgroup ((i : η) → f i)} : J ≤ AddSubgroup.pi I H ↔ ∀ i ∈ I, AddSubgroup.map (Pi.evalAddMonoidHom f i) J ≤ H i

theorem Subgroup.le_pi_iff {η : Type u_7} {f : η → Type u_8} [(i : η) → Group (f i)] {I : Set η} {H : (i : η) → Subgroup (f i)} {J : Subgroup ((i : η) → f i)} : J ≤ Subgroup.pi I H ↔ ∀ i ∈ I, Subgroup.map (Pi.evalMonoidHom f i) J ≤ H i

@[simp]

theorem AddSubgroup.single_mem_pi {η : Type u_7} {f : η → Type u_8} [(i : η) → AddGroup (f i)] [DecidableEq η] {I : Set η} {H : (i : η) → AddSubgroup (f i)} (i : η) (x : f i) : Pi.single i x ∈ AddSubgroup.pi I H ↔ i ∈ I → x ∈ H i

@[simp]

theorem Subgroup.mulSingle_mem_pi {η : Type u_7} {f : η → Type u_8} [(i : η) → Group (f i)] [DecidableEq η] {I : Set η} {H : (i : η) → Subgroup (f i)} (i : η) (x : f i) : Pi.mulSingle i x ∈ Subgroup.pi I H ↔ i ∈ I → x ∈ H i

theorem AddSubgroup.pi_eq_bot_iff {η : Type u_7} {f : η → Type u_8} [(i : η) → AddGroup (f i)] (H : (i : η) → AddSubgroup (f i)) : AddSubgroup.pi Set.univ H = ⊥ ↔ ∀ (i : η), H i = ⊥

theorem Subgroup.pi_eq_bot_iff {η : Type u_7} {f : η → Type u_8} [(i : η) → Group (f i)] (H : (i : η) → Subgroup (f i)) : Subgroup.pi Set.univ H = ⊥ ↔ ∀ (i : η), H i = ⊥

class Subgroup.Characteristic {G : Type u_1} [Group G] (H : Subgroup G) : Prop

A subgroup is characteristic if it is fixed by all automorphisms. Several equivalent conditions are provided by lemmas of the form Characteristic.iff...

• fixed : ∀ (ϕ : G ≃* G), Subgroup.comap ϕ.toMonoidHom H = H

  H is fixed by all automorphisms

theorem Subgroup.Characteristic.fixed {G : Type u_1} [Group G] {H : Subgroup G} (self : H.Characteristic) (ϕ : G ≃* G) : Subgroup.comap ϕ.toMonoidHom H = H

H is fixed by all automorphisms

@[instance 100]

instance Subgroup.normal_of_characteristic {G : Type u_1} [Group G] (H : Subgroup G) [h : H.Characteristic] : H.Normal

Equations

• ⋯ = ⋯

class AddSubgroup.Characteristic {A : Type u_4} [AddGroup A] (H : AddSubgroup A) : Prop

An AddSubgroup is characteristic if it is fixed by all automorphisms. Several equivalent conditions are provided by lemmas of the form Characteristic.iff...

• fixed : ∀ (ϕ : A ≃+ A), AddSubgroup.comap ϕ.toAddMonoidHom H = H

  H is fixed by all automorphisms

theorem AddSubgroup.Characteristic.fixed {A : Type u_4} [AddGroup A] {H : AddSubgroup A} (self : H.Characteristic) (ϕ : A ≃+ A) : AddSubgroup.comap ϕ.toAddMonoidHom H = H

H is fixed by all automorphisms

@[instance 100]

instance AddSubgroup.normal_of_characteristic {A : Type u_4} [AddGroup A] (H : AddSubgroup A) [h : H.Characteristic] : H.Normal

Equations

• ⋯ = ⋯

theorem AddSubgroup.characteristic_iff_comap_eq {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃+ G), AddSubgroup.comap ϕ.toAddMonoidHom H = H

theorem Subgroup.characteristic_iff_comap_eq {G : Type u_1} [Group G] {H : Subgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃* G), Subgroup.comap ϕ.toMonoidHom H = H

theorem AddSubgroup.characteristic_iff_comap_le {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃+ G), AddSubgroup.comap ϕ.toAddMonoidHom H ≤ H

theorem Subgroup.characteristic_iff_comap_le {G : Type u_1} [Group G] {H : Subgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃* G), Subgroup.comap ϕ.toMonoidHom H ≤ H

theorem AddSubgroup.characteristic_iff_le_comap {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃+ G), H ≤ AddSubgroup.comap ϕ.toAddMonoidHom H

theorem Subgroup.characteristic_iff_le_comap {G : Type u_1} [Group G] {H : Subgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ Subgroup.comap ϕ.toMonoidHom H

theorem AddSubgroup.characteristic_iff_map_eq {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃+ G), AddSubgroup.map ϕ.toAddMonoidHom H = H

theorem Subgroup.characteristic_iff_map_eq {G : Type u_1} [Group G] {H : Subgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃* G), Subgroup.map ϕ.toMonoidHom H = H

theorem AddSubgroup.characteristic_iff_map_le {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃+ G), AddSubgroup.map ϕ.toAddMonoidHom H ≤ H

theorem Subgroup.characteristic_iff_map_le {G : Type u_1} [Group G] {H : Subgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃* G), Subgroup.map ϕ.toMonoidHom H ≤ H

theorem AddSubgroup.characteristic_iff_le_map {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃+ G), H ≤ AddSubgroup.map ϕ.toAddMonoidHom H

theorem Subgroup.characteristic_iff_le_map {G : Type u_1} [Group G] {H : Subgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ Subgroup.map ϕ.toMonoidHom H

instance AddSubgroup.botCharacteristic {G : Type u_1} [AddGroup G] : ⊥.Characteristic

Equations

• ⋯ = ⋯

instance Subgroup.botCharacteristic {G : Type u_1} [Group G] : ⊥.Characteristic

Equations

• ⋯ = ⋯

instance AddSubgroup.topCharacteristic {G : Type u_1} [AddGroup G] : ⊤.Characteristic

Equations

• ⋯ = ⋯

instance Subgroup.topCharacteristic {G : Type u_1} [Group G] : ⊤.Characteristic

Equations

• ⋯ = ⋯

@[instance 100]

instance AddSubgroup.normal_in_normalizer {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : (H.addSubgroupOf H.normalizer).Normal

Equations

• ⋯ = ⋯

@[instance 100]

instance Subgroup.normal_in_normalizer {G : Type u_1} [Group G] {H : Subgroup G} : (H.subgroupOf H.normalizer).Normal

Equations

• ⋯ = ⋯

theorem AddSubgroup.normalizer_eq_top {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.normalizer = ⊤ ↔ H.Normal

theorem Subgroup.normalizer_eq_top {G : Type u_1} [Group G] {H : Subgroup G} : H.normalizer = ⊤ ↔ H.Normal

theorem AddSubgroup.le_normalizer_of_normal {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} [hK : (H.addSubgroupOf K).Normal] (HK : H ≤ K) : K ≤ H.normalizer

theorem Subgroup.le_normalizer_of_normal {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} [hK : (H.subgroupOf K).Normal] (HK : H ≤ K) : K ≤ H.normalizer

theorem AddSubgroup.le_normalizer_comap {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {N : Type u_5} [AddGroup N] (f : N →+ G) : AddSubgroup.comap f H.normalizer ≤ (AddSubgroup.comap f H).normalizer

The preimage of the normalizer is contained in the normalizer of the preimage.

theorem Subgroup.le_normalizer_comap {G : Type u_1} [Group G] {H : Subgroup G} {N : Type u_5} [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 AddSubgroup.le_normalizer_map {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {N : Type u_5} [AddGroup N] (f : G →+ N) : AddSubgroup.map f H.normalizer ≤ (AddSubgroup.map f H).normalizer

The image of the normalizer is contained in the normalizer of the image.

theorem Subgroup.le_normalizer_map {G : Type u_1} [Group G] {H : Subgroup G} {N : Type u_5} [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.

def NormalizerCondition (G : Type u_1) [Group G] : Prop

Every proper subgroup H of G is a proper normal subgroup of the normalizer of H in G.

Equations

• NormalizerCondition G = ∀ H < ⊤, H < H.normalizer

theorem normalizerCondition_iff_only_full_group_self_normalizing {G : Type u_1} [Group G] : NormalizerCondition 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.

instance AddSubgroup.map_isCommutative {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (f : G →+ G') [H.IsCommutative] : (AddSubgroup.map f H).IsCommutative

Equations

• ⋯ = ⋯

instance Subgroup.map_isCommutative {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (f : G →* G') [H.IsCommutative] : (Subgroup.map f H).IsCommutative

Equations

• ⋯ = ⋯

theorem AddSubgroup.comap_injective_isCommutative {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) {f : G' →+ G} (hf : Function.Injective ⇑f) [H.IsCommutative] : (AddSubgroup.comap f H).IsCommutative

theorem Subgroup.comap_injective_isCommutative {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) {f : G' →* G} (hf : Function.Injective ⇑f) [H.IsCommutative] : (Subgroup.comap f H).IsCommutative

instance AddSubgroup.addSubgroupOf_isCommutative {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {K : AddSubgroup G} [H.IsCommutative] : (H.addSubgroupOf K).IsCommutative

Equations

• ⋯ = ⋯

instance Subgroup.subgroupOf_isCommutative {G : Type u_1} [Group G] (H : Subgroup G) {K : Subgroup G} [H.IsCommutative] : (H.subgroupOf K).IsCommutative

Equations

• ⋯ = ⋯

@[simp]

theorem MulEquiv.comapSubgroup_symm_apply {G : Type u_1} [Group G] {H : Type u_5} [Group H✝] (f : G ≃* H✝) (H : Subgroup G) : (RelIso.symm f.comapSubgroup) H = Subgroup.comap (↑f.symm) H

@[simp]

theorem MulEquiv.comapSubgroup_apply {G : Type u_1} [Group G] {H : Type u_5} [Group H✝] (f : G ≃* H✝) (H : Subgroup H✝) : f.comapSubgroup H = Subgroup.comap (↑f) H

def MulEquiv.comapSubgroup {G : Type u_1} [Group G] {H : Type u_5} [Group H] (f : G ≃* H) : Subgroup H ≃o Subgroup G

An isomorphism of groups gives an order isomorphism between the lattices of subgroups, defined by sending subgroups to their inverse images.

See also MulEquiv.mapSubgroup which maps subgroups to their forward images.

Equations

• f.comapSubgroup = { toFun := Subgroup.comap ↑f, invFun := Subgroup.comap ↑f.symm, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem MulEquiv.mapSubgroup_apply {G : Type u_1} [Group G] {H : Type u_6} [Group H✝] (f : G ≃* H✝) (H : Subgroup G) : f.mapSubgroup H = Subgroup.map (↑f) H

@[simp]

theorem MulEquiv.mapSubgroup_symm_apply {G : Type u_1} [Group G] {H : Type u_6} [Group H✝] (f : G ≃* H✝) (H : Subgroup H✝) : (RelIso.symm f.mapSubgroup) H = Subgroup.map (↑f.symm) H

def MulEquiv.mapSubgroup {G : Type u_1} [Group G] {H : Type u_6} [Group H] (f : G ≃* H) : Subgroup G ≃o Subgroup H

An isomorphism of groups gives an order isomorphism between the lattices of subgroups, defined by sending subgroups to their forward images.

See also MulEquiv.comapSubgroup which maps subgroups to their inverse images.

Equations

• f.mapSubgroup = { toFun := Subgroup.map ↑f, invFun := Subgroup.map ↑f.symm, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

def Group.conjugatesOfSet {G : Type u_1} [Group G] (s : Set G) : Set G

Given a set s, conjugatesOfSet s is the set of all conjugates of the elements of s.

Equations

• Group.conjugatesOfSet s = ⋃ a ∈ s, conjugatesOf a

theorem Group.mem_conjugatesOfSet_iff {G : Type u_1} [Group G] {s : Set G} {x : G} : x ∈ Group.conjugatesOfSet s ↔ ∃ a ∈ s, IsConj a x

theorem Group.subset_conjugatesOfSet {G : Type u_1} [Group G] {s : Set G} : s ⊆ Group.conjugatesOfSet s

theorem Group.conjugatesOfSet_mono {G : Type u_1} [Group G] {s : Set G} {t : Set G} (h : s ⊆ t) : Group.conjugatesOfSet s ⊆ Group.conjugatesOfSet t

theorem Group.conjugates_subset_normal {G : Type u_1} [Group G] {N : Subgroup G} [tn : N.Normal] {a : G} (h : a ∈ N) : conjugatesOf a ⊆ ↑N

theorem Group.conjugatesOfSet_subset {G : Type u_1} [Group G] {s : Set G} {N : Subgroup G} [N.Normal] (h : s ⊆ ↑N) : Group.conjugatesOfSet s ⊆ ↑N

theorem Group.conj_mem_conjugatesOfSet {G : Type u_1} [Group G] {s : Set G} {x : G} {c : G} : x ∈ Group.conjugatesOfSet s → c * x * c⁻¹ ∈ Group.conjugatesOfSet s

The set of conjugates of s is closed under conjugation.

def Subgroup.normalClosure {G : Type u_1} [Group G] (s : Set G) : Subgroup G

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

• Subgroup.normalClosure s = Subgroup.closure (Group.conjugatesOfSet s)

theorem Subgroup.conjugatesOfSet_subset_normalClosure {G : Type u_1} [Group G] {s : Set G} : Group.conjugatesOfSet s ⊆ ↑(Subgroup.normalClosure s)

theorem Subgroup.subset_normalClosure {G : Type u_1} [Group G] {s : Set G} : s ⊆ ↑(Subgroup.normalClosure s)

theorem Subgroup.le_normalClosure {G : Type u_1} [Group G] {H : Subgroup G} : H ≤ Subgroup.normalClosure ↑H

instance Subgroup.normalClosure_normal {G : Type u_1} [Group G] {s : Set G} : (Subgroup.normalClosure s).Normal

The normal closure of s is a normal subgroup.

Equations

• ⋯ = ⋯

theorem Subgroup.normalClosure_le_normal {G : Type u_1} [Group G] {s : Set G} {N : Subgroup G} [N.Normal] (h : s ⊆ ↑N) : Subgroup.normalClosure s ≤ N

The normal closure of s is the smallest normal subgroup containing s.

theorem Subgroup.normalClosure_subset_iff {G : Type u_1} [Group G] {s : Set G} {N : Subgroup G} [N.Normal] : s ⊆ ↑N ↔ Subgroup.normalClosure s ≤ N

theorem Subgroup.normalClosure_mono {G : Type u_1} [Group G] {s : Set G} {t : Set G} (h : s ⊆ t) : Subgroup.normalClosure s ≤ Subgroup.normalClosure t

theorem Subgroup.normalClosure_eq_iInf {G : Type u_1} [Group G] {s : Set G} : Subgroup.normalClosure s = ⨅ (N : Subgroup G), ⨅ (_ : N.Normal), ⨅ (_ : s ⊆ ↑N), N

@[simp]

theorem Subgroup.normalClosure_eq_self {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] : Subgroup.normalClosure ↑H = H

theorem Subgroup.normalClosure_idempotent {G : Type u_1} [Group G] {s : Set G} : Subgroup.normalClosure ↑(Subgroup.normalClosure s) = Subgroup.normalClosure s

theorem Subgroup.closure_le_normalClosure {G : Type u_1} [Group G] {s : Set G} : Subgroup.closure s ≤ Subgroup.normalClosure s

@[simp]

theorem Subgroup.normalClosure_closure_eq_normalClosure {G : Type u_1} [Group G] {s : Set G} : Subgroup.normalClosure ↑(Subgroup.closure s) = Subgroup.normalClosure s

def Subgroup.normalCore {G : Type u_1} [Group G] (H : Subgroup G) : Subgroup G

The normal core of a subgroup H is the largest normal subgroup of G contained in H, as shown by Subgroup.normalCore_eq_iSup.

Equations

• H.normalCore = { carrier := {a : G | ∀ (b : G), b * a * b⁻¹ ∈ H}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

theorem Subgroup.normalCore_le {G : Type u_1} [Group G] (H : Subgroup G) : H.normalCore ≤ H

instance Subgroup.normalCore_normal {G : Type u_1} [Group G] (H : Subgroup G) : H.normalCore.Normal

Equations

• ⋯ = ⋯

theorem Subgroup.normal_le_normalCore {G : Type u_1} [Group G] {H : Subgroup G} {N : Subgroup G} [hN : N.Normal] : N ≤ H.normalCore ↔ N ≤ H

theorem Subgroup.normalCore_mono {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H ≤ K) : H.normalCore ≤ K.normalCore

theorem Subgroup.normalCore_eq_iSup {G : Type u_1} [Group G] (H : Subgroup G) : H.normalCore = ⨆ (N : Subgroup G), ⨆ (_ : N.Normal), ⨆ (_ : N ≤ H), N

@[simp]

theorem Subgroup.normalCore_eq_self {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] : H.normalCore = H

theorem Subgroup.normalCore_idempotent {G : Type u_1} [Group G] (H : Subgroup G) : H.normalCore.normalCore = H.normalCore

theorem AddMonoidHom.range.proof_1 {G : Type u_2} [AddGroup G] {N : Type u_1} [AddGroup N] (f : G →+ N) : Set.range ⇑f = ⇑f '' Set.univ

def AddMonoidHom.range {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : AddSubgroup N

The range of an AddMonoidHom from an AddGroup is an AddSubgroup.

Equations

• f.range = (AddSubgroup.map f ⊤).copy (Set.range ⇑f) ⋯

def MonoidHom.range {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : Subgroup N

The range of a monoid homomorphism from a group is a subgroup.

Equations

• f.range = (Subgroup.map f ⊤).copy (Set.range ⇑f) ⋯

@[simp]

theorem AddMonoidHom.coe_range {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : ↑f.range = Set.range ⇑f

@[simp]

theorem MonoidHom.coe_range {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : ↑f.range = Set.range ⇑f

@[simp]

theorem AddMonoidHom.mem_range {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {y : N} : y ∈ f.range ↔ ∃ (x : G), f x = y

@[simp]

theorem MonoidHom.mem_range {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {y : N} : y ∈ f.range ↔ ∃ (x : G), f x = y

theorem AddMonoidHom.range_eq_map {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : f.range = AddSubgroup.map f ⊤

theorem MonoidHom.range_eq_map {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : f.range = Subgroup.map f ⊤

instance AddMonoidHom.range_isCommutative {G : Type u_7} [AddCommGroup G] {N : Type u_8} [AddGroup N] (f : G →+ N) : f.range.IsCommutative

Equations

• ⋯ = ⋯

instance MonoidHom.range_isCommutative {G : Type u_7} [CommGroup G] {N : Type u_8} [Group N] (f : G →* N) : f.range.IsCommutative

Equations

• ⋯ = ⋯

@[simp]

theorem AddMonoidHom.restrict_range {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (K : AddSubgroup G) (f : G →+ N) : (f.restrict K).range = AddSubgroup.map f K

@[simp]

theorem MonoidHom.restrict_range {G : Type u_1} [Group G] {N : Type u_5} [Group N] (K : Subgroup G) (f : G →* N) : (f.restrict K).range = Subgroup.map f K

def AddMonoidHom.rangeRestrict {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : G →+ ↥f.range

The canonical surjective AddGroup homomorphism G →+ f(G) induced by a group homomorphism G →+ N.

Equations

• f.rangeRestrict = f.codRestrict f.range ⋯

theorem AddMonoidHom.rangeRestrict.proof_2 {G : Type u_1} [AddGroup G] {N : Type u_2} [AddGroup N] (f : G →+ N) (x : G) : ∃ (y : G), f y = f x

theorem AddMonoidHom.rangeRestrict.proof_1 {N : Type u_1} [AddGroup N] : AddSubmonoidClass (AddSubgroup N) N

def MonoidHom.rangeRestrict {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : G →* ↥f.range

The canonical surjective group homomorphism G →* f(G) induced by a group homomorphism G →* N.

Equations

• f.rangeRestrict = f.codRestrict f.range ⋯

@[simp]

theorem AddMonoidHom.coe_rangeRestrict {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (g : G) : ↑(f.rangeRestrict g) = f g

@[simp]

theorem MonoidHom.coe_rangeRestrict {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (g : G) : ↑(f.rangeRestrict g) = f g

theorem AddMonoidHom.coe_comp_rangeRestrict {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : Subtype.val ∘ ⇑f.rangeRestrict = ⇑f

theorem MonoidHom.coe_comp_rangeRestrict {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : Subtype.val ∘ ⇑f.rangeRestrict = ⇑f

theorem AddMonoidHom.subtype_comp_rangeRestrict {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : f.range.subtype.comp f.rangeRestrict = f

theorem MonoidHom.subtype_comp_rangeRestrict {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : f.range.subtype.comp f.rangeRestrict = f

theorem AddMonoidHom.rangeRestrict_surjective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : Function.Surjective ⇑f.rangeRestrict

theorem MonoidHom.rangeRestrict_surjective {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : Function.Surjective ⇑f.rangeRestrict

@[simp]

theorem AddMonoidHom.rangeRestrict_injective_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} : Function.Injective ⇑f.rangeRestrict ↔ Function.Injective ⇑f

@[simp]

theorem MonoidHom.rangeRestrict_injective_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} : Function.Injective ⇑f.rangeRestrict ↔ Function.Injective ⇑f

theorem AddMonoidHom.map_range {G : Type u_1} [AddGroup G] {N : Type u_5} {P : Type u_6} [AddGroup N] [AddGroup P] (g : N →+ P) (f : G →+ N) : AddSubgroup.map g f.range = (g.comp f).range

theorem MonoidHom.map_range {G : Type u_1} [Group G] {N : Type u_5} {P : Type u_6} [Group N] [Group P] (g : N →* P) (f : G →* N) : Subgroup.map g f.range = (g.comp f).range

theorem AddMonoidHom.range_top_iff_surjective {G : Type u_1} [AddGroup G] {N : Type u_7} [AddGroup N] {f : G →+ N} : f.range = ⊤ ↔ Function.Surjective ⇑f

theorem MonoidHom.range_top_iff_surjective {G : Type u_1} [Group G] {N : Type u_7} [Group N] {f : G →* N} : f.range = ⊤ ↔ Function.Surjective ⇑f

@[simp]

theorem AddMonoidHom.range_top_of_surjective {G : Type u_1} [AddGroup G] {N : Type u_7} [AddGroup N] (f : G →+ N) (hf : Function.Surjective ⇑f) : f.range = ⊤

The range of a surjective AddMonoid homomorphism is the whole of the codomain.

@[simp]

theorem MonoidHom.range_top_of_surjective {G : Type u_1} [Group G] {N : Type u_7} [Group N] (f : G →* N) (hf : Function.Surjective ⇑f) : f.range = ⊤

The range of a surjective monoid homomorphism is the whole of the codomain.

@[simp]

theorem AddMonoidHom.range_zero {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] : AddMonoidHom.range 0 = ⊥

@[simp]

theorem MonoidHom.range_one {G : Type u_1} [Group G] {N : Type u_5} [Group N] : MonoidHom.range 1 = ⊥

@[simp]

theorem AddSubgroup.subtype_range {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.subtype.range = H

@[simp]

theorem Subgroup.subtype_range {G : Type u_1} [Group G] (H : Subgroup G) : H.subtype.range = H

@[simp]

theorem AddSubgroup.inclusion_range {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h_le : H ≤ K) : (AddSubgroup.inclusion h_le).range = H.addSubgroupOf K

@[simp]

theorem Subgroup.inclusion_range {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h_le : H ≤ K) : (Subgroup.inclusion h_le).range = H.subgroupOf K

theorem AddMonoidHom.addSubgroupOf_range_eq_of_le {G₁ : Type u_7} {G₂ : Type u_8} [AddGroup G₁] [AddGroup G₂] {K : AddSubgroup G₂} (f : G₁ →+ G₂) (h : f.range ≤ K) : f.range.addSubgroupOf K = (f.codRestrict K ⋯).range

theorem MonoidHom.subgroupOf_range_eq_of_le {G₁ : Type u_7} {G₂ : Type u_8} [Group G₁] [Group G₂] {K : Subgroup G₂} (f : G₁ →* G₂) (h : f.range ≤ K) : f.range.subgroupOf K = (f.codRestrict K ⋯).range

@[simp]

theorem MonoidHom.coe_toAdditive_range {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') : (MonoidHom.toAdditive f).range = Subgroup.toAddSubgroup f.range

@[simp]

theorem MonoidHom.coe_toMultiplicative_range {A : Type u_7} {A' : Type u_8} [AddGroup A] [AddGroup A'] (f : A →+ A') : (AddMonoidHom.toMultiplicative f).range = AddSubgroup.toSubgroup f.range

theorem AddMonoidHom.ofLeftInverse.proof_1 {G : Type u_2} [AddGroup G] {N : Type u_1} [AddGroup N] {f : G →+ N} {g : N →+ G} (h : Function.LeftInverse ⇑g ⇑f) : ∀ (x : ↥f.range), f.rangeRestrict ((⇑g ∘ ⇑f.range.subtype) x) = x

theorem AddMonoidHom.ofLeftInverse.proof_2 {G : Type u_2} [AddGroup G] {N : Type u_1} [AddGroup N] {f : G →+ N} (x : G) (y : G) : (↑f.rangeRestrict).toFun (x + y) = (↑f.rangeRestrict).toFun x + (↑f.rangeRestrict).toFun y

def AddMonoidHom.ofLeftInverse {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {g : N →+ G} (h : Function.LeftInverse ⇑g ⇑f) : G ≃+ ↥f.range

Computable alternative to AddMonoidHom.ofInjective.

Equations

• AddMonoidHom.ofLeftInverse h = { toFun := ⇑f.rangeRestrict, invFun := ⇑g ∘ ⇑f.range.subtype, left_inv := h, right_inv := ⋯, map_add' := ⋯ }

def MonoidHom.ofLeftInverse {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {g : N →* G} (h : Function.LeftInverse ⇑g ⇑f) : G ≃* ↥f.range

Computable alternative to MonoidHom.ofInjective.

Equations

• MonoidHom.ofLeftInverse h = { toFun := ⇑f.rangeRestrict, invFun := ⇑g ∘ ⇑f.range.subtype, left_inv := h, right_inv := ⋯, map_mul' := ⋯ }

@[simp]

theorem AddMonoidHom.ofLeftInverse_apply {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {g : N →+ G} (h : Function.LeftInverse ⇑g ⇑f) (x : G) : ↑((AddMonoidHom.ofLeftInverse h) x) = f x

@[simp]

theorem MonoidHom.ofLeftInverse_apply {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {g : N →* G} (h : Function.LeftInverse ⇑g ⇑f) (x : G) : ↑((MonoidHom.ofLeftInverse h) x) = f x

@[simp]

theorem AddMonoidHom.ofLeftInverse_symm_apply {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {g : N →+ G} (h : Function.LeftInverse ⇑g ⇑f) (x : ↥f.range) : (AddMonoidHom.ofLeftInverse h).symm x = g ↑x

@[simp]

theorem MonoidHom.ofLeftInverse_symm_apply {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {g : N →* G} (h : Function.LeftInverse ⇑g ⇑f) (x : ↥f.range) : (MonoidHom.ofLeftInverse h).symm x = g ↑x

theorem AddMonoidHom.ofInjective.proof_2 {G : Type u_1} [AddGroup G] {N : Type u_2} [AddGroup N] {f : G →+ N} : AddHomClass (G →+ ↥f.range) G ↥f.range

noncomputable def AddMonoidHom.ofInjective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective ⇑f) : G ≃+ ↥f.range

The range of an injective additive group homomorphism is isomorphic to its domain.

Equations

• AddMonoidHom.ofInjective hf = AddEquiv.ofBijective (f.codRestrict f.range ⋯) ⋯

theorem AddMonoidHom.ofInjective.proof_4 {G : Type u_1} [AddGroup G] {N : Type u_2} [AddGroup N] {f : G →+ N} (hf : Function.Injective ⇑f) : Function.Injective ⇑(f.codRestrict f.range ⋯) ∧ Function.Surjective ⇑(f.codRestrict f.range ⋯)

theorem AddMonoidHom.ofInjective.proof_1 {N : Type u_1} [AddGroup N] : AddSubmonoidClass (AddSubgroup N) N

theorem AddMonoidHom.ofInjective.proof_3 {G : Type u_1} [AddGroup G] {N : Type u_2} [AddGroup N] {f : G →+ N} (x : G) : ∃ (y : G), f y = f x

noncomputable def MonoidHom.ofInjective {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (hf : Function.Injective ⇑f) : G ≃* ↥f.range

The range of an injective group homomorphism is isomorphic to its domain.

Equations

• MonoidHom.ofInjective hf = MulEquiv.ofBijective (f.codRestrict f.range ⋯) ⋯

theorem AddMonoidHom.ofInjective_apply {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective ⇑f) {x : G} : ↑((AddMonoidHom.ofInjective hf) x) = f x

theorem MonoidHom.ofInjective_apply {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (hf : Function.Injective ⇑f) {x : G} : ↑((MonoidHom.ofInjective hf) x) = f x

@[simp]

theorem AddMonoidHom.apply_ofInjective_symm {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective ⇑f) (x : ↥f.range) : f ((AddMonoidHom.ofInjective hf).symm x) = ↑x

@[simp]

theorem MonoidHom.apply_ofInjective_symm {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (hf : Function.Injective ⇑f) (x : ↥f.range) : f ((MonoidHom.ofInjective hf).symm x) = ↑x

def AddMonoidHom.ker {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) : AddSubgroup G

The additive kernel of an AddMonoid homomorphism is the AddSubgroup of elements such that f x = 0

Equations

• f.ker = { toAddSubmonoid := AddMonoidHom.mker f, neg_mem' := ⋯ }

theorem AddMonoidHom.ker.proof_2 {G : Type u_2} [AddGroup G] {M : Type u_1} [AddZeroClass M] (f : G →+ M) {x : G} (hx : f x = 0) : f (-x) = 0

theorem AddMonoidHom.ker.proof_1 {G : Type u_2} [AddGroup G] {M : Type u_1} [AddZeroClass M] : AddMonoidHomClass (G →+ M) G M

def MonoidHom.ker {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass 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

• f.ker = { toSubmonoid := MonoidHom.mker f, inv_mem' := ⋯ }

@[simp]

theorem AddMonoidHom.mem_ker {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] {f : G →+ M} {x : G} : x ∈ f.ker ↔ f x = 0

@[simp]

theorem MonoidHom.mem_ker {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] {f : G →* M} {x : G} : x ∈ f.ker ↔ f x = 1

theorem AddMonoidHom.sub_mem_ker_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) {x : G} {y : G} : x - y ∈ f.ker ↔ f x = f y

theorem MonoidHom.div_mem_ker_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) {x : G} {y : G} : x / y ∈ f.ker ↔ f x = f y

theorem AddMonoidHom.coe_ker {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) : ↑f.ker = ⇑f ⁻¹' {0}

theorem MonoidHom.coe_ker {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] (f : G →* M) : ↑f.ker = ⇑f ⁻¹' {1}

@[simp]

theorem AddMonoidHom.ker_toHomAddUnits {G : Type u_1} [AddGroup G] {M : Type u_8} [AddMonoid M] (f : G →+ M) : f.toHomAddUnits.ker = f.ker

@[simp]

theorem MonoidHom.ker_toHomUnits {G : Type u_1} [Group G] {M : Type u_8} [Monoid M] (f : G →* M) : f.toHomUnits.ker = f.ker

theorem AddMonoidHom.eq_iff {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) {x : G} {y : G} : f x = f y ↔ -y + x ∈ f.ker

theorem MonoidHom.eq_iff {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] (f : G →* M) {x : G} {y : G} : f x = f y ↔ y⁻¹ * x ∈ f.ker

instance AddMonoidHom.decidableMemKer {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] [DecidableEq M] (f : G →+ M) : DecidablePred fun (x : G) => x ∈ f.ker

Equations

• f.decidableMemKer x = decidable_of_iff (f x = 0) ⋯

instance MonoidHom.decidableMemKer {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] [DecidableEq M] (f : G →* M) : DecidablePred fun (x : G) => x ∈ f.ker

Equations

• f.decidableMemKer x = decidable_of_iff (f x = 1) ⋯

theorem AddMonoidHom.comap_ker {G : Type u_1} [AddGroup G] {N : Type u_5} {P : Type u_6} [AddGroup N] [AddGroup P] (g : N →+ P) (f : G →+ N) : AddSubgroup.comap f g.ker = (g.comp f).ker

theorem MonoidHom.comap_ker {G : Type u_1} [Group G] {N : Type u_5} {P : Type u_6} [Group N] [Group P] (g : N →* P) (f : G →* N) : Subgroup.comap f g.ker = (g.comp f).ker

@[simp]

theorem AddMonoidHom.comap_bot {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : AddSubgroup.comap f ⊥ = f.ker

@[simp]

theorem MonoidHom.comap_bot {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : Subgroup.comap f ⊥ = f.ker

@[simp]

theorem AddMonoidHom.ker_restrict {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (K : AddSubgroup G) (f : G →+ N) : (f.restrict K).ker = f.ker.addSubgroupOf K

@[simp]

theorem MonoidHom.ker_restrict {G : Type u_1} [Group G] {N : Type u_5} [Group N] (K : Subgroup G) (f : G →* N) : (f.restrict K).ker = f.ker.subgroupOf K

@[simp]

theorem AddMonoidHom.ker_codRestrict {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {S : Type u_8} [SetLike S N] [AddSubmonoidClass S N] (f : G →+ N) (s : S) (h : ∀ (x : G), f x ∈ s) : (f.codRestrict s h).ker = f.ker

@[simp]

theorem MonoidHom.ker_codRestrict {G : Type u_1} [Group G] {N : Type u_5} [Group N] {S : Type u_8} [SetLike S N] [SubmonoidClass S N] (f : G →* N) (s : S) (h : ∀ (x : G), f x ∈ s) : (f.codRestrict s h).ker = f.ker

@[simp]

theorem AddMonoidHom.ker_rangeRestrict {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : f.rangeRestrict.ker = f.ker

@[simp]

theorem MonoidHom.ker_rangeRestrict {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : f.rangeRestrict.ker = f.ker

@[simp]

theorem AddMonoidHom.ker_zero {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] : AddMonoidHom.ker 0 = ⊤

@[simp]

theorem MonoidHom.ker_one {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] : MonoidHom.ker 1 = ⊤

@[simp]

theorem AddMonoidHom.ker_id {G : Type u_1} [AddGroup G] : (AddMonoidHom.id G).ker = ⊥

@[simp]

theorem MonoidHom.ker_id {G : Type u_1} [Group G] : (MonoidHom.id G).ker = ⊥

theorem AddMonoidHom.ker_eq_bot_iff {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) : f.ker = ⊥ ↔ Function.Injective ⇑f

theorem MonoidHom.ker_eq_bot_iff {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] (f : G →* M) : f.ker = ⊥ ↔ Function.Injective ⇑f

@[simp]

theorem AddSubgroup.ker_subtype {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.subtype.ker = ⊥

@[simp]

theorem Subgroup.ker_subtype {G : Type u_1} [Group G] (H : Subgroup G) : H.subtype.ker = ⊥

@[simp]

theorem AddSubgroup.ker_inclusion {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H ≤ K) : (AddSubgroup.inclusion h).ker = ⊥

@[simp]

theorem Subgroup.ker_inclusion {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H ≤ K) : (Subgroup.inclusion h).ker = ⊥

theorem AddMonoidHom.ker_sum {G : Type u_1} [AddGroup G] {M : Type u_8} {N : Type u_9} [AddZeroClass M] [AddZeroClass N] (f : G →+ M) (g : G →+ N) : (f.prod g).ker = f.ker ⊓ g.ker

theorem MonoidHom.ker_prod {G : Type u_1} [Group G] {M : Type u_8} {N : Type u_9} [MulOneClass M] [MulOneClass N] (f : G →* M) (g : G →* N) : (f.prod g).ker = f.ker ⊓ g.ker

theorem AddMonoidHom.sumMap_comap_sum {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {G' : Type u_8} {N' : Type u_9} [AddGroup G'] [AddGroup N'] (f : G →+ N) (g : G' →+ N') (S : AddSubgroup N) (S' : AddSubgroup N') : AddSubgroup.comap (f.prodMap g) (S.prod S') = (AddSubgroup.comap f S).prod (AddSubgroup.comap g S')

theorem MonoidHom.prodMap_comap_prod {G : Type u_1} [Group G] {N : Type u_5} [Group N] {G' : Type u_8} {N' : Type u_9} [Group G'] [Group N'] (f : G →* N) (g : G' →* N') (S : Subgroup N) (S' : Subgroup N') : Subgroup.comap (f.prodMap g) (S.prod S') = (Subgroup.comap f S).prod (Subgroup.comap g S')

theorem AddMonoidHom.ker_sumMap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {G' : Type u_8} {N' : Type u_9} [AddGroup G'] [AddGroup N'] (f : G →+ N) (g : G' →+ N') : (f.prodMap g).ker = f.ker.prod g.ker

theorem MonoidHom.ker_prodMap {G : Type u_1} [Group G] {N : Type u_5} [Group N] {G' : Type u_8} {N' : Type u_9} [Group G'] [Group N'] (f : G →* N) (g : G' →* N') : (f.prodMap g).ker = f.ker.prod g.ker

theorem AddMonoidHom.range_le_ker_iff {G : Type u_1} {G' : Type u_2} {G'' : Type u_3} [AddGroup G] [AddGroup G'] [AddGroup G''] (f : G →+ G') (g : G' →+ G'') : f.range ≤ g.ker ↔ g.comp f = 0

theorem MonoidHom.range_le_ker_iff {G : Type u_1} {G' : Type u_2} {G'' : Type u_3} [Group G] [Group G'] [Group G''] (f : G →* G') (g : G' →* G'') : f.range ≤ g.ker ↔ g.comp f = 1

@[instance 100]

instance AddMonoidHom.normal_ker {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) : f.ker.Normal

Equations

• ⋯ = ⋯

@[instance 100]

instance MonoidHom.normal_ker {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] (f : G →* M) : f.ker.Normal

Equations

• ⋯ = ⋯

@[simp]

theorem AddMonoidHom.ker_fst {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] : (AddMonoidHom.fst G G').ker = ⊥.prod ⊤

@[simp]

theorem MonoidHom.ker_fst {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] : (MonoidHom.fst G G').ker = ⊥.prod ⊤

@[simp]

theorem AddMonoidHom.ker_snd {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] : (AddMonoidHom.snd G G').ker = ⊤.prod ⊥

@[simp]

theorem MonoidHom.ker_snd {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] : (MonoidHom.snd G G').ker = ⊤.prod ⊥

@[simp]

theorem MonoidHom.coe_toAdditive_ker {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') : (MonoidHom.toAdditive f).ker = Subgroup.toAddSubgroup f.ker

@[simp]

theorem MonoidHom.coe_toMultiplicative_ker {A : Type u_8} {A' : Type u_9} [AddGroup A] [AddGroup A'] (f : A →+ A') : (AddMonoidHom.toMultiplicative f).ker = AddSubgroup.toSubgroup f.ker

theorem AddMonoidHom.eqLocus.proof_1 {G : Type u_2} [AddGroup G] {M : Type u_1} [AddMonoid M] (f : G →+ M) (g : G →+ M) : ∀ {x : G}, f x = g x → f (-x) = g (-x)

def AddMonoidHom.eqLocus {G : Type u_1} [AddGroup G] {M : Type u_7} [AddMonoid M] (f : G →+ M) (g : G →+ M) : AddSubgroup G

The additive subgroup of elements x : G such that f x = g x

Equations

• f.eqLocus g = { toAddSubmonoid := f.eqLocusM g, neg_mem' := ⋯ }

def MonoidHom.eqLocus {G : Type u_1} [Group G] {M : Type u_7} [Monoid M] (f : G →* M) (g : G →* M) : Subgroup G

The subgroup of elements x : G such that f x = g x

Equations

• f.eqLocus g = { toSubmonoid := f.eqLocusM g, inv_mem' := ⋯ }

@[simp]

theorem AddMonoidHom.eqLocus_same {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : f.eqLocus f = ⊤

@[simp]

theorem MonoidHom.eqLocus_same {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : f.eqLocus f = ⊤

theorem AddMonoidHom.eqOn_closure {G : Type u_1} [AddGroup G] {M : Type u_7} [AddMonoid M] {f : G →+ M} {g : G →+ M} {s : Set G} (h : Set.EqOn (⇑f) (⇑g) s) : Set.EqOn ⇑f ⇑g ↑(AddSubgroup.closure s)

If two monoid homomorphisms are equal on a set, then they are equal on its subgroup closure.

theorem MonoidHom.eqOn_closure {G : Type u_1} [Group G] {M : Type u_7} [Monoid M] {f : G →* M} {g : G →* M} {s : Set G} (h : Set.EqOn (⇑f) (⇑g) s) : Set.EqOn ⇑f ⇑g ↑(Subgroup.closure s)

If two monoid homomorphisms are equal on a set, then they are equal on its subgroup closure.

theorem AddMonoidHom.eq_of_eqOn_top {G : Type u_1} [AddGroup G] {M : Type u_7} [AddMonoid M] {f : G →+ M} {g : G →+ M} (h : Set.EqOn ⇑f ⇑g ↑⊤) : f = g

theorem MonoidHom.eq_of_eqOn_top {G : Type u_1} [Group G] {M : Type u_7} [Monoid M] {f : G →* M} {g : G →* M} (h : Set.EqOn ⇑f ⇑g ↑⊤) : f = g

theorem AddMonoidHom.eq_of_eqOn_dense {G : Type u_1} [AddGroup G] {M : Type u_7} [AddMonoid M] {s : Set G} (hs : AddSubgroup.closure s = ⊤) {f : G →+ M} {g : G →+ M} (h : Set.EqOn (⇑f) (⇑g) s) : f = g

theorem MonoidHom.eq_of_eqOn_dense {G : Type u_1} [Group G] {M : Type u_7} [Monoid M] {s : Set G} (hs : Subgroup.closure s = ⊤) {f : G →* M} {g : G →* M} (h : Set.EqOn (⇑f) (⇑g) s) : f = g

theorem AddMonoidHom.closure_preimage_le {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (s : Set N) : AddSubgroup.closure (⇑f ⁻¹' s) ≤ AddSubgroup.comap f (AddSubgroup.closure s)

theorem MonoidHom.closure_preimage_le {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (s : Set N) : Subgroup.closure (⇑f ⁻¹' s) ≤ Subgroup.comap f (Subgroup.closure s)

theorem AddMonoidHom.map_closure {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (s : Set G) : AddSubgroup.map f (AddSubgroup.closure s) = AddSubgroup.closure (⇑f '' s)

The image under an AddMonoid hom of the AddSubgroup generated by a set equals the AddSubgroup generated by the image of the set.

theorem MonoidHom.map_closure {G : Type u_1} [Group G] {N : Type u_5} [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 AddSubgroup.Normal.map {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup G} (h : H.Normal) (f : G →+ N) (hf : Function.Surjective ⇑f) : (AddSubgroup.map f H).Normal

theorem Subgroup.Normal.map {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H : Subgroup G} (h : H.Normal) (f : G →* N) (hf : Function.Surjective ⇑f) : (Subgroup.map f H).Normal

theorem AddSubgroup.map_eq_bot_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) {f : G →+ N} : AddSubgroup.map f H = ⊥ ↔ H ≤ f.ker

theorem Subgroup.map_eq_bot_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) {f : G →* N} : Subgroup.map f H = ⊥ ↔ H ≤ f.ker

theorem AddSubgroup.map_eq_bot_iff_of_injective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) {f : G →+ N} (hf : Function.Injective ⇑f) : AddSubgroup.map f H = ⊥ ↔ H = ⊥

theorem Subgroup.map_eq_bot_iff_of_injective {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) {f : G →* N} (hf : Function.Injective ⇑f) : Subgroup.map f H = ⊥ ↔ H = ⊥

theorem AddSubgroup.map_le_range {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) : AddSubgroup.map f H ≤ f.range

theorem Subgroup.map_le_range {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup G) : Subgroup.map f H ≤ f.range

theorem AddSubgroup.map_subtype_le {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (K : AddSubgroup ↥H) : AddSubgroup.map H.subtype K ≤ H

theorem Subgroup.map_subtype_le {G : Type u_1} [Group G] {H : Subgroup G} (K : Subgroup ↥H) : Subgroup.map H.subtype K ≤ H

theorem AddSubgroup.ker_le_comap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) : f.ker ≤ AddSubgroup.comap f H

theorem Subgroup.ker_le_comap {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup N) : f.ker ≤ Subgroup.comap f H

theorem AddSubgroup.map_comap_le {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) : AddSubgroup.map f (AddSubgroup.comap f H) ≤ H

theorem Subgroup.map_comap_le {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup N) : Subgroup.map f (Subgroup.comap f H) ≤ H

theorem AddSubgroup.le_comap_map {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) : H ≤ AddSubgroup.comap f (AddSubgroup.map f H)

theorem Subgroup.le_comap_map {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup G) : H ≤ Subgroup.comap f (Subgroup.map f H)

theorem AddSubgroup.map_comap_eq {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) : AddSubgroup.map f (AddSubgroup.comap f H) = f.range ⊓ H

theorem Subgroup.map_comap_eq {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup N) : Subgroup.map f (Subgroup.comap f H) = f.range ⊓ H

theorem AddSubgroup.comap_map_eq {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) : AddSubgroup.comap f (AddSubgroup.map f H) = H ⊔ f.ker

theorem Subgroup.comap_map_eq {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup G) : Subgroup.comap f (Subgroup.map f H) = H ⊔ f.ker

theorem AddSubgroup.map_comap_eq_self {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H : AddSubgroup N} (h : H ≤ f.range) : AddSubgroup.map f (AddSubgroup.comap f H) = H

theorem Subgroup.map_comap_eq_self {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {H : Subgroup N} (h : H ≤ f.range) : Subgroup.map f (Subgroup.comap f H) = H

theorem AddSubgroup.map_comap_eq_self_of_surjective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (h : Function.Surjective ⇑f) (H : AddSubgroup N) : AddSubgroup.map f (AddSubgroup.comap f H) = H

theorem Subgroup.map_comap_eq_self_of_surjective {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (h : Function.Surjective ⇑f) (H : Subgroup N) : Subgroup.map f (Subgroup.comap f H) = H

theorem AddSubgroup.comap_le_comap_of_le_range {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K : AddSubgroup N} {L : AddSubgroup N} (hf : K ≤ f.range) : AddSubgroup.comap f K ≤ AddSubgroup.comap f L ↔ K ≤ L

theorem Subgroup.comap_le_comap_of_le_range {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {K : Subgroup N} {L : Subgroup N} (hf : K ≤ f.range) : Subgroup.comap f K ≤ Subgroup.comap f L ↔ K ≤ L

theorem AddSubgroup.comap_le_comap_of_surjective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K : AddSubgroup N} {L : AddSubgroup N} (hf : Function.Surjective ⇑f) : AddSubgroup.comap f K ≤ AddSubgroup.comap f L ↔ K ≤ L

theorem Subgroup.comap_le_comap_of_surjective {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {K : Subgroup N} {L : Subgroup N} (hf : Function.Surjective ⇑f) : Subgroup.comap f K ≤ Subgroup.comap f L ↔ K ≤ L

theorem AddSubgroup.comap_lt_comap_of_surjective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K : AddSubgroup N} {L : AddSubgroup N} (hf : Function.Surjective ⇑f) : AddSubgroup.comap f K < AddSubgroup.comap f L ↔ K < L

theorem Subgroup.comap_lt_comap_of_surjective {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {K : Subgroup N} {L : Subgroup N} (hf : Function.Surjective ⇑f) : Subgroup.comap f K < Subgroup.comap f L ↔ K < L

theorem AddSubgroup.comap_injective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (h : Function.Surjective ⇑f) : Function.Injective (AddSubgroup.comap f)

theorem Subgroup.comap_injective {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (h : Function.Surjective ⇑f) : Function.Injective (Subgroup.comap f)

theorem AddSubgroup.comap_map_eq_self {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H : AddSubgroup G} (h : f.ker ≤ H) : AddSubgroup.comap f (AddSubgroup.map f H) = H

theorem Subgroup.comap_map_eq_self {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {H : Subgroup G} (h : f.ker ≤ H) : Subgroup.comap f (Subgroup.map f H) = H

theorem AddSubgroup.comap_map_eq_self_of_injective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (h : Function.Injective ⇑f) (H : AddSubgroup G) : AddSubgroup.comap f (AddSubgroup.map f H) = H

theorem Subgroup.comap_map_eq_self_of_injective {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (h : Function.Injective ⇑f) (H : Subgroup G) : Subgroup.comap f (Subgroup.map f H) = H

theorem AddSubgroup.map_le_map_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H : AddSubgroup G} {K : AddSubgroup G} : AddSubgroup.map f H ≤ AddSubgroup.map f K ↔ H ≤ K ⊔ f.ker

theorem Subgroup.map_le_map_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {H : Subgroup G} {K : Subgroup G} : Subgroup.map f H ≤ Subgroup.map f K ↔ H ≤ K ⊔ f.ker

theorem AddSubgroup.map_le_map_iff' {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H : AddSubgroup G} {K : AddSubgroup G} : AddSubgroup.map f H ≤ AddSubgroup.map f K ↔ H ⊔ f.ker ≤ K ⊔ f.ker

theorem Subgroup.map_le_map_iff' {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {H : Subgroup G} {K : Subgroup G} : Subgroup.map f H ≤ Subgroup.map f K ↔ H ⊔ f.ker ≤ K ⊔ f.ker

theorem AddSubgroup.map_eq_map_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H : AddSubgroup G} {K : AddSubgroup G} : AddSubgroup.map f H = AddSubgroup.map f K ↔ H ⊔ f.ker = K ⊔ f.ker

theorem Subgroup.map_eq_map_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {H : Subgroup G} {K : Subgroup G} : Subgroup.map f H = Subgroup.map f K ↔ H ⊔ f.ker = K ⊔ f.ker

theorem AddSubgroup.map_eq_range_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H : AddSubgroup G} : AddSubgroup.map f H = f.range ↔ Codisjoint H f.ker

theorem Subgroup.map_eq_range_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {H : Subgroup G} : Subgroup.map f H = f.range ↔ Codisjoint H f.ker

theorem AddSubgroup.map_le_map_iff_of_injective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective ⇑f) {H : AddSubgroup G} {K : AddSubgroup G} : AddSubgroup.map f H ≤ AddSubgroup.map f K ↔ H ≤ K

theorem Subgroup.map_le_map_iff_of_injective {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (hf : Function.Injective ⇑f) {H : Subgroup G} {K : Subgroup G} : Subgroup.map f H ≤ Subgroup.map f K ↔ H ≤ K

@[simp]

theorem AddSubgroup.map_subtype_le_map_subtype {G : Type u_1} [AddGroup G] {G' : AddSubgroup G} {H : AddSubgroup ↥G'} {K : AddSubgroup ↥G'} : AddSubgroup.map G'.subtype H ≤ AddSubgroup.map G'.subtype K ↔ H ≤ K

@[simp]

theorem Subgroup.map_subtype_le_map_subtype {G : Type u_1} [Group G] {G' : Subgroup G} {H : Subgroup ↥G'} {K : Subgroup ↥G'} : Subgroup.map G'.subtype H ≤ Subgroup.map G'.subtype K ↔ H ≤ K

theorem AddSubgroup.map_injective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (h : Function.Injective ⇑f) : Function.Injective (AddSubgroup.map f)

theorem Subgroup.map_injective {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (h : Function.Injective ⇑f) : Function.Injective (Subgroup.map f)

theorem AddSubgroup.map_eq_comap_of_inverse {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {g : N →+ G} (hl : Function.LeftInverse ⇑g ⇑f) (hr : Function.RightInverse ⇑g ⇑f) (H : AddSubgroup G) : AddSubgroup.map f H = AddSubgroup.comap g H

theorem Subgroup.map_eq_comap_of_inverse {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {g : N →* G} (hl : Function.LeftInverse ⇑g ⇑f) (hr : Function.RightInverse ⇑g ⇑f) (H : Subgroup G) : Subgroup.map f H = Subgroup.comap g H

theorem AddSubgroup.map_injective_of_ker_le {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) {H : AddSubgroup G} {K : AddSubgroup G} (hH : f.ker ≤ H) (hK : f.ker ≤ K) (hf : AddSubgroup.map f H = AddSubgroup.map f K) : H = K

Given f(A) = f(B), ker f ≤ A, and ker f ≤ B, deduce that A = B.

theorem Subgroup.map_injective_of_ker_le {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) {H : Subgroup G} {K : Subgroup G} (hH : f.ker ≤ H) (hK : f.ker ≤ K) (hf : Subgroup.map f H = Subgroup.map f K) : H = K

Given f(A) = f(B), ker f ≤ A, and ker f ≤ B, deduce that A = B.

theorem AddSubgroup.closure_preimage_eq_top {G : Type u_1} [AddGroup G] (s : Set G) : AddSubgroup.closure (⇑(AddSubgroup.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 AddSubgroup.comap_sup_eq_of_le_range {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) {H : AddSubgroup N} {K : AddSubgroup N} (hH : H ≤ f.range) (hK : K ≤ f.range) : AddSubgroup.comap f H ⊔ AddSubgroup.comap f K = AddSubgroup.comap f (H ⊔ K)

theorem Subgroup.comap_sup_eq_of_le_range {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) {H : Subgroup N} {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 AddSubgroup.comap_sup_eq {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) (K : AddSubgroup N) (hf : Function.Surjective ⇑f) : AddSubgroup.comap f H ⊔ AddSubgroup.comap f K = AddSubgroup.comap f (H ⊔ K)

theorem Subgroup.comap_sup_eq {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup N) (K : Subgroup N) (hf : Function.Surjective ⇑f) : Subgroup.comap f H ⊔ Subgroup.comap f K = Subgroup.comap f (H ⊔ K)

theorem AddSubgroup.sup_addSubgroupOf_eq {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} {L : AddSubgroup G} (hH : H ≤ L) (hK : K ≤ L) : H.addSubgroupOf L ⊔ K.addSubgroupOf L = (H ⊔ K).addSubgroupOf L

theorem Subgroup.sup_subgroupOf_eq {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {L : Subgroup G} (hH : H ≤ L) (hK : K ≤ L) : H.subgroupOf L ⊔ K.subgroupOf L = (H ⊔ K).subgroupOf L

theorem AddSubgroup.codisjoint_addSubgroupOf_sup {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) : Codisjoint (H.addSubgroupOf (H ⊔ K)) (K.addSubgroupOf (H ⊔ K))

theorem Subgroup.codisjoint_subgroupOf_sup {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) : Codisjoint (H.subgroupOf (H ⊔ K)) (K.subgroupOf (H ⊔ K))

theorem AddSubgroup.equivMapOfInjective.proof_1 {G : Type u_1} [AddGroup G] {N : Type u_2} [AddGroup N] (H : AddSubgroup G) (f : G →+ N) (hf : Function.Injective ⇑f) : ∀ (x x_1 : ↥H), (Equiv.Set.image (⇑f) (↑H) hf).toFun (x + x_1) = (Equiv.Set.image (⇑f) (↑H) hf).toFun x + (Equiv.Set.image (⇑f) (↑H) hf).toFun x_1

noncomputable def AddSubgroup.equivMapOfInjective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (f : G →+ N) (hf : Function.Injective ⇑f) : ↥H ≃+ ↥(AddSubgroup.map f H)

An additive subgroup is isomorphic to its image under an injective function. If you have an isomorphism, use AddEquiv.addSubgroupMap for better definitional equalities.

Equations

• H.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑H) hf, map_add' := ⋯ }

noncomputable def Subgroup.equivMapOfInjective {G : Type u_1} [Group G] {N : Type u_5} [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 MulEquiv.subgroupMap for better definitional equalities.

Equations

• H.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑H) hf, map_mul' := ⋯ }

@[simp]

theorem AddSubgroup.coe_equivMapOfInjective_apply {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (f : G →+ N) (hf : Function.Injective ⇑f) (h : ↥H) : ↑((H.equivMapOfInjective f hf) h) = f ↑h

@[simp]

theorem Subgroup.coe_equivMapOfInjective_apply {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (f : G →* N) (hf : Function.Injective ⇑f) (h : ↥H) : ↑((H.equivMapOfInjective f hf) h) = f ↑h

theorem AddSubgroup.comap_normalizer_eq_of_surjective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) {f : N →+ G} (hf : Function.Surjective ⇑f) : AddSubgroup.comap f H.normalizer = (AddSubgroup.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_surjective {G : Type u_1} [Group G] {N : Type u_5} [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 AddSubgroup.comap_normalizer_eq_of_injective_of_le_range {G : Type u_1} [AddGroup G] {N : Type u_6} [AddGroup N] (H : AddSubgroup G) {f : N →+ G} (hf : Function.Injective ⇑f) (h : H.normalizer ≤ f.range) : AddSubgroup.comap f H.normalizer = (AddSubgroup.comap f H).normalizer

theorem Subgroup.comap_normalizer_eq_of_injective_of_le_range {G : Type u_1} [Group G] {N : Type u_6} [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 AddSubgroup.addSubgroupOf_normalizer_eq {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {N : AddSubgroup G} (h : H.normalizer ≤ N) : H.normalizer.addSubgroupOf N = (H.addSubgroupOf N).normalizer

theorem Subgroup.subgroupOf_normalizer_eq {G : Type u_1} [Group G] {H : Subgroup G} {N : Subgroup G} (h : H.normalizer ≤ N) : H.normalizer.subgroupOf N = (H.subgroupOf N).normalizer

theorem AddSubgroup.map_equiv_normalizer_eq {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (f : G ≃+ N) : AddSubgroup.map f.toAddMonoidHom H.normalizer = (AddSubgroup.map f.toAddMonoidHom H).normalizer

The image of the normalizer is equal to the normalizer of the image of an isomorphism.

theorem Subgroup.map_equiv_normalizer_eq {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (f : G ≃* N) : Subgroup.map f.toMonoidHom H.normalizer = (Subgroup.map f.toMonoidHom H).normalizer

The image of the normalizer is equal to the normalizer of the image of an isomorphism.

theorem AddSubgroup.map_normalizer_eq_of_bijective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) {f : G →+ N} (hf : Function.Bijective ⇑f) : AddSubgroup.map f H.normalizer = (AddSubgroup.map f H).normalizer

The image of the normalizer is equal to the normalizer of the image of a bijective function.

theorem Subgroup.map_normalizer_eq_of_bijective {G : Type u_1} [Group G] {N : Type u_5} [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 AddMonoidHom.liftOfRightInverseAux.proof_2 {G₁ : Type u_3} {G₂ : Type u_2} {G₃ : Type u_1} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : G₁ →+ G₃) (hg : f.ker ≤ g.ker) (x : G₂) (y : G₂) : { toFun := fun (b : G₂) => g (f_inv b), map_zero' := ⋯ }.toFun (x + y) = { toFun := fun (b : G₂) => g (f_inv b), map_zero' := ⋯ }.toFun x + { toFun := fun (b : G₂) => g (f_inv b), map_zero' := ⋯ }.toFun y

def AddMonoidHom.liftOfRightInverseAux {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : G₁ →+ G₃) (hg : f.ker ≤ g.ker) : G₂ →+ G₃

Auxiliary definition used to define liftOfRightInverse

Equations

• f.liftOfRightInverseAux f_inv hf g hg = { toFun := fun (b : G₂) => g (f_inv b), map_zero' := ⋯, map_add' := ⋯ }

theorem AddMonoidHom.liftOfRightInverseAux.proof_1 {G₁ : Type u_1} {G₂ : Type u_3} {G₃ : Type u_2} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : G₁ →+ G₃) (hg : f.ker ≤ g.ker) : f_inv 0 ∈ g.ker

def MonoidHom.liftOfRightInverseAux {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [Group G₁] [Group G₂] [Group G₃] (f : G₁ →* G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : G₁ →* G₃) (hg : f.ker ≤ g.ker) : G₂ →* G₃

Auxiliary definition used to define liftOfRightInverse

Equations

• f.liftOfRightInverseAux f_inv hf g hg = { toFun := fun (b : G₂) => g (f_inv b), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem AddMonoidHom.liftOfRightInverseAux_comp_apply {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : G₁ →+ G₃) (hg : f.ker ≤ g.ker) (x : G₁) : (f.liftOfRightInverseAux f_inv hf g hg) (f x) = g x

@[simp]

theorem MonoidHom.liftOfRightInverseAux_comp_apply {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [Group G₁] [Group G₂] [Group G₃] (f : G₁ →* G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : G₁ →* G₃) (hg : f.ker ≤ g.ker) (x : G₁) : (f.liftOfRightInverseAux f_inv hf g hg) (f x) = g x

def AddMonoidHom.liftOfRightInverse {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) : { g : G₁ →+ G₃ // f.ker ≤ g.ker } ≃ (G₂ →+ G₃)

liftOfRightInverse f f_inv hf g hg is the unique additive group homomorphism φ

• such that φ.comp f = g (AddMonoidHom.liftOfRightInverse_comp),
• where f : G₁ →+ G₂ has a RightInverse f_inv (hf),
• and g : G₂ →+ G₃ satisfies hg : f.ker ≤ g.ker. See AddMonoidHom.eq_liftOfRightInverse for the uniqueness lemma.

   G₁.
   |  \
 f |   \ g
   |    \
   v     \⌟
   G₂----> G₃
      ∃!φ

Equations

• One or more equations did not get rendered due to their size.

theorem AddMonoidHom.liftOfRightInverse.proof_3 {G₁ : Type u_1} {G₂ : Type u_3} {G₃ : Type u_2} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : { g : G₁ →+ G₃ // f.ker ≤ g.ker }) : (fun (φ : G₂ →+ G₃) => ⟨φ.comp f, ⋯⟩) ((fun (g : { g : G₁ →+ G₃ // f.ker ≤ g.ker }) => f.liftOfRightInverseAux f_inv hf ↑g ⋯) g) = g

theorem AddMonoidHom.liftOfRightInverse.proof_2 {G₁ : Type u_1} {G₂ : Type u_2} {G₃ : Type u_3} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (φ : G₂ →+ G₃) (x : G₁) (hx : x ∈ f.ker) : x ∈ (φ.comp f).ker

theorem AddMonoidHom.liftOfRightInverse.proof_4 {G₁ : Type u_3} {G₂ : Type u_1} {G₃ : Type u_2} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (φ : G₂ →+ G₃) : (fun (g : { g : G₁ →+ G₃ // f.ker ≤ g.ker }) => f.liftOfRightInverseAux f_inv hf ↑g ⋯) ((fun (φ : G₂ →+ G₃) => ⟨φ.comp f, ⋯⟩) φ) = φ

theorem AddMonoidHom.liftOfRightInverse.proof_1 {G₁ : Type u_1} {G₂ : Type u_2} {G₃ : Type u_3} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (g : { g : G₁ →+ G₃ // f.ker ≤ g.ker }) : f.ker ≤ (↑g).ker

def MonoidHom.liftOfRightInverse {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [Group G₁] [Group G₂] [Group G₃] (f : G₁ →* G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) : { g : G₁ →* G₃ // f.ker ≤ g.ker } ≃ (G₂ →* G₃)

liftOfRightInverse f hf g hg is the unique group homomorphism φ

• such that φ.comp f = g (MonoidHom.liftOfRightInverse_comp),
• where f : G₁ →+* G₂ has a RightInverse f_inv (hf),
• and g : G₂ →+* G₃ satisfies hg : f.ker ≤ g.ker.

See MonoidHom.eq_liftOfRightInverse for the uniqueness lemma.

   G₁.
   |  \
 f |   \ g
   |    \
   v     \⌟
   G₂----> G₃
      ∃!φ

Equations

• One or more equations did not get rendered due to their size.

theorem AddMonoidHom.liftOfSurjective.proof_1 {G₁ : Type u_1} {G₂ : Type u_2} [AddGroup G₁] [AddGroup G₂] (f : G₁ →+ G₂) (hf : Function.Surjective ⇑f) : Function.RightInverse (Function.surjInv hf) ⇑f

@[reducible, inline]

noncomputable abbrev AddMonoidHom.liftOfSurjective {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (hf : Function.Surjective ⇑f) : { g : G₁ →+ G₃ // f.ker ≤ g.ker } ≃ (G₂ →+ G₃)

A non-computable version of AddMonoidHom.liftOfRightInverse for when no computable right inverse is available.

Equations

• f.liftOfSurjective hf = f.liftOfRightInverse (Function.surjInv hf) ⋯

@[reducible, inline]

noncomputable abbrev MonoidHom.liftOfSurjective {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [Group G₁] [Group G₂] [Group G₃] (f : G₁ →* G₂) (hf : Function.Surjective ⇑f) : { g : G₁ →* G₃ // f.ker ≤ g.ker } ≃ (G₂ →* G₃)

A non-computable version of MonoidHom.liftOfRightInverse for when no computable right inverse is available, that uses Function.surjInv.

Equations

• f.liftOfSurjective hf = f.liftOfRightInverse (Function.surjInv hf) ⋯

@[simp]

theorem AddMonoidHom.liftOfRightInverse_comp_apply {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : { g : G₁ →+ G₃ // f.ker ≤ g.ker }) (x : G₁) : ((f.liftOfRightInverse f_inv hf) g) (f x) = ↑g x

@[simp]

theorem MonoidHom.liftOfRightInverse_comp_apply {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [Group G₁] [Group G₂] [Group G₃] (f : G₁ →* G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : { g : G₁ →* G₃ // f.ker ≤ g.ker }) (x : G₁) : ((f.liftOfRightInverse f_inv hf) g) (f x) = ↑g x

@[simp]

theorem AddMonoidHom.liftOfRightInverse_comp {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : { g : G₁ →+ G₃ // f.ker ≤ g.ker }) : ((f.liftOfRightInverse f_inv hf) g).comp f = ↑g

@[simp]

theorem MonoidHom.liftOfRightInverse_comp {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [Group G₁] [Group G₂] [Group G₃] (f : G₁ →* G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : { g : G₁ →* G₃ // f.ker ≤ g.ker }) : ((f.liftOfRightInverse f_inv hf) g).comp f = ↑g

theorem AddMonoidHom.eq_liftOfRightInverse {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : G₁ →+ G₃) (hg : f.ker ≤ g.ker) (h : G₂ →+ G₃) (hh : h.comp f = g) : h = (f.liftOfRightInverse f_inv hf) ⟨g, hg⟩

theorem MonoidHom.eq_liftOfRightInverse {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [Group G₁] [Group G₂] [Group G₃] (f : G₁ →* G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : G₁ →* G₃) (hg : f.ker ≤ g.ker) (h : G₂ →* G₃) (hh : h.comp f = g) : h = (f.liftOfRightInverse f_inv hf) ⟨g, hg⟩

theorem AddSubgroup.Normal.comap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup N} (hH : H.Normal) (f : G →+ N) : (AddSubgroup.comap f H).Normal

theorem Subgroup.Normal.comap {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H : Subgroup N} (hH : H.Normal) (f : G →* N) : (Subgroup.comap f H).Normal

@[instance 100]

instance AddSubgroup.normal_comap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup N} [nH : H.Normal] (f : G →+ N) : (AddSubgroup.comap f H).Normal

Equations

• ⋯ = ⋯

@[instance 100]

instance Subgroup.normal_comap {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H : Subgroup N} [nH : H.Normal] (f : G →* N) : (Subgroup.comap f H).Normal

Equations

• ⋯ = ⋯

theorem AddSubgroup.Normal.addSubgroupOf {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (hH : H.Normal) (K : AddSubgroup G) : (H.addSubgroupOf K).Normal

theorem Subgroup.Normal.subgroupOf {G : Type u_1} [Group G] {H : Subgroup G} (hH : H.Normal) (K : Subgroup G) : (H.subgroupOf K).Normal

@[instance 100]

instance AddSubgroup.normal_addSubgroupOf {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {N : AddSubgroup G} [N.Normal] : (N.addSubgroupOf H).Normal

Equations

• ⋯ = ⋯

@[instance 100]

instance Subgroup.normal_subgroupOf {G : Type u_1} [Group G] {H : Subgroup G} {N : Subgroup G} [N.Normal] : (N.subgroupOf H).Normal

Equations

• ⋯ = ⋯

theorem Subgroup.map_normalClosure {G : Type u_1} [Group G] {N : Type u_5} [Group N] (s : Set G) (f : G →* N) (hf : Function.Surjective ⇑f) : Subgroup.map f (Subgroup.normalClosure s) = Subgroup.normalClosure (⇑f '' s)

theorem Subgroup.comap_normalClosure {G : Type u_1} [Group G] {N : Type u_5} [Group N] (s : Set N) (f : G ≃* N) : Subgroup.normalClosure (⇑f ⁻¹' s) = Subgroup.comap (↑f) (Subgroup.normalClosure s)

theorem Subgroup.Normal.of_map_injective {G : Type u_6} {H : Type u_7} [Group G] [Group H] {φ : G →* H} (hφ : Function.Injective ⇑φ) {L : Subgroup G} (n : (Subgroup.map φ L).Normal) : L.Normal

theorem Subgroup.Normal.of_map_subtype {G : Type u_1} [Group G] {K : Subgroup G} {L : Subgroup ↥K} (n : (Subgroup.map K.subtype L).Normal) : L.Normal

def AddMonoidHom.addSubgroupComap {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H' : AddSubgroup G') : ↥(AddSubgroup.comap f H') →+ ↥H'

the AddMonoidHom from the preimage of an additive subgroup to itself.

Equations

• f.addSubgroupComap H' = f.addSubmonoidComap H'.toAddSubmonoid

@[simp]

theorem MonoidHom.subgroupComap_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'.toSubmonoid)) : ↑((f.subgroupComap H') x) = f ↑x

@[simp]

theorem AddMonoidHom.addSubgroupComap_apply_coe {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H' : AddSubgroup G') (x : ↥(AddSubmonoid.comap f H'.toAddSubmonoid)) : ↑((f.addSubgroupComap H') x) = f ↑x

def MonoidHom.subgroupComap {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (H' : Subgroup G') : ↥(Subgroup.comap f H') →* ↥H'

The MonoidHom from the preimage of a subgroup to itself.

Equations

• f.subgroupComap H' = f.submonoidComap H'.toSubmonoid

def AddMonoidHom.addSubgroupMap {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H : AddSubgroup G) : ↥H →+ ↥(AddSubgroup.map f H)

the AddMonoidHom from an additive subgroup to its image

Equations

• f.addSubgroupMap H = f.addSubmonoidMap H.toAddSubmonoid

@[simp]

theorem MonoidHom.subgroupMap_apply_coe {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (H : Subgroup G) (x : ↥H.toSubmonoid) : ↑((f.subgroupMap H) x) = f ↑x

@[simp]

theorem AddMonoidHom.addSubgroupMap_apply_coe {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H : AddSubgroup G) (x : ↥H.toAddSubmonoid) : ↑((f.addSubgroupMap H) x) = f ↑x

def MonoidHom.subgroupMap {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (H : Subgroup G) : ↥H →* ↥(Subgroup.map f H)

The MonoidHom from a subgroup to its image.

Equations

• f.subgroupMap H = f.submonoidMap H.toSubmonoid

theorem AddMonoidHom.addSubgroupMap_surjective {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H : AddSubgroup G) : Function.Surjective ⇑(f.addSubgroupMap H)

theorem MonoidHom.subgroupMap_surjective {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (H : Subgroup G) : Function.Surjective ⇑(f.subgroupMap H)

theorem AddEquiv.addSubgroupCongr.proof_1 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H = K) : ↑H = ↑K

def AddEquiv.addSubgroupCongr {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H = K) : ↥H ≃+ ↥K

Makes the identity additive isomorphism from a proof two subgroups of an additive group are equal.

Equations

• AddEquiv.addSubgroupCongr h = { toEquiv := Equiv.setCongr ⋯, map_add' := ⋯ }

theorem AddEquiv.addSubgroupCongr.proof_2 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H = K) : ∀ (x x_1 : ↥H), (Equiv.setCongr ⋯).toFun (x + x_1) = (Equiv.setCongr ⋯).toFun (x + x_1)

def MulEquiv.subgroupCongr {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H = K) : ↥H ≃* ↥K

Makes the identity isomorphism from a proof two subgroups of a multiplicative group are equal.

Equations

• MulEquiv.subgroupCongr h = { toEquiv := Equiv.setCongr ⋯, map_mul' := ⋯ }

@[simp]

theorem AddEquiv.addSubgroupCongr_apply {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H = K) (x : ↥H) : ↑((AddEquiv.addSubgroupCongr h) x) = ↑x

@[simp]

theorem MulEquiv.subgroupCongr_apply {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H = K) (x : ↥H) : ↑((MulEquiv.subgroupCongr h) x) = ↑x

@[simp]

theorem AddEquiv.addSubgroupCongr_symm_apply {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H = K) (x : ↥K) : ↑((AddEquiv.addSubgroupCongr h).symm x) = ↑x

@[simp]

theorem MulEquiv.subgroupCongr_symm_apply {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H = K) (x : ↥K) : ↑((MulEquiv.subgroupCongr h).symm x) = ↑x

def AddEquiv.addSubgroupMap {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (e : G ≃+ G') (H : AddSubgroup G) : ↥H ≃+ ↥(AddSubgroup.map (↑e) H)

An additive subgroup is isomorphic to its image under an isomorphism. If you only have an injective map, use AddSubgroup.equiv_map_of_injective.

Equations

• e.addSubgroupMap H = e.addSubmonoidMap H.toAddSubmonoid

def MulEquiv.subgroupMap {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.subgroupMap H = e.submonoidMap H.toSubmonoid

@[simp]

theorem AddEquiv.coe_addSubgroupMap_apply {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (e : G ≃+ G') (H : AddSubgroup G) (g : ↥H) : ↑((e.addSubgroupMap H) g) = e ↑g

@[simp]

theorem MulEquiv.coe_subgroupMap_apply {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (e : G ≃* G') (H : Subgroup G) (g : ↥H) : ↑((e.subgroupMap H) g) = e ↑g

@[simp]

theorem AddEquiv.addSubgroupMap_symm_apply {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (e : G ≃+ G') (H : AddSubgroup G) (g : ↥(AddSubgroup.map (↑e) H)) : (e.addSubgroupMap H).symm g = ⟨e.symm ↑g, ⋯⟩

@[simp]

theorem MulEquiv.subgroupMap_symm_apply {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (e : G ≃* G') (H : Subgroup G) (g : ↥(Subgroup.map (↑e) H)) : (e.subgroupMap H).symm g = ⟨e.symm ↑g, ⋯⟩

@[simp]

theorem AddSubgroup.equivMapOfInjective_coe_addEquiv {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (e : G ≃+ G') : H.equivMapOfInjective ↑e ⋯ = e.addSubgroupMap H

@[simp]

theorem Subgroup.equivMapOfInjective_coe_mulEquiv {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (e : G ≃* G') : H.equivMapOfInjective ↑e ⋯ = e.subgroupMap H

theorem AddSubgroup.mem_sup {C : Type u_6} [AddCommGroup C] {s : AddSubgroup C} {t : AddSubgroup C} {x : C} : x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y + z = x

theorem Subgroup.mem_sup {C : Type u_6} [CommGroup C] {s : Subgroup C} {t : Subgroup C} {x : C} : x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x

theorem AddSubgroup.mem_sup' {C : Type u_6} [AddCommGroup C] {s : AddSubgroup C} {t : AddSubgroup C} {x : C} : x ∈ s ⊔ t ↔ ∃ (y : ↥s) (z : ↥t), ↑y + ↑z = x

theorem Subgroup.mem_sup' {C : Type u_6} [CommGroup C] {s : Subgroup C} {t : Subgroup C} {x : C} : x ∈ s ⊔ t ↔ ∃ (y : ↥s) (z : ↥t), ↑y * ↑z = x

theorem AddSubgroup.mem_closure_pair {C : Type u_6} [AddCommGroup C] {x : C} {y : C} {z : C} : z ∈ AddSubgroup.closure {x, y} ↔ ∃ (m : ℤ) (n : ℤ), m • x + n • y = z

theorem Subgroup.mem_closure_pair {C : Type u_6} [CommGroup C] {x : C} {y : C} {z : C} : z ∈ Subgroup.closure {x, y} ↔ ∃ (m : ℤ) (n : ℤ), x ^ m * y ^ n = z

theorem AddSubgroup.normal_addSubgroupOf_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (hHK : H ≤ K) : (H.addSubgroupOf K).Normal ↔ ∀ (h k : G), h ∈ H → k ∈ K → k + h + -k ∈ H

theorem Subgroup.normal_subgroupOf_iff {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (hHK : H ≤ K) : (H.subgroupOf K).Normal ↔ ∀ (h k : G), h ∈ H → k ∈ K → k * h * k⁻¹ ∈ H

instance AddSubgroup.sum_addSubgroupOf_sum_normal {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H₁ : AddSubgroup G} {K₁ : AddSubgroup G} {H₂ : AddSubgroup N} {K₂ : AddSubgroup N} [h₁ : (H₁.addSubgroupOf K₁).Normal] [h₂ : (H₂.addSubgroupOf K₂).Normal] : ((H₁.prod H₂).addSubgroupOf (K₁.prod K₂)).Normal

Equations

• ⋯ = ⋯

instance Subgroup.prod_subgroupOf_prod_normal {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H₁ : Subgroup G} {K₁ : Subgroup G} {H₂ : Subgroup N} {K₂ : Subgroup N} [h₁ : (H₁.subgroupOf K₁).Normal] [h₂ : (H₂.subgroupOf K₂).Normal] : ((H₁.prod H₂).subgroupOf (K₁.prod K₂)).Normal

Equations

• ⋯ = ⋯

instance AddSubgroup.sum_normal {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (K : AddSubgroup N) [hH : H.Normal] [hK : K.Normal] : (H.prod K).Normal

Equations

• ⋯ = ⋯

instance Subgroup.prod_normal {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (K : Subgroup N) [hH : H.Normal] [hK : K.Normal] : (H.prod K).Normal

Equations

• ⋯ = ⋯

theorem AddSubgroup.inf_addSubgroupOf_inf_normal_of_right {G : Type u_1} [AddGroup G] (A : AddSubgroup G) (B' : AddSubgroup G) (B : AddSubgroup G) (hB : B' ≤ B) [hN : (B'.addSubgroupOf B).Normal] : ((A ⊓ B').addSubgroupOf (A ⊓ B)).Normal

theorem Subgroup.inf_subgroupOf_inf_normal_of_right {G : Type u_1} [Group G] (A : Subgroup G) (B' : Subgroup G) (B : Subgroup G) (hB : B' ≤ B) [hN : (B'.subgroupOf B).Normal] : ((A ⊓ B').subgroupOf (A ⊓ B)).Normal

theorem AddSubgroup.inf_addSubgroupOf_inf_normal_of_left {G : Type u_1} [AddGroup G] {A' : AddSubgroup G} {A : AddSubgroup G} (B : AddSubgroup G) (hA : A' ≤ A) [hN : (A'.addSubgroupOf A).Normal] : ((A' ⊓ B).addSubgroupOf (A ⊓ B)).Normal

theorem Subgroup.inf_subgroupOf_inf_normal_of_left {G : Type u_1} [Group G] {A' : Subgroup G} {A : Subgroup G} (B : Subgroup G) (hA : A' ≤ A) [hN : (A'.subgroupOf A).Normal] : ((A' ⊓ B).subgroupOf (A ⊓ B)).Normal

instance AddSubgroup.normal_inf_normal {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) [hH : H.Normal] [hK : K.Normal] : (H ⊓ K).Normal

Equations

• ⋯ = ⋯

instance Subgroup.normal_inf_normal {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) [hH : H.Normal] [hK : K.Normal] : (H ⊓ K).Normal

Equations

• ⋯ = ⋯

theorem AddSubgroup.addSubgroupOf_sup {G : Type u_1} [AddGroup G] (A : AddSubgroup G) (A' : AddSubgroup G) (B : AddSubgroup G) (hA : A ≤ B) (hA' : A' ≤ B) : (A ⊔ A').addSubgroupOf B = A.addSubgroupOf B ⊔ A'.addSubgroupOf B

theorem Subgroup.subgroupOf_sup {G : Type u_1} [Group G] (A : Subgroup G) (A' : Subgroup G) (B : Subgroup G) (hA : A ≤ B) (hA' : A' ≤ B) : (A ⊔ A').subgroupOf B = A.subgroupOf B ⊔ A'.subgroupOf B

theorem AddSubgroup.SubgroupNormal.mem_comm {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (hK : H ≤ K) [hN : (H.addSubgroupOf K).Normal] {a : G} {b : G} (hb : b ∈ K) (h : a + b ∈ H) : b + a ∈ H

theorem Subgroup.SubgroupNormal.mem_comm {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (hK : H ≤ K) [hN : (H.subgroupOf K).Normal] {a : G} {b : G} (hb : b ∈ K) (h : a * b ∈ H) : b * a ∈ H

theorem AddSubgroup.addCommute_of_normal_of_disjoint {G : Type u_1} [AddGroup G] (H₁ : AddSubgroup G) (H₂ : AddSubgroup G) (hH₁ : H₁.Normal) (hH₂ : H₂.Normal) (hdis : Disjoint H₁ H₂) (x : G) (y : G) (hx : x ∈ H₁) (hy : y ∈ H₂) : AddCommute x y

Elements of disjoint, normal subgroups commute.

theorem Subgroup.commute_of_normal_of_disjoint {G : Type u_1} [Group G] (H₁ : Subgroup G) (H₂ : Subgroup G) (hH₁ : H₁.Normal) (hH₂ : H₂.Normal) (hdis : Disjoint H₁ H₂) (x : G) (y : G) (hx : x ∈ H₁) (hy : y ∈ H₂) : Commute x y

Elements of disjoint, normal subgroups commute.

theorem AddSubgroup.disjoint_def {G : Type u_1} [AddGroup G] {H₁ : AddSubgroup G} {H₂ : AddSubgroup G} : Disjoint H₁ H₂ ↔ ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 0

theorem Subgroup.disjoint_def {G : Type u_1} [Group G] {H₁ : Subgroup G} {H₂ : Subgroup G} : Disjoint H₁ H₂ ↔ ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 1

theorem AddSubgroup.disjoint_def' {G : Type u_1} [AddGroup G] {H₁ : AddSubgroup G} {H₂ : AddSubgroup G} : Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x = y → x = 0

theorem Subgroup.disjoint_def' {G : Type u_1} [Group G] {H₁ : Subgroup G} {H₂ : Subgroup G} : Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x = y → x = 1

theorem AddSubgroup.disjoint_iff_add_eq_zero {G : Type u_1} [AddGroup G] {H₁ : AddSubgroup G} {H₂ : AddSubgroup G} : Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x + y = 0 → x = 0 ∧ y = 0

theorem Subgroup.disjoint_iff_mul_eq_one {G : Type u_1} [Group G] {H₁ : Subgroup G} {H₂ : Subgroup G} : Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x * y = 1 → x = 1 ∧ y = 1

theorem AddSubgroup.add_injective_of_disjoint {G : Type u_1} [AddGroup G] {H₁ : AddSubgroup G} {H₂ : AddSubgroup G} (h : Disjoint H₁ H₂) : Function.Injective fun (g : ↥H₁ × ↥H₂) => ↑g.1 + ↑g.2

theorem Subgroup.mul_injective_of_disjoint {G : Type u_1} [Group G] {H₁ : Subgroup G} {H₂ : Subgroup G} (h : Disjoint H₁ H₂) : Function.Injective fun (g : ↥H₁ × ↥H₂) => ↑g.1 * ↑g.2

theorem IsConj.normalClosure_eq_top_of {G : Type u_1} [Group G] {N : Subgroup G} [hn : N.Normal] {g : G} {g' : G} {hg : g ∈ N} {hg' : g' ∈ N} (hc : IsConj g g') (ht : Subgroup.normalClosure {⟨g, hg⟩} = ⊤) : Subgroup.normalClosure {⟨g', hg'⟩} = ⊤

def ConjClasses.noncenter (G : Type u_6) [Monoid G] : Set (ConjClasses G)

The conjugacy classes that are not trivial.

Equations

• ConjClasses.noncenter G = {x : ConjClasses G | x.carrier.Nontrivial}

@[simp]

theorem ConjClasses.mem_noncenter {G : Type u_6} [Monoid G] (g : ConjClasses G) : g ∈ ConjClasses.noncenter G ↔ g.carrier.Nontrivial