English
In the coherent Grothendieck topology setting, if Presheaf IsSheaf J ((J.plusObj P) ⋙ F) holds, then the inverse of (J.plusCompIso F P) equals the plusLift of whiskerRight (J.toPlus _) hP.
Русский
В рамках когерентной топологии Гротендийка, если Presheaf IsSheaf J ((J.plusObj P) ⋙ F) выполняется, то обратный образ (J.plusCompIso F P) равен plusLift(whiskerRight (J.toPlus P) F) для hP.
LaTeX
$$(J.plusCompIso F P)^{-1} = J.plusLift( whiskerRight (J.toPlus _) F )$$
Lean4
/-- The diagram used to define `P⁺`, composed with `F`, is isomorphic
to the diagram used to define `P ⋙ F`. -/
def diagramCompIso (X : C) : J.diagram P X ⋙ F ≅ J.diagram (P ⋙ F) X :=
NatIso.ofComponents
(fun W => by
refine ?_ ≪≫ HasLimit.isoOfNatIso (W.unop.multicospanComp _ _).symm
refine (isLimitOfPreserves F (limit.isLimit _)).conePointUniqueUpToIso (limit.isLimit _))
(by
intro A B f
dsimp
ext g
simp [← F.map_comp])
