Fiber

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

Statistics

Metric	Count
Definitions Fiber, fiberCategory, fiberInclusion, fiberInclusionCompIsoConst, homMk, inducedFunctor, inducedFunctorCompIsoSelf, mk	8
Theorems fiberInclusionCompIsoConst_hom_app, fiberInclusionCompIsoConst_inv_app, fiberInclusion_comp_eq_const, fiberInclusion_homMk, fiberInclusion_mk, fiberInclusion_obj_inj, homMk_comp, homMk_id, hom_ext, hom_ext_iff, inducedFunctorCompIsoSelf_hom_app, inducedFunctorCompIsoSelf_inv_app, inducedFunctor_comp, inducedFunctor_comp_map, inducedFunctor_comp_obj, instFaithfulFiberInclusion, instIsHomLiftIdMapFiberInclusion	17
Total	25

CategoryTheory.Functor

Definitions

Name	Category	Theorems
Fiber 📖	CompOp	25 math math: Fiber.fiberInclusionCompIsoConst_inv_app, CategoryTheory.Pseudofunctor.CoGrothendieck.instIsEquivalenceαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, Fiber.fiberInclusion_comp_eq_const, Fiber.inducedFunctor_comp_obj, CategoryTheory.Pseudofunctor.CoGrothendieck.instFullαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, HasFibers.inducedFunctor_obj_coe, HasFibers.inducedFunctor_comp, Fiber.fiberInclusion_mk, Fiber.fiberInclusion_homMk, Fiber.instIsHomLiftIdMapFiberInclusion, HasFibers.equiv, Fiber.inducedFunctorCompIsoSelf_hom_app, Fiber.homMk_comp, Fiber.hom_ext_iff, Fiber.fiberInclusion_obj_inj, CategoryTheory.Pseudofunctor.CoGrothendieck.instEssSurjαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, HasFibers.instIsEquivalenceFibFiberInducedFunctor, Fiber.inducedFunctor_comp_map, Fiber.inducedFunctor_comp, Fiber.homMk_id, Fiber.inducedFunctorCompIsoSelf_inv_app, HasFibers.inducedFunctor_map_coe, CategoryTheory.Pseudofunctor.CoGrothendieck.instFaithfulαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, Fiber.fiberInclusionCompIsoConst_hom_app, Fiber.instFaithfulFiberInclusion

CategoryTheory.Functor.Fiber

Definitions

