Fibered

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

Statistics

Metric	Count
Definitions IsFibered, pullbackPullbackIso, IsPreFibered, pullbackMap, pullbackObj	5
Theorems comp, isStronglyCartesian_of_exists_isCartesian, isStronglyCartesian_of_isCartesian, of_exists_isStronglyCartesian, toIsPreFibered, exists_isCartesian', IsCartesian, pullbackObj_proj, exists_isCartesian, instIsCartesianCompOfIsFibered	10
Total	15

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsCartesianCompOfIsFibered 📖	mathematical	—	Functor.IsCartesian CategoryStruct.comp Category.toCategoryStruct	—	Functor.IsFibered.comp

CategoryTheory.Functor

Definitions

Name	Category	Theorems
IsFibered 📖	CompData	2 math math: CategoryTheory.Pseudofunctor.CoGrothendieck.instIsFiberedForget, IsFibered.of_exists_isStronglyCartesian
IsPreFibered 📖	CompData	1 math math: IsFibered.toIsPreFibered

CategoryTheory.Functor.IsFibered

Definitions

Name	Category	Theorems
pullbackPullbackIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	—	CategoryTheory.Functor.IsCartesian CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
isStronglyCartesian_of_exists_isCartesian 📖	—	CategoryTheory.Functor.IsStronglyCartesian CategoryTheory.Functor.obj	—	—	CategoryTheory.Functor.IsCartesian.toIsHomLift CategoryTheory.Functor.IsStronglyCartesian.isCartesian_of_isStronglyCartesian CategoryTheory.IsHomLift.comp_lift_id_right CategoryTheory.Functor.IsStronglyCartesian.map_isHomLift CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso_inv_isHomLift CategoryTheory.Category.assoc CategoryTheory.Functor.IsCartesian.fac CategoryTheory.Functor.IsStronglyCartesian.fac CategoryTheory.Iso.comp_inv_eq CategoryTheory.Functor.IsStronglyCartesian.map_uniq CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso_hom_isHomLift
isStronglyCartesian_of_isCartesian 📖	mathematical	—	CategoryTheory.Functor.IsStronglyCartesian	—	CategoryTheory.Functor.IsCartesian.toIsHomLift toIsPreFibered CategoryTheory.IsHomLift.domain_eq CategoryTheory.instIsCartesianCompOfIsFibered CategoryTheory.Functor.IsPreFibered.pullbackMap.IsCartesian CategoryTheory.IsHomLift.comp_lift_id_left CategoryTheory.Functor.IsCartesian.map_isHomLift CategoryTheory.Category.assoc CategoryTheory.Functor.IsCartesian.fac CategoryTheory.Functor.IsCartesian.map_uniq
of_exists_isStronglyCartesian 📖	mathematical	CategoryTheory.Functor.IsStronglyCartesian CategoryTheory.Functor.obj	CategoryTheory.Functor.IsFibered	—	CategoryTheory.Functor.IsStronglyCartesian.isCartesian_of_isStronglyCartesian isStronglyCartesian_of_exists_isCartesian CategoryTheory.Functor.IsStronglyCartesian.comp
toIsPreFibered 📖	mathematical	—	CategoryTheory.Functor.IsPreFibered	—	—

CategoryTheory.Functor.IsPreFibered

Definitions

Name	Category	Theorems
pullbackMap 📖	CompOp	1 math math: pullbackMap.IsCartesian
pullbackObj 📖	CompOp	2 math math: pullbackObj_proj, pullbackMap.IsCartesian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isCartesian' 📖	mathematical	—	CategoryTheory.Functor.IsCartesian CategoryTheory.Functor.obj	—	—
pullbackObj_proj 📖	mathematical	CategoryTheory.Functor.obj	pullbackObj	—	CategoryTheory.IsHomLift.domain_eq CategoryTheory.Functor.IsCartesian.toIsHomLift pullbackMap.IsCartesian

CategoryTheory.Functor.IsPreFibered.pullbackMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
IsCartesian 📖	mathematical	CategoryTheory.Functor.obj	CategoryTheory.Functor.IsCartesian CategoryTheory.Functor.IsPreFibered.pullbackObj CategoryTheory.Functor.IsPreFibered.pullbackMap	—	CategoryTheory.IsPreFibered.exists_isCartesian

CategoryTheory.IsPreFibered

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isCartesian 📖	mathematical	CategoryTheory.Functor.obj	CategoryTheory.Functor.IsCartesian	—	CategoryTheory.Functor.IsPreFibered.exists_isCartesian'

---

← Back to Index