ker_le_range_iff — Mathlib

English

For monoid hom f and g with g.range normal, g.ker ≤ f.range iff the composition (mk' f.range) ∘ g.ker.subtype equals 1.

Русский

Пусть f и g — гомоморфизмы, нормальная нормализация образа g; тогда g.ker ≤ f.range эквивалентно тому, что композиция равна единице: (mk' f.range) ∘ g.ker.subtype = 1.

LaTeX

$$$g.ker \\le f.range \\iff (mk' f.range) \\circ g.ker.subtype = 1$$$

Lean4

@[to_additive]
theorem ker_le_range_iff {I : Type w} [MulOneClass I] (f : G →* H) [f.range.Normal] (g : H →* I) :
    g.ker ≤ f.range ↔ (mk' f.range).comp g.ker.subtype = 1 :=
  ⟨fun h => MonoidHom.ext fun ⟨_, hx⟩ => (eq_one_iff _).mpr <| h hx, fun h x hx =>
    (eq_one_iff _).mp <| by exact DFunLike.congr_fun h ⟨x, hx⟩⟩

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