Documentation

Mathlib.CategoryTheory.Limits.Shapes.PiProd

A product as a binary product #

We write a product indexed by I as a binary product of the products indexed by a subset of I and its complement.

source
๐Ÿ”ธ coverage
noncomputable def CategoryTheory.Limits.Pi.binaryFanOfProp {C : Type u_1} {I : Type u_2} [Category.{v_1, u_1} C] (X : I โ†’ C) (P : I โ†’ Prop) [HasProduct X] [HasProduct fun (i : { x : I // P x }) => X โ†‘i] [HasProduct fun (i : { x : I // ยฌP x }) => X โ†‘i] :
BinaryFan (โˆแถœ fun (i : { x : I // P x }) => X โ†‘i) (โˆแถœ fun (i : { x : I // ยฌP x }) => X โ†‘i)

The projection maps of a product to the products indexed by a subset and its complement, as a binary fan.

Equations
    Instances For
      source
      ๐Ÿ”ธ coverage
      noncomputable def CategoryTheory.Limits.Pi.binaryFanOfPropIsLimit {C : Type u_1} {I : Type u_2} [Category.{v_1, u_1} C] (X : I โ†’ C) (P : I โ†’ Prop) [HasProduct X] [HasProduct fun (i : { x : I // P x }) => X โ†‘i] [HasProduct fun (i : { x : I // ยฌP x }) => X โ†‘i] [(i : I) โ†’ Decidable (P i)] :
      IsLimit (binaryFanOfProp X P)

      A product indexed by I is a binary product of the products indexed by a subset of I and its complement.

      Equations
        Instances For
          source
          ๐Ÿ“ coverage
          theorem CategoryTheory.Limits.hasBinaryProduct_of_products {C : Type u_1} {I : Type u_2} [Category.{v_1, u_1} C] {X : I โ†’ C} (P : I โ†’ Prop) [HasProduct X] [HasProduct fun (i : { x : I // P x }) => X โ†‘i] [HasProduct fun (i : { x : I // ยฌP x }) => X โ†‘i] :
          HasBinaryProduct (โˆแถœ fun (i : { x : I // P x }) => X โ†‘i) (โˆแถœ fun (i : { x : I // ยฌP x }) => X โ†‘i)
          source
          ๐Ÿ“ coverage
          theorem CategoryTheory.Limits.Pi.map_eq_prod_map {C : Type u_1} {I : Type u_2} [Category.{v_1, u_1} C] {X Y : I โ†’ C} (f : (i : I) โ†’ X i โŸถ Y i) (P : I โ†’ Prop) [HasProduct X] [HasProduct Y] [HasProduct fun (i : { x : I // P x }) => X โ†‘i] [HasProduct fun (i : { x : I // ยฌP x }) => X โ†‘i] [HasProduct fun (i : { x : I // P x }) => Y โ†‘i] [HasProduct fun (i : { x : I // ยฌP x }) => Y โ†‘i] [(i : I) โ†’ Decidable (P i)] :
          map f = CategoryStruct.comp ((binaryFanOfPropIsLimit X P).conePointUniqueUpToIso (prodIsProd (โˆแถœ fun (i : { x : I // P x }) => X โ†‘i) (โˆแถœ fun (i : { x : I // ยฌP x }) => X โ†‘i))).hom (CategoryStruct.comp (prod.map (map fun (i : { x : I // P x }) => f โ†‘i) (map fun (i : { x : I // ยฌP x }) => f โ†‘i)) ((binaryFanOfPropIsLimit Y P).conePointUniqueUpToIso (prodIsProd (โˆแถœ fun (i : { x : I // P x }) => Y โ†‘i) (โˆแถœ fun (i : { x : I // ยฌP x }) => Y โ†‘i))).inv)