Quotients of groups by normal subgroups

This files develops the basic theory of quotients of groups by normal subgroups. In particular it proves Noether's first and second isomorphism theorems.

Main definitions

• mk': the canonical group homomorphism G →* G/N given a normal subgroup N of G.
• lift φ: the group homomorphism G/N →* H given a group homomorphism φ : G →* H such that N ⊆ ker φ.
• map f: the group homomorphism G/N →* H/M given a group homomorphism f : G →* H such that N ⊆ f⁻¹(M).

Main statements

• QuotientGroup.quotientKerEquivRange: Noether's first isomorphism theorem, an explicit isomorphism G/ker φ → range φ for every group homomorphism φ : G →* H.
• QuotientGroup.quotientInfEquivProdNormalQuotient: Noether's second isomorphism theorem, an explicit isomorphism between H/(H ∩ N) and (HN)/N given a subgroup H and a normal subgroup N of a group G.
• QuotientGroup.quotientQuotientEquivQuotient: Noether's third isomorphism theorem, the canonical isomorphism between (G / N) / (M / N) and G / M, where N ≤ M.

Tags

isomorphism theorems, quotient groups

def QuotientAddGroup.con {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] : AddCon G

The additive congruence relation generated by a normal additive subgroup.

Equations

• QuotientAddGroup.con N = { toSetoid := QuotientAddGroup.leftRel N, add' := (_ : ∀ (a b c d : G), Setoid.r a b → Setoid.r c d → Setoid.r (a + c) (b + d)) }

theorem QuotientAddGroup.con.proof_1 {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (a : G) (b : G) (c : G) (d : G) (hab : Setoid.r a b) (hcd : Setoid.r c d) : Setoid.r (a + c) (b + d)

def QuotientGroup.con {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] : Con G

The congruence relation generated by a normal subgroup.

Equations

• QuotientGroup.con N = { toSetoid := QuotientGroup.leftRel N, mul' := (_ : ∀ (a b c d : G), Setoid.r a b → Setoid.r c d → Setoid.r (a * c) (b * d)) }

instance QuotientAddGroup.Quotient.addGroup {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] : AddGroup (G ⧸ N)

Equations

• QuotientAddGroup.Quotient.addGroup N = AddCon.addGroup (QuotientAddGroup.con N)

instance QuotientGroup.Quotient.group {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] : Group (G ⧸ N)

Equations

• QuotientGroup.Quotient.group N = Con.group (QuotientGroup.con N)

theorem QuotientAddGroup.mk'.proof_1 {G : Type u_1} [AddGroup G] (N : AddSubgroup G) : ∀ (x x_1 : G), ↑(x + x_1) = ↑(x + x_1)

def QuotientAddGroup.mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] : G →+ G ⧸ N

The additive group homomorphism from G to G/N.

Equations

• QuotientAddGroup.mk' N = AddMonoidHom.mk' QuotientAddGroup.mk (_ : ∀ (x x_1 : G), ↑(x + x_1) = ↑(x + x_1))

def QuotientGroup.mk' {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] : G →* G ⧸ N

The group homomorphism from G to G/N.

Equations

• QuotientGroup.mk' N = MonoidHom.mk' QuotientGroup.mk (_ : ∀ (x x_1 : G), ↑(x * x_1) = ↑(x * x_1))

@[simp]

theorem QuotientAddGroup.coe_mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] : ↑(QuotientAddGroup.mk' N) = QuotientAddGroup.mk

@[simp]

theorem QuotientGroup.coe_mk' {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] : ↑(QuotientGroup.mk' N) = QuotientGroup.mk

@[simp]

theorem QuotientAddGroup.mk'_apply {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (x : G) : ↑(QuotientAddGroup.mk' N) x = ↑x

@[simp]

theorem QuotientGroup.mk'_apply {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] (x : G) : ↑(QuotientGroup.mk' N) x = ↑x

theorem QuotientAddGroup.mk'_surjective {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] : Function.Surjective ↑(QuotientAddGroup.mk' N)

theorem QuotientGroup.mk'_surjective {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] : Function.Surjective ↑(QuotientGroup.mk' N)

theorem QuotientAddGroup.mk'_eq_mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] {x : G} {y : G} : ↑(QuotientAddGroup.mk' N) x = ↑(QuotientAddGroup.mk' N) y ↔ ∃ z, z ∈ N ∧ x + z = y

theorem QuotientGroup.mk'_eq_mk' {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] {x : G} {y : G} : ↑(QuotientGroup.mk' N) x = ↑(QuotientGroup.mk' N) y ↔ ∃ z, z ∈ N ∧ x * z = y

theorem QuotientAddGroup.addMonoidHom_ext {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] {M : Type x} [AddMonoid M] ⦃f : G ⧸ N →+ M⦄ ⦃g : G ⧸ N →+ M⦄ (h : AddMonoidHom.comp f (QuotientAddGroup.mk' N) = AddMonoidHom.comp g (QuotientAddGroup.mk' N)) : f = g

Two AddMonoidHoms from an additive quotient group are equal if their compositions with AddQuotientGroup.mk' are equal.

See note [partially-applied ext lemmas].

theorem QuotientGroup.monoidHom_ext {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] {M : Type x} [Monoid M] ⦃f : G ⧸ N →* M⦄ ⦃g : G ⧸ N →* M⦄ (h : MonoidHom.comp f (QuotientGroup.mk' N) = MonoidHom.comp g (QuotientGroup.mk' N)) : f = g

Two MonoidHoms from a quotient group are equal if their compositions with QuotientGroup.mk' are equal.

See note [partially-applied ext lemmas].

@[simp]

theorem QuotientAddGroup.eq_zero_iff {G : Type u} [AddGroup G] {N : AddSubgroup G} [nN : AddSubgroup.Normal N] (x : G) : ↑x = 0 ↔ x ∈ N

@[simp]

theorem QuotientGroup.eq_one_iff {G : Type u} [Group G] {N : Subgroup G} [nN : Subgroup.Normal N] (x : G) : ↑x = 1 ↔ x ∈ N

theorem QuotientAddGroup.ker_le_range_iff {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] {I : Type w} [AddGroup I] (f : G →+ H) [AddSubgroup.Normal (AddMonoidHom.range f)] (g : H →+ I) : AddMonoidHom.ker g ≤ AddMonoidHom.range f ↔ AddMonoidHom.comp (QuotientAddGroup.mk' (AddMonoidHom.range f)) (AddSubgroup.subtype (AddMonoidHom.ker g)) = 0

abbrev QuotientAddGroup.ker_le_range_iff.match_1 {H : Type u_1} [AddGroup H] {I : Type u_2} [AddGroup I] (g : H →+ I) (motive : { x // x ∈ AddMonoidHom.ker g } → Prop) : (x : { x // x ∈ AddMonoidHom.ker g }) → ((val : H) → (hx : val ∈ AddMonoidHom.ker g) → motive { val := val, property := hx }) → motive x

Equations

• QuotientAddGroup.ker_le_range_iff.match_1 g motive x h_1 = Subtype.casesOn x fun val property => h_1 val property

theorem QuotientGroup.ker_le_range_iff {G : Type u} [Group G] {H : Type v} [Group H] {I : Type w} [Group I] (f : G →* H) [Subgroup.Normal (MonoidHom.range f)] (g : H →* I) : MonoidHom.ker g ≤ MonoidHom.range f ↔ MonoidHom.comp (QuotientGroup.mk' (MonoidHom.range f)) (Subgroup.subtype (MonoidHom.ker g)) = 1

@[simp]

theorem QuotientAddGroup.ker_mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] : AddMonoidHom.ker (QuotientAddGroup.mk' N) = N

@[simp]

theorem QuotientGroup.ker_mk' {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] : MonoidHom.ker (QuotientGroup.mk' N) = N

theorem QuotientAddGroup.eq_iff_sub_mem {G : Type u} [AddGroup G] {N : AddSubgroup G} [nN : AddSubgroup.Normal N] {x : G} {y : G} : ↑x = ↑y ↔ x - y ∈ N

theorem QuotientGroup.eq_iff_div_mem {G : Type u} [Group G] {N : Subgroup G} [nN : Subgroup.Normal N] {x : G} {y : G} : ↑x = ↑y ↔ x / y ∈ N

theorem QuotientAddGroup.Quotient.addCommGroup.proof_1 {G : Type u_1} [AddCommGroup G] (N : AddSubgroup G) (a : G ⧸ N) (b : G ⧸ N) : a + b = b + a

instance QuotientAddGroup.Quotient.addCommGroup {G : Type u_1} [AddCommGroup G] (N : AddSubgroup G) : AddCommGroup (G ⧸ N)

Equations

• QuotientAddGroup.Quotient.addCommGroup N = AddCommGroup.mk (_ : ∀ (a b : G ⧸ N), a + b = b + a)

instance QuotientGroup.Quotient.commGroup {G : Type u_1} [CommGroup G] (N : Subgroup G) : CommGroup (G ⧸ N)

Equations

• QuotientGroup.Quotient.commGroup N = CommGroup.mk (_ : ∀ (a b : G ⧸ N), a * b = b * a)

@[simp]

theorem QuotientAddGroup.mk_zero {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] : ↑0 = 0

@[simp]

theorem QuotientGroup.mk_one {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] : ↑1 = 1

@[simp]

theorem QuotientAddGroup.mk_add {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (a : G) (b : G) : ↑(a + b) = ↑a + ↑b

@[simp]

theorem QuotientGroup.mk_mul {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] (a : G) (b : G) : ↑(a * b) = ↑a * ↑b

@[simp]

theorem QuotientAddGroup.mk_neg {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (a : G) : ↑(-a) = -↑a

@[simp]

theorem QuotientGroup.mk_inv {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] (a : G) : ↑a⁻¹ = (↑a)⁻¹

@[simp]

theorem QuotientAddGroup.mk_sub {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (a : G) (b : G) : ↑(a - b) = ↑a - ↑b

@[simp]

theorem QuotientGroup.mk_div {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] (a : G) (b : G) : ↑(a / b) = ↑a / ↑b

@[simp]

theorem QuotientAddGroup.mk_nsmul {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (a : G) (n : ℕ) : ↑(n • a) = n • ↑a

@[simp]

theorem QuotientGroup.mk_pow {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] (a : G) (n : ℕ) : ↑(a ^ n) = ↑a ^ n

@[simp]

theorem QuotientAddGroup.mk_zsmul {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (a : G) (n : ℤ) : ↑(n • a) = n • ↑a

@[simp]

theorem QuotientGroup.mk_zpow {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] (a : G) (n : ℤ) : ↑(a ^ n) = ↑a ^ n

@[simp]

theorem QuotientAddGroup.mk_sum {G : Type u_1} {ι : Type u_2} [AddCommGroup G] (N : AddSubgroup G) (s : Finset ι) {f : ι → G} : ↑(Finset.sum s f) = Finset.sum s fun i => ↑(f i)

@[simp]

theorem QuotientGroup.mk_prod {G : Type u_1} {ι : Type u_2} [CommGroup G] (N : Subgroup G) (s : Finset ι) {f : ι → G} : ↑(Finset.prod s f) = Finset.prod s fun i => ↑(f i)

def QuotientAddGroup.lift {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] {M : Type x} [AddMonoid M] (φ : G →+ M) (HN : N ≤ AddMonoidHom.ker φ) : G ⧸ N →+ M

An AddGroup homomorphism φ : G →+ M with N ⊆ ker(φ) descends (i.e. lifts) to a group homomorphism G/N →* M.

Equations

• QuotientAddGroup.lift N φ HN = AddCon.lift (QuotientAddGroup.con N) φ (QuotientAddGroup.lift.proof_1 N φ HN)

theorem QuotientAddGroup.lift.proof_1 {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] {M : Type u_2} [AddMonoid M] (φ : G →+ M) (HN : N ≤ AddMonoidHom.ker φ) (x : G) (y : G) (h : ↑(QuotientAddGroup.con N) x y) : ↑(AddCon.ker φ) x y

def QuotientGroup.lift {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] {M : Type x} [Monoid M] (φ : G →* M) (HN : N ≤ MonoidHom.ker φ) : G ⧸ N →* M

A group homomorphism φ : G →* M with N ⊆ ker(φ) descends (i.e. lifts) to a group homomorphism G/N →* M.

Equations

• QuotientGroup.lift N φ HN = Con.lift (QuotientGroup.con N) φ (QuotientGroup.lift.proof_1 N φ HN)

@[simp]

theorem QuotientAddGroup.lift_mk {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] {M : Type x} [AddMonoid M] {φ : G →+ M} (HN : N ≤ AddMonoidHom.ker φ) (g : G) : ↑(QuotientAddGroup.lift N φ HN) ↑g = ↑φ g

@[simp]

theorem QuotientGroup.lift_mk {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] {M : Type x} [Monoid M] {φ : G →* M} (HN : N ≤ MonoidHom.ker φ) (g : G) : ↑(QuotientGroup.lift N φ HN) ↑g = ↑φ g

@[simp]

theorem QuotientAddGroup.lift_mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] {M : Type x} [AddMonoid M] {φ : G →+ M} (HN : N ≤ AddMonoidHom.ker φ) (g : G) : ↑(QuotientAddGroup.lift N φ HN) ↑g = ↑φ g

@[simp]

theorem QuotientGroup.lift_mk' {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] {M : Type x} [Monoid M] {φ : G →* M} (HN : N ≤ MonoidHom.ker φ) (g : G) : ↑(QuotientGroup.lift N φ HN) ↑g = ↑φ g

@[simp]

theorem QuotientAddGroup.lift_quot_mk {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] {M : Type x} [AddMonoid M] {φ : G →+ M} (HN : N ≤ AddMonoidHom.ker φ) (g : G) : ↑(QuotientAddGroup.lift N φ HN) (Quot.mk Setoid.r g) = ↑φ g

@[simp]

theorem QuotientGroup.lift_quot_mk {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] {M : Type x} [Monoid M] {φ : G →* M} (HN : N ≤ MonoidHom.ker φ) (g : G) : ↑(QuotientGroup.lift N φ HN) (Quot.mk Setoid.r g) = ↑φ g

theorem QuotientAddGroup.map.proof_1 {G : Type u_1} [AddGroup G] (N : AddSubgroup G) {H : Type u_2} [AddGroup H] (M : AddSubgroup H) (f : G →+ H) (h : N ≤ AddSubgroup.comap f M) ⦃x : G⦄ (hx : x ∈ N) : ↑(↑f x) = ↑0

def QuotientAddGroup.map {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] {H : Type v} [AddGroup H] (M : AddSubgroup H) [AddSubgroup.Normal M] (f : G →+ H) (h : N ≤ AddSubgroup.comap f M) : G ⧸ N →+ H ⧸ M

An AddGroup homomorphism f : G →+ H induces a map G/N →+ H/M if N ⊆ f⁻¹(M).

Equations

• QuotientAddGroup.map N M f h = QuotientAddGroup.lift N (AddMonoidHom.comp (QuotientAddGroup.mk' M) f) (_ : ∀ ⦃x : G⦄, x ∈ N → ↑(↑f x) = ↑0)

def QuotientGroup.map {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] {H : Type v} [Group H] (M : Subgroup H) [Subgroup.Normal M] (f : G →* H) (h : N ≤ Subgroup.comap f M) : G ⧸ N →* H ⧸ M

A group homomorphism f : G →* H induces a map G/N →* H/M if N ⊆ f⁻¹(M).

Equations

• QuotientGroup.map N M f h = QuotientGroup.lift N (MonoidHom.comp (QuotientGroup.mk' M) f) (_ : ∀ ⦃x : G⦄, x ∈ N → ↑(↑f x) = ↑1)

@[simp]

theorem QuotientAddGroup.map_mk {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] {H : Type v} [AddGroup H] (M : AddSubgroup H) [AddSubgroup.Normal M] (f : G →+ H) (h : N ≤ AddSubgroup.comap f M) (x : G) : ↑(QuotientAddGroup.map N M f h) ↑x = ↑(↑f x)

@[simp]

theorem QuotientGroup.map_mk {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] {H : Type v} [Group H] (M : Subgroup H) [Subgroup.Normal M] (f : G →* H) (h : N ≤ Subgroup.comap f M) (x : G) : ↑(QuotientGroup.map N M f h) ↑x = ↑(↑f x)

theorem QuotientAddGroup.map_mk' {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] {H : Type v} [AddGroup H] (M : AddSubgroup H) [AddSubgroup.Normal M] (f : G →+ H) (h : N ≤ AddSubgroup.comap f M) (x : G) : ↑(QuotientAddGroup.map N M f h) (↑(QuotientAddGroup.mk' N) x) = ↑(↑f x)

theorem QuotientGroup.map_mk' {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] {H : Type v} [Group H] (M : Subgroup H) [Subgroup.Normal M] (f : G →* H) (h : N ≤ Subgroup.comap f M) (x : G) : ↑(QuotientGroup.map N M f h) (↑(QuotientGroup.mk' N) x) = ↑(↑f x)

theorem QuotientAddGroup.map_id_apply {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (h : optParam (N ≤ AddSubgroup.comap (AddMonoidHom.id G) N) (_ : AddSubgroup.comap (AddMonoidHom.id G) N ≤ N)) (x : G ⧸ N) : ↑(QuotientAddGroup.map N N (AddMonoidHom.id G) h) x = x

theorem QuotientGroup.map_id_apply {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] (h : optParam (N ≤ Subgroup.comap (MonoidHom.id G) N) (_ : Subgroup.comap (MonoidHom.id G) N ≤ N)) (x : G ⧸ N) : ↑(QuotientGroup.map N N (MonoidHom.id G) h) x = x

@[simp]

theorem QuotientAddGroup.map_id {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (h : optParam (N ≤ AddSubgroup.comap (AddMonoidHom.id G) N) (_ : AddSubgroup.comap (AddMonoidHom.id G) N ≤ N)) : QuotientAddGroup.map N N (AddMonoidHom.id G) h = AddMonoidHom.id (G ⧸ N)

@[simp]

theorem QuotientGroup.map_id {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] (h : optParam (N ≤ Subgroup.comap (MonoidHom.id G) N) (_ : Subgroup.comap (MonoidHom.id G) N ≤ N)) : QuotientGroup.map N N (MonoidHom.id G) h = MonoidHom.id (G ⧸ N)

@[simp]

theorem QuotientAddGroup.map_map {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] {H : Type v} [AddGroup H] {I : Type u_1} [AddGroup I] (M : AddSubgroup H) (O : AddSubgroup I) [AddSubgroup.Normal M] [AddSubgroup.Normal O] (f : G →+ H) (g : H →+ I) (hf : N ≤ AddSubgroup.comap f M) (hg : M ≤ AddSubgroup.comap g O) (hgf : optParam (N ≤ AddSubgroup.comap (AddMonoidHom.comp g f) O) (_ : N ≤ AddSubgroup.comap (AddMonoidHom.comp g f) O)) (x : G ⧸ N) : ↑(QuotientAddGroup.map M O g hg) (↑(QuotientAddGroup.map N M f hf) x) = ↑(QuotientAddGroup.map N O (AddMonoidHom.comp g f) hgf) x

@[simp]

theorem QuotientGroup.map_map {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] {H : Type v} [Group H] {I : Type u_1} [Group I] (M : Subgroup H) (O : Subgroup I) [Subgroup.Normal M] [Subgroup.Normal O] (f : G →* H) (g : H →* I) (hf : N ≤ Subgroup.comap f M) (hg : M ≤ Subgroup.comap g O) (hgf : optParam (N ≤ Subgroup.comap (MonoidHom.comp g f) O) (_ : N ≤ Subgroup.comap (MonoidHom.comp g f) O)) (x : G ⧸ N) : ↑(QuotientGroup.map M O g hg) (↑(QuotientGroup.map N M f hf) x) = ↑(QuotientGroup.map N O (MonoidHom.comp g f) hgf) x

@[simp]

theorem QuotientAddGroup.map_comp_map {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] {H : Type v} [AddGroup H] {I : Type u_1} [AddGroup I] (M : AddSubgroup H) (O : AddSubgroup I) [AddSubgroup.Normal M] [AddSubgroup.Normal O] (f : G →+ H) (g : H →+ I) (hf : N ≤ AddSubgroup.comap f M) (hg : M ≤ AddSubgroup.comap g O) (hgf : optParam (N ≤ AddSubgroup.comap (AddMonoidHom.comp g f) O) (_ : N ≤ AddSubgroup.comap (AddMonoidHom.comp g f) O)) : AddMonoidHom.comp (QuotientAddGroup.map M O g hg) (QuotientAddGroup.map N M f hf) = QuotientAddGroup.map N O (AddMonoidHom.comp g f) hgf

@[simp]

theorem QuotientGroup.map_comp_map {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] {H : Type v} [Group H] {I : Type u_1} [Group I] (M : Subgroup H) (O : Subgroup I) [Subgroup.Normal M] [Subgroup.Normal O] (f : G →* H) (g : H →* I) (hf : N ≤ Subgroup.comap f M) (hg : M ≤ Subgroup.comap g O) (hgf : optParam (N ≤ Subgroup.comap (MonoidHom.comp g f) O) (_ : N ≤ Subgroup.comap (MonoidHom.comp g f) O)) : MonoidHom.comp (QuotientGroup.map M O g hg) (QuotientGroup.map N M f hf) = QuotientGroup.map N O (MonoidHom.comp g f) hgf

theorem QuotientAddGroup.congr.proof_5 {G : Type u_2} [AddGroup G] {H : Type u_1} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) [AddSubgroup.Normal G'] [AddSubgroup.Normal H'] (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H') (x : H ⧸ H') : ↑(QuotientAddGroup.map G' H' ↑e (_ : G' ≤ AddSubgroup.comap (↑e) H')) (↑(QuotientAddGroup.map H' G' ↑(AddEquiv.symm e) (_ : H' ≤ AddSubgroup.comap (↑(AddEquiv.symm e)) G')) x) = x

def QuotientAddGroup.congr {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) [AddSubgroup.Normal G'] [AddSubgroup.Normal H'] (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H') : G ⧸ G' ≃+ H ⧸ H'

QuotientAddGroup.congr lifts the isomorphism e : G ≃ H to G ⧸ G' ≃ H ⧸ H', given that e maps G to H.

Equations

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

theorem QuotientAddGroup.congr.proof_1 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H') : G' ≤ AddSubgroup.comap (↑e) H'

theorem QuotientAddGroup.congr.proof_6 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) [AddSubgroup.Normal G'] [AddSubgroup.Normal H'] (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H') (x : G ⧸ G') (y : G ⧸ G') : ZeroHom.toFun (↑(QuotientAddGroup.map G' H' ↑e (_ : G' ≤ AddSubgroup.comap (↑e) H'))) (x + y) = ZeroHom.toFun (↑(QuotientAddGroup.map G' H' ↑e (_ : G' ≤ AddSubgroup.comap (↑e) H'))) x + ZeroHom.toFun (↑(QuotientAddGroup.map G' H' ↑e (_ : G' ≤ AddSubgroup.comap (↑e) H'))) y

theorem QuotientAddGroup.congr.proof_3 {G : Type u_2} [AddGroup G] {H : Type u_1} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H') : H' ≤ AddSubgroup.comap (↑(AddEquiv.symm e)) G'

theorem QuotientAddGroup.congr.proof_2 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H') : G' ≤ AddSubgroup.comap (↑e) H'

theorem QuotientAddGroup.congr.proof_4 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) [AddSubgroup.Normal G'] [AddSubgroup.Normal H'] (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H') (x : G ⧸ G') : ↑(QuotientAddGroup.map H' G' ↑(AddEquiv.symm e) (_ : H' ≤ AddSubgroup.comap (↑(AddEquiv.symm e)) G')) (↑(QuotientAddGroup.map G' H' ↑e (_ : G' ≤ AddSubgroup.comap (↑e) H')) x) = x

def QuotientGroup.congr {G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [Subgroup.Normal G'] [Subgroup.Normal H'] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') : G ⧸ G' ≃* H ⧸ H'

QuotientGroup.congr lifts the isomorphism e : G ≃ H to G ⧸ G' ≃ H ⧸ H', given that e maps G to H.

Equations

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

@[simp]

theorem QuotientGroup.congr_mk {G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [Subgroup.Normal G'] [Subgroup.Normal H'] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') (x : G) : ↑(QuotientGroup.congr G' H' e he) ↑x = ↑(↑e x)

theorem QuotientGroup.congr_mk' {G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [Subgroup.Normal G'] [Subgroup.Normal H'] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') (x : G) : ↑(QuotientGroup.congr G' H' e he) (↑(QuotientGroup.mk' G') x) = ↑(QuotientGroup.mk' H') (↑e x)

@[simp]

theorem QuotientGroup.congr_apply {G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [Subgroup.Normal G'] [Subgroup.Normal H'] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') (x : G) : ↑(QuotientGroup.congr G' H' e he) ↑x = ↑(QuotientGroup.mk' H') (↑e x)

@[simp]

theorem QuotientGroup.congr_refl {G : Type u} [Group G] (G' : Subgroup G) [Subgroup.Normal G'] (he : optParam (Subgroup.map (↑(MulEquiv.refl G)) G' = G') (_ : Subgroup.map (MonoidHom.id G) G' = G')) : QuotientGroup.congr G' G' (MulEquiv.refl G) he = MulEquiv.refl (G ⧸ G')

@[simp]

theorem QuotientGroup.congr_symm {G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [Subgroup.Normal G'] [Subgroup.Normal H'] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') : MulEquiv.symm (QuotientGroup.congr G' H' e he) = QuotientGroup.congr H' G' (MulEquiv.symm e) (_ : Subgroup.map (↑(MulEquiv.symm e)) H' = G')

theorem QuotientAddGroup.kerLift.proof_2 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) (_g : G) : _g ∈ AddMonoidHom.ker φ → ↑φ _g = 0

def QuotientAddGroup.kerLift {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) : G ⧸ AddMonoidHom.ker φ →+ H

The induced map from the quotient by the kernel to the codomain.

Equations

• QuotientAddGroup.kerLift φ = QuotientAddGroup.lift (AddMonoidHom.ker φ) φ (_ : ∀ (_g : G), _g ∈ AddMonoidHom.ker φ → ↑φ _g = 0)

theorem QuotientAddGroup.kerLift.proof_1 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) : AddSubgroup.Normal (AddMonoidHom.ker φ)

def QuotientGroup.kerLift {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) : G ⧸ MonoidHom.ker φ →* H

The induced map from the quotient by the kernel to the codomain.

Equations

• QuotientGroup.kerLift φ = QuotientGroup.lift (MonoidHom.ker φ) φ (_ : ∀ (_g : G), _g ∈ MonoidHom.ker φ → ↑φ _g = 1)

@[simp]

theorem QuotientAddGroup.kerLift_mk {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (g : G) : ↑(QuotientAddGroup.kerLift φ) ↑g = ↑φ g

@[simp]

theorem QuotientGroup.kerLift_mk {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (g : G) : ↑(QuotientGroup.kerLift φ) ↑g = ↑φ g

@[simp]

theorem QuotientAddGroup.kerLift_mk' {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (g : G) : ↑(QuotientAddGroup.kerLift φ) ↑g = ↑φ g

@[simp]

theorem QuotientGroup.kerLift_mk' {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (g : G) : ↑(QuotientGroup.kerLift φ) ↑g = ↑φ g

theorem QuotientAddGroup.kerLift_injective {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) : Function.Injective ↑(QuotientAddGroup.kerLift φ)

theorem QuotientGroup.kerLift_injective {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) : Function.Injective ↑(QuotientGroup.kerLift φ)

theorem QuotientAddGroup.rangeKerLift.proof_1 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) : AddSubgroup.Normal (AddMonoidHom.ker φ)

theorem QuotientAddGroup.rangeKerLift.proof_2 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) (g : G) (hg : g ∈ AddMonoidHom.ker φ) : ↑(AddMonoidHom.rangeRestrict φ) g = 0

def QuotientAddGroup.rangeKerLift {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) : G ⧸ AddMonoidHom.ker φ →+ { x // x ∈ AddMonoidHom.range φ }

The induced map from the quotient by the kernel to the range.

Equations

• QuotientAddGroup.rangeKerLift φ = QuotientAddGroup.lift (AddMonoidHom.ker φ) (AddMonoidHom.rangeRestrict φ) (_ : ∀ (g : G), g ∈ AddMonoidHom.ker φ → ↑(AddMonoidHom.rangeRestrict φ) g = 0)

def QuotientGroup.rangeKerLift {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) : G ⧸ MonoidHom.ker φ →* { x // x ∈ MonoidHom.range φ }

The induced map from the quotient by the kernel to the range.

Equations

• QuotientGroup.rangeKerLift φ = QuotientGroup.lift (MonoidHom.ker φ) (MonoidHom.rangeRestrict φ) (_ : ∀ (g : G), g ∈ MonoidHom.ker φ → ↑(MonoidHom.rangeRestrict φ) g = 1)

theorem QuotientAddGroup.rangeKerLift_injective {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) : Function.Injective ↑(QuotientAddGroup.rangeKerLift φ)

theorem QuotientGroup.rangeKerLift_injective {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) : Function.Injective ↑(QuotientGroup.rangeKerLift φ)

theorem QuotientAddGroup.rangeKerLift_surjective {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) : Function.Surjective ↑(QuotientAddGroup.rangeKerLift φ)

theorem QuotientGroup.rangeKerLift_surjective {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) : Function.Surjective ↑(QuotientGroup.rangeKerLift φ)

theorem QuotientAddGroup.quotientKerEquivRange.proof_1 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) : AddSubgroup.Normal (AddMonoidHom.ker φ)

noncomputable def QuotientAddGroup.quotientKerEquivRange {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) : G ⧸ AddMonoidHom.ker φ ≃+ { x // x ∈ AddMonoidHom.range φ }

The first isomorphism theorem (a definition): the canonical isomorphism between G/(ker φ) to range φ.

Equations

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

theorem QuotientAddGroup.quotientKerEquivRange.proof_2 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) : Function.Injective ↑(QuotientAddGroup.rangeKerLift φ) ∧ Function.Surjective ↑(QuotientAddGroup.rangeKerLift φ)

noncomputable def QuotientGroup.quotientKerEquivRange {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) : G ⧸ MonoidHom.ker φ ≃* { x // x ∈ MonoidHom.range φ }

Noether's first isomorphism theorem (a definition): the canonical isomorphism between G/(ker φ) to range φ.

Equations

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

theorem QuotientAddGroup.quotientKerEquivOfRightInverse.proof_1 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) : AddSubgroup.Normal (AddMonoidHom.ker φ)

def QuotientAddGroup.quotientKerEquivOfRightInverse {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (ψ : H → G) (hφ : Function.RightInverse ψ ↑φ) : G ⧸ AddMonoidHom.ker φ ≃+ H

The canonical isomorphism G/(ker φ) ≃+ H induced by a homomorphism φ : G →+ H with a right inverse ψ : H → G.

Equations

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

theorem QuotientAddGroup.quotientKerEquivOfRightInverse.proof_2 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) (ψ : H → G) (hφ : Function.RightInverse ψ ↑φ) (x : G ⧸ AddMonoidHom.ker φ) : (QuotientAddGroup.mk ∘ ψ) (↑(QuotientAddGroup.kerLift φ) x) = x

theorem QuotientAddGroup.quotientKerEquivOfRightInverse.proof_3 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) (x : G ⧸ AddMonoidHom.ker φ) (y : G ⧸ AddMonoidHom.ker φ) : ZeroHom.toFun (↑(QuotientAddGroup.kerLift φ)) (x + y) = ZeroHom.toFun (↑(QuotientAddGroup.kerLift φ)) x + ZeroHom.toFun (↑(QuotientAddGroup.kerLift φ)) y

@[simp]

theorem QuotientGroup.quotientKerEquivOfRightInverse_apply {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (ψ : H → G) (hφ : Function.RightInverse ψ ↑φ) (a : G ⧸ MonoidHom.ker φ) : ↑(QuotientGroup.quotientKerEquivOfRightInverse φ ψ hφ) a = ↑(QuotientGroup.kerLift φ) a

@[simp]

theorem QuotientGroup.quotientKerEquivOfRightInverse_symm_apply {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (ψ : H → G) (hφ : Function.RightInverse ψ ↑φ) : ∀ (a : H), ↑(MulEquiv.symm (QuotientGroup.quotientKerEquivOfRightInverse φ ψ hφ)) a = (QuotientGroup.mk ∘ ψ) a

@[simp]

theorem QuotientAddGroup.quotientKerEquivOfRightInverse_apply {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (ψ : H → G) (hφ : Function.RightInverse ψ ↑φ) (a : G ⧸ AddMonoidHom.ker φ) : ↑(QuotientAddGroup.quotientKerEquivOfRightInverse φ ψ hφ) a = ↑(QuotientAddGroup.kerLift φ) a

@[simp]

theorem QuotientAddGroup.quotientKerEquivOfRightInverse_symm_apply {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (ψ : H → G) (hφ : Function.RightInverse ψ ↑φ) : ∀ (a : H), ↑(AddEquiv.symm (QuotientAddGroup.quotientKerEquivOfRightInverse φ ψ hφ)) a = (QuotientAddGroup.mk ∘ ψ) a

def QuotientGroup.quotientKerEquivOfRightInverse {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (ψ : H → G) (hφ : Function.RightInverse ψ ↑φ) : G ⧸ MonoidHom.ker φ ≃* H

The canonical isomorphism G/(ker φ) ≃* H induced by a homomorphism φ : G →* H with a right inverse ψ : H → G.

Equations

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

theorem QuotientAddGroup.quotientBot.proof_1 {G : Type u_1} [AddGroup G] (_x : G) : ↑(AddMonoidHom.id G) (id _x) = ↑(AddMonoidHom.id G) (id _x)

def QuotientAddGroup.quotientBot {G : Type u} [AddGroup G] : G ⧸ ⊥ ≃+ G

The canonical isomorphism G/⊥ ≃+ G.

Equations

• QuotientAddGroup.quotientBot = QuotientAddGroup.quotientKerEquivOfRightInverse (AddMonoidHom.id G) id (_ : ∀ (_x : G), ↑(AddMonoidHom.id G) (id _x) = ↑(AddMonoidHom.id G) (id _x))

@[simp]

theorem QuotientGroup.quotientBot_apply {G : Type u} [Group G] (a : G ⧸ MonoidHom.ker (MonoidHom.id G)) : ↑QuotientGroup.quotientBot a = ↑(QuotientGroup.kerLift (MonoidHom.id G)) a

@[simp]

theorem QuotientAddGroup.quotientBot_symm_apply {G : Type u} [AddGroup G] : ∀ (a : G), ↑(AddEquiv.symm QuotientAddGroup.quotientBot) a = ↑a

@[simp]

theorem QuotientGroup.quotientBot_symm_apply {G : Type u} [Group G] : ∀ (a : G), ↑(MulEquiv.symm QuotientGroup.quotientBot) a = ↑a

@[simp]

theorem QuotientAddGroup.quotientBot_apply {G : Type u} [AddGroup G] (a : G ⧸ AddMonoidHom.ker (AddMonoidHom.id G)) : ↑QuotientAddGroup.quotientBot a = ↑(QuotientAddGroup.kerLift (AddMonoidHom.id G)) a

def QuotientGroup.quotientBot {G : Type u} [Group G] : G ⧸ ⊥ ≃* G

The canonical isomorphism G/⊥ ≃* G.

Equations

• QuotientGroup.quotientBot = QuotientGroup.quotientKerEquivOfRightInverse (MonoidHom.id G) id (_ : ∀ (_x : G), ↑(MonoidHom.id G) (id _x) = ↑(MonoidHom.id G) (id _x))

noncomputable def QuotientAddGroup.quotientKerEquivOfSurjective {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (φ : G →+ H) (hφ : Function.Surjective ↑φ) : G ⧸ AddMonoidHom.ker φ ≃+ H

The canonical isomorphism G/(ker φ) ≃+ H induced by a surjection φ : G →+ H. For a computable version, see QuotientAddGroup.quotientKerEquivOfRightInverse.

Equations

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

theorem QuotientAddGroup.quotientKerEquivOfSurjective.proof_2 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) (hφ : Function.Surjective ↑φ) : Function.RightInverse (Exists.choose (_ : Function.HasRightInverse ↑φ)) ↑φ

theorem QuotientAddGroup.quotientKerEquivOfSurjective.proof_1 {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (φ : G →+ H) (hφ : Function.Surjective ↑φ) : Function.HasRightInverse ↑φ

noncomputable def QuotientGroup.quotientKerEquivOfSurjective {G : Type u} [Group G] {H : Type v} [Group H] (φ : G →* H) (hφ : Function.Surjective ↑φ) : G ⧸ MonoidHom.ker φ ≃* H

The canonical isomorphism G/(ker φ) ≃* H induced by a surjection φ : G →* H.

For a computable version, see QuotientGroup.quotientKerEquivOfRightInverse.

Equations

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

theorem QuotientAddGroup.quotientAddEquivOfEq.proof_2 {G : Type u_1} [AddGroup G] {M : AddSubgroup G} {N : AddSubgroup G} (h : M = N) : Function.RightInverse (AddSubgroup.quotientEquivOfEq h).invFun (AddSubgroup.quotientEquivOfEq h).toFun

theorem QuotientAddGroup.quotientAddEquivOfEq.proof_1 {G : Type u_1} [AddGroup G] {M : AddSubgroup G} {N : AddSubgroup G} (h : M = N) : Function.LeftInverse (AddSubgroup.quotientEquivOfEq h).invFun (AddSubgroup.quotientEquivOfEq h).toFun

def QuotientAddGroup.quotientAddEquivOfEq {G : Type u} [AddGroup G] {M : AddSubgroup G} {N : AddSubgroup G} [AddSubgroup.Normal M] [AddSubgroup.Normal N] (h : M = N) : G ⧸ M ≃+ G ⧸ N

If two normal subgroups M and N of G are the same, their quotient groups are isomorphic.

Equations

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

theorem QuotientAddGroup.quotientAddEquivOfEq.proof_3 {G : Type u_1} [AddGroup G] {M : AddSubgroup G} {N : AddSubgroup G} [AddSubgroup.Normal M] [AddSubgroup.Normal N] (h : M = N) (q : G ⧸ M) (r : G ⧸ M) : Equiv.toFun { toFun := (AddSubgroup.quotientEquivOfEq h).toFun, invFun := (AddSubgroup.quotientEquivOfEq h).invFun, left_inv := (_ : Function.LeftInverse (AddSubgroup.quotientEquivOfEq h).invFun (AddSubgroup.quotientEquivOfEq h).toFun), right_inv := (_ : Function.RightInverse (AddSubgroup.quotientEquivOfEq h).invFun (AddSubgroup.quotientEquivOfEq h).toFun) } (q + r) = Equiv.toFun { toFun := (AddSubgroup.quotientEquivOfEq h).toFun, invFun := (AddSubgroup.quotientEquivOfEq h).invFun, left_inv := (_ : Function.LeftInverse (AddSubgroup.quotientEquivOfEq h).invFun (AddSubgroup.quotientEquivOfEq h).toFun), right_inv := (_ : Function.RightInverse (AddSubgroup.quotientEquivOfEq h).invFun (AddSubgroup.quotientEquivOfEq h).toFun) } q + Equiv.toFun { toFun := (AddSubgroup.quotientEquivOfEq h).toFun, invFun := (AddSubgroup.quotientEquivOfEq h).invFun, left_inv := (_ : Function.LeftInverse (AddSubgroup.quotientEquivOfEq h).invFun (AddSubgroup.quotientEquivOfEq h).toFun), right_inv := (_ : Function.RightInverse (AddSubgroup.quotientEquivOfEq h).invFun (AddSubgroup.quotientEquivOfEq h).toFun) } r

def QuotientGroup.quotientMulEquivOfEq {G : Type u} [Group G] {M : Subgroup G} {N : Subgroup G} [Subgroup.Normal M] [Subgroup.Normal N] (h : M = N) : G ⧸ M ≃* G ⧸ N

If two normal subgroups M and N of G are the same, their quotient groups are isomorphic.

Equations

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

@[simp]

theorem QuotientAddGroup.quotientAddEquivOfEq_mk {G : Type u} [AddGroup G] {M : AddSubgroup G} {N : AddSubgroup G} [AddSubgroup.Normal M] [AddSubgroup.Normal N] (h : M = N) (x : G) : ↑(QuotientAddGroup.quotientAddEquivOfEq h) ↑x = ↑x

@[simp]

theorem QuotientGroup.quotientMulEquivOfEq_mk {G : Type u} [Group G] {M : Subgroup G} {N : Subgroup G} [Subgroup.Normal M] [Subgroup.Normal N] (h : M = N) (x : G) : ↑(QuotientGroup.quotientMulEquivOfEq h) ↑x = ↑x

def QuotientAddGroup.quotientMapAddSubgroupOfOfLe {G : Type u} [AddGroup G] {A' : AddSubgroup G} {A : AddSubgroup G} {B' : AddSubgroup G} {B : AddSubgroup G} [_hAN : AddSubgroup.Normal (AddSubgroup.addSubgroupOf A' A)] [_hBN : AddSubgroup.Normal (AddSubgroup.addSubgroupOf B' B)] (h' : A' ≤ B') (h : A ≤ B) : { x // x ∈ A } ⧸ AddSubgroup.addSubgroupOf A' A →+ { x // x ∈ B } ⧸ AddSubgroup.addSubgroupOf B' B

Let A', A, B', B be subgroups of G. If A' ≤ B' and A ≤ B, then there is a map A / (A' ⊓ A) →+ B / (B' ⊓ B) induced by the inclusions.

Equations

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

theorem QuotientAddGroup.quotientMapAddSubgroupOfOfLe.proof_1 {G : Type u_1} [AddGroup G] {A' : AddSubgroup G} {A : AddSubgroup G} {B' : AddSubgroup G} (h' : A' ≤ B') : AddSubgroup.comap (AddSubgroup.subtype A) A' ≤ AddSubgroup.comap (AddSubgroup.subtype A) B'

def QuotientGroup.quotientMapSubgroupOfOfLe {G : Type u} [Group G] {A' : Subgroup G} {A : Subgroup G} {B' : Subgroup G} {B : Subgroup G} [_hAN : Subgroup.Normal (Subgroup.subgroupOf A' A)] [_hBN : Subgroup.Normal (Subgroup.subgroupOf B' B)] (h' : A' ≤ B') (h : A ≤ B) : { x // x ∈ A } ⧸ Subgroup.subgroupOf A' A →* { x // x ∈ B } ⧸ Subgroup.subgroupOf B' B

Let A', A, B', B be subgroups of G. If A' ≤ B' and A ≤ B, then there is a map A / (A' ⊓ A) →* B / (B' ⊓ B) induced by the inclusions.

Equations

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

@[simp]

theorem QuotientAddGroup.quotientMapAddSubgroupOfOfLe_mk {G : Type u} [AddGroup G] {A' : AddSubgroup G} {A : AddSubgroup G} {B' : AddSubgroup G} {B : AddSubgroup G} [_hAN : AddSubgroup.Normal (AddSubgroup.addSubgroupOf A' A)] [_hBN : AddSubgroup.Normal (AddSubgroup.addSubgroupOf B' B)] (h' : A' ≤ B') (h : A ≤ B) (x : { x // x ∈ A }) : ↑(QuotientAddGroup.quotientMapAddSubgroupOfOfLe h' h) ↑x = ↑(↑(AddSubgroup.inclusion h) x)

@[simp]

theorem QuotientGroup.quotientMapSubgroupOfOfLe_mk {G : Type u} [Group G] {A' : Subgroup G} {A : Subgroup G} {B' : Subgroup G} {B : Subgroup G} [_hAN : Subgroup.Normal (Subgroup.subgroupOf A' A)] [_hBN : Subgroup.Normal (Subgroup.subgroupOf B' B)] (h' : A' ≤ B') (h : A ≤ B) (x : { x // x ∈ A }) : ↑(QuotientGroup.quotientMapSubgroupOfOfLe h' h) ↑x = ↑(↑(Subgroup.inclusion h) x)

theorem QuotientAddGroup.equivQuotientAddSubgroupOfOfEq.proof_3 {G : Type u_1} [AddGroup G] {A' : AddSubgroup G} {B' : AddSubgroup G} (h' : A' = B') : B' ≤ A'

theorem QuotientAddGroup.equivQuotientAddSubgroupOfOfEq.proof_1 {G : Type u_1} [AddGroup G] {A' : AddSubgroup G} {B' : AddSubgroup G} (h' : A' = B') : A' ≤ B'

theorem QuotientAddGroup.equivQuotientAddSubgroupOfOfEq.proof_6 {G : Type u_1} [AddGroup G] {A' : AddSubgroup G} {A : AddSubgroup G} {B' : AddSubgroup G} {B : AddSubgroup G} [hAN : AddSubgroup.Normal (AddSubgroup.addSubgroupOf A' A)] [hBN : AddSubgroup.Normal (AddSubgroup.addSubgroupOf B' B)] (h' : A' = B') (h : A = B) : AddMonoidHom.comp (QuotientAddGroup.quotientMapAddSubgroupOfOfLe (_ : A' ≤ B') (_ : A ≤ B)) (QuotientAddGroup.quotientMapAddSubgroupOfOfLe (_ : B' ≤ A') (_ : B ≤ A)) = AddMonoidHom.id ({ x // x ∈ B } ⧸ AddSubgroup.addSubgroupOf B' B)

theorem QuotientAddGroup.equivQuotientAddSubgroupOfOfEq.proof_5 {G : Type u_1} [AddGroup G] {A' : AddSubgroup G} {A : AddSubgroup G} {B' : AddSubgroup G} {B : AddSubgroup G} [hAN : AddSubgroup.Normal (AddSubgroup.addSubgroupOf A' A)] [hBN : AddSubgroup.Normal (AddSubgroup.addSubgroupOf B' B)] (h' : A' = B') (h : A = B) : AddMonoidHom.comp (QuotientAddGroup.quotientMapAddSubgroupOfOfLe (_ : B' ≤ A') (_ : B ≤ A)) (QuotientAddGroup.quotientMapAddSubgroupOfOfLe (_ : A' ≤ B') (_ : A ≤ B)) = AddMonoidHom.id ({ x // x ∈ A } ⧸ AddSubgroup.addSubgroupOf A' A)

theorem QuotientAddGroup.equivQuotientAddSubgroupOfOfEq.proof_2 {G : Type u_1} [AddGroup G] {A : AddSubgroup G} {B : AddSubgroup G} (h : A = B) : A ≤ B

theorem QuotientAddGroup.equivQuotientAddSubgroupOfOfEq.proof_4 {G : Type u_1} [AddGroup G] {A : AddSubgroup G} {B : AddSubgroup G} (h : A = B) : B ≤ A

def QuotientAddGroup.equivQuotientAddSubgroupOfOfEq {G : Type u} [AddGroup G] {A' : AddSubgroup G} {A : AddSubgroup G} {B' : AddSubgroup G} {B : AddSubgroup G} [hAN : AddSubgroup.Normal (AddSubgroup.addSubgroupOf A' A)] [hBN : AddSubgroup.Normal (AddSubgroup.addSubgroupOf B' B)] (h' : A' = B') (h : A = B) : { x // x ∈ A } ⧸ AddSubgroup.addSubgroupOf A' A ≃+ { x // x ∈ B } ⧸ AddSubgroup.addSubgroupOf B' B

Let A', A, B', B be subgroups of G. If A' = B' and A = B, then the quotients A / (A' ⊓ A) and B / (B' ⊓ B) are isomorphic. Applying this equiv is nicer than rewriting along the equalities, since the type of (A'.addSubgroupOf A : AddSubgroup A) depends on on A.

Equations

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

def QuotientGroup.equivQuotientSubgroupOfOfEq {G : Type u} [Group G] {A' : Subgroup G} {A : Subgroup G} {B' : Subgroup G} {B : Subgroup G} [hAN : Subgroup.Normal (Subgroup.subgroupOf A' A)] [hBN : Subgroup.Normal (Subgroup.subgroupOf B' B)] (h' : A' = B') (h : A = B) : { x // x ∈ A } ⧸ Subgroup.subgroupOf A' A ≃* { x // x ∈ B } ⧸ Subgroup.subgroupOf B' B

Let A', A, B', B be subgroups of G. If A' = B' and A = B, then the quotients A / (A' ⊓ A) and B / (B' ⊓ B) are isomorphic.

Applying this equiv is nicer than rewriting along the equalities, since the type of (A'.subgroupOf A : Subgroup A) depends on A.

Equations

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

theorem QuotientAddGroup.homQuotientZSMulOfHom.proof_1 {A : Type u_1} [AddCommGroup A] (n : ℤ) : AddSubgroup.Normal (AddMonoidHom.range (zsmulAddGroupHom n))

def QuotientAddGroup.homQuotientZSMulOfHom {A : Type u} {B : Type u} [AddCommGroup A] [AddCommGroup B] (f : A →+ B) (n : ℤ) : A ⧸ AddMonoidHom.range (zsmulAddGroupHom n) →+ B ⧸ AddMonoidHom.range (zsmulAddGroupHom n)

The map of quotients by multiples of an integer induced by an additive group homomorphism.

Equations

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

abbrev QuotientAddGroup.homQuotientZSMulOfHom.match_1 {A : Type u_1} [AddCommGroup A] (n : ℤ) (g : A) (motive : g ∈ AddMonoidHom.range (zsmulAddGroupHom n) → Prop) : (x : g ∈ AddMonoidHom.range (zsmulAddGroupHom n)) → ((h : A) → (hg : n • h = g) → motive (_ : ∃ y, ↑(zsmulAddGroupHom n) y = g)) → motive x

Equations

• QuotientAddGroup.homQuotientZSMulOfHom.match_1 n g motive x h_1 = Exists.casesOn x fun w h => h_1 w h

theorem QuotientAddGroup.homQuotientZSMulOfHom.proof_2 {B : Type u_1} [AddCommGroup B] (n : ℤ) : AddSubgroup.Normal (AddMonoidHom.range (zsmulAddGroupHom n))

theorem QuotientAddGroup.homQuotientZSMulOfHom.proof_3 {A : Type u_1} {B : Type u_1} [AddCommGroup A] [AddCommGroup B] (f : A →+ B) (n : ℤ) (g : A) : g ∈ AddMonoidHom.range (zsmulAddGroupHom n) → g ∈ AddMonoidHom.ker (AddMonoidHom.comp (QuotientAddGroup.mk' (AddMonoidHom.range (zsmulAddGroupHom n))) f)

def QuotientGroup.homQuotientZPowOfHom {A : Type u} {B : Type u} [CommGroup A] [CommGroup B] (f : A →* B) (n : ℤ) : A ⧸ MonoidHom.range (zpowGroupHom n) →* B ⧸ MonoidHom.range (zpowGroupHom n)

The map of quotients by powers of an integer induced by a group homomorphism.

Equations

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

@[simp]

theorem QuotientAddGroup.homQuotientZSMulOfHom_id {A : Type u} [AddCommGroup A] (n : ℤ) : QuotientAddGroup.homQuotientZSMulOfHom (AddMonoidHom.id A) n = AddMonoidHom.id (A ⧸ AddMonoidHom.range (zsmulAddGroupHom n))

@[simp]

theorem QuotientGroup.homQuotientZPowOfHom_id {A : Type u} [CommGroup A] (n : ℤ) : QuotientGroup.homQuotientZPowOfHom (MonoidHom.id A) n = MonoidHom.id (A ⧸ MonoidHom.range (zpowGroupHom n))

@[simp]

theorem QuotientAddGroup.homQuotientZSMulOfHom_comp {A : Type u} {B : Type u} [AddCommGroup A] [AddCommGroup B] (f : A →+ B) (g : B →+ A) (n : ℤ) : QuotientAddGroup.homQuotientZSMulOfHom (AddMonoidHom.comp f g) n = AddMonoidHom.comp (QuotientAddGroup.homQuotientZSMulOfHom f n) (QuotientAddGroup.homQuotientZSMulOfHom g n)

@[simp]

theorem QuotientGroup.homQuotientZPowOfHom_comp {A : Type u} {B : Type u} [CommGroup A] [CommGroup B] (f : A →* B) (g : B →* A) (n : ℤ) : QuotientGroup.homQuotientZPowOfHom (MonoidHom.comp f g) n = MonoidHom.comp (QuotientGroup.homQuotientZPowOfHom f n) (QuotientGroup.homQuotientZPowOfHom g n)

@[simp]

theorem QuotientAddGroup.homQuotientZSMulOfHom_comp_of_rightInverse {A : Type u} {B : Type u} [AddCommGroup A] [AddCommGroup B] (f : A →+ B) (g : B →+ A) (n : ℤ) (i : Function.RightInverse ↑g ↑f) : AddMonoidHom.comp (QuotientAddGroup.homQuotientZSMulOfHom f n) (QuotientAddGroup.homQuotientZSMulOfHom g n) = AddMonoidHom.id (B ⧸ AddMonoidHom.range (zsmulAddGroupHom n))

@[simp]

theorem QuotientGroup.homQuotientZPowOfHom_comp_of_rightInverse {A : Type u} {B : Type u} [CommGroup A] [CommGroup B] (f : A →* B) (g : B →* A) (n : ℤ) (i : Function.RightInverse ↑g ↑f) : MonoidHom.comp (QuotientGroup.homQuotientZPowOfHom f n) (QuotientGroup.homQuotientZPowOfHom g n) = MonoidHom.id (B ⧸ MonoidHom.range (zpowGroupHom n))

theorem QuotientAddGroup.equivQuotientZSMulOfEquiv.proof_2 {B : Type u_1} [AddCommGroup B] (n : ℤ) : AddSubgroup.Normal (AddMonoidHom.range (zsmulAddGroupHom n))

def QuotientAddGroup.equivQuotientZSMulOfEquiv {A : Type u} {B : Type u} [AddCommGroup A] [AddCommGroup B] (e : A ≃+ B) (n : ℤ) : A ⧸ AddMonoidHom.range (zsmulAddGroupHom n) ≃+ B ⧸ AddMonoidHom.range (zsmulAddGroupHom n)

The equivalence of quotients by multiples of an integer induced by an additive group isomorphism.

Equations

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

theorem QuotientAddGroup.equivQuotientZSMulOfEquiv.proof_1 {A : Type u_1} [AddCommGroup A] (n : ℤ) : AddSubgroup.Normal (AddMonoidHom.range (zsmulAddGroupHom n))

theorem QuotientAddGroup.equivQuotientZSMulOfEquiv.proof_3 {A : Type u_1} {B : Type u_1} [AddCommGroup A] [AddCommGroup B] (e : A ≃+ B) (n : ℤ) : AddMonoidHom.comp (QuotientAddGroup.homQuotientZSMulOfHom (↑(AddEquiv.symm e)) n) (QuotientAddGroup.homQuotientZSMulOfHom (↑e) n) = AddMonoidHom.id (A ⧸ AddMonoidHom.range (zsmulAddGroupHom n))

theorem QuotientAddGroup.equivQuotientZSMulOfEquiv.proof_4 {A : Type u_1} {B : Type u_1} [AddCommGroup A] [AddCommGroup B] (e : A ≃+ B) (n : ℤ) : AddMonoidHom.comp (QuotientAddGroup.homQuotientZSMulOfHom (↑e) n) (QuotientAddGroup.homQuotientZSMulOfHom (↑(AddEquiv.symm e)) n) = AddMonoidHom.id (B ⧸ AddMonoidHom.range (zsmulAddGroupHom n))

def QuotientGroup.equivQuotientZPowOfEquiv {A : Type u} {B : Type u} [CommGroup A] [CommGroup B] (e : A ≃* B) (n : ℤ) : A ⧸ MonoidHom.range (zpowGroupHom n) ≃* B ⧸ MonoidHom.range (zpowGroupHom n)

The equivalence of quotients by powers of an integer induced by a group isomorphism.

Equations

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

@[simp]

theorem QuotientAddGroup.equivQuotientZSMulOfEquiv_refl {A : Type u} [AddCommGroup A] (n : ℤ) : AddEquiv.refl (A ⧸ AddMonoidHom.range (zsmulAddGroupHom n)) = QuotientAddGroup.equivQuotientZSMulOfEquiv (AddEquiv.refl A) n

@[simp]

theorem QuotientGroup.equivQuotientZPowOfEquiv_refl {A : Type u} [CommGroup A] (n : ℤ) : MulEquiv.refl (A ⧸ MonoidHom.range (zpowGroupHom n)) = QuotientGroup.equivQuotientZPowOfEquiv (MulEquiv.refl A) n

@[simp]

theorem QuotientAddGroup.equivQuotientZSMulOfEquiv_symm {A : Type u} {B : Type u} [AddCommGroup A] [AddCommGroup B] (e : A ≃+ B) (n : ℤ) : AddEquiv.symm (QuotientAddGroup.equivQuotientZSMulOfEquiv e n) = QuotientAddGroup.equivQuotientZSMulOfEquiv (AddEquiv.symm e) n

@[simp]

theorem QuotientGroup.equivQuotientZPowOfEquiv_symm {A : Type u} {B : Type u} [CommGroup A] [CommGroup B] (e : A ≃* B) (n : ℤ) : MulEquiv.symm (QuotientGroup.equivQuotientZPowOfEquiv e n) = QuotientGroup.equivQuotientZPowOfEquiv (MulEquiv.symm e) n

@[simp]

theorem QuotientAddGroup.equivQuotientZSMulOfEquiv_trans {A : Type u} {B : Type u} {C : Type u} [AddCommGroup A] [AddCommGroup B] [AddCommGroup C] (e : A ≃+ B) (d : B ≃+ C) (n : ℤ) : AddEquiv.trans (QuotientAddGroup.equivQuotientZSMulOfEquiv e n) (QuotientAddGroup.equivQuotientZSMulOfEquiv d n) = QuotientAddGroup.equivQuotientZSMulOfEquiv (AddEquiv.trans e d) n

@[simp]

theorem QuotientGroup.equivQuotientZPowOfEquiv_trans {A : Type u} {B : Type u} {C : Type u} [CommGroup A] [CommGroup B] [CommGroup C] (e : A ≃* B) (d : B ≃* C) (n : ℤ) : MulEquiv.trans (QuotientGroup.equivQuotientZPowOfEquiv e n) (QuotientGroup.equivQuotientZPowOfEquiv d n) = QuotientGroup.equivQuotientZPowOfEquiv (MulEquiv.trans e d) n

noncomputable def QuotientAddGroup.quotientInfEquivSumNormalQuotient {G : Type u} [AddGroup G] (H : AddSubgroup G) (N : AddSubgroup G) [AddSubgroup.Normal N] : { x // x ∈ H } ⧸ AddSubgroup.addSubgroupOf N H ≃+ { x // x ∈ H ⊔ N } ⧸ AddSubgroup.addSubgroupOf N (H ⊔ N)

The second isomorphism theorem: given two subgroups H and N of a group G, where N is normal, defines an isomorphism between H/(H ∩ N) and (H + N)/N

Equations

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

theorem QuotientAddGroup.quotientInfEquivSumNormalQuotient.proof_2 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (N : AddSubgroup G) : H ≤ H ⊔ N

theorem QuotientAddGroup.quotientInfEquivSumNormalQuotient.proof_3 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (N : AddSubgroup G) [AddSubgroup.Normal N] (x : { x // x ∈ H ⊔ N } ⧸ AddSubgroup.addSubgroupOf N (H ⊔ N)) : ∃ a, ↑(AddMonoidHom.comp (QuotientAddGroup.mk' (AddSubgroup.addSubgroupOf N (H ⊔ N))) (AddSubgroup.inclusion (_ : H ≤ H ⊔ N))) a = x

theorem QuotientAddGroup.quotientInfEquivSumNormalQuotient.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (N : AddSubgroup G) [AddSubgroup.Normal N] : AddSubgroup.Normal (AddSubgroup.addSubgroupOf N (H ⊔ N))

noncomputable def QuotientGroup.quotientInfEquivProdNormalQuotient {G : Type u} [Group G] (H : Subgroup G) (N : Subgroup G) [Subgroup.Normal N] : { x // x ∈ H } ⧸ Subgroup.subgroupOf N H ≃* { x // x ∈ H ⊔ N } ⧸ Subgroup.subgroupOf N (H ⊔ N)

Noether's second isomorphism theorem: given two subgroups H and N of a group G, where N is normal, defines an isomorphism between H/(H ∩ N) and (HN)/N.

Equations

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

instance QuotientAddGroup.map_normal {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (M : AddSubgroup G) [nM : AddSubgroup.Normal M] : AddSubgroup.Normal (AddSubgroup.map (QuotientAddGroup.mk' N) M)

Equations

• @QuotientAddGroup.map_normal = @QuotientAddGroup.map_normal.proof_1

theorem QuotientAddGroup.map_normal.proof_1 {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (M : AddSubgroup G) [nM : AddSubgroup.Normal M] : AddSubgroup.Normal (AddSubgroup.map (QuotientAddGroup.mk' N) M)

instance QuotientGroup.map_normal {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] (M : Subgroup G) [nM : Subgroup.Normal M] : Subgroup.Normal (Subgroup.map (QuotientGroup.mk' N) M)

Equations

• @QuotientGroup.map_normal = @QuotientGroup.map_normal.proof_1

def QuotientAddGroup.quotientQuotientEquivQuotientAux {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (M : AddSubgroup G) [nM : AddSubgroup.Normal M] (h : N ≤ M) : (G ⧸ N) ⧸ AddSubgroup.map (QuotientAddGroup.mk' N) M →+ G ⧸ M

The map from the third isomorphism theorem for additive groups: (A / N) / (M / N) → A / M.

Equations

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

theorem QuotientAddGroup.quotientQuotientEquivQuotientAux.proof_1 {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (M : AddSubgroup G) [nM : AddSubgroup.Normal M] (h : N ≤ M) : ∀ ⦃x : G ⧸ N⦄, x ∈ AddSubgroup.map (QuotientAddGroup.mk' N) M → x ∈ AddMonoidHom.ker (QuotientAddGroup.map N M (AddMonoidHom.id G) h)

def QuotientGroup.quotientQuotientEquivQuotientAux {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] (M : Subgroup G) [nM : Subgroup.Normal M] (h : N ≤ M) : (G ⧸ N) ⧸ Subgroup.map (QuotientGroup.mk' N) M →* G ⧸ M

The map from the third isomorphism theorem for groups: (G / N) / (M / N) → G / M.

Equations

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

@[simp]

theorem QuotientAddGroup.quotientQuotientEquivQuotientAux_mk {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (M : AddSubgroup G) [nM : AddSubgroup.Normal M] (h : N ≤ M) (x : G ⧸ N) : ↑(QuotientAddGroup.quotientQuotientEquivQuotientAux N M h) ↑x = ↑(QuotientAddGroup.map N M (AddMonoidHom.id G) h) x

@[simp]

theorem QuotientGroup.quotientQuotientEquivQuotientAux_mk {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] (M : Subgroup G) [nM : Subgroup.Normal M] (h : N ≤ M) (x : G ⧸ N) : ↑(QuotientGroup.quotientQuotientEquivQuotientAux N M h) ↑x = ↑(QuotientGroup.map N M (MonoidHom.id G) h) x

theorem QuotientAddGroup.quotientQuotientEquivQuotientAux_mk_mk {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (M : AddSubgroup G) [nM : AddSubgroup.Normal M] (h : N ≤ M) (x : G) : ↑(QuotientAddGroup.quotientQuotientEquivQuotientAux N M h) ↑↑x = ↑x

theorem QuotientGroup.quotientQuotientEquivQuotientAux_mk_mk {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] (M : Subgroup G) [nM : Subgroup.Normal M] (h : N ≤ M) (x : G) : ↑(QuotientGroup.quotientQuotientEquivQuotientAux N M h) ↑↑x = ↑x

theorem QuotientAddGroup.quotientQuotientEquivQuotient.proof_1 {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (M : AddSubgroup G) : M ≤ AddSubgroup.comap (QuotientAddGroup.mk' N) (AddSubgroup.map (QuotientAddGroup.mk' N) M)

theorem QuotientAddGroup.quotientQuotientEquivQuotient.proof_3 {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (M : AddSubgroup G) [nM : AddSubgroup.Normal M] (h : N ≤ M) : AddMonoidHom.comp (QuotientAddGroup.quotientQuotientEquivQuotientAux N M h) (QuotientAddGroup.map M (AddSubgroup.map (QuotientAddGroup.mk' N) M) (QuotientAddGroup.mk' N) (_ : M ≤ AddSubgroup.comap (QuotientAddGroup.mk' N) (AddSubgroup.map (QuotientAddGroup.mk' N) M))) = AddMonoidHom.id (G ⧸ M)

theorem QuotientAddGroup.quotientQuotientEquivQuotient.proof_2 {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (M : AddSubgroup G) [nM : AddSubgroup.Normal M] (h : N ≤ M) : AddMonoidHom.comp (QuotientAddGroup.map M (AddSubgroup.map (QuotientAddGroup.mk' N) M) (QuotientAddGroup.mk' N) (_ : M ≤ AddSubgroup.comap (QuotientAddGroup.mk' N) (AddSubgroup.map (QuotientAddGroup.mk' N) M))) (QuotientAddGroup.quotientQuotientEquivQuotientAux N M h) = AddMonoidHom.id ((G ⧸ N) ⧸ AddSubgroup.map (QuotientAddGroup.mk' N) M)

def QuotientAddGroup.quotientQuotientEquivQuotient {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : AddSubgroup.Normal N] (M : AddSubgroup G) [nM : AddSubgroup.Normal M] (h : N ≤ M) : (G ⧸ N) ⧸ AddSubgroup.map (QuotientAddGroup.mk' N) M ≃+ G ⧸ M

Noether's third isomorphism theorem for additive groups: (A / N) / (M / N) ≃+ A / M.

Equations

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

def QuotientGroup.quotientQuotientEquivQuotient {G : Type u} [Group G] (N : Subgroup G) [nN : Subgroup.Normal N] (M : Subgroup G) [nM : Subgroup.Normal M] (h : N ≤ M) : (G ⧸ N) ⧸ Subgroup.map (QuotientGroup.mk' N) M ≃* G ⧸ M

Noether's third isomorphism theorem for groups: (G / N) / (M / N) ≃* G / M.

Equations

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

theorem QuotientAddGroup.subsingleton_quotient_top {G : Type u} [AddGroup G] : Subsingleton (G ⧸ ⊤)

theorem QuotientGroup.subsingleton_quotient_top {G : Type u} [Group G] : Subsingleton (G ⧸ ⊤)

theorem QuotientAddGroup.addSubgroup_eq_top_of_subsingleton {G : Type u} [AddGroup G] (H : AddSubgroup G) (h : Subsingleton (G ⧸ H)) : H = ⊤

If the quotient by an additive subgroup gives a singleton then the additive subgroup is the whole additive group.

theorem QuotientGroup.subgroup_eq_top_of_subsingleton {G : Type u} [Group G] (H : Subgroup G) (h : Subsingleton (G ⧸ H)) : H = ⊤

If the quotient by a subgroup gives a singleton then the subgroup is the whole group.

theorem QuotientAddGroup.comap_comap_center {G : Type u} [AddGroup G] {H₁ : AddSubgroup G} [AddSubgroup.Normal H₁] {H₂ : AddSubgroup (G ⧸ H₁)} [AddSubgroup.Normal H₂] : AddSubgroup.comap (QuotientAddGroup.mk' H₁) (AddSubgroup.comap (QuotientAddGroup.mk' H₂) (AddSubgroup.center ((G ⧸ H₁) ⧸ H₂))) = AddSubgroup.comap (QuotientAddGroup.mk' (AddSubgroup.comap (QuotientAddGroup.mk' H₁) H₂)) (AddSubgroup.center (G ⧸ AddSubgroup.comap (QuotientAddGroup.mk' H₁) H₂))

theorem QuotientGroup.comap_comap_center {G : Type u} [Group G] {H₁ : Subgroup G} [Subgroup.Normal H₁] {H₂ : Subgroup (G ⧸ H₁)} [Subgroup.Normal H₂] : Subgroup.comap (QuotientGroup.mk' H₁) (Subgroup.comap (QuotientGroup.mk' H₂) (Subgroup.center ((G ⧸ H₁) ⧸ H₂))) = Subgroup.comap (QuotientGroup.mk' (Subgroup.comap (QuotientGroup.mk' H₁) H₂)) (Subgroup.center (G ⧸ Subgroup.comap (QuotientGroup.mk' H₁) H₂))

theorem AddGroup.fintypeOfKerLeRange.proof_2 {F : Type u_1} {G : Type u_1} {H : Type u_1} [AddGroup F] [AddGroup G] [AddGroup H] (f : F →+ G) (g : G →+ H) (h : AddMonoidHom.ker g ≤ AddMonoidHom.range f) : Function.Injective ↑(AddSubgroup.inclusion h)

noncomputable def AddGroup.fintypeOfKerLeRange {F : Type u} {G : Type u} {H : Type u} [AddGroup F] [AddGroup G] [AddGroup H] [Fintype F] [Fintype H] (f : F →+ G) (g : G →+ H) (h : AddMonoidHom.ker g ≤ AddMonoidHom.range f) : Fintype G

If F and H are finite such that ker(G →+ H) ≤ im(F →+ G), then G is finite.

Equations

• AddGroup.fintypeOfKerLeRange f g h = Fintype.ofEquiv ((G ⧸ AddMonoidHom.ker g) × { x // x ∈ AddMonoidHom.ker g }) AddSubgroup.addGroupEquivQuotientProdAddSubgroup.symm

theorem AddGroup.fintypeOfKerLeRange.proof_1 {G : Type u_1} {H : Type u_1} [AddGroup G] [AddGroup H] (g : G →+ H) : AddSubgroup.Normal (AddMonoidHom.ker g)

noncomputable def Group.fintypeOfKerLeRange {F : Type u} {G : Type u} {H : Type u} [Group F] [Group G] [Group H] [Fintype F] [Fintype H] (f : F →* G) (g : G →* H) (h : MonoidHom.ker g ≤ MonoidHom.range f) : Fintype G

If F and H are finite such that ker(G →* H) ≤ im(F →* G), then G is finite.

Equations

• Group.fintypeOfKerLeRange f g h = Fintype.ofEquiv ((G ⧸ MonoidHom.ker g) × { x // x ∈ MonoidHom.ker g }) Subgroup.groupEquivQuotientProdSubgroup.symm

theorem AddGroup.fintypeOfKerEqRange.proof_1 {F : Type u_1} {G : Type u_1} {H : Type u_1} [AddGroup F] [AddGroup G] [AddGroup H] (f : F →+ G) (g : G →+ H) (h : AddMonoidHom.ker g = AddMonoidHom.range f) : AddMonoidHom.ker g ≤ AddMonoidHom.range f

noncomputable def AddGroup.fintypeOfKerEqRange {F : Type u} {G : Type u} {H : Type u} [AddGroup F] [AddGroup G] [AddGroup H] [Fintype F] [Fintype H] (f : F →+ G) (g : G →+ H) (h : AddMonoidHom.ker g = AddMonoidHom.range f) : Fintype G

If F and H are finite such that ker(G →+ H) = im(F →+ G), then G is finite.

Equations

• AddGroup.fintypeOfKerEqRange f g h = AddGroup.fintypeOfKerLeRange f g (_ : AddMonoidHom.ker g ≤ AddMonoidHom.range f)

noncomputable def Group.fintypeOfKerEqRange {F : Type u} {G : Type u} {H : Type u} [Group F] [Group G] [Group H] [Fintype F] [Fintype H] (f : F →* G) (g : G →* H) (h : MonoidHom.ker g = MonoidHom.range f) : Fintype G

If F and H are finite such that ker(G →* H) = im(F →* G), then G is finite.

Equations

• Group.fintypeOfKerEqRange f g h = Group.fintypeOfKerLeRange f g (_ : MonoidHom.ker g ≤ MonoidHom.range f)

theorem AddGroup.fintypeOfKerOfCodom.proof_1 {G : Type u_1} {H : Type u_1} [AddGroup G] [AddGroup H] (g : G →+ H) : AddMonoidHom.ker g ≤ ⊤

noncomputable def AddGroup.fintypeOfKerOfCodom {G : Type u} {H : Type u} [AddGroup G] [AddGroup H] [Fintype H] (g : G →+ H) [Fintype { x // x ∈ AddMonoidHom.ker g }] : Fintype G

If ker(G →+ H) and H are finite, then G is finite.

Equations

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

theorem AddGroup.fintypeOfKerOfCodom.proof_2 {G : Type u_1} {H : Type u_1} [AddGroup G] [AddGroup H] (g : G →+ H) (x : G) (hx : x ∈ AddMonoidHom.ker g) : ∃ y, ↑(AddMonoidHom.comp (AddEquiv.toAddMonoidHom AddSubgroup.topEquiv) (AddSubgroup.inclusion (_ : AddMonoidHom.ker g ≤ ⊤))) y = x

noncomputable def Group.fintypeOfKerOfCodom {G : Type u} {H : Type u} [Group G] [Group H] [Fintype H] (g : G →* H) [Fintype { x // x ∈ MonoidHom.ker g }] : Fintype G

If ker(G →* H) and H are finite, then G is finite.

Equations

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

noncomputable def AddGroup.fintypeOfDomOfCoker {F : Type u} {G : Type u} [AddGroup F] [AddGroup G] [Fintype F] (f : F →+ G) [AddSubgroup.Normal (AddMonoidHom.range f)] [Fintype (G ⧸ AddMonoidHom.range f)] : Fintype G

If F and coker(F →+ G) are finite, then G is finite.

Equations

• AddGroup.fintypeOfDomOfCoker f = AddGroup.fintypeOfKerLeRange f (QuotientAddGroup.mk' (AddMonoidHom.range f)) (_ : ∀ (x : G), ↑x = 0 → x ∈ AddMonoidHom.range f)

theorem AddGroup.fintypeOfDomOfCoker.proof_1 {F : Type u_1} {G : Type u_1} [AddGroup F] [AddGroup G] (f : F →+ G) [AddSubgroup.Normal (AddMonoidHom.range f)] (x : G) : ↑x = 0 → x ∈ AddMonoidHom.range f

noncomputable def Group.fintypeOfDomOfCoker {F : Type u} {G : Type u} [Group F] [Group G] [Fintype F] (f : F →* G) [Subgroup.Normal (MonoidHom.range f)] [Fintype (G ⧸ MonoidHom.range f)] : Fintype G

If F and coker(F →* G) are finite, then G is finite.

Equations

• Group.fintypeOfDomOfCoker f = Group.fintypeOfKerLeRange f (QuotientGroup.mk' (MonoidHom.range f)) (_ : ∀ (x : G), ↑x = 1 → x ∈ MonoidHom.range f)