Special shapes for limits in Type.

The general shape (co)limits defined in CategoryTheory.Limits.Types are intended for use through the limits API, and the actual implementation should mostly be considered "sealed".

In this file, we provide definitions of the "standard" special shapes of limits in Type, giving the expected definitional implementation:

• the terminal object is PUnit
• the binary product of X and Y is X × Y
• the product of a family f : J → Type is Π j, f j
• the coproduct of a family f : J → Type is Σ j, f j
• the binary coproduct of X and Y is the sum type X ⊕ Y
• the equalizer of a pair of maps (g, h) is the subtype {x : Y // g x = h x}
• the coequalizer of a pair of maps (f, g) is the quotient of Y by ∀ x : Y, f x ~ g x
• the pullback of f : X ⟶ Z and g : Y ⟶ Z is the subtype { p : X × Y // f p.1 = g p.2 } of the product

We first construct terms of IsLimit and LimitCone, and then provide isomorphisms with the types generated by the HasLimit API.

As an example, when setting up the monoidal category structure on Type we use the Types.terminalLimitCone and Types.binaryProductLimitCone definitions.

instance CategoryTheory.Limits.Types.instHasProductsTypeTypes : CategoryTheory.Limits.HasProducts (Type v)

Equations

• CategoryTheory.Limits.Types.instHasProductsTypeTypes = ⋯

@[simp]

theorem CategoryTheory.Limits.Types.pi_lift_π_apply {β : Type v} [Small.{u, v} β] (f : β → Type u) {P : Type u} (s : (b : β) → P ⟶ f b) (b : β) (x : P) : CategoryTheory.Limits.Pi.π f b (CategoryTheory.Limits.Pi.lift s x) = s b x

A restatement of Types.Limit.lift_π_apply that uses Pi.π and Pi.lift.

theorem CategoryTheory.Limits.Types.pi_lift_π_apply' {β : Type v} (f : β → Type v) {P : Type v} (s : (b : β) → P ⟶ f b) (b : β) (x : P) : CategoryTheory.Limits.Pi.π f b (CategoryTheory.Limits.Pi.lift s x) = s b x

A restatement of Types.Limit.lift_π_apply that uses Pi.π and Pi.lift, with specialized universes.

@[simp]

theorem CategoryTheory.Limits.Types.pi_map_π_apply {β : Type v} [Small.{u, v} β] {f : β → Type u} {g : β → Type u} (α : (j : β) → f j ⟶ g j) (b : β) (x : ∏ fun (b : β) => f b) : CategoryTheory.Limits.Pi.π g b (CategoryTheory.Limits.Pi.map α x) = α b (CategoryTheory.Limits.Pi.π f b x)

A restatement of Types.Limit.map_π_apply that uses Pi.π and Pi.map.

theorem CategoryTheory.Limits.Types.pi_map_π_apply' {β : Type v} {f : β → Type v} {g : β → Type v} (α : (j : β) → f j ⟶ g j) (b : β) (x : ∏ fun (b : β) => f b) : CategoryTheory.Limits.Pi.π g b (CategoryTheory.Limits.Pi.map α x) = α b (CategoryTheory.Limits.Pi.π f b x)

A restatement of Types.Limit.map_π_apply that uses Pi.π and Pi.map, with specialized universes.

def CategoryTheory.Limits.Types.terminalLimitCone : CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty (Type u))

The category of types has PUnit as a terminal object.

Equations

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

noncomputable def CategoryTheory.Limits.Types.terminalIso : ⊤_ Type u ≅ PUnit.{u + 1}

The terminal object in Type u is PUnit.

Equations

• CategoryTheory.Limits.Types.terminalIso = CategoryTheory.Limits.limit.isoLimitCone CategoryTheory.Limits.Types.terminalLimitCone

noncomputable def CategoryTheory.Limits.Types.isTerminalPunit : CategoryTheory.Limits.IsTerminal PUnit.{u + 1}

The terminal object in Type u is PUnit.

Equations

• CategoryTheory.Limits.Types.isTerminalPunit = CategoryTheory.Limits.IsTerminal.ofIso CategoryTheory.Limits.terminalIsTerminal CategoryTheory.Limits.Types.terminalIso

noncomputable instance CategoryTheory.Limits.Types.instInhabitedTerminalTypeTypesHasLimitsOfShapeDiscretePEmptyDiscreteCategoryInstSmallDiscreteUnivLE_of_maxSmall_self : Inhabited (⊤_ Type u)

Equations

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

instance CategoryTheory.Limits.Types.instSubsingletonTerminalTypeTypesHasLimitsOfShapeDiscretePEmptyDiscreteCategoryInstSmallDiscreteUnivLE_of_maxSmall_self : Subsingleton (⊤_ Type u)

Equations

• CategoryTheory.Limits.Types.instSubsingletonTerminalTypeTypesHasLimitsOfShapeDiscretePEmptyDiscreteCategoryInstSmallDiscreteUnivLE_of_maxSmall_self = ⋯

noncomputable instance CategoryTheory.Limits.Types.instUniqueTerminalTypeTypesHasLimitsOfShapeDiscretePEmptyDiscreteCategoryInstSmallDiscreteUnivLE_of_maxSmall_self : Unique (⊤_ Type u)

Equations

• CategoryTheory.Limits.Types.instUniqueTerminalTypeTypesHasLimitsOfShapeDiscretePEmptyDiscreteCategoryInstSmallDiscreteUnivLE_of_maxSmall_self = Unique.mk' (⊤_ Type u)

noncomputable def CategoryTheory.Limits.Types.isTerminalEquivUnique (X : Type u) : CategoryTheory.Limits.IsTerminal X ≃ Unique X

A type is terminal if and only if it contains exactly one element.

Equations

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

noncomputable def CategoryTheory.Limits.Types.isTerminalEquivIsoPUnit (X : Type u) : CategoryTheory.Limits.IsTerminal X ≃ (X ≅ PUnit.{u + 1} )

A type is terminal if and only if it is isomorphic to PUnit.

Equations

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

def CategoryTheory.Limits.Types.initialColimitCocone : CategoryTheory.Limits.ColimitCocone (CategoryTheory.Functor.empty (Type u))

The category of types has PEmpty as an initial object.

Equations

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

noncomputable def CategoryTheory.Limits.Types.initialIso : ⊥_ Type u ≅ PEmpty.{u + 1}

The initial object in Type u is PEmpty.

Equations

• CategoryTheory.Limits.Types.initialIso = CategoryTheory.Limits.colimit.isoColimitCocone CategoryTheory.Limits.Types.initialColimitCocone

noncomputable def CategoryTheory.Limits.Types.isInitialPunit : CategoryTheory.Limits.IsInitial PEmpty.{u + 1}

The initial object in Type u is PEmpty.

Equations

• CategoryTheory.Limits.Types.isInitialPunit = CategoryTheory.Limits.IsInitial.ofIso CategoryTheory.Limits.initialIsInitial CategoryTheory.Limits.Types.initialIso

theorem CategoryTheory.Limits.Types.initial_iff_empty (X : Type u) : Nonempty (CategoryTheory.Limits.IsInitial X) ↔ IsEmpty X

An object in Type u is initial if and only if it is empty.

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductCone_pt (X : Type u) (Y : Type u) : (CategoryTheory.Limits.Types.binaryProductCone X Y).pt = (X × Y)

def CategoryTheory.Limits.Types.binaryProductCone (X : Type u) (Y : Type u) : CategoryTheory.Limits.BinaryFan X Y

The product type X × Y forms a cone for the binary product of X and Y.

Equations

• CategoryTheory.Limits.Types.binaryProductCone X Y = CategoryTheory.Limits.BinaryFan.mk Prod.fst Prod.snd

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductCone_fst (X : Type u) (Y : Type u) : CategoryTheory.Limits.BinaryFan.fst (CategoryTheory.Limits.Types.binaryProductCone X Y) = Prod.fst

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductCone_snd (X : Type u) (Y : Type u) : CategoryTheory.Limits.BinaryFan.snd (CategoryTheory.Limits.Types.binaryProductCone X Y) = Prod.snd

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductLimit_lift (X : Type u) (Y : Type u) (s : CategoryTheory.Limits.BinaryFan X Y) (x : s.pt) : (CategoryTheory.Limits.Types.binaryProductLimit X Y).lift s x = (CategoryTheory.Limits.BinaryFan.fst s x, CategoryTheory.Limits.BinaryFan.snd s x)

def CategoryTheory.Limits.Types.binaryProductLimit (X : Type u) (Y : Type u) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Types.binaryProductCone X Y)

