card_fiber_coprod_eq_sum — Mathlib

English

The fiber cardinality of a coproduct is the sum of the fiber cardinalities of the summands.

Русский

Кардинальность фибера coproduct равно сумме кардинальностей фиберов слагаемых.

LaTeX

$$$ Nat.card (F.obj (X \ ⨿ Y)).carrier = Nat.card (F.obj X).carrier + Nat.card (F.obj Y).carrier $$$

Lean4

/-- The cardinality of the fiber of a coproduct is the sum of the cardinalities of the fibers. -/
theorem card_fiber_coprod_eq_sum (X Y : C) : Nat.card (F.obj (X ⨿ Y)) = Nat.card (F.obj X) + Nat.card (F.obj Y) :=
  by
  let e : F.obj (X ⨿ Y) ≃ F.obj X ⊕ F.obj Y :=
    Iso.toEquiv <|
      (PreservesColimitPair.iso (F ⋙ FintypeCat.incl) X Y).symm.trans <|
        Types.binaryCoproductIso (FintypeCat.incl.obj (F.obj X)) (FintypeCat.incl.obj (F.obj Y))
  rw [← Nat.card_sum]
  exact Nat.card_eq_of_bijective e.toFun (Equiv.bijective e)

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