Documentation Verification Report

Descent

📁 Source: Mathlib/CategoryTheory/MorphismProperty/Descent.lean

Statistics

Metric	Count
Definitions `CodescendsAlong`, `DescendsAlong`	2
Theorems `inf`, `mk'`, `of_isPushout`, `of_le`, `top`, `inf`, `mk'`, `of_isPullback`, `of_le`, `top`, `eq_of_isomorphisms_descendsAlong`, `faithful_overPullback_of_isomorphisms_descendAlong`, `iff_of_isPullback`, `iff_of_isPushout`, `instCodescendsAlongOfIsStableUnderCobaseChangeOfHasOfPostcompPropertyOfRespectsLeft`, `instDescendsAlongDiagonalOfRespectsIsoOfIsStableUnderBaseChange`, `instDescendsAlongOfIsStableUnderBaseChangeOfHasOfPrecompPropertyOfRespectsRight`, `of_isPullback_of_descendsAlong`, `of_isPushout_of_codescendsAlong`, `of_pullback_fst_of_descendsAlong`, `of_pullback_snd_of_descendsAlong`, `of_pushout_inl_of_codescendsAlong`, `of_pushout_inr_of_descendsAlong`, `pullback_fst_iff`, `pullback_snd_iff`, `pushout_inl_iff`, `pushout_inr_iff`	27
Total	29

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
`CodescendsAlong` 📖	CompData	5 math math: `CodescendsAlong.mk'`, `CodescendsAlong.inf`, `instCodescendsAlongOfIsStableUnderCobaseChangeOfHasOfPostcompPropertyOfRespectsLeft`, `CodescendsAlong.of_le`, `CodescendsAlong.top`
`DescendsAlong` 📖	CompData	19 math math: `AlgebraicGeometry.descendsAlong_isOpenImmersion_surjective_inf_flat_inf_quasicompact'`, `AlgebraicGeometry.descendsAlong_universallyClosed_surjective_inf_flat_inf_quasicompact`, `DescendsAlong.top`, `instDescendsAlongDiagonalOfRespectsIsoOfIsStableUnderBaseChange`, `AlgebraicGeometry.descendsAlong_isomorphisms_surjective_inf_flat_inf_quasicompact`, `DescendsAlong.of_le`, `DescendsAlong.inf`, `AlgebraicGeometry.instDescendsAlongSchemeMinMorphismPropertySurjectiveFlatLocallyOfFinitePresentationOfQuasiCompactOfIsZariskiLocalAtTarget`, `DescendsAlong.mk'`, `AlgebraicGeometry.IsLocalAtTarget.descendsAlong`, `AlgebraicGeometry.HasAffineProperty.descendsAlong_of_affineAnd`, `AlgebraicGeometry.IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact`, `AlgebraicGeometry.HasRingHomProperty.descendsAlong`, `AlgebraicGeometry.Flat.surjective_descendsAlong_surjective_inf_flat_inf_quasicompact`, `AlgebraicGeometry.IsZariskiLocalAtTarget.descendsAlong`, `AlgebraicGeometry.IsLocalAtTarget.descendsAlong_inf_quasiCompact`, `AlgebraicGeometry.descendsAlong_universallyOpen_surjective_inf_flat_inf_quasicompact`, `AlgebraicGeometry.descendsAlong_universallyInjective_surjective_inf_flat_inf_quasicompact`, `instDescendsAlongOfIsStableUnderBaseChangeOfHasOfPrecompPropertyOfRespectsRight`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_isomorphisms_descendsAlong` 📖	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.pullback.map` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan` `CategoryTheory.CategoryStruct.id`	—	—	`CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `of_isPullback_of_descendsAlong` `CategoryTheory.IsPullback.instHasPullbackFst` `CategoryTheory.IsPullback.flip` `CategoryTheory.IsPullback.of_hasPullback` `pullback_fst` `instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `CategoryTheory.Limits.pullback.hom_ext` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_fst` `CategoryTheory.Limits.pullback.condition` `CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_snd` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.Limits.equalizer.ι_of_eq` `CategoryTheory.Limits.eq_of_epi_equalizer` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso`
`faithful_overPullback_of_isomorphisms_descendAlong` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Over.pullback` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan`	—	`CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Over.OverMorphism.ext` `eq_of_isomorphisms_descendsAlong` `CategoryTheory.Over.w` `CategoryTheory.Limits.pullback.hom_ext` `CategoryTheory.Limits.limit.lift_π` `CategoryTheory.Category.comp_id`
`iff_of_isPullback` 📖	—	`CategoryTheory.IsPullback`	—	—	`of_isPullback_of_descendsAlong` `of_isPullback` `CategoryTheory.IsPullback.flip`
`iff_of_isPushout` 📖	—	`CategoryTheory.IsPushout`	—	—	`of_isPushout_of_codescendsAlong` `of_isPushout`
`instCodescendsAlongOfIsStableUnderCobaseChangeOfHasOfPostcompPropertyOfRespectsLeft` 📖	mathematical	—	`CodescendsAlong`	—	`of_postcomp` `of_isPushout` `CategoryTheory.IsPushout.flip` `CategoryTheory.CommSq.w` `CategoryTheory.IsPushout.toCommSq` `RespectsLeft.precomp`
`instDescendsAlongDiagonalOfRespectsIsoOfIsStableUnderBaseChange` 📖	mathematical	—	`DescendsAlong` `diagonal`	—	`DescendsAlong.mk'` `RespectsIso.diagonal` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasPullbackHorizPaste` `CategoryTheory.IsPullback.instHasPullbackFst` `CategoryTheory.Limits.hasPullback_symmetry` `CategoryTheory.Limits.pullback.diagonal_snd_assoc` `CategoryTheory.Limits.pullback.hom_ext` `CategoryTheory.Limits.pullback.condition` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.pullback.diagonal_fst` `CategoryTheory.Category.comp_id` `CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_fst` `CategoryTheory.Limits.pullback.diagonal_fst_assoc` `CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd` `CategoryTheory.Limits.limit.lift_π` `CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst` `CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst` `CategoryTheory.Limits.pullback.diagonal_snd` `CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_snd` `CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_snd` `CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_snd` `CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd_assoc` `diagonal_iff` `of_pullback_fst_of_descendsAlong` `pullback_fst` `instIsStableUnderBaseChangeAlongCompOfHasPullbacksAlong` `instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `instHasPullbacksAlongOfHasPullbacks` `instHasPullbacksOfHasPullbacks` `cancel_left_of_respectsIso` `CategoryTheory.Iso.isIso_hom` `cancel_right_of_respectsIso`
`instDescendsAlongOfIsStableUnderBaseChangeOfHasOfPrecompPropertyOfRespectsRight` 📖	mathematical	—	`DescendsAlong`	—	`of_precomp` `of_isPullback` `CategoryTheory.CommSq.w` `CategoryTheory.IsPullback.toCommSq` `RespectsRight.postcomp`
`of_isPullback_of_descendsAlong` 📖	—	`CategoryTheory.IsPullback`	—	—	`DescendsAlong.of_isPullback`
`of_isPushout_of_codescendsAlong` 📖	—	`CategoryTheory.IsPushout`	—	—	`CodescendsAlong.of_isPushout`
`of_pullback_fst_of_descendsAlong` 📖	—	`CategoryTheory.Limits.pullback` `CategoryTheory.Limits.pullback.fst`	—	—	`of_isPullback_of_descendsAlong` `CategoryTheory.IsPullback.of_hasPullback`
`of_pullback_snd_of_descendsAlong` 📖	—	`CategoryTheory.Limits.pullback` `CategoryTheory.Limits.pullback.snd`	—	—	`of_isPullback_of_descendsAlong` `CategoryTheory.IsPullback.flip` `CategoryTheory.IsPullback.of_hasPullback`
`of_pushout_inl_of_codescendsAlong` 📖	—	`CategoryTheory.Limits.pushout` `CategoryTheory.Limits.pushout.inl`	—	—	`of_isPushout_of_codescendsAlong` `CategoryTheory.IsPushout.of_hasPushout`
`of_pushout_inr_of_descendsAlong` 📖	—	`CategoryTheory.Limits.pushout` `CategoryTheory.Limits.pushout.inr`	—	—	`of_isPushout_of_codescendsAlong` `CategoryTheory.IsPushout.flip` `CategoryTheory.IsPushout.of_hasPushout`
`pullback_fst_iff` 📖	mathematical	—	`CategoryTheory.Limits.pullback` `CategoryTheory.Limits.pullback.fst`	—	`iff_of_isPullback` `CategoryTheory.IsPullback.of_hasPullback`
`pullback_snd_iff` 📖	mathematical	—	`CategoryTheory.Limits.pullback` `CategoryTheory.Limits.pullback.snd`	—	`iff_of_isPullback` `CategoryTheory.IsPullback.flip` `CategoryTheory.IsPullback.of_hasPullback`
`pushout_inl_iff` 📖	mathematical	—	`CategoryTheory.Limits.pushout` `CategoryTheory.Limits.pushout.inl`	—	`iff_of_isPushout` `CategoryTheory.IsPushout.of_hasPushout`
`pushout_inr_iff` 📖	mathematical	—	`CategoryTheory.Limits.pushout` `CategoryTheory.Limits.pushout.inr`	—	`iff_of_isPushout` `CategoryTheory.IsPushout.flip` `CategoryTheory.IsPushout.of_hasPushout`

CategoryTheory.MorphismProperty.CodescendsAlong

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inf` 📖	mathematical	—	`CategoryTheory.MorphismProperty.CodescendsAlong` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	—	`of_isPushout`
`mk'` 📖	mathematical	—	`CategoryTheory.MorphismProperty.CodescendsAlong`	—	`CategoryTheory.IsPushout.hasPushout` `CategoryTheory.MorphismProperty.cancel_right_of_respectsIso` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.IsPushout.inl_isoPushout_inv`
`of_isPushout` 📖	—	`CategoryTheory.IsPushout`	—	—	—
`of_le` 📖	mathematical	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	`CategoryTheory.MorphismProperty.CodescendsAlong`	—	`of_isPushout`
`top` 📖	mathematical	—	`CategoryTheory.MorphismProperty.CodescendsAlong` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	—	—

CategoryTheory.MorphismProperty.DescendsAlong

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inf` 📖	mathematical	—	`CategoryTheory.MorphismProperty.DescendsAlong` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	—	`of_isPullback`
`mk'` 📖	mathematical	—	`CategoryTheory.MorphismProperty.DescendsAlong`	—	`CategoryTheory.IsPullback.hasPullback` `CategoryTheory.MorphismProperty.cancel_left_of_respectsIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.IsPullback.isoPullback_hom_fst`
`of_isPullback` 📖	—	`CategoryTheory.IsPullback`	—	—	—
`of_le` 📖	mathematical	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	`CategoryTheory.MorphismProperty.DescendsAlong`	—	`of_isPullback`
`top` 📖	mathematical	—	`CategoryTheory.MorphismProperty.DescendsAlong` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	—	—

---

← Back to Index