map_injective_of_ker_le — Mathlib

English

The kernel of the subgroup map equals the subgroup of the kernel, i.e., (f.subgroupMap H) .ker = f.ker .subgroupOf H.

Русский

Ядро отображения подгрупп равно подгруппе ядра: (f.subgroupMap H).ker = f.ker .subgroupOf H.

LaTeX

$$$\\ker(f.subgroupMap H) = \\ker(f)\\;\\text{subgroupOf } H$$$

Lean4

/-- Given `f(A) = f(B)`, `ker f ≤ A`, and `ker f ≤ B`, deduce that `A = B`. -/
@[to_additive /-- Given `f(A) = f(B)`, `ker f ≤ A`, and `ker f ≤ B`, deduce that `A = B`. -/
    ]
theorem map_injective_of_ker_le {H K : Subgroup G} (hH : f.ker ≤ H) (hK : f.ker ≤ K) (hf : map f H = map f K) : H = K :=
  by
  apply_fun comap f at hf
  rwa [comap_map_eq, comap_map_eq, sup_of_le_left hH, sup_of_le_left hK] at hf

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