preservesEqualizers_of_preservesPullbacks_and_binaryProducts

English

A functor preserving pullbacks and binary products preserves equalizers.

Русский

Функтор, сохраняющий pullbacks и бинарные произведения, сохраняет равносиленные.

LaTeX

$$$[PreservesLimitsOfShape WalkingParallelPair G] \\Rightarrow [PreservesLimitsOfShape WalkingCospan G] \\Rightarrow PreservesLimitsOfShape WalkingParallelPair G$$$

Lean4

/-- A functor that preserves pullbacks and binary products also presrves equalizers. -/
theorem preservesEqualizers_of_preservesPullbacks_and_binaryProducts [HasBinaryProducts C] [HasPullbacks C]
    [PreservesLimitsOfShape (Discrete WalkingPair) G] [PreservesLimitsOfShape WalkingCospan G] :
    PreservesLimitsOfShape WalkingParallelPair G :=
  ⟨fun {K} =>
    preservesLimit_of_preserves_limit_cone (equalizerConeIsLimit K) <|
      { lift := fun c => by
          refine pullback.lift ?_ ?_ ?_ ≫ (PreservesPullback.iso _ _ _).inv
          · exact c.π.app WalkingParallelPair.zero
          · exact c.π.app WalkingParallelPair.zero
          apply (mapIsLimitOfPreservesOfIsLimit G _ _ (prodIsProd _ _)).hom_ext
          rintro (_ | _)
          · simp only [Category.assoc, ← G.map_comp, prod.lift_fst, BinaryFan.π_app_left, BinaryFan.mk_fst]
          · simp only [BinaryFan.π_app_right, BinaryFan.mk_snd, Category.assoc, ← G.map_comp, prod.lift_snd]
            exact (c.π.naturality WalkingParallelPairHom.left).symm.trans (c.π.naturality WalkingParallelPairHom.right)
        fac := fun c j =>
          by
          rcases j with (_ | _) <;>
            simp only [Category.comp_id, PreservesPullback.iso_inv_fst, Cone.ofFork_π, G.map_comp,
              PreservesPullback.iso_inv_fst_assoc, Functor.mapCone_π_app, eqToHom_refl, Category.assoc, Fork.ofι_π_app,
              pullback.lift_fst, pullback.lift_fst_assoc]
          exact (c.π.naturality WalkingParallelPairHom.left).symm.trans (Category.id_comp _)
        uniq := fun s m h => by
          rw [Iso.eq_comp_inv]
          have := h WalkingParallelPair.zero
          dsimp [equalizerCone] at this
          ext <;>
            simp only [PreservesPullback.iso_hom_snd, Category.assoc, PreservesPullback.iso_hom_fst, pullback.lift_fst,
              pullback.lift_snd, Category.comp_id, ← pullbackFst_eq_pullback_snd, ← this] }⟩
    -- We hide the "implementation details" inside a namespace

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