isLocalHom_comp — Mathlib

English

If f: R → S and g: S → T are local homomorphisms of commutative rings, then the composition f ≫ g is a local homomorphism.

Русский

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

LaTeX

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

Lean4

@[instance]
theorem isLocalHom_comp {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) [IsLocalHom g.hom] [IsLocalHom f.hom] :
    IsLocalHom (f ≫ g).hom :=
  RingHom.isLocalHom_comp _ _

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