isLocalHom_comp — Mathlib

English

If g and f are local, then their composition g ∘ f is local.

Русский

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

LaTeX

$$$\text{IsLocalHom}(g) \land \text{IsLocalHom}(f) \Rightarrow \text{IsLocalHom}(g \circ 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)

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