range_le_equalizer_iff — Mathlib

English

For a φ : G ⟶ A.toPresheaf, range(φ ≫ A.ι) ≤ equalizer f g iff φ ≫ f = φ ≫ g.

Русский

Для φ: G ⟶ A.toPresheaf, выполняется равенство: range(φ ≫ A.ι) ≤ равнитель f g тогда и только тогда, когда φ ≫ f = φ ≫ g.

LaTeX

$$$\\operatorname{range}(\\phi \\gg A.\\iota) \\le \\text{equalizer}(f,g) \\iff \\phi \\gg f = \\phi \\gg g$$$

Lean4

theorem range_le_equalizer_iff {G : Cᵒᵖ ⥤ Type w} (φ : G ⟶ A.toPresheaf) :
    range (φ ≫ A.ι) ≤ Subpresheaf.equalizer f g ↔ φ ≫ f = φ ≫ g :=
  by
  rw [NatTrans.ext_iff]
  simp [le_def, Set.subset_def, funext_iff, CategoryTheory.types_ext_iff]

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