wideCospan_map_term — Mathlib

English

For a set s of subobjects of A and a suitable index j, the map along the term of the wide pullback shape lands on the corresponding subobject arrow; this equality holds by construction.

Русский

Для множества подпредметов s и индекса j отображение вдоль терма широкой формы гильдии достигает соответствующей стрелки подпредмета; равенство следует из конструкций.

LaTeX

$$$(\text{wideCospan } s).map(\text{WidePullbackShape.Hom.term } j) = ((\text{equivShrink}(\text{Subobject } A)).symm j).arrow$$$

Lean4

@[simp]
theorem wideCospan_map_term {A : C} (s : Set (Subobject A)) (j) :
    (wideCospan s).map (WidePullbackShape.Hom.term j) = ((equivShrink (Subobject A)).symm j).arrow :=
  rfl

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