hom_ext — Mathlib

English

A standard hom-ext lemma in RanIsSheafOfIsCocontinuous: two morphisms are equal if they agree on a generating family.

Русский

Стандартная лемма hom-ext: два морфизма равны, если они совпадают на порождении.

LaTeX

$$$\\forall f,g:\\; f = g \\text{ iff } \\forall i \\text{ (i ∈ S.Arrow)}, f \\cdot i = g \\cdot i$$$

Lean4

theorem hom_ext {W : A} {f g : W ⟶ R.obj (op X)} (h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op) : f = g :=
  by
  apply (hR (op X)).hom_ext
  intro j
  apply hF.hom_ext ⟨_, G.cover_lift J K (K.pullback_stable j.hom.unop S.2)⟩
  intro ⟨W, i, hi⟩
  have eq := h (GrothendieckTopology.Cover.Arrow.mk _ (G.map i ≫ j.hom.unop) hi)
  dsimp at eq ⊢
  simp only [Category.assoc, ← NatTrans.naturality, Functor.comp_map, ← Functor.map_comp_assoc, Functor.op_map,
    Quiver.Hom.unop_op]
  rw [reassoc_of% eq]

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