A structure to describe transfinite compositions

Given a well-ordered type J and a morphism f : X ⟶ Y in a category, we introduce a structure TransfiniteCompositionOfShape J f expressing that f is a transfinite composition of shape J. This allows to extend this structure in order to require more properties or data for the morphisms F.obj j ⟶ F.obj (Order.succ j) which appear in the transfinite composition. See MorphismProperty.TransfiniteCompositionOfShape in the file MorphismProperty.TransfiniteComposition.

structure CategoryTheory.TransfiniteCompositionOfShape {C : Type u} [Category.{v, u} C] (J : Type w) [LinearOrder J] [OrderBot J] {X Y : C} (f : X ⟶ Y) [SuccOrder J] [WellFoundedLT J] : Type (max (max u v) w)

Given a well-ordered type J, a morphism f : X ⟶ Y in a category C is a transfinite composition of shape J if we have a well order continuous functor F : J ⥤ C, an isomorphism F.obj ⊥ ≅ X, a colimit cocone for F whose point is Y, such that the composition X ⟶ F.obj ⊥ ⟶ Y is f.

• F : Functor J C

  a well order continuous functor F : J ⥤ C

• isoBot : self.F.obj ⊥ ≅ X

  the isomorphism F.obj ⊥ ≅ X

• isWellOrderContinuous : self.F.IsWellOrderContinuous
• incl : self.F ⟶ (Functor.const J).obj Y

  the natural morphism F.obj j ⟶ Y

• isColimit : Limits.IsColimit { pt := Y, ι := self.incl }

  the colimit of F identifies to Y

• fac : CategoryStruct.comp self.isoBot.inv (self.incl.app ⊥) = f

@[simp]

