Documentation Verification Report

Local

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

Statistics

Metric	Count
Definitions `IsLocalAtSource`, `IsLocalAtTarget`	2
Theorems `comp`, `iff_of_zeroHypercover`, `inf`, `mk_of_iff`, `of_le`, `of_zeroHypercover`, `toRespects`, `top`, `iff_of_zeroHypercover`, `inf`, `mk_of_iff`, `mk_of_isStableUnderBaseChange`, `of_isPullback`, `of_le`, `of_zeroHypercover`, `pullbackSnd`, `toRespects`, `top`, `iff_of_zeroHypercover_source`, `iff_of_zeroHypercover_target`, `of_zeroHypercover_source`, `of_zeroHypercover_target`, `eq_of_zeroHypercover_target`	23
Total	25

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_zeroHypercover_target` 📖	—	`CategoryStruct.comp` `Category.toCategoryStruct` `Limits.pullback.map` `PreZeroHypercover.X` `Precoverage.ZeroHypercover.toPreZeroHypercover` `PreZeroHypercover.f` `Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1` `Precoverage.ZeroHypercover.instHasPullbacksPresieve₀OfHasPullbacks` `Precoverage.instHasPullbacksOfHasPullbacks` `CategoryStruct.id`	—	—	`Precoverage.instHasPullbacksOfHasPullbacks` `Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1` `Precoverage.ZeroHypercover.instHasPullbacksPresieve₀OfHasPullbacks` `Limits.hasLimitOfHasLimitsOfShape` `MorphismProperty.iff_of_zeroHypercover_target` `IsPullback.instHasPullbackFst` `Limits.pullback.hom_ext` `Category.assoc` `Limits.equalizerPullbackMapIso_inv_ι_fst` `Limits.pullback.condition` `Limits.equalizerPullbackMapIso_inv_ι_snd` `Iso.isIso_inv` `Limits.equalizer.ι_of_eq` `Limits.eq_of_epi_equalizer` `epi_of_effectiveEpi` `instEffectiveEpiOfIsIso`

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
`IsLocalAtSource` 📖	CompData	4 math math: `IsLocalAtSource.inf`, `IsLocalAtSource.top`, `IsLocalAtSource.of_le`, `IsLocalAtSource.mk_of_iff`
`IsLocalAtTarget` 📖	CompData	7 math math: `IsLocalAtTarget.mk_of_iff`, `IsLocalAtTarget.top`, `CategoryTheory.Precoverage.ZeroHypercover.instIsLocalAtTargetIsomorphisms`, `IsLocalAtTarget.of_le`, `AlgebraicGeometry.Scheme.instIsLocalAtTargetIsomorphismsZariskiPrecoverage`, `IsLocalAtTarget.inf`, `IsLocalAtTarget.mk_of_isStableUnderBaseChange`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iff_of_zeroHypercover_source` 📖	mathematical	—	`CategoryTheory.PreZeroHypercover.X` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.PreZeroHypercover.f`	—	`IsLocalAtSource.iff_of_zeroHypercover`
`iff_of_zeroHypercover_target` 📖	mathematical	—	`CategoryTheory.Limits.pullback` `CategoryTheory.PreZeroHypercover.X` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `CategoryTheory.PreZeroHypercover.f` `CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1` `CategoryTheory.Precoverage.ZeroHypercover.instHasPullbacksPresieve₀OfHasPullbacks` `CategoryTheory.Limits.pullback.snd`	—	`IsLocalAtTarget.iff_of_zeroHypercover`
`of_zeroHypercover_source` 📖	—	`CategoryTheory.PreZeroHypercover.X` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.PreZeroHypercover.f`	—	—	`IsLocalAtSource.iff_of_zeroHypercover`
`of_zeroHypercover_target` 📖	—	`CategoryTheory.Limits.pullback` `CategoryTheory.PreZeroHypercover.X` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `CategoryTheory.PreZeroHypercover.f` `CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1` `CategoryTheory.Precoverage.ZeroHypercover.instHasPullbacksPresieve₀OfHasPullbacks` `CategoryTheory.Limits.pullback.snd`	—	—	`CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1` `CategoryTheory.Precoverage.ZeroHypercover.instHasPullbacksPresieve₀OfHasPullbacks` `IsLocalAtTarget.iff_of_zeroHypercover`