The product type X × Y is a binary product for X and Y.

Equations

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

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductLimitCone_isLimit (X : Type u) (Y : Type u) : (CategoryTheory.Limits.Types.binaryProductLimitCone X Y).isLimit = CategoryTheory.Limits.Types.binaryProductLimit X Y

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductLimitCone_cone (X : Type u) (Y : Type u) : (CategoryTheory.Limits.Types.binaryProductLimitCone X Y).cone = CategoryTheory.Limits.Types.binaryProductCone X Y

def CategoryTheory.Limits.Types.binaryProductLimitCone (X : Type u) (Y : Type u) : CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)

The category of types has X × Y, the usual cartesian product, as the binary product of X and Y.

Equations

• CategoryTheory.Limits.Types.binaryProductLimitCone X Y = { cone := CategoryTheory.Limits.Types.binaryProductCone X Y, isLimit := CategoryTheory.Limits.Types.binaryProductLimit X Y }

noncomputable def CategoryTheory.Limits.Types.binaryProductIso (X : Type u) (Y : Type u) : X ⨯ Y ≅ X × Y

The categorical binary product in Type u is cartesian product.

Equations

• CategoryTheory.Limits.Types.binaryProductIso X Y = CategoryTheory.Limits.limit.isoLimitCone (CategoryTheory.Limits.Types.binaryProductLimitCone X Y)

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_hom_comp_fst_apply (X : Type u) (Y : Type u) (x : CategoryTheory.Limits.limit (CategoryTheory.Limits.pair X Y)) : Prod.fst ((CategoryTheory.Limits.limit.isoLimitCone (CategoryTheory.Limits.Types.binaryProductLimitCone X Y)).hom x) = CategoryTheory.Limits.limit.π (CategoryTheory.Limits.pair X Y) { as := CategoryTheory.Limits.WalkingPair.left } x

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_hom_comp_fst (X : Type u) (Y : Type u) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.binaryProductIso X Y).hom Prod.fst = CategoryTheory.Limits.prod.fst

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_hom_comp_snd_apply (X : Type u) (Y : Type u) (x : CategoryTheory.Limits.limit (CategoryTheory.Limits.pair X Y)) : Prod.snd ((CategoryTheory.Limits.limit.isoLimitCone (CategoryTheory.Limits.Types.binaryProductLimitCone X Y)).hom x) = CategoryTheory.Limits.limit.π (CategoryTheory.Limits.pair X Y) { as := CategoryTheory.Limits.WalkingPair.right } x

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_hom_comp_snd (X : Type u) (Y : Type u) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.binaryProductIso X Y).hom Prod.snd = CategoryTheory.Limits.prod.snd

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_inv_comp_fst_apply (X : Type u) (Y : Type u) (x : (CategoryTheory.Limits.Types.binaryProductLimitCone X Y).cone.pt) : CategoryTheory.Limits.limit.π (CategoryTheory.Limits.pair X Y) { as := CategoryTheory.Limits.WalkingPair.left } ((CategoryTheory.Limits.limit.isoLimitCone (CategoryTheory.Limits.Types.binaryProductLimitCone X Y)).inv x) = Prod.fst x

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_inv_comp_fst (X : Type u) (Y : Type u) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.binaryProductIso X Y).inv CategoryTheory.Limits.prod.fst = Prod.fst

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_inv_comp_snd_apply (X : Type u) (Y : Type u) (x : (CategoryTheory.Limits.Types.binaryProductLimitCone X Y).cone.pt) : CategoryTheory.Limits.limit.π (CategoryTheory.Limits.pair X Y) { as := CategoryTheory.Limits.WalkingPair.right } ((CategoryTheory.Limits.limit.isoLimitCone (CategoryTheory.Limits.Types.binaryProductLimitCone X Y)).inv x) = Prod.snd x

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_inv_comp_snd (X : Type u) (Y : Type u) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.binaryProductIso X Y).inv CategoryTheory.Limits.prod.snd = Prod.snd

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductFunctor_obj_map (X : Type u) {Y₁ : Type u} {Y₂ : Type u} (f : Y₁ ⟶ Y₂) : ∀ (a : (CategoryTheory.Limits.BinaryFan.mk Prod.fst (CategoryTheory.CategoryStruct.comp Prod.snd f)).pt), (CategoryTheory.Limits.Types.binaryProductFunctor.obj X).map f a = (CategoryTheory.Limits.Types.binaryProductLimit X Y₂).lift (CategoryTheory.Limits.BinaryFan.mk Prod.fst (CategoryTheory.CategoryStruct.comp Prod.snd f)) a

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductFunctor_map_app {X₁ : Type u} {X₂ : Type u} (f : X₁ ⟶ X₂) (Y : Type u) : ∀ (a : (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.CategoryStruct.comp Prod.fst f) Prod.snd).pt), (CategoryTheory.Limits.Types.binaryProductFunctor.map f).app Y a = (CategoryTheory.Limits.Types.binaryProductLimit X₂ Y).lift (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.CategoryStruct.comp Prod.fst f) Prod.snd) a

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductFunctor_obj_obj (X : Type u) (Y : Type u) : (CategoryTheory.Limits.Types.binaryProductFunctor.obj X).obj Y = (X × Y)

