Documentation Verification Report

HasFibers

📁 Source: Mathlib/CategoryTheory/FiberedCategory/HasFibers.lean

Statistics

Metric	Count
Definitions `HasFibers`, `Fib`, `homMk`, `isoMk`, `mk`, `mkIsoSelf`, `canonical`, `category`, `inducedFunctor`, `natIso`, `inducedMap`, `mkPullback`, `projMap`, `pullbackMap`, `ι`	15
Theorems `hom_ext`, `hom_ext_iff`, `isoMk_hom`, `isoMk_inv`, `map_homMk`, `mkIsoSelfIsHomLift`, `comp_const`, `equiv`, `fiber_factorization`, `homLift`, `inducedFunctor_comp`, `inducedFunctor_map_coe`, `inducedFunctor_obj_coe`, `inducedMap_comp`, `inducedMap_comp_assoc`, `instFaithfulFibι`, `instIsEquivalenceFibFiberInducedFunctor`, `proj_eq`, `isCartesian`	19
Total	34

HasFibers

Definitions

Name	Category	Theorems
`Fib` 📖	CompOp	18 math math: `inducedMap_comp`, `homLift`, `comp_const`, `inducedFunctor_obj_coe`, `inducedFunctor_comp`, `pullbackMap.isCartesian`, `Fib.mkIsoSelfIsHomLift`, `Fib.map_homMk`, `Fib.hom_ext_iff`, `equiv`, `instFaithfulFibι`, `inducedMap_comp_assoc`, `Fib.isoMk_inv`, `instIsEquivalenceFibFiberInducedFunctor`, `Fib.isoMk_hom`, `proj_eq`, `inducedFunctor_map_coe`, `fiber_factorization`
`canonical` 📖	CompOp	—
`category` 📖	CompOp	18 math math: `inducedMap_comp`, `homLift`, `comp_const`, `inducedFunctor_obj_coe`, `inducedFunctor_comp`, `pullbackMap.isCartesian`, `Fib.mkIsoSelfIsHomLift`, `Fib.map_homMk`, `Fib.hom_ext_iff`, `equiv`, `instFaithfulFibι`, `inducedMap_comp_assoc`, `Fib.isoMk_inv`, `instIsEquivalenceFibFiberInducedFunctor`, `Fib.isoMk_hom`, `proj_eq`, `inducedFunctor_map_coe`, `fiber_factorization`
`inducedFunctor` 📖	CompOp	4 math math: `inducedFunctor_obj_coe`, `inducedFunctor_comp`, `instIsEquivalenceFibFiberInducedFunctor`, `inducedFunctor_map_coe`
`inducedMap` 📖	CompOp	2 math math: `inducedMap_comp`, `inducedMap_comp_assoc`
`mkPullback` 📖	CompOp	1 math math: `pullbackMap.isCartesian`
`projMap` 📖	CompOp	—
`pullbackMap` 📖	CompOp	1 math math: `pullbackMap.isCartesian`
`ι` 📖	CompOp	17 math math: `inducedMap_comp`, `homLift`, `comp_const`, `inducedFunctor_obj_coe`, `inducedFunctor_comp`, `pullbackMap.isCartesian`, `Fib.mkIsoSelfIsHomLift`, `Fib.map_homMk`, `Fib.hom_ext_iff`, `equiv`, `instFaithfulFibι`, `inducedMap_comp_assoc`, `Fib.isoMk_inv`, `Fib.isoMk_hom`, `proj_eq`, `inducedFunctor_map_coe`, `fiber_factorization`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_const` 📖	mathematical	—	`CategoryTheory.Functor.comp` `Fib` `category` `ι` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const`	—	—
`equiv` 📖	mathematical	—	`CategoryTheory.Functor.IsEquivalence` `Fib` `category` `CategoryTheory.Functor.Fiber` `CategoryTheory.Functor.Fiber.fiberCategory` `CategoryTheory.Functor.Fiber.inducedFunctor` `ι` `comp_const`	—	—
`fiber_factorization` 📖	mathematical	`CategoryTheory.Functor.obj`	`CategoryTheory.Functor.IsStronglyCartesian` `Fib` `category` `ι` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.map`	—	`CategoryTheory.Functor.IsFibered.toIsPreFibered` `pullbackMap.isCartesian` `CategoryTheory.Functor.IsFibered.isStronglyCartesian_of_isCartesian` `inducedMap_comp`
`homLift` 📖	mathematical	—	`CategoryTheory.Functor.IsHomLift` `CategoryTheory.Functor.obj` `Fib` `category` `ι` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.map`	—	`CategoryTheory.IsHomLift.of_fac` `proj_eq` `CategoryTheory.Functor.comp_map` `CategoryTheory.Functor.congr_obj` `comp_const` `CategoryTheory.Functor.congr_hom` `CategoryTheory.eqToHom_naturality` `CategoryTheory.Category.comp_id` `CategoryTheory.eqToHom_trans`
`inducedFunctor_comp` 📖	mathematical	—	`ι` `CategoryTheory.Functor.comp` `Fib` `category` `CategoryTheory.Functor.Fiber` `CategoryTheory.Functor.Fiber.fiberCategory` `inducedFunctor` `CategoryTheory.Functor.Fiber.fiberInclusion`	—	`CategoryTheory.Functor.Fiber.inducedFunctor_comp` `comp_const`
`inducedFunctor_map_coe` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Fib` `category` `ι` `comp_const` `CategoryTheory.Functor.IsHomLift` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Functor.map` `CategoryTheory.Functor.Fiber` `CategoryTheory.Functor.Fiber.fiberCategory` `inducedFunctor`	—	`comp_const`
`inducedFunctor_obj_coe` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Fib` `category` `CategoryTheory.Functor.Fiber` `CategoryTheory.Functor.Fiber.fiberCategory` `inducedFunctor` `ι`	—	—
`inducedMap_comp` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Fib` `category` `ι` `CategoryTheory.Functor.map` `inducedMap`	—	`Fib.map_homMk` `CategoryTheory.Functor.IsCartesian.fac`
`inducedMap_comp_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `Fib` `category` `ι` `CategoryTheory.Functor.map` `inducedMap`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inducedMap_comp`
`instFaithfulFibι` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `Fib` `category` `ι`	—	`CategoryTheory.Functor.Faithful.of_iso` `CategoryTheory.Functor.Faithful.comp` `CategoryTheory.Functor.IsEquivalence.faithful` `instIsEquivalenceFibFiberInducedFunctor` `CategoryTheory.Functor.Fiber.instFaithfulFiberInclusion`
`instIsEquivalenceFibFiberInducedFunctor` 📖	mathematical	—	`CategoryTheory.Functor.IsEquivalence` `Fib` `category` `CategoryTheory.Functor.Fiber` `CategoryTheory.Functor.Fiber.fiberCategory` `inducedFunctor`	—	`equiv`
`proj_eq` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Fib` `category` `ι`	—	`comp_const`

HasFibers.Fib

Definitions

Name	Category	Theorems
`homMk` 📖	CompOp	3 math math: `map_homMk`, `isoMk_inv`, `isoMk_hom`
`isoMk` 📖	CompOp	2 math math: `isoMk_inv`, `isoMk_hom`
`mk` 📖	CompOp	—
`mkIsoSelf` 📖	CompOp	1 math math: `mkIsoSelfIsHomLift`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_ext` 📖	—	`CategoryTheory.Functor.map` `HasFibers.Fib` `HasFibers.category` `HasFibers.ι`	—	—	`CategoryTheory.Functor.map_injective` `HasFibers.instFaithfulFibι`
`hom_ext_iff` 📖	mathematical	—	`CategoryTheory.Functor.map` `HasFibers.Fib` `HasFibers.category` `HasFibers.ι`	—	`hom_ext`
`isoMk_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `HasFibers.Fib` `HasFibers.category` `isoMk` `homMk` `CategoryTheory.Functor.obj` `HasFibers.ι`	—	—
`isoMk_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `HasFibers.Fib` `HasFibers.category` `isoMk` `homMk` `CategoryTheory.Functor.obj` `HasFibers.ι`	—	—
`map_homMk` 📖	mathematical	—	`CategoryTheory.Functor.map` `HasFibers.Fib` `HasFibers.category` `HasFibers.ι` `homMk`	—	`CategoryTheory.Functor.congr_obj` `HasFibers.inducedFunctor_comp` `CategoryTheory.Functor.congr_hom` `CategoryTheory.Functor.map_preimage` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`mkIsoSelfIsHomLift` 📖	mathematical	`CategoryTheory.Functor.obj`	`CategoryTheory.Functor.IsHomLift` `HasFibers.Fib` `HasFibers.category` `HasFibers.ι` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Iso.hom` `mkIsoSelf`	—	`CategoryTheory.Functor.IsEquivalence.essSurj` `HasFibers.instIsEquivalenceFibFiberInducedFunctor`

HasFibers.inducedFunctor

Definitions

Name	Category	Theorems
`natIso` 📖	CompOp	—

HasFibers.pullbackMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCartesian` 📖	mathematical	`CategoryTheory.Functor.obj`	`CategoryTheory.Functor.IsCartesian` `HasFibers.Fib` `HasFibers.category` `HasFibers.ι` `HasFibers.mkPullback` `HasFibers.pullbackMap`	—	`CategoryTheory.Category.id_comp` `CategoryTheory.Functor.IsCartesian.of_iso_comp` `CategoryTheory.Functor.IsPreFibered.pullbackMap.IsCartesian` `HasFibers.Fib.mkIsoSelfIsHomLift`

(root)

Definitions

Name	Category	Theorems
`HasFibers` 📖	CompData	—

---

← Back to Index