Documentation Verification Report

Limits

📁 Source: Mathlib/Algebra/Category/Ring/Under/Limits.lean

Statistics

Metric	Count
Definitions `equalizerFork`, `equalizerFork'`, `equalizerFork'IsLimit`, `equalizerForkIsLimit`, `equalizerForkTensorProdIso`, `piFan`, `piFanIsLimit`, `piFanTensorProductIsLimit`, `tensorProdEqualizer`, `tensorProdMapEqualizerForkIsLimit`, `tensorProductFan`, `tensorProductFan'`, `tensorProductFanIsLimit`, `tensorProductFanIso`	14
Theorems `equalizerFork'_ι`, `equalizerFork_ι`, `equalizer_comp`, `instPreservesFiniteLimitsUnderTensorProdOfFlatCarrier`, `instPreservesFiniteProductsUnderPushout`, `instPreservesFiniteProductsUnderTensorProd`, `instPreservesLimitUnderDiscreteFunctorTensorProdOfFinite`, `instPreservesLimitUnderWalkingParallelPairParallelPairTensorProdOfFlatCarrier`, `instPreservesLimitsOfShapeUnderWalkingParallelPairTensorProdOfFlatCarrier`, `preservesFiniteLimits_of_flat`, `tensorProdEqualizer_ι`	11
Total	25

CommRingCat.Under

Definitions