Name	Category	Theorems
fiberCategory 📖	CompOp	25 math math: fiberInclusionCompIsoConst_inv_app, CategoryTheory.Pseudofunctor.CoGrothendieck.instIsEquivalenceαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, fiberInclusion_comp_eq_const, inducedFunctor_comp_obj, CategoryTheory.Pseudofunctor.CoGrothendieck.instFullαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, HasFibers.inducedFunctor_obj_coe, HasFibers.inducedFunctor_comp, fiberInclusion_mk, fiberInclusion_homMk, instIsHomLiftIdMapFiberInclusion, HasFibers.equiv, inducedFunctorCompIsoSelf_hom_app, homMk_comp, hom_ext_iff, fiberInclusion_obj_inj, CategoryTheory.Pseudofunctor.CoGrothendieck.instEssSurjαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, HasFibers.instIsEquivalenceFibFiberInducedFunctor, inducedFunctor_comp_map, inducedFunctor_comp, homMk_id, inducedFunctorCompIsoSelf_inv_app, HasFibers.inducedFunctor_map_coe, CategoryTheory.Pseudofunctor.CoGrothendieck.instFaithfulαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, fiberInclusionCompIsoConst_hom_app, instFaithfulFiberInclusion
fiberInclusion 📖	CompOp	15 math math: fiberInclusionCompIsoConst_inv_app, fiberInclusion_comp_eq_const, inducedFunctor_comp_obj, HasFibers.inducedFunctor_comp, fiberInclusion_mk, fiberInclusion_homMk, instIsHomLiftIdMapFiberInclusion, inducedFunctorCompIsoSelf_hom_app, hom_ext_iff, fiberInclusion_obj_inj, inducedFunctor_comp_map, inducedFunctor_comp, inducedFunctorCompIsoSelf_inv_app, fiberInclusionCompIsoConst_hom_app, instFaithfulFiberInclusion
fiberInclusionCompIsoConst 📖	CompOp	2 math math: fiberInclusionCompIsoConst_inv_app, fiberInclusionCompIsoConst_hom_app
homMk 📖	CompOp	3 math math: fiberInclusion_homMk, homMk_comp, homMk_id
inducedFunctor 📖	CompOp	10 math math: CategoryTheory.Pseudofunctor.CoGrothendieck.instIsEquivalenceαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, inducedFunctor_comp_obj, CategoryTheory.Pseudofunctor.CoGrothendieck.instFullαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, HasFibers.equiv, inducedFunctorCompIsoSelf_hom_app, CategoryTheory.Pseudofunctor.CoGrothendieck.instEssSurjαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor, inducedFunctor_comp_map, inducedFunctor_comp, inducedFunctorCompIsoSelf_inv_app, CategoryTheory.Pseudofunctor.CoGrothendieck.instFaithfulαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor
inducedFunctorCompIsoSelf 📖	CompOp	2 math math: inducedFunctorCompIsoSelf_hom_app, inducedFunctorCompIsoSelf_inv_app
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fiberInclusionCompIsoConst_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.Fiber fiberCategory CategoryTheory.Functor.comp fiberInclusion CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Iso.hom fiberInclusionCompIsoConst CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct	—	—
fiberInclusionCompIsoConst_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.Fiber fiberCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.comp fiberInclusion CategoryTheory.Iso.inv fiberInclusionCompIsoConst CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct	—	—
fiberInclusion_comp_eq_const 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.Functor.Fiber fiberCategory fiberInclusion CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const	—	CategoryTheory.Functor.ext_of_iso
fiberInclusion_homMk 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor.Fiber fiberCategory fiberInclusion CategoryTheory.IsHomLift.domain_eq CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.IsHomLift.codomain_eq homMk	—	CategoryTheory.IsHomLift.domain_eq CategoryTheory.IsHomLift.codomain_eq
fiberInclusion_mk 📖	mathematical	CategoryTheory.Functor.obj	CategoryTheory.Functor.Fiber fiberCategory fiberInclusion	—	—
fiberInclusion_obj_inj 📖	mathematical	—	CategoryTheory.Functor.Fiber CategoryTheory.Functor.obj fiberCategory fiberInclusion	—	—
homMk_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.Fiber CategoryTheory.Category.toCategoryStruct fiberCategory CategoryTheory.IsHomLift.domain_eq CategoryTheory.CategoryStruct.id CategoryTheory.IsHomLift.codomain_eq homMk CategoryTheory.IsHomLift.comp_of_lift_id	—	CategoryTheory.IsHomLift.domain_eq CategoryTheory.IsHomLift.codomain_eq
homMk_id 📖	mathematical	—	homMk CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.Fiber fiberCategory CategoryTheory.IsHomLift.domain_eq	—	CategoryTheory.IsHomLift.domain_eq CategoryTheory.IsHomLift.codomain_eq
hom_ext 📖	—	CategoryTheory.Functor.map CategoryTheory.Functor.Fiber fiberCategory fiberInclusion	—	—	—
hom_ext_iff 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor.Fiber fiberCategory fiberInclusion	—	hom_ext
inducedFunctorCompIsoSelf_hom_app 📖	mathematical	CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const	CategoryTheory.NatTrans.app CategoryTheory.Functor.Fiber fiberCategory inducedFunctor fiberInclusion CategoryTheory.Iso.hom inducedFunctorCompIsoSelf CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
inducedFunctorCompIsoSelf_inv_app 📖	mathematical	CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const	CategoryTheory.NatTrans.app CategoryTheory.Functor.Fiber fiberCategory inducedFunctor fiberInclusion CategoryTheory.Iso.inv inducedFunctorCompIsoSelf CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
inducedFunctor_comp 📖	mathematical	CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const	CategoryTheory.Functor.Fiber fiberCategory inducedFunctor fiberInclusion	—	—
inducedFunctor_comp_map 📖	mathematical	CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const	CategoryTheory.Functor.map CategoryTheory.Functor.Fiber fiberCategory fiberInclusion inducedFunctor	—	—
inducedFunctor_comp_obj 📖	mathematical	CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const	CategoryTheory.Functor.Fiber fiberCategory fiberInclusion inducedFunctor	—	—
instFaithfulFiberInclusion 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Functor.Fiber fiberCategory fiberInclusion	—	hom_ext
instIsHomLiftIdMapFiberInclusion 📖	mathematical	—	CategoryTheory.Functor.IsHomLift CategoryTheory.Functor.obj CategoryTheory.Functor.Fiber fiberCategory fiberInclusion CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map	—	—

---

← Back to Index