instIsLocallyInjectiveHomObjForgetTypeImageι

Mathlib.CategoryTheory.Sites.LocallyInjective

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Sheaf.instIsLocallyInjectiveHomObjForgetTypeImageι

English

If each component φ.app X is injective, then φ is a monomorphism.

Русский

Если каждый компонент φ.app X инъективен, то φ мономорфизм.

LaTeX

$$Mono φ$$

Lean4

instance {F G : Sheaf J (Type w)} (f : F ⟶ G) : IsLocallyInjective (Sheaf.imageι f) :=
  by
  dsimp [Sheaf.imageι]
  infer_instance

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru