strongEpi_map_of_strongEpi — Mathlib

English

Given an adjunction F ⊣ F' with F'.PreservesMonomorphisms and F.PreservesEpimorphisms, if f is StrongEpi in C, then F.map f is StrongEpi in D.

Русский

При наличии сопряжения F ⊣ F' и условий сохранения мономорфизмов и эпиморфизмов, если f — сильный эпиморфизм в C, тогда F.map f — сильный эпиморфизм в D.

LaTeX

$$$$ \\operatorname{StrongEpi}(f) \\Rightarrow \\operatorname{StrongEpi}(F.map\\,f). $$$$

Lean4

theorem strongEpi_map_of_strongEpi (adj : F ⊣ F') (f : A ⟶ B) [F'.PreservesMonomorphisms] [F.PreservesEpimorphisms]
    [StrongEpi f] : StrongEpi (F.map f) :=
  ⟨inferInstance, fun X Y Z => by
    intro
    rw [adj.hasLiftingProperty_iff]
    infer_instance⟩

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