English
If G preserves the pullback of f and g, then G also preserves the pullback of g and f.
Русский
Если G сохраняет притяжение f,g, тогда G сохраняет притяжение g,f.
LaTeX
$$$Preserves\\Pullback\\symmetry(G,f,g)$$$
Lean4
/-- If `F` preserves the pullback of `f, g`, it also preserves the pullback of `g, f`. -/
theorem preservesPullback_symmetry : PreservesLimit (cospan g f) G where
preserves {c}
hc :=
⟨by
apply (IsLimit.postcomposeHomEquiv (diagramIsoCospan.{v₂} _) _).toFun
apply IsLimit.ofIsoLimit _ (PullbackCone.isoMk _).symm
apply PullbackCone.isLimitOfFlip
apply (isLimitMapConePullbackConeEquiv _ _).toFun
· refine @isLimitOfPreserves _ _ _ _ _ _ _ _ _ ?_ ?_
· apply PullbackCone.isLimitOfFlip
apply IsLimit.ofIsoLimit _ (PullbackCone.isoMk _)
exact (IsLimit.postcomposeHomEquiv (diagramIsoCospan.{v₁} _) _).invFun hc
· dsimp
infer_instance
· exact (c.π.naturality WalkingCospan.Hom.inr).symm.trans (c.π.naturality WalkingCospan.Hom.inl :)⟩
