Documentation Verification Report

Prod

📁 Source: Mathlib/CategoryTheory/Localization/Prod.lean

Statistics

Metric	Count
Definitions `prod`, `prodLift`, `prodLift₁`	3
Theorems `prod`, `prodIsLocalization`, `prod_fac`, `prod_fac₁`, `prod_fac₂`, `prod_uniq`	6
Total	9

CategoryTheory.Functor.IsLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod` 📖	mathematical	—	`CategoryTheory.Functor.IsLocalization` `CategoryTheory.prod'` `CategoryTheory.Functor.prod` `CategoryTheory.MorphismProperty.prod` `CategoryTheory.Category.toCategoryStruct`	—	`of_equivalence_target` `CategoryTheory.Functor.q_isLocalization` `CategoryTheory.Localization.Construction.prodIsLocalization`

CategoryTheory.Localization.Construction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prodIsLocalization` 📖	mathematical	—	`CategoryTheory.Functor.IsLocalization` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.prod'` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.Functor.prod` `CategoryTheory.MorphismProperty.Q` `CategoryTheory.MorphismProperty.prod` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.Functor.IsLocalization.mk'`

CategoryTheory.Localization.StrictUniversalPropertyFixedTarget

Definitions

Name	Category	Theorems
`prod` 📖	CompOp	—
`prodLift` 📖	CompOp	2 math math: `prod_fac`, `prod_fac₂`
`prodLift₁` 📖	CompOp	2 math math: `prod_fac₂`, `prod_fac₁`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_fac` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy` `CategoryTheory.prod'` `CategoryTheory.MorphismProperty.prod` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.Functor.comp` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.Functor.prod` `CategoryTheory.MorphismProperty.Q` `prodLift`	—	`CategoryTheory.Functor.uncurry_obj_curry_obj_flip_flip'` `prod_fac₂` `CategoryTheory.Functor.flip_flip` `prod_fac₁` `CategoryTheory.Functor.uncurry_obj_curry_obj`
`prod_fac₁` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy` `CategoryTheory.prod'` `CategoryTheory.MorphismProperty.prod` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.Functor.comp` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MorphismProperty.Q` `prodLift₁` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.curry`	—	`CategoryTheory.Localization.Construction.fac`
`prod_fac₂` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy` `CategoryTheory.prod'` `CategoryTheory.MorphismProperty.prod` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.Functor.comp` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MorphismProperty.Q` `CategoryTheory.Functor.flip` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.curry` `prodLift` `prodLift₁`	—	`CategoryTheory.Functor.curry_obj_uncurry_obj` `CategoryTheory.Localization.Construction.fac`
`prod_uniq` 📖	—	`CategoryTheory.Functor.comp` `CategoryTheory.prod'` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.Functor.prod` `CategoryTheory.MorphismProperty.Q`	—	—	`CategoryTheory.Functor.curry_obj_injective` `CategoryTheory.Localization.Construction.uniq` `CategoryTheory.Functor.flip_injective` `CategoryTheory.Functor.uncurry_obj_injective` `CategoryTheory.Functor.uncurry_obj_curry_obj_flip_flip`

---

← Back to Index