Documentation Verification Report

Equifibered

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/Pullback/Equifibered.lean

Statistics

Metric	Count
Definitions `Coequifibered`, `Equifibered`	2
Theorems `comp`, `of_discrete`, `of_isIso`, `op`, `rightOp`, `unop`, `whiskerLeft`, `whiskerRight`, `Coequifibered_of_isIso`, `comp`, `of_discrete`, `of_isIso`, `op`, `rightOp`, `unop`, `whiskerLeft`, `whiskerRight`, `coequifibered_op_iff`, `coequifibered_unop_iff`, `equifibered_of_discrete`, `equifibered_of_isIso`, `equifibered_op_iff`, `equifibered_unop_iff`, `instIsMultiplicativeFunctorCoequifibered`, `instIsMultiplicativeFunctorEquifibered`, `instRespectsIsoFunctorCoequifibered`, `instRespectsIsoFunctorEquifibered`, `mapPair_equifibered`	28
Total	30

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mapPair_equifibered` 📖	mathematical	—	`NatTrans.Equifibered` `Discrete` `discreteCategory`	—	`NatTrans.Equifibered.of_discrete`

CategoryTheory.NatTrans

Definitions

Name	Category	Theorems
`Coequifibered` 📖	CompOp	16 math math: `Equifibered.rightOp`, `AlgebraicGeometry.Scheme.Hom.coequifibered_normalizationDiagramMap`, `instIsClosedUnderColimitsOfShapeUnderFunctorCoequifiberedHomDiscretePUnitOfHasProductsOfShapeHom`, `AlgebraicGeometry.Scheme.AffineZariskiSite.coequifibered_iff_forall_isLocalizationAway`, `equifibered_op_iff`, `AlgebraicGeometry.Scheme.Hom.preservesLocalization_normalizationDiagramMap`, `Coequifibered_of_isIso`, `coequifibered_op_iff`, `Coequifibered.of_isIso`, `instRespectsIsoFunctorCoequifibered`, `equifibered_unop_iff`, `coequifibered_unop_iff`, `Equifibered.unop`, `Equifibered.op`, `instIsMultiplicativeFunctorCoequifibered`, `AlgebraicGeometry.Scheme.preservesLocalization_toOpensFunctor`
`Equifibered` 📖	CompOp	17 math math: `equifibered_of_isIso`, `Equifibered.of_isIso`, `instIsClosedUnderLimitsOfShapeOverFunctorEquifiberedHomDiscretePUnitOfHasCoproductsOfShapeHom`, `equifibered_of_discrete`, `AlgebraicGeometry.Scheme.Cover.RelativeGluingData.equifibered`, `Equifibered.of_discrete`, `equifibered_op_iff`, `coequifibered_op_iff`, `Coequifibered.op`, `equifibered_unop_iff`, `Coequifibered.rightOp`, `coequifibered_unop_iff`, `Coequifibered.unop`, `Coequifibered.of_discrete`, `instIsMultiplicativeFunctorEquifibered`, `instRespectsIsoFunctorEquifibered`, `CategoryTheory.mapPair_equifibered`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Coequifibered_of_isIso` 📖	mathematical	—	`Coequifibered`	—	`Coequifibered.of_isIso`
`coequifibered_op_iff` 📖	mathematical	—	`Coequifibered` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.op` `op` `Equifibered`	—	`Coequifibered.unop` `Equifibered.op`
`coequifibered_unop_iff` 📖	mathematical	—	`Coequifibered` `CategoryTheory.Functor.unop` `unop` `Equifibered` `Opposite` `CategoryTheory.Category.opposite`	—	`Coequifibered.op` `Equifibered.unop`
`equifibered_of_discrete` 📖	mathematical	—	`Equifibered` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory`	—	`Equifibered.of_discrete`
`equifibered_of_isIso` 📖	mathematical	—	`Equifibered`	—	`Equifibered.of_isIso`
`equifibered_op_iff` 📖	mathematical	—	`Equifibered` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.op` `op` `Coequifibered`	—	`Equifibered.unop` `Coequifibered.op`
`equifibered_unop_iff` 📖	mathematical	—	`Equifibered` `CategoryTheory.Functor.unop` `unop` `Coequifibered` `Opposite` `CategoryTheory.Category.opposite`	—	`Equifibered.op` `Coequifibered.unop`
`instIsMultiplicativeFunctorCoequifibered` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMultiplicative` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `Coequifibered`	—	`Coequifibered.of_isIso` `CategoryTheory.IsIso.id` `Coequifibered.comp`
`instIsMultiplicativeFunctorEquifibered` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMultiplicative` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `Equifibered`	—	`Equifibered.of_isIso` `CategoryTheory.IsIso.id` `Equifibered.comp`
`instRespectsIsoFunctorCoequifibered` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RespectsIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `Coequifibered`	—	`CategoryTheory.MorphismProperty.respectsIso_of_isStableUnderComposition` `CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition` `instIsMultiplicativeFunctorCoequifibered` `Coequifibered.of_isIso`
`instRespectsIsoFunctorEquifibered` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RespectsIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `Equifibered`	—	`CategoryTheory.MorphismProperty.respectsIso_of_isStableUnderComposition` `CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition` `instIsMultiplicativeFunctorEquifibered` `Equifibered.of_isIso`

CategoryTheory.NatTrans.Coequifibered

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`CategoryTheory.NatTrans.Coequifibered`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category`	—	`CategoryTheory.IsPushout.paste_vert`
`of_discrete` 📖	mathematical	—	`CategoryTheory.NatTrans.Equifibered` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory`	—	`CategoryTheory.Discrete.functor_map_id` `CategoryTheory.IsPullback.of_horiz_isIso` `CategoryTheory.IsIso.id` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id`
`of_isIso` 📖	mathematical	—	`CategoryTheory.NatTrans.Coequifibered`	—	`CategoryTheory.IsPushout.of_vert_isIso` `CategoryTheory.NatIso.isIso_app_of_isIso` `CategoryTheory.NatTrans.naturality`
`op` 📖	mathematical	`CategoryTheory.NatTrans.Coequifibered`	`CategoryTheory.NatTrans.Equifibered` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.op` `CategoryTheory.NatTrans.op`	—	`CategoryTheory.IsPushout.op`
`rightOp` 📖	mathematical	`CategoryTheory.NatTrans.Coequifibered` `Opposite` `CategoryTheory.Category.opposite`	`CategoryTheory.NatTrans.Equifibered` `CategoryTheory.Functor.rightOp` `CategoryTheory.NatTrans.rightOp`	—	`CategoryTheory.IsPushout.op`
`unop` 📖	mathematical	`CategoryTheory.NatTrans.Coequifibered` `Opposite` `CategoryTheory.Category.opposite`	`CategoryTheory.NatTrans.Equifibered` `CategoryTheory.Functor.unop` `CategoryTheory.NatTrans.unop`	—	`CategoryTheory.IsPushout.unop`
`whiskerLeft` 📖	mathematical	`CategoryTheory.NatTrans.Coequifibered`	`CategoryTheory.Functor.comp` `CategoryTheory.Functor.whiskerLeft`	—	—
`whiskerRight` 📖	mathematical	`CategoryTheory.NatTrans.Coequifibered` `CategoryTheory.Limits.PreservesColimit` `CategoryTheory.Limits.WalkingSpan` `CategoryTheory.Limits.WidePushoutShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.span` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app`	`CategoryTheory.Functor.comp` `CategoryTheory.Functor.whiskerRight`	—	`CategoryTheory.IsPushout.map`

