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
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
  • One or more equations did not get rendered due to their size.
Instances For
    source
    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
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      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
      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)