Factorization

📁 Source: Mathlib/CategoryTheory/MorphismProperty/Factorization.lean

Statistics

Metric	Count
Definitions FactorizationData, FunctorialFactorizationData, Z, factorizationData, functorCategory, Z, i, mapZ, ofLE, p, HasFactorization, HasFunctorialFactorization, MapFactorizationData, Z, i, op, p, comp, factorizationData, functorialFactorizationData	20
Theorems fac, fac_app, fac_app_assoc, fac_assoc, Z_map_app, Z_obj_map, Z_obj_obj, hi, hp, i_mapZ, i_mapZ_assoc, mapZ_comp, mapZ_comp_assoc, mapZ_id, mapZ_p, mapZ_p_assoc, nonempty_mapFactorizationData, nonempty_functorialFactorizationData, fac, fac_assoc, hi, hp, op_Z, op_i, op_p, comp_eq_top_iff, instHasFactorizationOfHasFunctorialFactorization, instHasFactorizationOppositeOp, instHasFunctorialFactorizationFunctorFunctorCategory	29
Total	49

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
FactorizationData 📖	CompOp	—
FunctorialFactorizationData 📖	CompData	1 math math: HasFunctorialFactorization.nonempty_functorialFactorizationData
HasFactorization 📖	CompData	12 math math: comp_eq_top_iff, HasFactorization.over, HomotopicalAlgebra.instHasFactorizationOppositeCofibrationsTrivialFibrationsOfTrivialCofibrationsFibrations, instHasFactorizationOppositeOp, HomotopicalAlgebra.instHasFactorizationOppositeTrivialCofibrationsFibrationsOfCofibrationsTrivialFibrations, IsWeakFactorizationSystem.hasFactorization, HomotopicalAlgebra.ModelCategory.cm5b, HomotopicalAlgebra.ModelCategory.cm5a, HomotopicalAlgebra.instHasFactorizationOverTrivialCofibrationsFibrations, HomotopicalAlgebra.instHasFactorizationOverCofibrationsTrivialFibrations, instHasFactorizationOfHasFunctorialFactorization, SimplexCategoryGenRel.instHasFactorizationP_σP_δ
HasFunctorialFactorization 📖	CompData	5 math math: CategoryTheory.SmallObject.hasFunctorialFactorization, CategoryTheory.Sheaf.instHasFunctorialFactorizationLocallySurjectiveLocallyInjective, instHasFunctorialFactorizationLlpRlp, instHasFunctorialFactorizationFunctorFunctorCategory, CategoryTheory.IsGrothendieckAbelian.instHasFunctorialFactorizationMonomorphismsRlp
MapFactorizationData 📖	CompData	1 math math: HasFactorization.nonempty_mapFactorizationData
comp 📖	CompOp	1 math math: comp_eq_top_iff
factorizationData 📖	CompOp	—
functorialFactorizationData 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_eq_top_iff 📖	mathematical	—	comp Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra instCompleteBooleanAlgebra HasFactorization	—	ext
instHasFactorizationOfHasFunctorialFactorization 📖	mathematical	—	HasFactorization	—	—
instHasFactorizationOppositeOp 📖	mathematical	—	HasFactorization Opposite CategoryTheory.Category.opposite op CategoryTheory.Category.toCategoryStruct	—	—
instHasFunctorialFactorizationFunctorFunctorCategory 📖	mathematical	—	HasFunctorialFactorization CategoryTheory.Functor CategoryTheory.Functor.category functorCategory	—	—

CategoryTheory.MorphismProperty.FunctorialFactorizationData

Definitions

