hom_ext' — Mathlib

English

In the relative representability setting, F.map (hf.lift i h hi) ≫ hf.fst g = i, i.e., the lift recovers i on the left leg.

Русский

В контексте относительного представления отображение F.map (hf.lift i h hi) ≫ hf.fst g = i восстанавливает i по левой ноге.

LaTeX

$$$ F.map (hf.lift i h hi) \\;\\circ\\; hf.fst g = i $$$

Lean4

/-- In the case of a representable morphism `f' : F.obj Y ⟶ G`, whose codomain lies
in the image of `F`, we get that two morphism `a b : Z ⟶ hf.pullback g` are equal if
* Their compositions (in `C`) with `hf'.snd g : hf.pullback  ⟶ X` are equal.
* Their compositions (in `C`) with `hf'.fst' g : hf.pullback  ⟶ Y` are equal. -/
@[ext]
theorem hom_ext' [Full F] [Faithful F] {c : C} {a b : c ⟶ hf'.pullback g} (h₁ : a ≫ hf'.fst' g = b ≫ hf'.fst' g)
    (h₂ : a ≫ hf'.snd g = b ≫ hf'.snd g) : a = b :=
  hf'.hom_ext (by simpa [map_fst'] using F.congr_map h₁) h₂

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