Third isomorphism theorem

Stream: Is there code for X?

[Anne Baanen]

I can't find the third isomorphism theorem for submodules or subgroups anywhere, do we not have this yet? (I need to show that |M / S| * |S / T| = |M / T|, assuming all these cardinalities are finite.)

[Oliver Nash]

Aren't we supposed to do this from lattice theory or something using https://github.com/leanprover-community/mathlib/blob/8ba94ab79b5d75bbb562665326666ea675c8ff88/src/linear_algebra/basic.lean#L2825 ?

[Oliver Nash]

Oh wait, maybe that's the second.

[Anne Baanen]

I believe that's the second :(

[Anne Baanen]

For subgroups:

namespace quotient_group

@[simp, to_additive quotient_add_group.map_coe] lemma map_coe {G H : Type*} [group G] [group H]
  (S : subgroup G) (T : subgroup H) [hS : S.normal] [hT : T.normal] (f h) (x : G) :
  quotient_group.map S T f h ↑x = ↑(f x) :=
quotient_group.lift_mk' S _ x

@[simp, to_additive quotient_add_group.map_mk'] lemma map_mk' {G H : Type*} [group G] [group H]
  (S : subgroup G) (T : subgroup H) [hS : S.normal] [hT : T.normal] (f h) (x : G) :
  quotient_group.map S T f h (quotient_group.mk' _ x) = ↑(f x) :=
quotient_group.lift_mk' S _ x

variables {G : Type*} [group G] (S T : subgroup G) [hS : S.normal] [hT : T.normal] (h : S ≤ T)

include hS hT

@[to_additive quotient_add_group.map_normal]
instance map_normal : (T.map (quotient_group.mk' S)).normal :=
{ conj_mem := begin
    rintro _ ⟨x, hx, rfl⟩ y,
    refine induction_on' y (λ y, ⟨y * x * y⁻¹, subgroup.normal.conj_mem hT x hx y, _⟩),
    simp only [mk'_apply, coe_mul, coe_inv]
  end }

/-- The map from the isomorphism theorem for groups: `(G / S) / (T / S) → G / T`. -/
@[to_additive quotient_add_group.quotient_quotient_equiv_quotient_aux]
def quotient_quotient_equiv_quotient_aux :
  quotient (T.map (mk' S)) →* quotient T :=
lift (T.map (mk' S))
  (map S T (monoid_hom.id G) h)
  (by { rintro _ ⟨x, hx, rfl⟩, rw map_mk' S T _ _ x,
        exact (quotient_group.eq_one_iff _).mpr hx })

@[simp, to_additive quotient_add_group.quotient_quotient_equiv_quotient_aux_coe]
lemma quotient_quotient_equiv_quotient_aux_coe (x : quotient_group.quotient S) :
  quotient_quotient_equiv_quotient_aux S T h x = quotient_group.map S T (monoid_hom.id G) h x :=
quotient_group.lift_mk' _ _ x

@[to_additive quotient_add_group.quotient_quotient_equiv_quotient_aux_coe_coe]
lemma quotient_quotient_equiv_quotient_aux_coe_coe (x : G) :
  quotient_quotient_equiv_quotient_aux S T h (x : quotient_group.quotient S) =
    x :=
quotient_group.lift_mk' _ _ x

/-- Third isomorphism theorem for groups: `(G / S) / (T / S) ≃ G / T`. -/
@[to_additive quotient_add_group.quotient_quotient_equiv_quotient]
def quotient_quotient_equiv_quotient :
  quotient_group.quotient (T.map (quotient_group.mk' S)) ≃* quotient_group.quotient T :=
{ to_fun := quotient_quotient_equiv_quotient_aux S T h,
  inv_fun := quotient_group.map _ _ (quotient_group.mk' S) (subgroup.le_comap_map _ _),
  left_inv := λ x, quotient_group.induction_on' x $ λ x, quotient_group.induction_on' x $
    λ x, by rw [quotient_quotient_equiv_quotient_aux_coe_coe, quotient_group.map_coe,
                quotient_group.mk'_apply],
  right_inv := λ x, quotient_group.induction_on' x $ λ x,
    by rw [quotient_group.map_coe, quotient_group.mk'_apply, quotient_quotient_equiv_quotient_aux_coe_coe],
  map_mul' := monoid_hom.map_mul _ }

end quotient_group

[Anne Baanen]

For submodules, the simp lemmas seem to work a lot better:

namespace submodule

variables {R M : Type*} [ring R] [add_comm_group M] [module R M] (S T : submodule R M) (h : S ≤ T)

/-- The map from the third isomorphism theorem for modules: `(M / S) / (T / S) → M / T`. -/
def quotient_quotient_equiv_quotient_aux :
  quotient (T.map S.mkq) →ₗ[R] quotient T :=
liftq _ (mapq S T linear_map.id h)
  (by { rintro _ ⟨x, hx, rfl⟩, rw [linear_map.mem_ker, mkq_apply, mapq_apply],
        exact (quotient.mk_eq_zero _).mpr hx })

@[simp] lemma quotient_quotient_equiv_quotient_aux_mk (x : S.quotient) :
  quotient_quotient_equiv_quotient_aux S T h (quotient.mk x) = mapq S T linear_map.id h x :=
liftq_apply _ _ _

/-- Third isomorphism theorem for modules: `(M / S) / (T / S) ≃ M / T`. -/
def quotient_quotient_equiv_quotient :
  quotient (T.map S.mkq) ≃ₗ[R] quotient T :=
{ to_fun := quotient_quotient_equiv_quotient_aux S T h,
  inv_fun := mapq _ _ (mkq S) (le_comap_map _ _),
  left_inv := λ x, quotient.induction_on' x $ λ x, quotient.induction_on' x $ λ x, by simp,
  right_inv := λ x, quotient.induction_on' x $ λ x, by simp,
  .. quotient_quotient_equiv_quotient_aux S T h }


end submodule

[Anne Baanen]

#8203