isSeparating_proj_preimage — Mathlib

English

If a set 𝒢 is detecting in C, then P ≤ Q and (∀ G ∈ 𝒢, ∀ {f: G ⟶ X}, P.Factors f ↔ Q.Factors f) implies P = Q.

Русский

Если 𝒢 — обнаруживающий набор в C, тогда P ≤ Q и (∀ G ∈ 𝒢, ∀ {f: G ⟶ X}, P.Factors f ↔ Q.Factors f) тогда P = Q.

LaTeX

$$$$\forall {G} \in 𝒢,\forall f:G\to X,\ P.Factors f \iff Q.Factors f\quad\Rightarrow\quad P = Q.$$$$

Lean4

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

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