isSeparatedFor_singleton — Mathlib

English

For X, Y and a morphism f: X → Y, IsSeparatedFor P (singleton f) is equivalent to injectivity of P.map f^op.

Русский

Для стрелки f: X → Y, IsSeparatedFor P (singleton f) эквивалентно инъективности отображения P.map f^op.

LaTeX

$$$\mathrm{IsSeparatedFor}(P, \{f\}) \iff \mathrm{Function.Injective}(P.map f^op)$$$

Lean4

@[simp]
theorem isSeparatedFor_singleton {X Y : C} {f : X ⟶ Y} :
    Presieve.IsSeparatedFor P (.singleton f) ↔ Function.Injective (P.map f.op) :=
  by
  rw [IsSeparatedFor, Equiv.forall_congr_left (Presieve.FamilyOfElements.singletonEquiv P f)]
  simp_rw [FamilyOfElements.isAmalgamation_singleton_iff, FamilyOfElements.singletonEquiv_symm_apply_self,
    Function.Injective]
  aesop

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