CategoryTheory.MorphismProperty.IsLocalAtSource

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	—	`CategoryTheory.PreZeroHypercover.X` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.PreZeroHypercover.f`	—	—
`iff_of_zeroHypercover` 📖	mathematical	—	`CategoryTheory.PreZeroHypercover.X` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.PreZeroHypercover.f`	—	`comp` `of_zeroHypercover`
`inf` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsLocalAtSource` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	—	`CategoryTheory.MorphismProperty.inf` `toRespects` `comp` `of_zeroHypercover`
`mk_of_iff` 📖	mathematical	`CategoryTheory.PreZeroHypercover.X` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.PreZeroHypercover.f`	`CategoryTheory.MorphismProperty.IsLocalAtSource`	—	—
`of_le` 📖	mathematical	`CategoryTheory.Precoverage` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.Precoverage.instPartialOrder`	`CategoryTheory.MorphismProperty.IsLocalAtSource`	—	`toRespects` `comp` `of_zeroHypercover`
`of_zeroHypercover` 📖	—	`CategoryTheory.PreZeroHypercover.X` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.PreZeroHypercover.f`	—	—	—
`toRespects` 📖	mathematical	—	`CategoryTheory.MorphismProperty.Respects` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MorphismProperty.isomorphisms`	—	—
`top` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsLocalAtSource` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	—	`CategoryTheory.MorphismProperty.instRespectsIsoTop`

CategoryTheory.MorphismProperty.IsLocalAtTarget

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iff_of_zeroHypercover` 📖	mathematical	—	`CategoryTheory.Limits.pullback` `CategoryTheory.PreZeroHypercover.X` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `CategoryTheory.PreZeroHypercover.f` `CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1` `CategoryTheory.Precoverage.ZeroHypercover.instHasPullbacksPresieve₀OfHasPullbacks` `CategoryTheory.Limits.pullback.snd`	—	`CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1` `CategoryTheory.Precoverage.ZeroHypercover.instHasPullbacksPresieve₀OfHasPullbacks` `pullbackSnd` `of_zeroHypercover`
`inf` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsLocalAtTarget` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	—	`CategoryTheory.MorphismProperty.inf` `toRespects` `CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1` `CategoryTheory.Precoverage.ZeroHypercover.instHasPullbacksPresieve₀OfHasPullbacks` `pullbackSnd` `of_zeroHypercover`
`mk_of_iff` 📖	mathematical	`CategoryTheory.Limits.pullback` `CategoryTheory.PreZeroHypercover.X` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `CategoryTheory.PreZeroHypercover.f` `CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1` `CategoryTheory.Precoverage.ZeroHypercover.instHasPullbacksPresieve₀OfHasPullbacks` `CategoryTheory.Limits.pullback.snd`	`CategoryTheory.MorphismProperty.IsLocalAtTarget`	—	`CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1` `CategoryTheory.Precoverage.ZeroHypercover.instHasPullbacksPresieve₀OfHasPullbacks`
`mk_of_isStableUnderBaseChange` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsLocalAtTarget`	—	`CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1` `CategoryTheory.Precoverage.ZeroHypercover.instHasPullbacksPresieve₀OfHasPullbacks` `CategoryTheory.MorphismProperty.IsStableUnderBaseChange.respectsIso` `CategoryTheory.MorphismProperty.pullback_snd` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange`
`of_isPullback` 📖	—	`CategoryTheory.IsPullback` `CategoryTheory.PreZeroHypercover.X` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `CategoryTheory.PreZeroHypercover.f`	—	—	`CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1` `CategoryTheory.Precoverage.ZeroHypercover.instHasPullbacksPresieve₀OfHasPullbacks` `CategoryTheory.MorphismProperty.cancel_left_of_respectsIso` `toRespects` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.IsPullback.isoPullback_inv_snd` `pullbackSnd`
`of_le` 📖	mathematical	`CategoryTheory.Precoverage` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.Precoverage.instPartialOrder`	`CategoryTheory.MorphismProperty.IsLocalAtTarget`	—	`toRespects` `pullbackSnd` `of_zeroHypercover`
`of_zeroHypercover` 📖	—	`CategoryTheory.Limits.pullback` `CategoryTheory.PreZeroHypercover.X` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `CategoryTheory.PreZeroHypercover.f` `CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1` `CategoryTheory.Precoverage.ZeroHypercover.instHasPullbacksPresieve₀OfHasPullbacks` `CategoryTheory.Limits.pullback.snd`	—	—	—
`pullbackSnd` 📖	mathematical	—	`CategoryTheory.Limits.pullback` `CategoryTheory.PreZeroHypercover.X` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `CategoryTheory.PreZeroHypercover.f` `CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1` `CategoryTheory.Precoverage.ZeroHypercover.instHasPullbacksPresieve₀OfHasPullbacks` `CategoryTheory.Limits.pullback.snd`	—	—
`toRespects` 📖	mathematical	—	`CategoryTheory.MorphismProperty.Respects` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MorphismProperty.isomorphisms`	—	—
`top` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsLocalAtTarget` `Top.top` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra`	—	`CategoryTheory.MorphismProperty.instRespectsIsoTop` `CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1` `CategoryTheory.Precoverage.ZeroHypercover.instHasPullbacksPresieve₀OfHasPullbacks`

---

← Back to Index