hom_ext — Mathlib

English

A higher-arity version of hom_ext asserting equality of two arrows from E to P(X) given pointwise equality on a cover with a family of arrows.

Русский

Универсальная версия hom_ext для множественных стрелок от E к P(X) с заданной покровной семействой стрелок.

LaTeX

$$$\\forall S, e_1, e_2, (\\forall I: S.Arrow, \\cdot) \\Rightarrow e_1=e_2$$$

Lean4

theorem hom_ext {A : Type u₂} [Category.{v₂} A] {E : A} {X : C} {P : Cᵒᵖ ⥤ A} (hP : Presheaf.IsSheaf J P)
    (S : J.Cover X) (e₁ e₂ : E ⟶ P.obj (op X)) (h : ∀ I : S.Arrow, e₁ ≫ P.map I.f.op = e₂ ≫ P.map I.f.op) : e₁ = e₂ :=
  (hP _ _ S.condition).isSeparatedFor.ext fun Y f hf => h ⟨Y, f, hf⟩

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