def CategoryTheory.Limits.Types.binaryProductFunctor : CategoryTheory.Functor (Type u) (CategoryTheory.Functor (Type u) (Type u))

The functor which sends X, Y to the product type X × Y.

Equations

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

noncomputable def CategoryTheory.Limits.Types.binaryProductIsoProd : CategoryTheory.Limits.Types.binaryProductFunctor ≅ CategoryTheory.Limits.prod.functor

The product functor given by the instance HasBinaryProducts (Type u) is isomorphic to the explicit binary product functor given by the product type.

Equations

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

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductCocone_ι_app (X : Type u) (Y : Type u) : ∀ (x : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) (a : (CategoryTheory.Limits.pair X Y).obj x), (CategoryTheory.Limits.Types.binaryCoproductCocone X Y).ι.app x a = CategoryTheory.Limits.WalkingPair.rec (motive := fun (t : CategoryTheory.Limits.WalkingPair) => x.as = t → ((CategoryTheory.Limits.pair X Y).obj x ⟶ X ⊕ Y)) (fun (h : x.as = CategoryTheory.Limits.WalkingPair.left) => ⋯ ▸ Sum.inl) (fun (h : x.as = CategoryTheory.Limits.WalkingPair.right) => ⋯ ▸ Sum.inr) x.as ⋯ a

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductCocone_pt (X : Type u) (Y : Type u) : (CategoryTheory.Limits.Types.binaryCoproductCocone X Y).pt = (X ⊕ Y)

def CategoryTheory.Limits.Types.binaryCoproductCocone (X : Type u) (Y : Type u) : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)

The sum type X ⊕ Y forms a cocone for the binary coproduct of X and Y.

Equations

• CategoryTheory.Limits.Types.binaryCoproductCocone X Y = CategoryTheory.Limits.BinaryCofan.mk Sum.inl Sum.inr

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductColimit_desc (X : Type u) (Y : Type u) (s : CategoryTheory.Limits.BinaryCofan X Y) : ∀ (a : X ⊕ Y), (CategoryTheory.Limits.Types.binaryCoproductColimit X Y).desc s a = Sum.elim (CategoryTheory.Limits.BinaryCofan.inl s) (CategoryTheory.Limits.BinaryCofan.inr s) a

def CategoryTheory.Limits.Types.binaryCoproductColimit (X : Type u) (Y : Type u) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Types.binaryCoproductCocone X Y)

The sum type X ⊕ Y is a binary coproduct for X and Y.

Equations

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

def CategoryTheory.Limits.Types.binaryCoproductColimitCocone (X : Type u) (Y : Type u) : CategoryTheory.Limits.ColimitCocone (CategoryTheory.Limits.pair X Y)

The category of types has X ⊕ Y, as the binary coproduct of X and Y.

Equations

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

noncomputable def CategoryTheory.Limits.Types.binaryCoproductIso (X : Type u) (Y : Type u) : X ⨿ Y ≅ X ⊕ Y

The categorical binary coproduct in Type u is the sum X ⊕ Y.

Equations

