Documentation Verification Report

Pullbacks

📁 Source: Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean

Statistics

Metric	Count
Definitions `iso`, `iso`, `isLimitCoyonedaEquiv`, `isLimitMapConeEquiv`, `map`, `isColimitMapCoconeEquiv`, `isColimitYonedaEquiv`, `map`, `isColimitMapCoconePushoutCoconeEquiv`, `isColimitOfHasPushoutOfPreservesColimit`, `isColimitOfIsColimitPushoutCoconeMap`, `isColimitPushoutCoconeMapOfIsColimit`, `isLimitMapConePullbackConeEquiv`, `isLimitOfHasPullbackOfPreservesLimit`, `isLimitOfIsLimitPullbackConeMap`, `isLimitPullbackConeMapOfIsLimit`	16
Theorems `iso_hom`, `iso_hom_fst`, `iso_hom_fst_assoc`, `iso_hom_snd`, `iso_hom_snd_assoc`, `iso_inv_fst`, `iso_inv_fst_assoc`, `iso_inv_snd`, `iso_inv_snd_assoc`, `of_iso_comparison`, `inl_iso_hom`, `inl_iso_hom_assoc`, `inl_iso_inv`, `inl_iso_inv_assoc`, `inr_iso_hom`, `inr_iso_hom_assoc`, `inr_iso_inv`, `inr_iso_inv_assoc`, `iso_hom`, `of_iso_comparison`, `hasPullback_of_preservesPullback`, `hasPushout_of_preservesPushout`, `instIsIsoPullbackComparison`, `instIsIsoPushoutComparison`, `preservesPullback_symmetry`, `preservesPushout_symmetry`	26
Total	42

CategoryTheory.Limits

Definitions

Name	Category	Theorems
`isColimitMapCoconePushoutCoconeEquiv` 📖	CompOp	—
`isColimitOfHasPushoutOfPreservesColimit` 📖	CompOp	—
`isColimitOfIsColimitPushoutCoconeMap` 📖	CompOp	—
`isColimitPushoutCoconeMapOfIsColimit` 📖	CompOp	—
`isLimitMapConePullbackConeEquiv` 📖	CompOp	—
`isLimitOfHasPullbackOfPreservesLimit` 📖	CompOp	—
`isLimitOfIsLimitPullbackConeMap` 📖	CompOp	—
`isLimitPullbackConeMapOfIsLimit` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasPullback_of_preservesPullback` 📖	mathematical	—	`HasPullback` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	—	`pullback.condition`
`hasPushout_of_preservesPushout` 📖	mathematical	—	`HasPushout` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	—	`pushout.condition`
`instIsIsoPullbackComparison` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `pullback` `CategoryTheory.Functor.map` `pullbackComparison`	—	`PreservesPullback.iso_hom` `CategoryTheory.Iso.isIso_hom`
`instIsIsoPushoutComparison` 📖	mathematical	—	`CategoryTheory.IsIso` `pushout` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `pushoutComparison`	—	`PreservesPushout.iso_hom` `CategoryTheory.Iso.isIso_hom`
`preservesPullback_symmetry` 📖	mathematical	—	`PreservesLimit` `WalkingCospan` `WidePullbackShape.category` `WalkingPair` `cospan`	—	`CategoryTheory.NatTrans.naturality`
`preservesPushout_symmetry` 📖	mathematical	—	`PreservesColimit` `WalkingSpan` `WidePushoutShape.category` `WalkingPair` `span`	—	`CategoryTheory.NatTrans.naturality`

CategoryTheory.Limits.PreservesPullback

Definitions

Name	Category	Theorems
`iso` 📖	CompOp	10 math math: `iso_inv_fst_assoc`, `iso_inv_snd`, `iso_inv_fst`, `iso_hom_fst`, `iso_inv_snd_assoc`, `iso_hom_snd_assoc`, `iso_hom_fst_assoc`, `iso_hom_snd`, `iso_hom`, `CategoryTheory.GlueData.mapGlueData_t'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.pullback` `CategoryTheory.Functor.map` `iso` `CategoryTheory.Limits.pullbackComparison`	—	—
`iso_hom_fst` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.pullback` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `iso` `CategoryTheory.Limits.pullback.fst`	—	`CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp`
`iso_hom_fst_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.pullback` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `iso` `CategoryTheory.Limits.pullback.fst`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `iso_hom_fst`
`iso_hom_snd` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.pullback` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `iso` `CategoryTheory.Limits.pullback.snd`	—	`CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp`
`iso_hom_snd_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.pullback` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `iso` `CategoryTheory.Limits.pullback.snd`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `iso_hom_snd`
`iso_inv_fst` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.pullback` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `iso` `CategoryTheory.Limits.pullback.fst`	—	`CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp`
`iso_inv_fst_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.pullback` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `iso` `CategoryTheory.Limits.pullback.fst`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `iso_inv_fst`
`iso_inv_snd` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.pullback` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `iso` `CategoryTheory.Limits.pullback.snd`	—	`CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp`
`iso_inv_snd_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.pullback` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `iso` `CategoryTheory.Limits.pullback.snd`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `iso_inv_snd`
`of_iso_comparison` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimit` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan`	—	`CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone` `CategoryTheory.Limits.pullback.condition`

