isAmalgamation_singleton_iff — Mathlib

English

For a singleton presieve generated by a morphism f: X → Y, an element x of (singleton f).FamilyOfElements P amalgamates y ∈ P(op Y) iff P.map f^{op} y = x_f(⟨⟨⟩⟩).

Русский

Для предрассыпь размера singleton f: X → Y амальгамма x к y эквивалентна равенству P.map f^{op} y = x_f(⟨⟩).

LaTeX

$$x.IsAmalgamation y ↔ P.map f.op y = x f ⟨⟩$$

Lean4

@[simp]
theorem isAmalgamation_singleton_iff {X Y : C} (f : X ⟶ Y) (x : (singleton f).FamilyOfElements P) (y : P.obj (op Y)) :
    x.IsAmalgamation y ↔ P.map f.op y = x f ⟨⟩ :=
  by
  refine ⟨fun H ↦ H _ _, ?_⟩
  rintro H Y g ⟨rfl⟩
  exact H

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