Poly.ForMathlib.CategoryTheory.PartialProduct

Partial Products #

A partial product is a simultaneous generalization of a product and an exponential object.

A partial product of an object X over a morphism s : E ⟶ B is is an object P together with morphisms fst : P —> A and snd : pullback fst s —> X which is universal among such data.

source

structure CategoryTheory.PartialProduct.Fan {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} (s : E ⟶ B) (X : C) :

Type (max u_1 u_2)

A partial product cone over an object X : C and a morphism s : E ⟶ B is an object pt : C together with morphisms Fan.fst : pt —> B and Fan.snd : pullback Fan.fst s —> X.

          X
          ^
  Fan.snd |
          |
          • --------------->   pt
          |                    |
          |        (pb)        | Fan.fst
          v                    v
          E ---------------->  B
                    s

pt : C
fst : self.pt ⟶ B
snd : Limits.pullback self.fst s ⟶ X

Instances For

source

theorem CategoryTheory.PartialProduct.Fan.fst_mk {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} (s : E ⟶ B) (X : C) {pt : C} (f : pt ⟶ B) (g : Limits.pullback f s ⟶ X) :

{ pt := pt, fst := f, snd := g }.fst = f

source

def CategoryTheory.PartialProduct.Fan.over {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X : C} (c : Fan s X) :

Over B

Equations

c.over = CategoryTheory.Over.mk c.fst

Instances For

source

def CategoryTheory.PartialProduct.Fan.overPullbackToStar {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X : C} [Limits.HasBinaryProducts C] (c : Fan s X) :

(Over.pullback s).obj c.over ⟶ (Over.star E).obj X

Equations

c.overPullbackToStar = ((CategoryTheory.Over.forgetAdjStar E).homEquiv ((CategoryTheory.Over.pullback s).obj c.over) X) c.snd

Instances For

source

@[simp]

theorem CategoryTheory.PartialProduct.Fan.overPullbackToStar_snd {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X : C} {c : Fan s X} [Limits.HasBinaryProducts C] :

CategoryStruct.comp c.overPullbackToStar.left Limits.prod.snd = c.snd

source

@[simp]

theorem CategoryTheory.PartialProduct.Fan.overPullbackToStar_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X : C} {c : Fan s X} [Limits.HasBinaryProducts C] {Z : C} (h : X ⟶ Z) :

CategoryStruct.comp c.overPullbackToStar.left (CategoryStruct.comp Limits.prod.snd h) = CategoryStruct.comp c.snd h

source

def CategoryTheory.PartialProduct.comparison {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X P : C} {c : Fan s X} (f : P ⟶ c.pt) :

Limits.pullback (CategoryStruct.comp f c.fst) s ⟶ Limits.pullback c.fst s

Equations

CategoryTheory.PartialProduct.comparison f = ((CategoryTheory.Over.pullback s).map (CategoryTheory.Over.homMk f ⋯)).left

Instances For

source

theorem CategoryTheory.PartialProduct.comparison_pullback.map {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X P : C} {c : Fan s X} {f : P ⟶ c.pt} :

comparison f = Limits.pullback.map (CategoryStruct.comp f c.fst) s c.fst s f (CategoryStruct.id E) (CategoryStruct.id B) ⋯ ⋯

source

def CategoryTheory.PartialProduct.pullbackMap {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X : C} {c' c : Fan s X} (f : c'.pt ⟶ c.pt) :

autoParam (CategoryStruct.comp f c.fst = c'.fst) _auto✝ → (Limits.pullback c'.fst s ⟶ Limits.pullback c.fst s)

Equations

CategoryTheory.PartialProduct.pullbackMap f x✝ = ((CategoryTheory.Over.pullback s).map (CategoryTheory.Over.homMk f ⋯)).left

Instances For

source

theorem CategoryTheory.PartialProduct.pullbackMap_comparison {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X P : C} {c : Fan s X} (f : P ⟶ c.pt) :

pullbackMap f ⋯ = comparison f

source

def CategoryTheory.PartialProduct.Fan.extend {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X : C} (c : Fan s X) {A : C} (f : A ⟶ c.pt) :

Fan s X

A map to the apex of a partial product cone induces a partial product cone by precomposition.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CategoryTheory.PartialProduct.Fan.extend_pt {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X : C} (c : Fan s X) {A : C} (f : A ⟶ c.pt) :

(c.extend f).pt = A

source

@[simp]

theorem CategoryTheory.PartialProduct.Fan.extend_snd {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X : C} (c : Fan s X) {A : C} (f : A ⟶ c.pt) :

(c.extend f).snd = CategoryStruct.comp (Limits.pullback.map (CategoryStruct.comp f c.fst) s c.fst s f (CategoryStruct.id E) (CategoryStruct.id B) ⋯ ⋯) c.snd

