English
The restricted transition map t' between pullbacks is defined by composing pullback isomorphisms with the canonical map to the product, reflecting the overlaps in two-step identifications.
Русский
Ограниченное переходное отображение t' между притянутыми прообразами задаётся как композиция изоморфизм pullback с каноническим отображением в произведение, отражая пересечения во времени двух шагов идентификаций.
LaTeX
$$t' : pullback(...).inclusion' ⟶ pullback(...).inclusion'$$
Lean4
/-- (Implementation) the restricted transition map to be fed into `TopCat.GlueData`. -/
def t' (h : MkCore.{u}) (i j k : h.J) :
pullback (h.V i j).inclusion' (h.V i k).inclusion' ⟶ pullback (h.V j k).inclusion' (h.V j i).inclusion' :=
by
refine (pullbackIsoProdSubtype _ _).hom ≫ ofHom ⟨?_, ?_⟩ ≫ (pullbackIsoProdSubtype _ _).inv
· intro x
refine ⟨⟨⟨(h.t i j x.1.1).1, ?_⟩, h.t i j x.1.1⟩, rfl⟩
rcases x with ⟨⟨⟨x, hx⟩, ⟨x', hx'⟩⟩, rfl : x = x'⟩
exact h.t_inter _ ⟨x, hx⟩ hx'
fun_prop
