preservesPushout_symmetry — Mathlib

English

If pullbacks exist and G preserves the relevant limits, then the pullback comparison map is an isomorphism.

Русский

Если существуют притяжения и G сохраняет соответствующие пределы, то сопоставление притяжения является изоморфизмом.

LaTeX

$$$IsIso( pullbackComparison\\ G\\ f\\ g )$$$

Lean4

/-- If `F` preserves the pushout of `f, g`, it also preserves the pushout of `g, f`. -/
theorem preservesPushout_symmetry : PreservesColimit (span g f) G where
  preserves {c}
    hc :=
    ⟨by
      apply (IsColimit.precomposeHomEquiv (diagramIsoSpan.{v₂} _).symm _).toFun
      apply IsColimit.ofIsoColimit _ (PushoutCocone.isoMk _).symm
      apply PushoutCocone.isColimitOfFlip
      apply (isColimitMapCoconePushoutCoconeEquiv _ _).toFun
      · -- Need to unfold these to allow the `PreservesColimit` instance to be found.

        dsimp only [span_map_fst, span_map_snd]
        exact isColimitOfPreserves _ (PushoutCocone.flipIsColimit hc)⟩

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