Name	Category	Theorems
`equalizerFork` 📖	CompOp	1 math math: `equalizerFork_ι`
`equalizerFork'` 📖	CompOp	1 math math: `equalizerFork'_ι`
`equalizerFork'IsLimit` 📖	CompOp	—
`equalizerForkIsLimit` 📖	CompOp	—
`equalizerForkTensorProdIso` 📖	CompOp	—
`piFan` 📖	CompOp	—
`piFanIsLimit` 📖	CompOp	—
`piFanTensorProductIsLimit` 📖	CompOp	—
`tensorProdEqualizer` 📖	CompOp	1 math math: `tensorProdEqualizer_ι`
`tensorProdMapEqualizerForkIsLimit` 📖	CompOp	—
`tensorProductFan` 📖	CompOp	—
`tensorProductFan'` 📖	CompOp	—
`tensorProductFanIsLimit` 📖	CompOp	—
`tensorProductFanIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equalizerFork'_ι` 📖	mathematical	—	`CategoryTheory.Limits.Fork.ι` `CategoryTheory.Under` `CommRingCat` `CommRingCat.instCategory` `CategoryTheory.instCategoryUnder` `CommRingCat.mkUnder` `AlgHom.toUnder` `equalizerFork'` `Subalgebra` `CommRingCat.carrier` `CommRing.toCommSemiring` `CommRingCat.commRing` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.equalizer` `AlgHom` `AlgHom.funLike` `AlgHom.algHomClass` `Subalgebra.toCommRing` `Subalgebra.algebra` `Subalgebra.val`	—	—
`equalizerFork_ι` 📖	mathematical	—	`CategoryTheory.Limits.Fork.ι` `CategoryTheory.Under` `CommRingCat` `CommRingCat.instCategory` `CategoryTheory.instCategoryUnder` `equalizerFork` `AlgHom.toUnder` `CommRingCat.carrier` `CategoryTheory.Comma.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Functor.id` `Subalgebra` `CommRing.toCommSemiring` `CommRingCat.commRing` `CommSemiring.toSemiring` `CommRingCat.instAlgebraCarrierRightDiscretePUnit` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.equalizer` `AlgHom` `CommRingCat.toAlgHom` `AlgHom.funLike` `AlgHom.algHomClass` `Subalgebra.toCommRing` `Subalgebra.algebra` `Subalgebra.val`	—	—
`equalizer_comp` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Under` `CommRingCat` `CommRingCat.instCategory` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.instCategoryUnder` `CommRingCat.mkUnder` `CommRingCat.carrier` `CategoryTheory.Comma.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Functor.id` `Subalgebra` `CommRing.toCommSemiring` `CommRingCat.commRing` `CommSemiring.toSemiring` `CommRingCat.instAlgebraCarrierRightDiscretePUnit` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.equalizer` `AlgHom` `CommRingCat.toAlgHom` `AlgHom.funLike` `AlgHom.algHomClass` `Subalgebra.toCommRing` `Subalgebra.algebra` `AlgHom.toUnder` `Subalgebra.val`	—	`CommRingCat.mkUnder_ext` `AlgHom.algHomClass`
`instPreservesFiniteLimitsUnderTensorProdOfFlatCarrier` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteLimits` `CategoryTheory.Under` `CommRingCat` `CommRingCat.instCategory` `CategoryTheory.instCategoryUnder` `CommRingCat.tensorProd`	—	`CategoryTheory.Limits.preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts` `CategoryTheory.Under.instHasLimitsOfShape` `CommRingCat.hasLimitsOfShape` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits` `CategoryTheory.Limits.hasFiniteLimits_of_hasLimits` `CategoryTheory.Under.instHasLimits` `CommRingCat.hasLimits` `instPreservesLimitsOfShapeUnderWalkingParallelPairTensorProdOfFlatCarrier` `instPreservesFiniteProductsUnderTensorProd`
`instPreservesFiniteProductsUnderPushout` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteProducts` `CategoryTheory.Under` `CommRingCat` `CommRingCat.instCategory` `CategoryTheory.instCategoryUnder` `CategoryTheory.Under.pushout` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.WalkingSpan` `CategoryTheory.Limits.WidePushoutShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits` `CategoryTheory.Limits.hasFiniteColimits_of_hasColimits` `CommRingCat.Colimits.hasColimits_commRingCat` `CategoryTheory.Limits.span`	—	`CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits` `CategoryTheory.Limits.hasFiniteColimits_of_hasColimits` `CommRingCat.Colimits.hasColimits_commRingCat` `CategoryTheory.Limits.preservesLimitsOfShape_of_natIso` `CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts` `instPreservesFiniteProductsUnderTensorProd`
`instPreservesFiniteProductsUnderTensorProd` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteProducts` `CategoryTheory.Under` `CommRingCat` `CommRingCat.instCategory` `CategoryTheory.instCategoryUnder` `CommRingCat.tensorProd`	—	`CategoryTheory.Limits.preservesLimitsOfShape_of_discrete` `instPreservesLimitUnderDiscreteFunctorTensorProdOfFinite` `instFiniteULift` `Finite.of_fintype` `CategoryTheory.Limits.preservesLimitsOfShape_of_equiv`
`instPreservesLimitUnderDiscreteFunctorTensorProdOfFinite` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimit` `CategoryTheory.Under` `CommRingCat` `CommRingCat.instCategory` `CategoryTheory.instCategoryUnder` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `CommRingCat.tensorProd`	—	`CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone`
`instPreservesLimitUnderWalkingParallelPairParallelPairTensorProdOfFlatCarrier` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimit` `CategoryTheory.Under` `CommRingCat` `CommRingCat.instCategory` `CategoryTheory.instCategoryUnder` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `CommRingCat.tensorProd`	—	`CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone`
`instPreservesLimitsOfShapeUnderWalkingParallelPairTensorProdOfFlatCarrier` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimitsOfShape` `CategoryTheory.Under` `CommRingCat` `CommRingCat.instCategory` `CategoryTheory.instCategoryUnder` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CommRingCat.tensorProd`	—	`CategoryTheory.Limits.preservesLimit_of_iso_diagram` `instPreservesLimitUnderWalkingParallelPairParallelPairTensorProdOfFlatCarrier`
`preservesFiniteLimits_of_flat` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteLimits` `CategoryTheory.Under` `CommRingCat` `CommRingCat.instCategory` `CategoryTheory.instCategoryUnder` `CategoryTheory.Under.pushout` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.WalkingSpan` `CategoryTheory.Limits.WidePushoutShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits` `CategoryTheory.Limits.hasFiniteColimits_of_hasColimits` `CommRingCat.Colimits.hasColimits_commRingCat` `CategoryTheory.Limits.span`	—	`CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits` `CategoryTheory.Limits.hasFiniteColimits_of_hasColimits` `CommRingCat.Colimits.hasColimits_commRingCat` `CategoryTheory.Limits.preservesLimitsOfShape_of_natIso` `CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits` `instPreservesFiniteLimitsUnderTensorProdOfFlatCarrier`
`tensorProdEqualizer_ι` 📖	mathematical	—	`CategoryTheory.Limits.Fork.ι` `CategoryTheory.Under` `CommRingCat` `CommRingCat.instCategory` `CategoryTheory.instCategoryUnder` `CategoryTheory.Functor.obj` `CommRingCat.tensorProd` `CategoryTheory.Functor.map` `tensorProdEqualizer` `CommRingCat.mkUnder` `CommRingCat.carrier` `CategoryTheory.Comma.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Functor.id` `Subalgebra` `CommRing.toCommSemiring` `CommRingCat.commRing` `CommSemiring.toSemiring` `CommRingCat.instAlgebraCarrierRightDiscretePUnit` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.equalizer` `AlgHom` `CommRingCat.toAlgHom` `AlgHom.funLike` `AlgHom.algHomClass` `Subalgebra.toCommRing` `Subalgebra.algebra` `AlgHom.toUnder` `Subalgebra.val`	—	—

---

← Back to Index