monoCoprod — Mathlib

English

As above, the result that left distributivity implies Cartesian distributivity.

Русский

Как и выше, следствие слева распределимости в декартовой распределимости.

LaTeX

$$$IsCartesianDistributive\\, C$$$

Lean4

/-- The coproduct coprojections are monic in a Cartesian distributive category. -/
instance monoCoprod [IsCartesianDistributive C] : MonoCoprod C :=
  MonoCoprod.mk' fun A B =>
    ⟨_, coprodIsCoprod A B,
      ⟨fun {Z} f g he ↦ by
        let ι := coprod.inl (X := A) (Y := B)
        have : Mono (Z ◁ ι) :=
          SplitMono.mono { retraction := (∂L Z A B).inv ≫ coprod.desc (𝟙 _) (fst Z B ≫ lift (𝟙 Z) f) }
        have : lift (𝟙 Z) f = lift (𝟙 Z) g := by rw [← cancel_mono (Z ◁ ι)]; aesop
        simpa only [lift_snd] using this =≫ snd _ _⟩⟩

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