• CategoryTheory.Limits.Types.binaryCoproductIso X Y = CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.Limits.Types.binaryCoproductColimitCocone X Y)

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_hom_apply (X : Type u) (Y : Type u) (x : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left }) : (CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.Limits.Types.binaryCoproductColimitCocone X Y)).hom (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.pair X Y) { as := CategoryTheory.Limits.WalkingPair.left } x) = (CategoryTheory.Limits.BinaryCofan.inl (CategoryTheory.Limits.Types.binaryCoproductColimitCocone X Y).cocone) x

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_hom (X : Type u) (Y : Type u) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.Types.binaryCoproductIso X Y).hom = Sum.inl

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_hom_apply (X : Type u) (Y : Type u) (x : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right }) : (CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.Limits.Types.binaryCoproductColimitCocone X Y)).hom (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.pair X Y) { as := CategoryTheory.Limits.WalkingPair.right } x) = (CategoryTheory.Limits.BinaryCofan.inr (CategoryTheory.Limits.Types.binaryCoproductColimitCocone X Y).cocone) x

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_hom (X : Type u) (Y : Type u) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.Limits.Types.binaryCoproductIso X Y).hom = Sum.inr

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_inv_apply (X : Type u) (Y : Type u) (x : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left }) : (CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.Limits.Types.binaryCoproductColimitCocone X Y)).inv (CategoryTheory.Limits.BinaryCofan.inl (CategoryTheory.Limits.Types.binaryCoproductColimitCocone X Y).cocone x) = CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.pair X Y) { as := CategoryTheory.Limits.WalkingPair.left } x

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_inv (X : Type u) (Y : Type u) : CategoryTheory.CategoryStruct.comp (CategoryTheory.asHom Sum.inl) (CategoryTheory.Limits.Types.binaryCoproductIso X Y).inv = CategoryTheory.Limits.coprod.inl

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_inv_apply (X : Type u) (Y : Type u) (x : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right }) : (CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.Limits.Types.binaryCoproductColimitCocone X Y)).inv (CategoryTheory.Limits.BinaryCofan.inr (CategoryTheory.Limits.Types.binaryCoproductColimitCocone X Y).cocone x) = CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.pair X Y) { as := CategoryTheory.Limits.WalkingPair.right } x

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_inv (X : Type u) (Y : Type u) : CategoryTheory.CategoryStruct.comp (CategoryTheory.asHom Sum.inr) (CategoryTheory.Limits.Types.binaryCoproductIso X Y).inv = CategoryTheory.Limits.coprod.inr

theorem CategoryTheory.Limits.Types.binaryCofan_isColimit_iff {X : Type u} {Y : Type u} (c : CategoryTheory.Limits.BinaryCofan X Y) : Nonempty (CategoryTheory.Limits.IsColimit c) ↔ Function.Injective (CategoryTheory.Limits.BinaryCofan.inl c) ∧ Function.Injective (CategoryTheory.Limits.BinaryCofan.inr c) ∧ IsCompl (Set.range (CategoryTheory.Limits.BinaryCofan.inl c)) (Set.range (CategoryTheory.Limits.BinaryCofan.inr c))

noncomputable def CategoryTheory.Limits.Types.isCoprodOfMono {X : Type u} {Y : Type u} (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk f Subtype.val)

Any monomorphism in Type is a coproduct injection.

Equations

• CategoryTheory.Limits.Types.isCoprodOfMono f = Nonempty.some ⋯

def CategoryTheory.Limits.Types.productLimitCone {J : Type v} (F : J → TypeMax) : CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor F)

The category of types has Π j, f j as the product of a type family f : J → TypeMax.{v, u}.

Equations

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

noncomputable def CategoryTheory.Limits.Types.productIso {J : Type v} (F : J → TypeMax) : ∏ F ≅ (j : J) → F j

The categorical product in TypeMax.{v, u} is the type theoretic product Π j, F j.

Equations

• CategoryTheory.Limits.Types.productIso F = CategoryTheory.Limits.limit.isoLimitCone (CategoryTheory.Limits.Types.productLimitCone F)

@[simp]

theorem CategoryTheory.Limits.Types.productIso_hom_comp_eval {J : Type v} (F : J → TypeMax) (j : J) : (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.productIso F).hom fun (f : (j : J) → F j) => f j) = CategoryTheory.Limits.Pi.π F j

@[simp]

theorem CategoryTheory.Limits.Types.productIso_hom_comp_eval_apply {J : Type v} (F : J → TypeMax) (j : J) (x : ∏ F) : (CategoryTheory.Limits.Types.productIso F).hom x j = CategoryTheory.Limits.Pi.π F j x

@[simp]

theorem CategoryTheory.Limits.Types.productIso_inv_comp_π_apply {J : Type v} (F : J → TypeMax) (j : J) (x : (CategoryTheory.Limits.Types.productLimitCone F).cone.pt) : CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor F) { as := j } ((CategoryTheory.Limits.limit.isoLimitCone (CategoryTheory.Limits.Types.productLimitCone F)).inv x) = ((CategoryTheory.Limits.Types.productLimitCone F).cone.π.app { as := j }) x

@[simp]

theorem CategoryTheory.Limits.Types.productIso_inv_comp_π {J : Type v} (F : J → TypeMax) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.productIso F).inv (CategoryTheory.Limits.Pi.π F j) = fun (f : (j : J) → F j) => f j

noncomputable def CategoryTheory.Limits.Types.Small.productLimitCone {J : Type v} (F : J → Type u) [Small.{u, v} J] : CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor F)

A variant of productLimitCone using a Small hypothesis rather than a function to TypeMax.

Equations

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

noncomputable def CategoryTheory.Limits.Types.Small.productIso {J : Type v} (F : J → Type u) [Small.{u, v} J] : ∏ F ≅ Shrink.{u, max u v} ((j : J) → F j)

The categorical product in Type u indexed in Type v is the type theoretic product Π j, F j, after shrinking back to Type u.

Equations

• CategoryTheory.Limits.Types.Small.productIso F = CategoryTheory.Limits.limit.isoLimitCone (CategoryTheory.Limits.Types.Small.productLimitCone F)

@[simp]

