Documentation Verification Report

Square

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

Statistics

Metric	Count
Definitions `IsPullback`, `isLimit`, `IsPushout`, `isColimit`, `pullbackCone`, `pushoutCocone`	6
Theorems `flip`, `iff_of_iso`, `mk`, `mono_f₁₂`, `mono_f₁₃`, `of_iso`, `op`, `unop`, `epi_f₂₄`, `epi_f₃₄`, `flip`, `iff_of_iso`, `mk`, `of_iso`, `op`, `unop`, `isPullback_iff`, `isPushout_iff`	18
Total	24

CategoryTheory.Square

Definitions

Name	Category	Theorems
`IsPullback` 📖	MathDef	10 math math: `IsPullback.mk`, `IsPullback.map_iff`, `CategoryTheory.Sheaf.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff`, `IsPullback.iff_of_equiv`, `IsPullback.iff_of_iso`, `isPullback_iff`, `isPullback_iff_map_coyoneda_isPullback`, `IsPushout.op`, `IsPushout.unop`, `isPushout_iff_op_map_yoneda_isPullback`
`IsPushout` 📖	MathDef	9 math math: `IsPushout.iff_of_iso`, `IsPushout.mk`, `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushout`, `IsPushout.map_iff`, `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushoutAddCommGrpFreeSheaf`, `IsPullback.op`, `isPushout_iff`, `IsPullback.unop`, `isPushout_iff_op_map_yoneda_isPullback`
`pullbackCone` 📖	CompOp	1 math math: `isPullback_iff`
`pushoutCocone` 📖	CompOp	1 math math: `isPushout_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPullback_iff` 📖	mathematical	—	`IsPullback` `CategoryTheory.Limits.IsLimit` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan` `X₂` `X₃` `X₄` `f₂₄` `f₃₄` `pullbackCone`	—	`fac`
`isPushout_iff` 📖	mathematical	—	`IsPushout` `CategoryTheory.Limits.IsColimit` `CategoryTheory.Limits.WalkingSpan` `CategoryTheory.Limits.WidePushoutShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.span` `X₁` `X₂` `X₃` `f₁₂` `f₁₃` `pushoutCocone`	—	`fac`

CategoryTheory.Square.IsPullback

Definitions

Name	Category	Theorems
`isLimit` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`flip` 📖	mathematical	`CategoryTheory.Square.IsPullback`	`CategoryTheory.Square.flip`	—	`CategoryTheory.IsPullback.flip`
`iff_of_iso` 📖	mathematical	—	`CategoryTheory.Square.IsPullback`	—	`of_iso`
`mk` 📖	mathematical	—	`CategoryTheory.Square.IsPullback`	—	`CategoryTheory.Square.isPullback_iff`
`mono_f₁₂` 📖	mathematical	`CategoryTheory.Square.IsPullback`	`CategoryTheory.Mono` `CategoryTheory.Square.X₁` `CategoryTheory.Square.X₂` `CategoryTheory.Square.f₁₂`	—	`mono_f₁₃` `flip`
`mono_f₁₃` 📖	mathematical	`CategoryTheory.Square.IsPullback`	`CategoryTheory.Mono` `CategoryTheory.Square.X₁` `CategoryTheory.Square.X₃` `CategoryTheory.Square.f₁₃`	—	`CategoryTheory.MorphismProperty.of_isPullback` `CategoryTheory.MorphismProperty.IsStableUnderBaseChange.monomorphisms`
`of_iso` 📖	—	`CategoryTheory.Square.IsPullback`	—	—	`CategoryTheory.IsPullback.of_iso` `CategoryTheory.Square.Hom.comm₁₂` `CategoryTheory.Square.Hom.comm₁₃` `CategoryTheory.Square.Hom.comm₂₄` `CategoryTheory.Square.Hom.comm₃₄`
`op` 📖	mathematical	`CategoryTheory.Square.IsPullback`	`CategoryTheory.Square.IsPushout` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Square.op`	—	`CategoryTheory.IsPullback.op` `CategoryTheory.IsPullback.flip`
`unop` 📖	mathematical	`CategoryTheory.Square.IsPullback` `Opposite` `CategoryTheory.Category.opposite`	`CategoryTheory.Square.IsPushout` `CategoryTheory.Square.unop`	—	`CategoryTheory.IsPullback.unop` `CategoryTheory.IsPullback.flip`

CategoryTheory.Square.IsPushout

Definitions

Name	Category	Theorems
`isColimit` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi_f₂₄` 📖	mathematical	`CategoryTheory.Square.IsPushout`	`CategoryTheory.Epi` `CategoryTheory.Square.X₂` `CategoryTheory.Square.X₄` `CategoryTheory.Square.f₂₄`	—	`CategoryTheory.MorphismProperty.of_isPushout` `CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.epimorphisms`
`epi_f₃₄` 📖	mathematical	`CategoryTheory.Square.IsPushout`	`CategoryTheory.Epi` `CategoryTheory.Square.X₃` `CategoryTheory.Square.X₄` `CategoryTheory.Square.f₃₄`	—	`epi_f₂₄` `flip`
`flip` 📖	mathematical	`CategoryTheory.Square.IsPushout`	`CategoryTheory.Square.flip`	—	`CategoryTheory.IsPushout.flip`
`iff_of_iso` 📖	mathematical	—	`CategoryTheory.Square.IsPushout`	—	`of_iso`
`mk` 📖	mathematical	—	`CategoryTheory.Square.IsPushout`	—	`CategoryTheory.Square.isPushout_iff`
`of_iso` 📖	—	`CategoryTheory.Square.IsPushout`	—	—	`CategoryTheory.IsPushout.of_iso` `CategoryTheory.Square.Hom.comm₁₂` `CategoryTheory.Square.Hom.comm₁₃` `CategoryTheory.Square.Hom.comm₂₄` `CategoryTheory.Square.Hom.comm₃₄`
`op` 📖	mathematical	`CategoryTheory.Square.IsPushout`	`CategoryTheory.Square.IsPullback` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Square.op`	—	`CategoryTheory.IsPushout.op` `CategoryTheory.IsPushout.flip`
`unop` 📖	mathematical	`CategoryTheory.Square.IsPushout` `Opposite` `CategoryTheory.Category.opposite`	`CategoryTheory.Square.IsPullback` `CategoryTheory.Square.unop`	—	`CategoryTheory.IsPushout.unop` `CategoryTheory.IsPushout.flip`

---

← Back to Index