mkIsoSelfIsHomLift — Mathlib

English

If ha expresses p.obj a = S, then Fib.mkIsoSelf ha is mapped by ι to a morphism that is an IsHomLift over id S.

Русский

Если ha задаёт p.obj a = S, то Fib.mkIsoSelf ha под действием ι превращается в морфизм, который является IsHomLift над id S.

LaTeX

$$$IsHomLift(p)(id S)((Fib.mkIsoSelf ha).hom)$$$

Lean4

instance mkIsoSelfIsHomLift {S : 𝒮} {a : 𝒳} (ha : p.obj a = S) : IsHomLift p (𝟙 S) (Fib.mkIsoSelf ha).hom :=
  (Functor.objObjPreimageIso (inducedFunctor p S) (Fiber.mk ha)).hom.2

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