theorem CategoryTheory.Limits.Types.Small.productIso_hom_comp_eval {J : Type v} (F : J → Type u) [Small.{u, v} J] (j : J) : (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.Small.productIso F).hom fun (f : Shrink.{u, max u v} ((j : J) → F j)) => (equivShrink ((j : J) → F j)).symm f j) = CategoryTheory.Limits.Pi.π F j

@[simp]

theorem CategoryTheory.Limits.Types.Small.productIso_hom_comp_eval_apply {J : Type v} (F : J → Type u) [Small.{u, v} J] (j : J) (x : ∏ F) : (equivShrink ((j : J) → F j)).symm ((CategoryTheory.Limits.Types.Small.productIso F).hom x) j = CategoryTheory.Limits.Pi.π F j x

@[simp]

theorem CategoryTheory.Limits.Types.Small.productIso_inv_comp_π_apply {J : Type v} (F : J → Type u) [Small.{u, v} J] (j : J) (x : (CategoryTheory.Limits.Types.Small.productLimitCone F).cone.pt) : CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor F) { as := j } ((CategoryTheory.Limits.limit.isoLimitCone (CategoryTheory.Limits.Types.Small.productLimitCone F)).inv x) = ((CategoryTheory.Limits.Types.Small.productLimitCone F).cone.π.app { as := j }) x

@[simp]

theorem CategoryTheory.Limits.Types.Small.productIso_inv_comp_π {J : Type v} (F : J → Type u) [Small.{u, v} J] (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.Small.productIso F).inv (CategoryTheory.Limits.Pi.π F j) = fun (f : Shrink.{u, max u v} ((j : J) → F j)) => (equivShrink ((j : J) → F j)).symm f j

def CategoryTheory.Limits.Types.coproductColimitCocone {J : Type v} (F : J → TypeMax) : CategoryTheory.Limits.ColimitCocone (CategoryTheory.Discrete.functor F)

The category of types has Σ j, f j as the coproduct of a type family f : J → Type.

Equations

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

noncomputable def CategoryTheory.Limits.Types.coproductIso {J : Type v} (F : J → TypeMax) : ∐ F ≅ (j : J) × F j

The categorical coproduct in Type u is the type theoretic coproduct Σ j, F j.

Equations

• CategoryTheory.Limits.Types.coproductIso F = CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.Limits.Types.coproductColimitCocone F)

@[simp]

theorem CategoryTheory.Limits.Types.coproductIso_ι_comp_hom_apply {J : Type v} (F : J → TypeMax) (j : J) (x : (CategoryTheory.Discrete.functor F).obj { as := j }) : (CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.Limits.Types.coproductColimitCocone F)).hom (CategoryTheory.Limits.colimit.ι (CategoryTheory.Discrete.functor F) { as := j } x) = ((CategoryTheory.Limits.Types.coproductColimitCocone F).cocone.ι.app { as := j }) x

@[simp]

theorem CategoryTheory.Limits.Types.coproductIso_ι_comp_hom {J : Type v} (F : J → TypeMax) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι F j) (CategoryTheory.Limits.Types.coproductIso F).hom = fun (x : F j) => { fst := j, snd := x }

theorem CategoryTheory.Limits.Types.coproductIso_mk_comp_inv {J : Type v} (F : J → TypeMax) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.asHom fun (x : F j) => { fst := j, snd := x }) (CategoryTheory.Limits.Types.coproductIso F).inv = CategoryTheory.Limits.Sigma.ι F j

noncomputable def CategoryTheory.Limits.Types.typeEqualizerOfUnique {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Y) {g : Y ⟶ Z} {h : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h) (t : ∀ (y : Y), g y = h y → ∃! x : X, f x = y) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f w)

Show the given fork in Type u is an equalizer given that any element in the "difference kernel" comes from X. The converse of unique_of_type_equalizer.

Equations

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

theorem CategoryTheory.Limits.Types.unique_of_type_equalizer {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Y) {g : Y ⟶ Z} {h : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h) (t : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f w)) (y : Y) (hy : g y = h y) : ∃! x : X, f x = y

The converse of type_equalizer_of_unique.

theorem CategoryTheory.Limits.Types.type_equalizer_iff_unique {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Y) {g : Y ⟶ Z} {h : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h) : Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f w)) ↔ ∀ (y : Y), g y = h y → ∃! x : X, f x = y

def CategoryTheory.Limits.Types.equalizerLimit {Y : Type u} {Z : Type u} {g : Y ⟶ Z} {h : Y ⟶ Z} : CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.parallelPair g h)

