English
Isomorphism of a CatCospanTransform morphism f is equivalent to the triple of isomorphisms of its left, base, and right components; i.e., f is an isomorphism iff each of f.left, f.base, f.right is an isomorphism.
Русский
Изоморфизм морфизма CatCospanTransform f эквивалентен трем изоморфизмам его компонент: f.left, f.base, f.right; то есть f является изоморфизмом тогда и только тогда, когда каждая из компонент изоморфизм.
LaTeX
$$$ \\text{IsIso}(f) \\iff (\\text{IsIso}(f.left) \\wedge (\\text{IsIso}(f.base) \\wedge \\text{IsIso}(f.right)))$$$
Lean4
/-- The square `transformPrecomposeSquare` respects compositions. -/
theorem transformPrecomposeObjSquare_iso_hom_comp {A₂ : Type u₇} {B₂ : Type u₈} {C₂ : Type u₉} [Category.{v₇} A₂]
[Category.{v₈} B₂] [Category.{v₉} C₂] {F₂ : A₂ ⥤ B₂} {G₂ : C₂ ⥤ B₂} {X : Type u₁₀} {Y : Type u₁₁} [Category.{v₁₀} X]
[Category.{v₁₁} Y] (U : X ⥤ Y) (ψ : CatCospanTransform F G F₁ G₁) (ψ' : CatCospanTransform F₁ G₁ F₂ G₂) :
(CatCommSq.iso (transform Y |>.obj <| ψ.comp ψ') (precompose F G |>.obj U) (precompose F₂ G₂ |>.obj U)
(transform X |>.obj <| ψ.comp ψ')).hom ≫
whiskerLeft (precompose F G |>.obj U) (transformObjComp X ψ ψ').hom =
whiskerRight (transformObjComp Y ψ ψ').hom (precompose F₂ G₂ |>.obj U) ≫
(Functor.associator _ _ _).hom ≫
whiskerLeft (transform Y |>.obj ψ)
(CatCommSq.iso _ (precompose F₁ G₁ |>.obj U) _ (transform X |>.obj ψ')).hom ≫
(Functor.associator _ _ _).inv ≫
whiskerRight (CatCommSq.iso _ _ _ _).hom (transform X |>.obj ψ') ≫ (Functor.associator _ _ _).hom :=
by cat_disch