source

@[simp]

theorem CategoryTheory.PartialProduct.Fan.extend_fst {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X : C} (c : Fan s X) {A : C} (f : A ⟶ c.pt) :

(c.extend f).fst = CategoryStruct.comp f c.fst

source

structure CategoryTheory.PartialProduct.Fan.Hom {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X : C} (c c' : Fan s X) :

Type u_2

hom : c.pt ⟶ c'.pt
w_left : CategoryStruct.comp self.hom c'.fst = c.fst
w_right : CategoryStruct.comp (pullbackMap self.hom ⋯) c'.snd = c.snd

Instances For

source

theorem CategoryTheory.PartialProduct.Fan.Hom.ext_iff {C : Type u_1} {inst✝ : Category.{u_2, u_1} C} {inst✝¹ : Limits.HasPullbacks C} {E B : C} {s : E ⟶ B} {X : C} {c c' : Fan s X} {x y : c.Hom c'} :

x = y ↔ x.hom = y.hom

source

theorem CategoryTheory.PartialProduct.Fan.Hom.ext {C : Type u_1} {inst✝ : Category.{u_2, u_1} C} {inst✝¹ : Limits.HasPullbacks C} {E B : C} {s : E ⟶ B} {X : C} {c c' : Fan s X} {x y : c.Hom c'} (hom : x.hom = y.hom) :

x = y

source

@[simp]

theorem CategoryTheory.PartialProduct.Fan.Hom.w_left_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X : C} {c c' : Fan s X} (self : c.Hom c') {Z : C} (h : B ⟶ Z) :

CategoryStruct.comp self.hom (CategoryStruct.comp c'.fst h) = CategoryStruct.comp c.fst h

source

@[simp]

theorem CategoryTheory.PartialProduct.Fan.Hom.w_right_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X : C} {c c' : Fan s X} (self : c.Hom c') {Z : C} (h : X ⟶ Z) :