Show that the subtype {x : Y // g x = h x} is an equalizer for the pair (g,h).

Equations

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

noncomputable def CategoryTheory.Limits.Types.equalizerIso {Y : Type u} {Z : Type u} (g : Y ⟶ Z) (h : Y ⟶ Z) : CategoryTheory.Limits.equalizer g h ≅ { x : Y // g x = h x }

The categorical equalizer in Type u is {x : Y // g x = h x}.

Equations

• CategoryTheory.Limits.Types.equalizerIso g h = CategoryTheory.Limits.limit.isoLimitCone CategoryTheory.Limits.Types.equalizerLimit

@[simp]

theorem CategoryTheory.Limits.Types.equalizerIso_hom_comp_subtype {Y : Type u} {Z : Type u} (g : Y ⟶ Z) (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.equalizerIso g h).hom Subtype.val = CategoryTheory.Limits.equalizer.ι g h

@[simp]

theorem CategoryTheory.Limits.Types.equalizerIso_inv_comp_ι_apply {Y : Type u} {Z : Type u} (g : Y ⟶ Z) (h : Y ⟶ Z) (x : CategoryTheory.Limits.Types.equalizerLimit.cone.pt) : CategoryTheory.Limits.limit.π (CategoryTheory.Limits.parallelPair g h) CategoryTheory.Limits.WalkingParallelPair.zero ((CategoryTheory.Limits.limit.isoLimitCone CategoryTheory.Limits.Types.equalizerLimit).inv x) = (CategoryTheory.Limits.Fork.ι CategoryTheory.Limits.Types.equalizerLimit.cone) x

@[simp]

theorem CategoryTheory.Limits.Types.equalizerIso_inv_comp_ι {Y : Type u} {Z : Type u} (g : Y ⟶ Z) (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.equalizerIso g h).inv (CategoryTheory.Limits.equalizer.ι g h) = Subtype.val

inductive CategoryTheory.Limits.Types.CoequalizerRel {X : Type u} {Y : Type u} (f : X ⟶ Y) (g : X ⟶ Y) : Y → Y → Prop

(Implementation) The relation to be quotiented to obtain the coequalizer.

• Rel: ∀ {X Y : Type u} {f g : X ⟶ Y} (x : X), CategoryTheory.Limits.Types.CoequalizerRel f g (f x) (g x)

def CategoryTheory.Limits.Types.coequalizerColimit {X : Type u} {Y : Type u} (f : X ⟶ Y) (g : X ⟶ Y) : CategoryTheory.Limits.ColimitCocone (CategoryTheory.Limits.parallelPair f g)

Show that the quotient by the relation generated by f(x) ~ g(x) is a coequalizer for the pair (f, g).

Equations

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

theorem CategoryTheory.Limits.Types.coequalizer_preimage_image_eq_of_preimage_eq {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Y) (g : X ⟶ Y) (π : Y ⟶ Z) (e : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π) (h : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ π e)) (U : Set Y) (H : f ⁻¹' U = g ⁻¹' U) : π ⁻¹' (π '' U) = U

If π : Y ⟶ Z is an equalizer for (f, g), and U ⊆ Y such that f ⁻¹' U = g ⁻¹' U, then π ⁻¹' (π '' U) = U.

noncomputable def CategoryTheory.Limits.Types.coequalizerIso {X : Type u} {Y : Type u} (f : X ⟶ Y) (g : X ⟶ Y) : CategoryTheory.Limits.coequalizer f g ≅ Quot (CategoryTheory.Limits.Types.CoequalizerRel f g)

The categorical coequalizer in Type u is the quotient by f g ~ g x.

Equations

• CategoryTheory.Limits.Types.coequalizerIso f g = CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.Limits.Types.coequalizerColimit f g)

@[simp]

theorem CategoryTheory.Limits.Types.coequalizerIso_π_comp_hom_apply {X : Type u} {Y : Type u} (f : X ⟶ Y) (g : X ⟶ Y) (x : (CategoryTheory.Limits.parallelPair f g).obj CategoryTheory.Limits.WalkingParallelPair.one) : (CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.Limits.Types.coequalizerColimit f g)).hom (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.parallelPair f g) CategoryTheory.Limits.WalkingParallelPair.one x) = (CategoryTheory.Limits.Cofork.π (CategoryTheory.Limits.Types.coequalizerColimit f g).cocone) x

@[simp]

theorem CategoryTheory.Limits.Types.coequalizerIso_π_comp_hom {X : Type u} {Y : Type u} (f : X ⟶ Y) (g : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g) (CategoryTheory.Limits.Types.coequalizerIso f g).hom = Quot.mk (CategoryTheory.Limits.Types.CoequalizerRel f g)

@[simp]

theorem CategoryTheory.Limits.Types.coequalizerIso_quot_comp_inv {X : Type u} {Y : Type u} (f : X ⟶ Y) (g : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.asHom (Quot.mk (CategoryTheory.Limits.Types.CoequalizerRel f g))) (CategoryTheory.Limits.Types.coequalizerIso f g).inv = CategoryTheory.Limits.coequalizer.π f g

instance CategoryTheory.Limits.Types.instHasPullbacksTypeTypes : CategoryTheory.Limits.HasPullbacks (Type u)

Equations

• CategoryTheory.Limits.Types.instHasPullbacksTypeTypes = ⋯

instance CategoryTheory.Limits.Types.instHasPushoutsTypeTypes : CategoryTheory.Limits.HasPushouts (Type u)

Equations

• CategoryTheory.Limits.Types.instHasPushoutsTypeTypes = ⋯

@[inline, reducible]

