isLocalHom_comp — Mathlib

English

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

Русский

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

LaTeX

$$$[IsLocalHom](g \\circ f) \\Rightarrow IsLocalHom(f)$$$

Lean4

@[instance]
theorem isLocalHom_comp (g : S →* T) (f : R →* S) [IsLocalHom g] [IsLocalHom f] : IsLocalHom (g.comp f) where
  map_nonunit
    a :=
    IsLocalHom.map_nonunit a ∘
      IsLocalHom.map_nonunit (f := g)
        (f a)
          -- see note [lower instance priority]

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