hom_ext_ofArrows — Mathlib

English

A version of hom_ext specialized to arrows from a family of arrows f_i : X_i → S, showing equality when all arrows agree after mapping under P.

Русский

Специализированная версия hom_ext для стрелок вида f_i : X_i → S, равенство следует из совпадения после отображений P.

LaTeX

$$$\\forall f: \\text{Arrows}, e_1 \\circ f = e_2 \\circ f$$$

Lean4

theorem hom_ext_ofArrows {P : Cᵒᵖ ⥤ A} (hP : Presheaf.IsSheaf J P) {I : Type*} {S : C} {X : I → C} (f : ∀ i, X i ⟶ S)
    (hf : Sieve.ofArrows _ f ∈ J S) {E : A} {x y : E ⟶ P.obj (op S)}
    (h : ∀ i, x ≫ P.map (f i).op = y ≫ P.map (f i).op) : x = y :=
  by
  apply hP.hom_ext ⟨_, hf⟩
  rintro ⟨Z, _, _, g, _, ⟨i⟩, rfl⟩
  dsimp
  rw [P.map_comp, reassoc_of% (h i)]

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