abbrev CategoryTheory.Limits.Types.PullbackObj {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : Type u

The usual explicit pullback in the category of types, as a subtype of the product. The full LimitCone data is bundled as pullbackLimitCone f g.

Equations

• CategoryTheory.Limits.Types.PullbackObj f g = { p : X × Y // f p.1 = g p.2 }

@[inline, reducible]

abbrev CategoryTheory.Limits.Types.pullbackCone {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.Limits.PullbackCone f g

The explicit pullback cone on PullbackObj f g. This is bundled with the IsLimit data as pullbackLimitCone f g.

Equations

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

@[simp]

theorem CategoryTheory.Limits.Types.pullbackLimitCone_cone {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : (CategoryTheory.Limits.Types.pullbackLimitCone f g).cone = CategoryTheory.Limits.Types.pullbackCone f g

@[simp]

theorem CategoryTheory.Limits.Types.pullbackLimitCone_isLimit {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : (CategoryTheory.Limits.Types.pullbackLimitCone f g).isLimit = CategoryTheory.Limits.PullbackCone.isLimitAux (CategoryTheory.Limits.Types.pullbackCone f g) (fun (s : CategoryTheory.Limits.PullbackCone f g) (x : s.pt) => { val := (CategoryTheory.Limits.PullbackCone.fst s x, CategoryTheory.Limits.PullbackCone.snd s x), property := ⋯ }) ⋯ ⋯ ⋯

def CategoryTheory.Limits.Types.pullbackLimitCone {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.cospan f g)

The explicit pullback in the category of types, bundled up as a LimitCone for given f and g.

Equations

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

noncomputable def CategoryTheory.Limits.Types.pullbackConeIsoPullback {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.cospan f g) ≅ CategoryTheory.Limits.Types.pullbackCone f g

The pullback cone given by the instance HasPullbacks (Type u) is isomorphic to the explicit pullback cone given by pullbackLimitCone.

Equations

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

noncomputable def CategoryTheory.Limits.Types.pullbackIsoPullback {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.Limits.pullback f g ≅ CategoryTheory.Limits.Types.PullbackObj f g

The pullback given by the instance HasPullbacks (Type u) is isomorphic to the explicit pullback object given by PullbackObj.

Equations

• CategoryTheory.Limits.Types.pullbackIsoPullback f g = (CategoryTheory.Limits.Cones.forget (CategoryTheory.Limits.cospan f g)).mapIso (CategoryTheory.Limits.Types.pullbackConeIsoPullback f g)

@[simp]

theorem CategoryTheory.Limits.Types.pullbackIsoPullback_hom_fst {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) (p : CategoryTheory.Limits.pullback f g) : (↑((CategoryTheory.Limits.Types.pullbackIsoPullback f g).hom p)).1 = CategoryTheory.Limits.pullback.fst p

@[simp]

theorem CategoryTheory.Limits.Types.pullbackIsoPullback_hom_snd {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) (p : CategoryTheory.Limits.pullback f g) : (↑((CategoryTheory.Limits.Types.pullbackIsoPullback f g).hom p)).2 = CategoryTheory.Limits.pullback.snd p

@[simp]

theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.pullbackIsoPullback f g).inv CategoryTheory.Limits.pullback.fst = fun (p : CategoryTheory.Limits.Types.PullbackObj f g) => (↑p).1

@[simp]

theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst_apply {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) (x : (CategoryTheory.Limits.Types.pullbackCone f g).pt) : CategoryTheory.Limits.pullback.fst ((CategoryTheory.Limits.Types.pullbackIsoPullback f g).inv x) = (fun (p : (CategoryTheory.Limits.Types.pullbackCone f g).pt) => (↑p).1) x

@[simp]

theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_snd {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.pullbackIsoPullback f g).inv CategoryTheory.Limits.pullback.snd = fun (p : CategoryTheory.Limits.Types.PullbackObj f g) => (↑p).2

@[simp]

theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_snd_apply {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) (x : (CategoryTheory.Limits.Types.pullbackCone f g).pt) : CategoryTheory.Limits.pullback.snd ((CategoryTheory.Limits.Types.pullbackIsoPullback f g).inv x) = (fun (p : (CategoryTheory.Limits.Types.pullbackCone f g).pt) => (↑p).2) x

inductive CategoryTheory.Limits.Types.Pushout.Rel {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : X₁ ⊕ X₂ → X₁ ⊕ X₂ → Prop

The pushout of two maps f : S ⟶ X₁ and g : S ⟶ X₂ is the quotient by the equivalence relation on X₁ ⊕ X₂ generated by this relation.

• inl_inr: ∀ {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} (s : S), CategoryTheory.Limits.Types.Pushout.Rel f g (Sum.inl (f s)) (Sum.inr (g s))

def CategoryTheory.Limits.Types.Pushout {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : Type u

Construction of the pushout in the category of types, as a quotient of X₁ ⊕ X₂.

Equations

• CategoryTheory.Limits.Types.Pushout f g = Quot (CategoryTheory.Limits.Types.Pushout.Rel f g)

inductive CategoryTheory.Limits.Types.Pushout.Rel' {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : X₁ ⊕ X₂ → X₁ ⊕ X₂ → Prop

In case f : S ⟶ X₁ is a monomorphism, this relation is the equivalence relation generated by Pushout.Rel f g.

• refl: ∀ {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} (x : X₁ ⊕ X₂), CategoryTheory.Limits.Types.Pushout.Rel' f g x x
• inl_inl: ∀ {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} (x₀ y₀ : S), g x₀ = g y₀ → CategoryTheory.Limits.Types.Pushout.Rel' f g (Sum.inl (f x₀)) (Sum.inl (f y₀))
• inl_inr: ∀ {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} (s : S), CategoryTheory.Limits.Types.Pushout.Rel' f g (Sum.inl (f s)) (Sum.inr (g s))
• inr_inl: ∀ {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} (s : S), CategoryTheory.Limits.Types.Pushout.Rel' f g (Sum.inr (g s)) (Sum.inl (f s))

def CategoryTheory.Limits.Types.Pushout' {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : Type u

The quotient of X₁ ⊕ X₂ by the relation PushoutRel' f g.

Equations

• CategoryTheory.Limits.Types.Pushout' f g = Quot (CategoryTheory.Limits.Types.Pushout.Rel' f g)

def CategoryTheory.Limits.Types.Pushout.inl {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : X₁ ⟶ CategoryTheory.Limits.Types.Pushout f g

The left inclusion in the constructed pushout Pushout f g.

Equations

• CategoryTheory.Limits.Types.Pushout.inl f g x = Quot.mk (CategoryTheory.Limits.Types.Pushout.Rel f g) (Sum.inl x)

def CategoryTheory.Limits.Types.Pushout.inr {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : X₂ ⟶ CategoryTheory.Limits.Types.Pushout f g

The right inclusion in the constructed pushout Pushout f g.

Equations

• CategoryTheory.Limits.Types.Pushout.inr f g x = Quot.mk (CategoryTheory.Limits.Types.Pushout.Rel f g) (Sum.inr x)

theorem CategoryTheory.Limits.Types.Pushout.condition {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Types.Pushout.inl f g) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.Types.Pushout.inr f g)

@[simp]

theorem CategoryTheory.Limits.Types.Pushout.cocone_ι_app {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) (j : CategoryTheory.Limits.WalkingSpan) : ∀ (a : (CategoryTheory.Limits.span f g).obj j), (CategoryTheory.Limits.Types.Pushout.cocone f g).ι.app j a = Option.rec (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Types.Pushout.inl f g)) (fun (val : CategoryTheory.Limits.WalkingPair) => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Limits.Types.Pushout.inl f g) (CategoryTheory.Limits.Types.Pushout.inr f g) val) j a

@[simp]

theorem CategoryTheory.Limits.Types.Pushout.cocone_pt {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : (CategoryTheory.Limits.Types.Pushout.cocone f g).pt = CategoryTheory.Limits.Types.Pushout f g

def CategoryTheory.Limits.Types.Pushout.cocone {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : CategoryTheory.Limits.PushoutCocone f g

The constructed pushout cocone in the category of types.

Equations

• CategoryTheory.Limits.Types.Pushout.cocone f g = CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.Limits.Types.Pushout.inl f g) (CategoryTheory.Limits.Types.Pushout.inr f g) ⋯

def CategoryTheory.Limits.Types.Pushout.isColimitCocone {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Types.Pushout.cocone f g)

The cocone cocone f g is colimit.

Equations

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

@[simp]

theorem CategoryTheory.Limits.Types.Pushout.inl_rel'_inl_iff {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) (x₁ : X₁) (y₁ : X₁) : CategoryTheory.Limits.Types.Pushout.Rel' f g (Sum.inl x₁) (Sum.inl y₁) ↔ x₁ = y₁ ∨ ∃ (x₀ : S) (y₀ : S) (_ : g x₀ = g y₀), x₁ = f x₀ ∧ y₁ = f y₀

@[simp]

theorem CategoryTheory.Limits.Types.Pushout.inl_rel'_inr_iff {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) (x₁ : X₁) (x₂ : X₂) : CategoryTheory.Limits.Types.Pushout.Rel' f g (Sum.inl x₁) (Sum.inr x₂) ↔ ∃ (s : S), x₁ = f s ∧ x₂ = g s

@[simp]

theorem CategoryTheory.Limits.Types.Pushout.inr_rel'_inr_iff {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) (x₂ : X₂) (y₂ : X₂) : CategoryTheory.Limits.Types.Pushout.Rel' f g (Sum.inr x₂) (Sum.inr y₂) ↔ x₂ = y₂

theorem CategoryTheory.Limits.Types.Pushout.Rel'.symm {S : Type u} {X₁ : Type u} {X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} {x : X₁ ⊕ X₂} {y : X₁ ⊕ X₂} (h : CategoryTheory.Limits.Types.Pushout.Rel' f g x y) : CategoryTheory.Limits.Types.Pushout.Rel' f g y x

theorem CategoryTheory.Limits.Types.Pushout.equivalence_rel' {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) [CategoryTheory.Mono f] : Equivalence (CategoryTheory.Limits.Types.Pushout.Rel' f g)

def CategoryTheory.Limits.Types.Pushout.equivPushout' {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) : CategoryTheory.Limits.Types.Pushout f g ≃ CategoryTheory.Limits.Types.Pushout' f g

The obvious equivalence Pushout f g ≃ Pushout' f g.

Equations

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

theorem CategoryTheory.Limits.Types.Pushout.quot_mk_eq_iff {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) [CategoryTheory.Mono f] (a : X₁ ⊕ X₂) (b : X₁ ⊕ X₂) : Quot.mk (CategoryTheory.Limits.Types.Pushout.Rel f g) a = Quot.mk (CategoryTheory.Limits.Types.Pushout.Rel f g) b ↔ CategoryTheory.Limits.Types.Pushout.Rel' f g a b

theorem CategoryTheory.Limits.Types.Pushout.inl_eq_inr_iff {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) [CategoryTheory.Mono f] (x₁ : X₁) (x₂ : X₂) : CategoryTheory.Limits.Types.Pushout.inl f g x₁ = CategoryTheory.Limits.Types.Pushout.inr f g x₂ ↔ ∃ (s : S), f s = x₁ ∧ g s = x₂

theorem CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_imp_of_iso {S : Type u} {X₁ : Type u} {X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} {c : CategoryTheory.Limits.PushoutCocone f g} {c' : CategoryTheory.Limits.PushoutCocone f g} (e : c ≅ c') (x₁ : X₁) (x₂ : X₂) (h : CategoryTheory.Limits.PushoutCocone.inl c x₁ = CategoryTheory.Limits.PushoutCocone.inr c x₂) : CategoryTheory.Limits.PushoutCocone.inl c' x₁ = CategoryTheory.Limits.PushoutCocone.inr c' x₂

theorem CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_iff_of_iso {S : Type u} {X₁ : Type u} {X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} {c : CategoryTheory.Limits.PushoutCocone f g} {c' : CategoryTheory.Limits.PushoutCocone f g} (e : c ≅ c') (x₁ : X₁) (x₂ : X₂) : CategoryTheory.Limits.PushoutCocone.inl c x₁ = CategoryTheory.Limits.PushoutCocone.inr c x₂ ↔ CategoryTheory.Limits.PushoutCocone.inl c' x₁ = CategoryTheory.Limits.PushoutCocone.inr c' x₂

theorem CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_iff_of_isColimit {S : Type u} {X₁ : Type u} {X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} {c : CategoryTheory.Limits.PushoutCocone f g} (hc : CategoryTheory.Limits.IsColimit c) (h₁ : Function.Injective f) (x₁ : X₁) (x₂ : X₂) : CategoryTheory.Limits.PushoutCocone.inl c x₁ = CategoryTheory.Limits.PushoutCocone.inr c x₂ ↔ ∃ (s : S), f s = x₁ ∧ g s = x₂