widePullback_ext' — Mathlib

English

In a concrete category, two elements of a wide pullback are equal if all corresponding base and projection components agree.

Русский

В конкретной категории две точки в широком вытянутом пределе равны, если совпадают их основанные части и все проекции.

LaTeX

$$$x=y \\;\\Rightarrow\\; (base\_f\\, x)=(base\_f\\, y)\\;\\land\\; \\forall j, \\pi\_f j x = \\pi\_f j y$; conversely, equality of these components implies $x=y$.$$

Lean4

theorem widePullback_ext' {B : C} {ι : Type w} [Nonempty ι] {X : ι → C} (f : ∀ j : ι, X j ⟶ B)
    [HasWidePullback.{w} B X f] [PreservesLimit (wideCospan B X f) (forget C)] (x y : ToType (widePullback B X f))
    (h : ∀ j, π f j x = π f j y) : x = y :=
  by
  apply Concrete.widePullback_ext _ _ _ _ h
  inhabit ι
  simp only [← π_arrow f default, ConcreteCategory.comp_apply, h]

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