# Documentation

Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products

# Preserving products #

Constructions to relate the notions of preserving products and reflecting products to concrete fans.

In particular, we show that piComparison G f is an isomorphism iff G preserves the limit of f.

def CategoryTheory.Limits.isLimitMapConeFanMkEquiv {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (f : JC) {P : C} (g : (j : J) → P f j) :

The map of a fan is a limit iff the fan consisting of the mapped morphisms is a limit. This essentially lets us commute Fan.mk with Functor.mapCone.

Instances For
def CategoryTheory.Limits.isLimitFanMkObjOfIsLimit {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (f : JC) {P : C} (g : (j : J) → P f j) :

The property of preserving products expressed in terms of fans.

Instances For
def CategoryTheory.Limits.isLimitOfIsLimitFanMkObj {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (f : JC) {P : C} (g : (j : J) → P f j) (t : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk (G.obj P) fun j => G.map (g j))) :

The property of reflecting products expressed in terms of fans.

Instances For
def CategoryTheory.Limits.isLimitOfHasProductOfPreservesLimit {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (f : JC) :

If G preserves products and C has them, then the fan constructed of the mapped projection of a product is a limit.

Instances For
def CategoryTheory.Limits.PreservesProduct.ofIsoComparison {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (f : JC) [CategoryTheory.Limits.HasProduct fun j => G.obj (f j)] :

If pi_comparison G f is an isomorphism, then G preserves the limit of f.

Instances For
def CategoryTheory.Limits.PreservesProduct.iso {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (f : JC) [CategoryTheory.Limits.HasProduct fun j => G.obj (f j)] :
G.obj ( f) fun j => G.obj (f j)

If G preserves limits, we have an isomorphism from the image of a product to the product of the images.

Instances For
@[simp]
theorem CategoryTheory.Limits.PreservesProduct.iso_hom {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (f : JC) [CategoryTheory.Limits.HasProduct fun j => G.obj (f j)] :
def CategoryTheory.Limits.isColimitMapCoconeCofanMkEquiv {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (f : JC) {P : C} (g : (j : J) → f j P) :

The map of a cofan is a colimit iff the cofan consisting of the mapped morphisms is a colimit. This essentially lets us commute Cofan.mk with Functor.mapCocone.

Instances For
def CategoryTheory.Limits.isColimitCofanMkObjOfIsColimit {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (f : JC) {P : C} (g : (j : J) → f j P) :

The property of preserving coproducts expressed in terms of cofans.

Instances For
def CategoryTheory.Limits.isColimitOfIsColimitCofanMkObj {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (f : JC) {P : C} (g : (j : J) → f j P) (t : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (G.obj P) fun j => G.map (g j))) :

The property of reflecting coproducts expressed in terms of cofans.

Instances For
def CategoryTheory.Limits.isColimitOfHasCoproductOfPreservesColimit {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (f : JC) :

If G preserves coproducts and C has them, then the cofan constructed of the mapped inclusion of a coproduct is a colimit.

Instances For
def CategoryTheory.Limits.PreservesCoproduct.ofIsoComparison {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (f : JC) [CategoryTheory.Limits.HasCoproduct fun j => G.obj (f j)] :

If sigma_comparison G f is an isomorphism, then G preserves the colimit of f.

Instances For
def CategoryTheory.Limits.PreservesCoproduct.iso {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (f : JC) [CategoryTheory.Limits.HasCoproduct fun j => G.obj (f j)] :
G.obj ( f) fun j => G.obj (f j)

If G preserves colimits, we have an isomorphism from the image of a coproduct to the coproduct of the images.

Instances For
@[simp]
theorem CategoryTheory.Limits.PreservesCoproduct.inv_hom {C : Type u₁} [] {D : Type u₂} [] (G : ) {J : Type w} (f : JC) [CategoryTheory.Limits.HasCoproduct fun j => G.obj (f j)] :