Name	Category	Theorems
Z 📖	CompOp	12 math math: CategoryTheory.Sheaf.instIsLocallySurjectiveAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization, hi, fac, CategoryTheory.SmallObject.functorialFactorizationData_Z_obj, CategoryTheory.Sheaf.instMonoAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization, CategoryTheory.SmallObject.functorialFactorizationData_Z_map, CategoryTheory.Sheaf.instIsLocallyInjectiveAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization, fac_app, fac_assoc, hp, fac_app_assoc, CategoryTheory.Sheaf.instEpiAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization
factorizationData 📖	CompOp	9 math math: mapZ_p, i_mapZ_assoc, functorCategory.Z_map_app, i_mapZ, functorCategory.Z_obj_obj, mapZ_p_assoc, mapZ_comp, mapZ_comp_assoc, mapZ_id
functorCategory 📖	CompOp	—
i 📖	CompOp	8 math math: CategoryTheory.Sheaf.instIsLocallySurjectiveAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization, hi, fac, CategoryTheory.SmallObject.functorialFactorizationData_i_app, fac_app, fac_assoc, fac_app_assoc, CategoryTheory.Sheaf.instEpiAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization
mapZ 📖	CompOp	9 math math: mapZ_p, i_mapZ_assoc, functorCategory.Z_map_app, functorCategory.Z_obj_map, i_mapZ, mapZ_p_assoc, mapZ_comp, mapZ_comp_assoc, mapZ_id
ofLE 📖	CompOp	—
p 📖	CompOp	8 math math: fac, CategoryTheory.Sheaf.instMonoAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization, CategoryTheory.Sheaf.instIsLocallyInjectiveAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization, fac_app, CategoryTheory.SmallObject.functorialFactorizationData_p_app, fac_assoc, hp, fac_app_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Arrow.leftFunc Z CategoryTheory.Arrow.rightFunc i p CategoryTheory.Arrow.leftToRight	—	—
fac_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Arrow.leftFunc Z CategoryTheory.Arrow.rightFunc CategoryTheory.NatTrans.app i p CategoryTheory.Comma.hom CategoryTheory.Functor.id	—	CategoryTheory.NatTrans.comp_app fac CategoryTheory.Arrow.leftToRight_app
fac_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Arrow.leftFunc Z CategoryTheory.NatTrans.app i CategoryTheory.Arrow.rightFunc p CategoryTheory.Comma.hom CategoryTheory.Functor.id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fac_app
fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Arrow.leftFunc Z i CategoryTheory.Arrow.rightFunc p CategoryTheory.Arrow.leftToRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fac
hi 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Arrow.leftFunc Z CategoryTheory.NatTrans.app i	—	—
hp 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow Z CategoryTheory.Arrow.rightFunc CategoryTheory.NatTrans.app p	—	—
i_mapZ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MorphismProperty.MapFactorizationData.Z factorizationData CategoryTheory.MorphismProperty.MapFactorizationData.i mapZ CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.CommaMorphism.left	—	CategoryTheory.NatTrans.naturality
i_mapZ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MorphismProperty.MapFactorizationData.Z factorizationData CategoryTheory.MorphismProperty.MapFactorizationData.i mapZ CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.CommaMorphism.left	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' i_mapZ
mapZ_comp 📖	mathematical	—	mapZ CategoryTheory.CategoryStruct.comp CategoryTheory.Arrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryArrow CategoryTheory.MorphismProperty.MapFactorizationData.Z factorizationData	—	CategoryTheory.Functor.map_comp
mapZ_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MorphismProperty.MapFactorizationData.Z factorizationData mapZ CategoryTheory.Arrow CategoryTheory.instCategoryArrow	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapZ_comp
mapZ_id 📖	mathematical	—	mapZ CategoryTheory.CategoryStruct.id CategoryTheory.Arrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryArrow CategoryTheory.MorphismProperty.MapFactorizationData.Z factorizationData	—	CategoryTheory.Functor.map_id
mapZ_p 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MorphismProperty.MapFactorizationData.Z factorizationData mapZ CategoryTheory.MorphismProperty.MapFactorizationData.p CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right	—	CategoryTheory.NatTrans.naturality
mapZ_p_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MorphismProperty.MapFactorizationData.Z factorizationData mapZ CategoryTheory.MorphismProperty.MapFactorizationData.p CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapZ_p

CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory

Definitions

Name	Category	Theorems
Z 📖	CompOp	3 math math: Z_map_app, Z_obj_map, Z_obj_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Z_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MorphismProperty.MapFactorizationData.Z CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.MorphismProperty.FunctorialFactorizationData.factorizationData CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ CategoryTheory.Functor.map CategoryTheory.Arrow CategoryTheory.instCategoryArrow Z CategoryTheory.CommaMorphism.left CategoryTheory.CommaMorphism.right	—	—
Z_obj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.instCategoryArrow Z CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.NatTrans.app CategoryTheory.Comma.hom	—	—
Z_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.instCategoryArrow Z CategoryTheory.MorphismProperty.MapFactorizationData.Z CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.NatTrans.app CategoryTheory.Comma.hom CategoryTheory.MorphismProperty.FunctorialFactorizationData.factorizationData	—	—

CategoryTheory.MorphismProperty.HasFactorization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonempty_mapFactorizationData 📖	mathematical	—	CategoryTheory.MorphismProperty.MapFactorizationData	—	—

CategoryTheory.MorphismProperty.HasFunctorialFactorization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonempty_functorialFactorizationData 📖	mathematical	—	CategoryTheory.MorphismProperty.FunctorialFactorizationData	—	—

CategoryTheory.MorphismProperty.MapFactorizationData

Definitions

