goursat — Mathlib

English

For an arbitrary subgroup I ≤ G × H, there exist subgroups G' ≤ G, H' ≤ H and normal subgroups M ⊴ G', N ⊴ H' such that M × N ≤ I and the image of I in G'/M × H'/N is the graph of an isomorphism G'/M ≃ H'/N.

Русский

Для произвольной подгруппы I ≤ G × H существуют подгруппы G' ≤ G, H' ≤ H и нормальные подгруппы M ⊴ G', N ⊴ H' такие, что M × N ≤ I и образ I в G'/M × H'/N является графиком изоморфизма G'/M ≃ H'/N.

LaTeX

$$$$\\exists (G' \\le G) (H' \\le H) (M \\lhd G') (N \\lhd H')(e: G'/M \\cong H'/N), I = (e.graph.coneap (G'.subtype.prodMap H'.subtype)).$$$$

Lean4

/-- **Goursat's lemma** for an arbitrary subgroup.

If `I` is a subgroup of `G × H`, then there exist subgroups `G' ≤ G`, `H' ≤ H` and normal subgroups
`M ⊴ G'` and `N ⊴ H'` such that `M × N ≤ I` and the image of `I` in `G' ⧸ M × H' ⧸ N` is the graph
of an isomorphism `G' ⧸ M ≃ H' ⧸ N`. -/
@[to_additive /-- **Goursat's lemma** for an arbitrary subgroup.

    If `I` is a subgroup of `G × H`, then there exist subgroups `G' ≤ G`, `H' ≤ H` and normal subgroups
    `M ≤ G'` and `N ≤ H'` such that `M × N ≤ I` and the image of `I` in `G' ⧸ M × H' ⧸ N` is the graph
    of an isomorphism `G ⧸ G' ≃ H ⧸ H'`. -/
    ]
theorem goursat :
    ∃ (G' : Subgroup G) (H' : Subgroup H) (M : Subgroup G') (N : Subgroup H') (_ : M.Normal) (_ : N.Normal) (e :
      G' ⧸ M ≃* H' ⧸ N),
      I =
        (e.toMonoidHom.graph.comap <| (QuotientGroup.mk' M).prodMap (QuotientGroup.mk' N)).map
          (G'.subtype.prodMap H'.subtype) :=
  by
  let G' := I.map (MonoidHom.fst ..)
  let H' := I.map (MonoidHom.snd ..)
  let P : I →* G' := (MonoidHom.fst ..).subgroupMap I
  let Q : I →* H' := (MonoidHom.snd ..).subgroupMap I
  let I' : Subgroup (G' × H') := (P.prod Q).range
  have hI₁' : Surjective (Prod.fst ∘ I'.subtype) :=
    by
    simp only [← MonoidHom.coe_fst, ← MonoidHom.coe_comp, ← MonoidHom.range_eq_top, MonoidHom.range_comp,
      Subgroup.range_subtype, I']
    simp only [← MonoidHom.range_comp, MonoidHom.fst_comp_prod, MonoidHom.range_eq_top]
    exact (MonoidHom.fst ..).subgroupMap_surjective I
  have hI₂' : Surjective (Prod.snd ∘ I'.subtype) :=
    by
    simp only [← MonoidHom.coe_snd, ← MonoidHom.coe_comp, ← MonoidHom.range_eq_top, MonoidHom.range_comp,
      Subgroup.range_subtype, I']
    simp only [← MonoidHom.range_comp, MonoidHom.range_eq_top]
    exact (MonoidHom.snd ..).subgroupMap_surjective I
  have := normal_goursatFst hI₁'
  have := normal_goursatSnd hI₂'
  obtain ⟨e, he⟩ := goursat_surjective hI₁' hI₂'
  refine
    ⟨I.map (MonoidHom.fst ..), I.map (MonoidHom.snd ..), I'.goursatFst, I'.goursatSnd, inferInstance, inferInstance, e,
      ?_⟩
  rw [← he]
  simp only [MonoidHom.range_comp, Subgroup.range_subtype, I']
  rw [comap_map_eq_self]
  · ext ⟨g, h⟩
    constructor
    · intro hgh
      simpa only [G', H', mem_map, MonoidHom.mem_range, MonoidHom.prod_apply, Subtype.exists, Prod.exists,
        MonoidHom.coe_prodMap, coe_subtype, Prod.mk.injEq, Prod.map_apply, MonoidHom.coe_snd, exists_eq_right,
        exists_and_right, exists_eq_right_right, MonoidHom.coe_fst] using ⟨⟨h, hgh⟩, ⟨g, hgh⟩, g, h, hgh, ⟨rfl, rfl⟩⟩
    · simp only [G', H', mem_map, MonoidHom.mem_range, MonoidHom.prod_apply, Subtype.exists, Prod.exists,
        MonoidHom.coe_prodMap, coe_subtype, Prod.mk.injEq, Prod.map_apply, MonoidHom.coe_snd, exists_eq_right,
        exists_and_right, exists_eq_right_right, MonoidHom.coe_fst, forall_exists_index, and_imp]
      rintro h₁ hgh₁ g₁ hg₁h g₂ h₂ hg₂h₂ hP hQ
      simp only [Subtype.ext_iff] at hP hQ
      rwa [← hP, ← hQ]
  · convert goursatFst_prod_goursatSnd_le (P.prod Q).range
    ext ⟨g, h⟩
    simp_rw [G', H', MonoidHom.mem_ker, MonoidHom.coe_prodMap, Prod.map_apply, Subgroup.mem_prod, Prod.one_eq_mk,
      Prod.ext_iff, ← MonoidHom.mem_ker, QuotientGroup.ker_mk']

Похожие утверждения