comap_map_eq — Mathlib

English

For a subgroup H of G, the comap of the image equals H joined with the kernel: comap f (map f H) = H ⊔ ker f.

Русский

Обратное образа отображения f отобразится на H, объединенную с ядром: comap f (map f H) = H ⊔ ker f.

LaTeX

$$$\mathrm{comap}_f(\mathrm{map}_f H) = H \sqcup \ker f$$$

Lean4

@[to_additive]
theorem comap_map_eq (H : Subgroup G) : comap f (map f H) = H ⊔ f.ker :=
  by
  refine le_antisymm ?_ (sup_le (le_comap_map _ _) (ker_le_comap _ _))
  intro x hx; simp only [mem_map, mem_comap] at hx
  rcases hx with ⟨y, hy, hy'⟩
  rw [← mul_inv_cancel_left y x]
  exact mul_mem_sup hy (by simp [mem_ker, hy'])

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