frattini_le_comap_frattini_of_surjective

English

If φ: G → H is surjective, then Frattini(G) is contained in the preimage (comap) of Frattini(H).

Русский

Если φ: G → H сюрьективно, то Frattini(G) ⊆ φ^{-1}(Frattini(H)).

LaTeX

$$$\\operatorname{frattini}(G) \\le \\operatorname{comap}_{\\phi}(\\operatorname{frattini}(H))$$$

Lean4

theorem frattini_le_comap_frattini_of_surjective (hφ : Function.Surjective φ) : frattini G ≤ (frattini H).comap φ :=
  by
  simp_rw [frattini, Order.radical, comap_iInf, le_iInf_iff]
  intro M hM
  apply biInf_le
  exact isCoatom_comap_of_surjective hφ hM

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