theorem CategoryTheory.TransfiniteCompositionOfShape.fac_assoc {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (self : TransfiniteCompositionOfShape J f) {Z : C} (h : ((Functor.const J).obj Y).obj ⊥ ⟶ Z) : CategoryStruct.comp self.isoBot.inv (CategoryStruct.comp (self.incl.app ⊥) h) = CategoryStruct.comp f h

def CategoryTheory.TransfiniteCompositionOfShape.ofArrowIso {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) {X' Y' : C} {f' : X' ⟶ Y'} (e : Arrow.mk f ≅ Arrow.mk f') : TransfiniteCompositionOfShape J f'

If f and f' are two isomorphic morphisms, and f is a transfinite composition of shape J, then f' also is.

Equations

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

@[simp]

theorem CategoryTheory.TransfiniteCompositionOfShape.ofArrowIso_isColimit {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) {X' Y' : C} {f' : X' ⟶ Y'} (e : Arrow.mk f ≅ Arrow.mk f') : (c.ofArrowIso e).isColimit = c.isColimit.ofIsoColimit (Limits.Cocones.ext (Arrow.rightFunc.mapIso e) ⋯)

@[simp]

theorem CategoryTheory.TransfiniteCompositionOfShape.ofArrowIso_F {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) {X' Y' : C} {f' : X' ⟶ Y'} (e : Arrow.mk f ≅ Arrow.mk f') : (c.ofArrowIso e).F = c.F

@[simp]

theorem CategoryTheory.TransfiniteCompositionOfShape.ofArrowIso_incl {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) {X' Y' : C} {f' : X' ⟶ Y'} (e : Arrow.mk f ≅ Arrow.mk f') : (c.ofArrowIso e).incl = CategoryStruct.comp c.incl ((Functor.const J).map e.hom.right)

@[simp]

theorem CategoryTheory.TransfiniteCompositionOfShape.ofArrowIso_isoBot {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) {X' Y' : C} {f' : X' ⟶ Y'} (e : Arrow.mk f ≅ Arrow.mk f') : (c.ofArrowIso e).isoBot = c.isoBot ≪≫ Arrow.leftFunc.mapIso e

def CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows {C : Type u} [Category.{v, u} C] {n : ℕ} (G : ComposableArrows C n) : TransfiniteCompositionOfShape (Fin (n + 1)) G.hom

If G : ComposableArrows C n, then G.hom : G.left ⟶ G.right is a transfinite composition of shape Fin (n + 1).

Equations

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

@[simp]

theorem CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isColimit {C : Type u} [Category.{v, u} C] {n : ℕ} (G : ComposableArrows C n) : (ofComposableArrows G).isColimit = Limits.colimitOfDiagramTerminal (Fin.isTerminalLast n) G

@[simp]

theorem CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_incl_app {C : Type u} [Category.{v, u} C] {n : ℕ} (G : ComposableArrows C n) (j : Fin (n + 1)) : (ofComposableArrows G).incl.app j = G.map ((Fin.isTerminalLast n).from j)

@[simp]

theorem CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isoBot {C : Type u} [Category.{v, u} C] {n : ℕ} (G : ComposableArrows C n) : (ofComposableArrows G).isoBot = Iso.refl (G.obj ⊥)

@[simp]

theorem CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_F {C : Type u} [Category.{v, u} C] {n : ℕ} (G : ComposableArrows C n) : (ofComposableArrows G).F = G

def CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) {J' : Type w'} [LinearOrder J'] [OrderBot J'] [SuccOrder J'] [WellFoundedLT J'] (e : J' ≃o J) : TransfiniteCompositionOfShape J' f

If f is a transfinite composition of shape J, then it is also a transfinite composition of shape J' if J' ≃o J.

Equations

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

@[simp]

theorem CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso_isColimit {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) {J' : Type w'} [LinearOrder J'] [OrderBot J'] [SuccOrder J'] [WellFoundedLT J'] (e : J' ≃o J) : (c.ofOrderIso e).isColimit = c.isColimit.whiskerEquivalence e.equivalence

@[simp]

theorem CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso_isoBot {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) {J' : Type w'} [LinearOrder J'] [OrderBot J'] [SuccOrder J'] [WellFoundedLT J'] (e : J' ≃o J) : (c.ofOrderIso e).isoBot = c.F.mapIso (eqToIso ⋯) ≪≫ c.isoBot

@[simp]

theorem CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso_incl {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) {J' : Type w'} [LinearOrder J'] [OrderBot J'] [SuccOrder J'] [WellFoundedLT J'] (e : J' ≃o J) : (c.ofOrderIso e).incl = whiskerLeft e.equivalence.functor c.incl

@[simp]

theorem CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso_F {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) {J' : Type w'} [LinearOrder J'] [OrderBot J'] [SuccOrder J'] [WellFoundedLT J'] (e : J' ≃o J) : (c.ofOrderIso e).F = e.equivalence.functor.comp c.F

noncomputable def CategoryTheory.TransfiniteCompositionOfShape.map {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) (F : Functor C D) [Limits.PreservesWellOrderContinuousOfShape J F] [Limits.PreservesColimitsOfShape J F] : TransfiniteCompositionOfShape J (F.map f)

If f is a transfinite composition of shape J, then F.map f also is provided F preserves suitable colimits.

Equations

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

@[simp]

theorem CategoryTheory.TransfiniteCompositionOfShape.map_incl {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) (F : Functor C D) [Limits.PreservesWellOrderContinuousOfShape J F] [Limits.PreservesColimitsOfShape J F] : (c.map F).incl = CategoryStruct.comp (whiskerRight c.incl F) (Functor.constComp J Y F).hom

@[simp]

theorem CategoryTheory.TransfiniteCompositionOfShape.map_isoBot {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) (F : Functor C D) [Limits.PreservesWellOrderContinuousOfShape J F] [Limits.PreservesColimitsOfShape J F] : (c.map F).isoBot = F.mapIso c.isoBot

@[simp]

theorem CategoryTheory.TransfiniteCompositionOfShape.map_F {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) (F : Functor C D) [Limits.PreservesWellOrderContinuousOfShape J F] [Limits.PreservesColimitsOfShape J F] : (c.map F).F = c.F.comp F

@[simp]

theorem CategoryTheory.TransfiniteCompositionOfShape.map_isColimit {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) (F : Functor C D) [Limits.PreservesWellOrderContinuousOfShape J F] [Limits.PreservesColimitsOfShape J F] : (c.map F).isColimit = (Limits.isColimitOfPreserves F c.isColimit).ofIsoColimit (Limits.Cocones.ext (Iso.refl (F.mapCocone { pt := Y, ι := c.incl }).pt) ⋯)

def CategoryTheory.TransfiniteCompositionOfShape.iic {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] [OrderBot J] {X Y : C} {f : X ⟶ Y} [SuccOrder J] [WellFoundedLT J] (c : TransfiniteCompositionOfShape J f) (j : J) : TransfiniteCompositionOfShape (↑(Set.Iic j)) (c.F.map (homOfLE ⋯))

A transfinite composition of shape J induces a transfinite composition of shape Set.Iic j for any j : J.

Equations

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