CategoryTheory.Limits.PreservesPushout

Definitions

Name	Category	Theorems
`iso` 📖	CompOp	9 math math: `inr_iso_inv_assoc`, `inr_iso_inv`, `inr_iso_hom_assoc`, `inl_iso_inv`, `inl_iso_inv_assoc`, `inl_iso_hom_assoc`, `inr_iso_hom`, `inl_iso_hom`, `iso_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inl_iso_hom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.pushout` `CategoryTheory.Functor.map` `CategoryTheory.Limits.pushout.inl` `CategoryTheory.Iso.hom` `iso`	—	`CategoryTheory.Limits.inl_comp_pushoutComparison`
`inl_iso_hom_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.pushout` `CategoryTheory.Functor.map` `CategoryTheory.Limits.pushout.inl` `CategoryTheory.Iso.hom` `iso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inl_iso_hom`
`inl_iso_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.pushout` `CategoryTheory.Functor.map` `CategoryTheory.Limits.pushout.inl` `CategoryTheory.Iso.inv` `iso`	—	`CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom`
`inl_iso_inv_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.pushout` `CategoryTheory.Functor.map` `CategoryTheory.Limits.pushout.inl` `CategoryTheory.Iso.inv` `iso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inl_iso_inv`
`inr_iso_hom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.pushout` `CategoryTheory.Functor.map` `CategoryTheory.Limits.pushout.inr` `CategoryTheory.Iso.hom` `iso`	—	`CategoryTheory.Limits.inr_comp_pushoutComparison`
`inr_iso_hom_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.pushout` `CategoryTheory.Functor.map` `CategoryTheory.Limits.pushout.inr` `CategoryTheory.Iso.hom` `iso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inr_iso_hom`
`inr_iso_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.pushout` `CategoryTheory.Functor.map` `CategoryTheory.Limits.pushout.inr` `CategoryTheory.Iso.inv` `iso`	—	`CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom`
`inr_iso_inv_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.pushout` `CategoryTheory.Functor.map` `CategoryTheory.Limits.pushout.inr` `CategoryTheory.Iso.inv` `iso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inr_iso_inv`
`iso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.Limits.pushout` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `iso` `CategoryTheory.Limits.pushoutComparison`	—	—
`of_iso_comparison` 📖	mathematical	—	`CategoryTheory.Limits.PreservesColimit` `CategoryTheory.Limits.WalkingSpan` `CategoryTheory.Limits.WidePushoutShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.span`	—	`CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone` `CategoryTheory.Limits.pushout.condition`

CategoryTheory.Limits.PullbackCone

Definitions

Name	Category	Theorems
`isLimitCoyonedaEquiv` 📖	CompOp	—
`isLimitMapConeEquiv` 📖	CompOp	—
`map` 📖	CompOp	—

CategoryTheory.Limits.PushoutCocone

Definitions

Name	Category	Theorems
`isColimitMapCoconeEquiv` 📖	CompOp	—
`isColimitYonedaEquiv` 📖	CompOp	—
`map` 📖	CompOp	—

---

← Back to Index