CategoryStruct.comp (pullbackMap self.hom ⋯) (CategoryStruct.comp c'.snd h) = CategoryStruct.comp c.snd h

source

instance CategoryTheory.PartialProduct.instCategoryFan {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X : C} :

Category.{u_2, max u_2 u_1} (Fan s X)

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem CategoryTheory.PartialProduct.id_hom {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X : C} (c : Fan s X) :

(CategoryStruct.id c).hom = CategoryStruct.id c.pt

source

@[simp]

theorem CategoryTheory.PartialProduct.comp_hom {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X : C} {X✝ Y Z : Fan s X} (f : X✝.Hom Y) (g : Y.Hom Z) :

(CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

source

def CategoryTheory.PartialProduct.Fan.ext {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X : C} {c c' : Fan s X} (e : c.pt ≅ c'.pt) (h₁ : CategoryStruct.comp e.hom c'.fst = c.fst) (h₂ : CategoryStruct.comp (pullbackMap e.hom ⋯) c'.snd = c.snd) :

c ≅ c'

Constructs an isomorphism of PartialProduct.Fans out of an isomorphism of the apexes that commutes with the projections.

Equations

CategoryTheory.PartialProduct.Fan.ext e h₁ h₂ = { hom := { hom := e.hom, w_left := h₁, w_right := h₂ }, inv := { hom := e.inv, w_left := ⋯, w_right := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

source

structure CategoryTheory.PartialProduct.IsLimit {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X : C} (cone : Fan s X) :

Type (max u_1 u_2)

lift (c : Fan s X) : c.pt ⟶ cone.pt
There is a morphism from any cone apex to cone.pt
fac_left (c : Fan s X) : CategoryStruct.comp (self.lift c) cone.fst = c.fst
For any cone c, the morphism lift c followed by the first project cone.fst is equal to c.fst.
fac_right (c : Fan s X) : CategoryStruct.comp (pullbackMap (self.lift c) ⋯) cone.snd = c.snd
For any cone c, the pullback pullbackMap of the cones followed by the second project cone.snd is equal to c.snd
uniq (c : Fan s X) (m : c.pt ⟶ cone.pt) (x✝ : CategoryStruct.comp m cone.fst = c.fst) : CategoryStruct.comp (pullbackMap m ⋯) cone.snd = c.snd → m = self.lift c
lift c is the unique such map

Instances For

source

structure CategoryTheory.PartialProduct.LimitFan {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} (s : E ⟶ B) (X : C) :

Type (max u_1 u_2)

A partial product of an object X over a morphism s : E ⟶ B is the universal partial product cone over X and s.

cone : Fan s X
The cone itself
isLimit : IsLimit self.cone
The proof that is the limit cone

Instances For

source

def CategoryTheory.overPullbackToStar {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X : C} [Limits.HasBinaryProducts C] {W : C} (f : W ⟶ B) (g : Limits.pullback f s ⟶ X) :

(Over.pullback s).obj (Over.mk f) ⟶ (Over.star E).obj X

Equations

CategoryTheory.overPullbackToStar f g = { pt := W, fst := f, snd := g }.overPullbackToStar

Instances For

source

theorem CategoryTheory.overPullbackToStar_prod_snd {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X : C} [Limits.HasBinaryProducts C] {W : C} {f : W ⟶ B} {g : Limits.pullback f s ⟶ X} :

CategoryStruct.comp (overPullbackToStar f g).left Limits.prod.snd = g

source

@[reducible, inline]

abbrev CategoryTheory.partialProd {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X : C} (c : PartialProduct.LimitFan s X) :

Equations

CategoryTheory.partialProd c = c.cone.pt

Instances For

source

@[reducible, inline]

abbrev CategoryTheory.partialProd.cone {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X : C} (c : PartialProduct.LimitFan s X) :

PartialProduct.Fan s X

Equations

CategoryTheory.partialProd.cone c = c.cone

Instances For

source

@[reducible, inline]

abbrev CategoryTheory.partialProd.isLimit {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X : C} (c : PartialProduct.LimitFan s X) :

PartialProduct.IsLimit (cone c)

Equations

CategoryTheory.partialProd.isLimit c = c.isLimit

Instances For

source

@[reducible, inline]

abbrev CategoryTheory.partialProd.fst {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X : C} (c : PartialProduct.LimitFan s X) :

partialProd c ⟶ B

Equations

CategoryTheory.partialProd.fst c = (CategoryTheory.partialProd.cone c).fst

Instances For

source

@[reducible, inline]

abbrev CategoryTheory.partialProd.snd {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X : C} (c : PartialProduct.LimitFan s X) :

Limits.pullback (fst c) s ⟶ X

Equations

CategoryTheory.partialProd.snd c = (CategoryTheory.partialProd.cone c).snd

Instances For

source

@[reducible, inline]

abbrev CategoryTheory.partialProd.lift {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X W : C} (c : PartialProduct.LimitFan s X) (f : W ⟶ B) (g : Limits.pullback f s ⟶ X) :

W ⟶ partialProd c

If the partial product of s and X exists, then every pair of morphisms f : W ⟶ B and g : pullback f s ⟶ X induces a morphism W ⟶ partialProd s X.

Equations

CategoryTheory.partialProd.lift c f g = (CategoryTheory.partialProd.isLimit c).lift { pt := W, fst := f, snd := g }

Instances For

source

@[simp]

theorem CategoryTheory.partialProd.lift_fst {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X W : C} {c : PartialProduct.LimitFan s X} (f : W ⟶ B) (g : Limits.pullback f s ⟶ X) :

CategoryStruct.comp (lift c f g) (fst c) = f

source

theorem CategoryTheory.partialProd.lift_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X W : C} {c : PartialProduct.LimitFan s X} (f : W ⟶ B) (g : Limits.pullback f s ⟶ X) {Z : C} (h : B ⟶ Z) :

CategoryStruct.comp (lift c f g) (CategoryStruct.comp (fst c) h) = CategoryStruct.comp f h

source

theorem CategoryTheory.partialProd.lift_snd {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X W : C} (c : PartialProduct.LimitFan s X) (f : W ⟶ B) (g : Limits.pullback f s ⟶ X) :

CategoryStruct.comp (PartialProduct.comparison (lift c f g)) (snd c) = CategoryStruct.comp (Limits.pullback.congrHom ⋯ ⋯).hom g

source

theorem CategoryTheory.partialProd.lift_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X W : C} (c : PartialProduct.LimitFan s X) (f : W ⟶ B) (g : Limits.pullback f s ⟶ X) {Z : C} (h : X ⟶ Z) :

CategoryStruct.comp (PartialProduct.comparison (lift c f g)) (CategoryStruct.comp (snd c) h) = CategoryStruct.comp (Limits.pullback.congrHom ⋯ ⋯).hom (CategoryStruct.comp g h)

source

theorem CategoryTheory.partialProd.hom_ext {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B : C} {s : E ⟶ B} {X W : C} (c : PartialProduct.LimitFan s X) {f g : W ⟶ partialProd c} (h₁ : CategoryStruct.comp f (fst c) = CategoryStruct.comp g (fst c)) (h₂ : CategoryStruct.comp (PartialProduct.comparison f) (snd c) = CategoryStruct.comp (Limits.pullback.congrHom h₁ ⋯).hom (CategoryStruct.comp (PartialProduct.comparison g) (snd c))) :

f = g