The factorization axiom #
In this file, we introduce a type-class HasFactorization W₁ W₂, which, given
two classes of morphisms W₁ and W₂ in a category C, asserts that any morphism
in C can be factored as a morphism in W₁ followed by a morphism in W₂. The data
of such factorizations can be packaged in the type FactorizationData W₁ W₂.
This shall be used in the formalization of model categories for which the CM5 axiom asserts that any morphism can be factored as a cofibration followed by a trivial fibration (or a trivial cofibration followed by a fibration).
We also provide a structure FunctorialFactorizationData W₁ W₂ which contains
the data of a functorial factorization as above. With this design, when we
formalize certain constructions (e.g. cylinder objects in model categories),
we may first construct them using using data : FactorizationData W₁ W₂.
Without duplication of code, it shall be possible to show these cylinders
are functorial when a term data : FunctorialFactorizationData W₁ W₂ is available,
the existence of which is asserted in the type-class HasFunctorialFactorization W₁ W₂.
We also introduce the class W₁.comp W₂ of morphisms of the form i ≫ p with W₁ i
and W₂ p and show that W₁.comp W₂ = ⊤ iff HasFactorization W₁ W₂ holds (this
is MorphismProperty.comp_eq_top_iff).
structure
CategoryTheory.MorphismProperty.MapFactorizationData
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
(W₁ : CategoryTheory.MorphismProperty C)
(W₂ : CategoryTheory.MorphismProperty C)
{X : C}
{Y : C}
(f : X ⟶ Y)
:
Type (max u_1 u_2)
Given two classes of morphisms W₁ and W₂ on a category C, this is
the data of the factorization of a morphism f : X ⟶ Y as i ≫ p with
W₁ i and W₂ p.
- Z : C
the intermediate object in the factorization
- i : X ⟶ self.Z
the first morphism in the factorization
- p : self.Z ⟶ Y
the second morphism in the factorization
- fac : CategoryTheory.CategoryStruct.comp self.i self.p = f
- hi : W₁ self.i
- hp : W₂ self.p
Instances For
@[simp]
theorem
CategoryTheory.MorphismProperty.MapFactorizationData.fac
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
{f : X ⟶ Y}
(self : W₁.MapFactorizationData W₂ f)
:
CategoryTheory.CategoryStruct.comp self.i self.p = f
theorem
CategoryTheory.MorphismProperty.MapFactorizationData.hi
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
{f : X ⟶ Y}
(self : W₁.MapFactorizationData W₂ f)
:
W₁ self.i
theorem
CategoryTheory.MorphismProperty.MapFactorizationData.hp
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
{f : X ⟶ Y}
(self : W₁.MapFactorizationData W₂ f)
:
W₂ self.p
@[simp]
theorem
CategoryTheory.MorphismProperty.MapFactorizationData.fac_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
{X : C}
{Y : C}
{f : X ⟶ Y}
(self : W₁.MapFactorizationData W₂ f)
{Z : C}
(h : Y ⟶ Z)
:
@[reducible, inline]
abbrev
CategoryTheory.MorphismProperty.FactorizationData
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
(W₁ : CategoryTheory.MorphismProperty C)
(W₂ : CategoryTheory.MorphismProperty C)
:
Type (max u_1 u_2)
The data of a term in MapFactorizationData W₁ W₂ f for any morphism f.
Instances For
class
CategoryTheory.MorphismProperty.HasFactorization
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
(W₁ : CategoryTheory.MorphismProperty C)
(W₂ : CategoryTheory.MorphismProperty C)
:
The factorization axiom for two classes of morphisms W₁ and W₂ in a category C. It
asserts that any morphism can be factored as a morphism in W₁ followed by a morphism
in W₂.
Instances
theorem
CategoryTheory.MorphismProperty.HasFactorization.nonempty_mapFactorizationData
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
[self : W₁.HasFactorization W₂]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
Nonempty (W₁.MapFactorizationData W₂ f)
noncomputable def
CategoryTheory.MorphismProperty.factorizationData
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
(W₁ : CategoryTheory.MorphismProperty C)
(W₂ : CategoryTheory.MorphismProperty C)
[W₁.HasFactorization W₂]
:
W₁.FactorizationData W₂
A chosen term in FactorizationData W₁ W₂ when HasFactorization W₁ W₂ holds.
Equations
- W₁.factorizationData W₂ x = ⋯.some
Instances For
def
CategoryTheory.MorphismProperty.comp
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
(W₁ : CategoryTheory.MorphismProperty C)
(W₂ : CategoryTheory.MorphismProperty C)
:
The class of morphisms that are of the form i ≫ p with W₁ i and W₂ p.
Instances For
theorem
CategoryTheory.MorphismProperty.comp_eq_top_iff
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
(W₁ : CategoryTheory.MorphismProperty C)
(W₂ : CategoryTheory.MorphismProperty C)
:
structure
CategoryTheory.MorphismProperty.FunctorialFactorizationData
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
(W₁ : CategoryTheory.MorphismProperty C)
(W₂ : CategoryTheory.MorphismProperty C)
:
Type (max u_1 u_2)
The data of a functorial factorization of any morphism in C as a morphism in W₁
followed by a morphism in W₂.
- Z : CategoryTheory.Functor (CategoryTheory.Arrow C) C
the intermediate objects in the factorizations
- i : CategoryTheory.Arrow.leftFunc ⟶ self.Z
the first morphism in the factorizations
- p : self.Z ⟶ CategoryTheory.Arrow.rightFunc
the second morphism in the factorizations
- fac : CategoryTheory.CategoryStruct.comp self.i self.p = CategoryTheory.Arrow.leftToRight
- hi : ∀ (f : CategoryTheory.Arrow C), W₁ (self.i.app f)
- hp : ∀ (f : CategoryTheory.Arrow C), W₂ (self.p.app f)
Instances For
@[simp]
theorem
CategoryTheory.MorphismProperty.FunctorialFactorizationData.fac
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
(self : W₁.FunctorialFactorizationData W₂)
:
CategoryTheory.CategoryStruct.comp self.i self.p = CategoryTheory.Arrow.leftToRight
theorem
CategoryTheory.MorphismProperty.FunctorialFactorizationData.hi
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
(self : W₁.FunctorialFactorizationData W₂)
(f : CategoryTheory.Arrow C)
:
W₁ (self.i.app f)
theorem
CategoryTheory.MorphismProperty.FunctorialFactorizationData.hp
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
(self : W₁.FunctorialFactorizationData W₂)
(f : CategoryTheory.Arrow C)
:
W₂ (self.p.app f)
@[simp]
theorem
CategoryTheory.MorphismProperty.FunctorialFactorizationData.fac_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
(self : W₁.FunctorialFactorizationData W₂)
{Z : CategoryTheory.Functor (CategoryTheory.Arrow C) C}
(h : CategoryTheory.Arrow.rightFunc ⟶ Z)
:
CategoryTheory.CategoryStruct.comp self.i (CategoryTheory.CategoryStruct.comp self.p h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Arrow.leftToRight h
@[simp]
theorem
CategoryTheory.MorphismProperty.FunctorialFactorizationData.fac_app_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
(data : W₁.FunctorialFactorizationData W₂)
{f : CategoryTheory.Arrow C}
{Z : C}
(h : CategoryTheory.Arrow.rightFunc.obj f ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (data.i.app f) (CategoryTheory.CategoryStruct.comp (data.p.app f) h) = CategoryTheory.CategoryStruct.comp f.hom h
@[simp]
theorem
CategoryTheory.MorphismProperty.FunctorialFactorizationData.fac_app
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
(data : W₁.FunctorialFactorizationData W₂)
{f : CategoryTheory.Arrow C}
:
CategoryTheory.CategoryStruct.comp (data.i.app f) (data.p.app f) = f.hom
def
CategoryTheory.MorphismProperty.FunctorialFactorizationData.ofLE
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
(data : W₁.FunctorialFactorizationData W₂)
{W₁' : CategoryTheory.MorphismProperty C}
{W₂' : CategoryTheory.MorphismProperty C}
(le₁ : W₁ ≤ W₁')
(le₂ : W₂ ≤ W₂')
:
W₁'.FunctorialFactorizationData W₂'
If W₁ ≤ W₁' and W₂ ≤ W₂', then a functorial factorization for W₁ and W₂ induces
a functorial factorization for W₁' and W₂'.
Equations
- data.ofLE le₁ le₂ = { Z := data.Z, i := data.i, p := data.p, fac := ⋯, hi := ⋯, hp := ⋯ }
Instances For
def
CategoryTheory.MorphismProperty.FunctorialFactorizationData.factorizationData
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
(data : W₁.FunctorialFactorizationData W₂)
:
W₁.FactorizationData W₂
The term in FactorizationData W₁ W₂ that is deduced from a functorial factorization.
Equations
- data.factorizationData f = { Z := data.Z.obj (CategoryTheory.Arrow.mk f), i := data.i.app (CategoryTheory.Arrow.mk f), p := data.p.app (CategoryTheory.Arrow.mk f), fac := ⋯, hi := ⋯, hp := ⋯ }
Instances For
def
CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
(data : W₁.FunctorialFactorizationData W₂)
{X : C}
{Y : C}
{X' : C}
{Y' : C}
{f : X ⟶ Y}
{g : X' ⟶ Y'}
(φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g)
:
(data.factorizationData f).Z ⟶ (data.factorizationData g).Z
When data : FunctorialFactorizationData W₁ W₂, this is the
morphism (data.factorizationData f).Z ⟶ (data.factorizationData g).Z expressing the
functoriality of the intermediate objects of the factorizations
for φ : Arrow.mk f ⟶ Arrow.mk g.
Equations
- data.mapZ φ = data.Z.map φ
Instances For
@[simp]
theorem
CategoryTheory.MorphismProperty.FunctorialFactorizationData.i_mapZ_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
(data : W₁.FunctorialFactorizationData W₂)
{X : C}
{Y : C}
{X' : C}
{Y' : C}
{f : X ⟶ Y}
{g : X' ⟶ Y'}
(φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g)
{Z : C}
(h : (data.factorizationData g).Z ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (data.factorizationData f).i (CategoryTheory.CategoryStruct.comp (data.mapZ φ) h) = CategoryTheory.CategoryStruct.comp φ.left (CategoryTheory.CategoryStruct.comp (data.factorizationData g).i h)
@[simp]
theorem
CategoryTheory.MorphismProperty.FunctorialFactorizationData.i_mapZ
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
(data : W₁.FunctorialFactorizationData W₂)
{X : C}
{Y : C}
{X' : C}
{Y' : C}
{f : X ⟶ Y}
{g : X' ⟶ Y'}
(φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g)
:
CategoryTheory.CategoryStruct.comp (data.factorizationData f).i (data.mapZ φ) = CategoryTheory.CategoryStruct.comp φ.left (data.factorizationData g).i
@[simp]
theorem
CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_p_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
(data : W₁.FunctorialFactorizationData W₂)
{X : C}
{Y : C}
{X' : C}
{Y' : C}
{f : X ⟶ Y}
{g : X' ⟶ Y'}
(φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g)
{Z : C}
(h : Y' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (data.mapZ φ) (CategoryTheory.CategoryStruct.comp (data.factorizationData g).p h) = CategoryTheory.CategoryStruct.comp (data.factorizationData f).p (CategoryTheory.CategoryStruct.comp φ.right h)
@[simp]
theorem
CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_p
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
(data : W₁.FunctorialFactorizationData W₂)
{X : C}
{Y : C}
{X' : C}
{Y' : C}
{f : X ⟶ Y}
{g : X' ⟶ Y'}
(φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g)
:
CategoryTheory.CategoryStruct.comp (data.mapZ φ) (data.factorizationData g).p = CategoryTheory.CategoryStruct.comp (data.factorizationData f).p φ.right
@[simp]
theorem
CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_id
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
(data : W₁.FunctorialFactorizationData W₂)
{X : C}
{Y : C}
(f : X ⟶ Y)
:
data.mapZ (CategoryTheory.CategoryStruct.id (CategoryTheory.Arrow.mk f)) = CategoryTheory.CategoryStruct.id (data.factorizationData f).Z
theorem
CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_comp_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
(data : W₁.FunctorialFactorizationData W₂)
{X : C}
{Y : C}
{X' : C}
{Y' : C}
{f : X ⟶ Y}
{g : X' ⟶ Y'}
(φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g)
{X'' : C}
{Y'' : C}
{h : X'' ⟶ Y''}
(ψ : CategoryTheory.Arrow.mk g ⟶ CategoryTheory.Arrow.mk h✝)
{Z : C}
(h : (data.factorizationData h✝).Z ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (data.mapZ (CategoryTheory.CategoryStruct.comp φ ψ)) h = CategoryTheory.CategoryStruct.comp (data.mapZ φ) (CategoryTheory.CategoryStruct.comp (data.mapZ ψ) h)
@[simp]
theorem
CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_comp
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
(data : W₁.FunctorialFactorizationData W₂)
{X : C}
{Y : C}
{X' : C}
{Y' : C}
{f : X ⟶ Y}
{g : X' ⟶ Y'}
(φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g)
{X'' : C}
{Y'' : C}
{h : X'' ⟶ Y''}
(ψ : CategoryTheory.Arrow.mk g ⟶ CategoryTheory.Arrow.mk h)
:
data.mapZ (CategoryTheory.CategoryStruct.comp φ ψ) = CategoryTheory.CategoryStruct.comp (data.mapZ φ) (data.mapZ ψ)
@[simp]
theorem
CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z_map_app
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
(data : W₁.FunctorialFactorizationData W₂)
(J : Type u_2)
[CategoryTheory.Category.{u_4, u_2} J]
:
∀ {X Y : CategoryTheory.Arrow (CategoryTheory.Functor J C)} (τ : X ⟶ Y) (j : J),
((CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z data J).map τ).app j = data.mapZ { left := τ.left.app j, right := τ.right.app j, w := ⋯ }
@[simp]
theorem
CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z_obj_obj
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
(data : W₁.FunctorialFactorizationData W₂)
(J : Type u_2)
[CategoryTheory.Category.{u_4, u_2} J]
(f : CategoryTheory.Arrow (CategoryTheory.Functor J C))
(j : J)
:
((CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z data J).obj f).obj j = (data.factorizationData (f.hom.app j)).Z
@[simp]
theorem
CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z_obj_map
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
(data : W₁.FunctorialFactorizationData W₂)
(J : Type u_2)
[CategoryTheory.Category.{u_4, u_2} J]
(f : CategoryTheory.Arrow (CategoryTheory.Functor J C))
:
∀ {X Y : J} (φ : X ⟶ Y),
((CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z data J).obj f).map φ = data.mapZ { left := f.left.map φ, right := f.right.map φ, w := ⋯ }
def
CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
(data : W₁.FunctorialFactorizationData W₂)
(J : Type u_2)
[CategoryTheory.Category.{u_4, u_2} J]
:
Auxiliary definition for FunctorialFactorizationData.functorCategory.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
(data : W₁.FunctorialFactorizationData W₂)
(J : Type u_2)
[CategoryTheory.Category.{u_4, u_2} J]
:
(W₁.functorCategory J).FunctorialFactorizationData (W₂.functorCategory J)
A functorial factorization in the category C extends to the functor category J ⥤ C.
Equations
- One or more equations did not get rendered due to their size.
Instances For
class
CategoryTheory.MorphismProperty.HasFunctorialFactorization
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
(W₁ : CategoryTheory.MorphismProperty C)
(W₂ : CategoryTheory.MorphismProperty C)
:
The functorial factorization axiom for two classes of morphisms W₁ and W₂ in a
category C. It asserts that any morphism can be factored in a functorial manner
as a morphism in W₁ followed by a morphism in W₂.
- nonempty_functorialFactorizationData : Nonempty (W₁.FunctorialFactorizationData W₂)
Instances
theorem
CategoryTheory.MorphismProperty.HasFunctorialFactorization.nonempty_functorialFactorizationData
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W₁ : CategoryTheory.MorphismProperty C}
{W₂ : CategoryTheory.MorphismProperty C}
[self : W₁.HasFunctorialFactorization W₂]
:
Nonempty (W₁.FunctorialFactorizationData W₂)
noncomputable def
CategoryTheory.MorphismProperty.functorialFactorizationData
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
(W₁ : CategoryTheory.MorphismProperty C)
(W₂ : CategoryTheory.MorphismProperty C)
[W₁.HasFunctorialFactorization W₂]
:
W₁.FunctorialFactorizationData W₂
A chosen term in FunctorialFactorizationData W₁ W₂ when the functorial factorization
axiom HasFunctorialFactorization W₁ W₂ holds.
Equations
- W₁.functorialFactorizationData W₂ = ⋯.some
Instances For
instance
CategoryTheory.MorphismProperty.instHasFactorizationOfHasFunctorialFactorization
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
(W₁ : CategoryTheory.MorphismProperty C)
(W₂ : CategoryTheory.MorphismProperty C)
[W₁.HasFunctorialFactorization W₂]
:
W₁.HasFactorization W₂
Equations
- ⋯ = ⋯
instance
CategoryTheory.MorphismProperty.instHasFunctorialFactorizationFunctorFunctorCategory
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
(W₁ : CategoryTheory.MorphismProperty C)
(W₂ : CategoryTheory.MorphismProperty C)
[W₁.HasFunctorialFactorization W₂]
(J : Type u_2)
[CategoryTheory.Category.{u_4, u_2} J]
:
(W₁.functorCategory J).HasFunctorialFactorization (W₂.functorCategory J)
Equations
- ⋯ = ⋯