Name	Category	Theorems
Z 📖	CompOp	46 math math: CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_p, CategoryTheory.IsGrothendieckAbelian.instMonoIMonomorphismsRlpMonoMapFactorizationDataRlp, CategoryTheory.MorphismProperty.FunctorialFactorizationData.i_mapZ_assoc, HomotopicalAlgebra.FibrantBrownFactorization.i_r_assoc, CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z_map_app, HomotopicalAlgebra.Cylinder.ofFactorizationData_i₀, HomotopicalAlgebra.FibrantBrownFactorization.instWeakEquivalenceR, HomotopicalAlgebra.Cylinder.ofFactorizationData_i₁, HomotopicalAlgebra.CofibrantBrownFactorization.instWeakEquivalenceICofibrationsTrivialFibrations, HomotopicalAlgebra.FibrantBrownFactorization.instWeakEquivalencePTrivialCofibrationsFibrations, HomotopicalAlgebra.instFibrationPCofibrationsTrivialFibrations, HomotopicalAlgebra.instWeakEquivalenceITrivialCofibrationsFibrations, HomotopicalAlgebra.FibrantBrownFactorization.mk'_Z, HomotopicalAlgebra.Cylinder.ofFactorizationData_I, op_Z, fac, CategoryTheory.MorphismProperty.FunctorialFactorizationData.i_mapZ, HomotopicalAlgebra.PathObject.ofFactorizationData_p₁, HomotopicalAlgebra.CofibrantBrownFactorization.s_p, HomotopicalAlgebra.instCofibrationITrivialCofibrationsFibrations, op_i, fac_assoc, HomotopicalAlgebra.FibrantBrownFactorization.fibration_r, CategoryTheory.MorphismProperty.FunctorialFactorizationData.functorCategory.Z_obj_obj, CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_p_assoc, HomotopicalAlgebra.PathObject.ofFactorizationData_P, HomotopicalAlgebra.CofibrantBrownFactorization.cofibration_s, HomotopicalAlgebra.CofibrantBrownFactorization.mk'_s, HomotopicalAlgebra.instFibrationPTrivialCofibrationsFibrations, CategoryTheory.IsGrothendieckAbelian.instInjectiveZMonomorphismsRlpMonoMapFactorizationDataRlpOfNatHom, HomotopicalAlgebra.CofibrantBrownFactorization.s_p_assoc, CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_comp, HomotopicalAlgebra.FibrantBrownFactorization.mk'_r, HomotopicalAlgebra.instWeakEquivalencePCofibrationsTrivialFibrations, HomotopicalAlgebra.PathObject.ofFactorizationData_p₀, HomotopicalAlgebra.CofibrantBrownFactorization.mk'_Z, HomotopicalAlgebra.instCofibrationICofibrationsTrivialFibrations, HomotopicalAlgebra.FibrantBrownFactorization.mk'_p, hi, CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_comp_assoc, HomotopicalAlgebra.CofibrantBrownFactorization.instWeakEquivalenceS, HomotopicalAlgebra.FibrantBrownFactorization.i_r, hp, op_p, HomotopicalAlgebra.CofibrantBrownFactorization.mk'_i, CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_id
i 📖	CompOp	21 math math: CategoryTheory.IsGrothendieckAbelian.instMonoIMonomorphismsRlpMonoMapFactorizationDataRlp, CategoryTheory.MorphismProperty.FunctorialFactorizationData.i_mapZ_assoc, HomotopicalAlgebra.FibrantBrownFactorization.i_r_assoc, HomotopicalAlgebra.Cylinder.ofFactorizationData_i₀, HomotopicalAlgebra.Cylinder.ofFactorizationData_i₁, HomotopicalAlgebra.FibrantBrownFactorization.mk'_i, HomotopicalAlgebra.CofibrantBrownFactorization.instWeakEquivalenceICofibrationsTrivialFibrations, HomotopicalAlgebra.instWeakEquivalenceITrivialCofibrationsFibrations, HomotopicalAlgebra.Cylinder.ofFactorizationData_i, fac, CategoryTheory.MorphismProperty.FunctorialFactorizationData.i_mapZ, HomotopicalAlgebra.instCofibrationITrivialCofibrationsFibrations, op_i, fac_assoc, HomotopicalAlgebra.CofibrantBrownFactorization.mk'_s, HomotopicalAlgebra.instCofibrationICofibrationsTrivialFibrations, HomotopicalAlgebra.PathObject.ofFactorizationData_ι, hi, HomotopicalAlgebra.FibrantBrownFactorization.i_r, op_p, HomotopicalAlgebra.CofibrantBrownFactorization.mk'_i
op 📖	CompOp	3 math math: op_Z, op_i, op_p
p 📖	CompOp	20 math math: CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_p, HomotopicalAlgebra.FibrantBrownFactorization.instWeakEquivalencePTrivialCofibrationsFibrations, HomotopicalAlgebra.instFibrationPCofibrationsTrivialFibrations, HomotopicalAlgebra.PathObject.ofFactorizationData_p, fac, HomotopicalAlgebra.PathObject.ofFactorizationData_p₁, HomotopicalAlgebra.CofibrantBrownFactorization.s_p, op_i, fac_assoc, CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ_p_assoc, HomotopicalAlgebra.Cylinder.ofFactorizationData_π, HomotopicalAlgebra.instFibrationPTrivialCofibrationsFibrations, HomotopicalAlgebra.CofibrantBrownFactorization.mk'_p, HomotopicalAlgebra.CofibrantBrownFactorization.s_p_assoc, HomotopicalAlgebra.FibrantBrownFactorization.mk'_r, HomotopicalAlgebra.instWeakEquivalencePCofibrationsTrivialFibrations, HomotopicalAlgebra.PathObject.ofFactorizationData_p₀, HomotopicalAlgebra.FibrantBrownFactorization.mk'_p, hp, op_p

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Z i p	—	—
fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Z i p	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fac
hi 📖	mathematical	—	Z i	—	—
hp 📖	mathematical	—	Z p	—	—
op_Z 📖	mathematical	—	Z Opposite CategoryTheory.Category.opposite CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver op	—	—
op_i 📖	mathematical	—	i Opposite CategoryTheory.Category.opposite CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver op Z p	—	—
op_p 📖	mathematical	—	p Opposite CategoryTheory.Category.opposite CategoryTheory.MorphismProperty.op CategoryTheory.Category.toCategoryStruct Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver op Z i	—	—

---

← Back to Index