isLocalHom_of_comp — Mathlib

English

If the composition g ∘ f is a local homomorphism, then f is a local homomorphism.

Русский

Если композиция g ∘ f — локальный гомоморфизм, то и f — локальный гомоморфизм.

LaTeX

$$$\\text{IsLocalHom}(g \\circ f) \\Rightarrow \\text{IsLocalHom}(f)$$$

Lean4

theorem isLocalHom_of_comp (f : R →* S) (g : S →* T) [IsLocalHom (g.comp f)] : IsLocalHom f :=
  ⟨fun _ ha => (isUnit_map_iff (g.comp f) _).mp (ha.map g)⟩

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