CategoryTheory.NatTrans.Equifibered

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`CategoryTheory.NatTrans.Equifibered`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category`	—	`CategoryTheory.IsPullback.paste_vert`
`of_discrete` 📖	mathematical	—	`CategoryTheory.NatTrans.Equifibered` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory`	—	`CategoryTheory.Discrete.functor_map_id` `CategoryTheory.IsPullback.of_horiz_isIso` `CategoryTheory.IsIso.id` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id`
`of_isIso` 📖	mathematical	—	`CategoryTheory.NatTrans.Equifibered`	—	`CategoryTheory.IsPullback.of_vert_isIso` `CategoryTheory.NatIso.isIso_app_of_isIso` `CategoryTheory.NatTrans.naturality`
`op` 📖	mathematical	`CategoryTheory.NatTrans.Equifibered`	`CategoryTheory.NatTrans.Coequifibered` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.op` `CategoryTheory.NatTrans.op`	—	`CategoryTheory.IsPullback.op`
`rightOp` 📖	mathematical	`CategoryTheory.NatTrans.Equifibered` `Opposite` `CategoryTheory.Category.opposite`	`CategoryTheory.NatTrans.Coequifibered` `CategoryTheory.Functor.rightOp` `CategoryTheory.NatTrans.rightOp`	—	`CategoryTheory.IsPullback.op`
`unop` 📖	mathematical	`CategoryTheory.NatTrans.Equifibered` `Opposite` `CategoryTheory.Category.opposite`	`CategoryTheory.NatTrans.Coequifibered` `CategoryTheory.Functor.unop` `CategoryTheory.NatTrans.unop`	—	`CategoryTheory.IsPullback.unop`
`whiskerLeft` 📖	mathematical	`CategoryTheory.NatTrans.Equifibered`	`CategoryTheory.Functor.comp` `CategoryTheory.Functor.whiskerLeft`	—	—
`whiskerRight` 📖	mathematical	`CategoryTheory.NatTrans.Equifibered` `CategoryTheory.Limits.PreservesLimit` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan` `CategoryTheory.Functor.obj` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.map`	`CategoryTheory.Functor.comp` `CategoryTheory.Functor.whiskerRight`	—	`CategoryTheory.IsPullback.map`

---

← Back to Index