isCoseparating_proj_preimage — Mathlib

English

IsSeparator G is equivalent to the property that, for all X,Y and arrows f,g: X ⟶ Y, if h ≔ the precomposition with G yields equality h ≫ f = h ≫ g for all h: G ⟶ X, then f = g.

Русский

IsSeparator G эквивалентно свойству: для любых X,Y и стрелок f,g: X ⟶ Y, если для всех h: G ⟶ X выполняется h ≫ f = h ≫ g, то f = g.

LaTeX

$$$$\text{IsSeparator}(G) \iff \forall X,Y:\, \forall f,g:X\to Y,\ (\forall h:G\to X,\ h\to f = h\to g) \Rightarrow f=g.$$$$

Lean4

theorem isCoseparating_proj_preimage {𝒢 : Set C} (h𝒢 : IsCoseparating 𝒢) : IsCoseparating ((proj S T).obj ⁻¹' 𝒢) :=
  by
  refine fun X Y f g hfg => ext _ _ (h𝒢 _ _ fun G hG h => ?_)
  exact congr_arg CommaMorphism.right (hfg (mk (Y.hom ≫ T.map h)) hG (homMk h rfl))

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