ker_eq_lift_of_injective — Mathlib

English

If f has a kernel relation r and the lift is injective, then ker f = r.

Русский

Если для функции f ядро r удовлетворяет условиям инъекции лифта, то ker f = r.

LaTeX

$$$$ ker f = r. $$$$

Lean4

/-- Given a map f from α to β, the kernel of f is the unique equivalence relation on α whose
induced map from the quotient of α to β is injective. -/
theorem ker_eq_lift_of_injective {r : Setoid α} (f : α → β) (H : ∀ x y, r x y → f x = f y)
    (h : Injective (Quotient.lift f H)) : ker f = r :=
  le_antisymm (fun x y hk => Quotient.exact <| h <| show Quotient.lift f H ⟦x⟧ = Quotient.lift f H ⟦y⟧ from hk) H

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