instPreservesFiniteProducts — Mathlib

English

μ_comp asserts the associativity compatibility of μ under composition of functors: μ (F ⋙ G) X Y = μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y).

Русский

μ_comp задаёт совместимость μ с ассоциативностью при композиции функторов: μ(F⋙G) X Y = μ G (F.obj X) (F.obj Y) ≫ G.map(μ F X Y).

LaTeX

$$$\mu_{F \gg G} X Y = μ_G (F.obj X) (F.obj Y) \;\gg\; G.map(μ_F X Y)$$$

Lean4

instance [F.Monoidal] : PreservesFiniteProducts F :=
  have (A B : _) : IsIso (CartesianMonoidalCategory.prodComparison F A B) :=
    δ_of_cartesianMonoidalCategory F A B ▸ inferInstance
  have : IsIso (CartesianMonoidalCategory.terminalComparison F) := η_of_cartesianMonoidalCategory F ▸ inferInstance
  have := preservesLimitsOfShape_discrete_walkingPair_of_isIso_prodComparison F
  have := preservesLimit_empty_of_isIso_terminalComparison F
  have := Limits.preservesLimitsOfShape_pempty_of_preservesTerminal F
  .of_preserves_binary_and_terminal _

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