limMap_mono — Mathlib

English

Let F,G : J → C be functors with limits, and α: F ⟶ G a natural transformation such that each component α.app j is mono. Then the induced morphism limMap α : lim F ⟶ lim G is mono.

Русский

Пусть F,G : J → C — функторы, у которых существуют пределы, и α: F ⟶ G — натурное преобразование, для которого каждый компонент α.app j является монообразным. Тогда полученный переход limMap α: lim F ⟶ lim G монообразен.

LaTeX

$$$\\operatorname{Mono}(\\limMap \\alpha)$$$

Lean4

instance limMap_mono {F G : J ⥤ C} [HasLimit F] [HasLimit G] (α : F ⟶ G) [∀ j, Mono (α.app j)] : Mono (limMap α) :=
  ⟨fun {Z} u v h => limit.hom_ext fun j => (cancel_mono (α.app j)).1 <| by simpa using h =≫ limit.π _ j⟩

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