Constructions

📁 Source: Mathlib/Algebra/Category/Ring/Constructions.lean

Statistics

Metric	Count
Definitions `coproductCocone`, `coproductCoconeIsColimit`, `coproductColimitCocone`, `equalizerFork`, `equalizerForkIsLimit`, `instUniqueHomOfPUnit`, `isInitial`, `piFan`, `piFanIsLimit`, `piIsoPi`, `prodFan`, `prodFanIsLimit`, `pullbackCone`, `pullbackConeIsLimit`, `punitIsTerminal`, `pushoutCocone`, `pushoutCoconeIsColimit`, `zIsInitial`, `piEquivPi`	19
Theorems `closure_range_union_range_eq_top_of_isPushout`, `commRingCat_hasStrictTerminalObjects`, `coproductCoconeIsColimit_desc`, `coproductCocone_inl`, `coproductCocone_inr`, `coproductCocone_pt`, `coproductCocone_ι`, `equalizer_ι_isLocalHom`, `equalizer_ι_isLocalHom'`, `instIsLocalHomCarrierObjWalkingParallelPairFunctorConstPtEqualizerForkZeroParallelPairRingHomHomι`, `isPushout_iff_isPushout`, `isPushout_of_isLocalization`, `isPushout_of_isPushout`, `isPushout_tensorProduct`, `piFan_pt`, `prodFan_pt`, `pushoutCocone_inl`, `pushoutCocone_inr`, `pushoutCocone_pt`, `subsingleton_of_isTerminal`	20
Total	39

CommRingCat

Definitions

Name	Category	Theorems
`coproductCocone` 📖	CompOp	5 math math: `coproductCocone_inl`, `coproductCocone_inr`, `coproductCocone_pt`, `coproductCoconeIsColimit_desc`, `coproductCocone_ι`
`coproductCoconeIsColimit` 📖	CompOp	1 math math: `coproductCoconeIsColimit_desc`
`coproductColimitCocone` 📖	CompOp	—
`equalizerFork` 📖	CompOp	1 math math: `instIsLocalHomCarrierObjWalkingParallelPairFunctorConstPtEqualizerForkZeroParallelPairRingHomHomι`
`equalizerForkIsLimit` 📖	CompOp	—
`instUniqueHomOfPUnit` 📖	CompOp	—
`isInitial` 📖	CompOp	—
`piFan` 📖	CompOp	1 math math: `piFan_pt`
`piFanIsLimit` 📖	CompOp	—
`piIsoPi` 📖	CompOp	—
`prodFan` 📖	CompOp	1 math math: `prodFan_pt`
`prodFanIsLimit` 📖	CompOp	—
`pullbackCone` 📖	CompOp	—
`pullbackConeIsLimit` 📖	CompOp	—
`punitIsTerminal` 📖	CompOp	1 math math: `AlgebraicGeometry.Scheme.emptyTo_c_app`
`pushoutCocone` 📖	CompOp	3 math math: `pushoutCocone_pt`, `pushoutCocone_inl`, `pushoutCocone_inr`
`pushoutCoconeIsColimit` 📖	CompOp	—
`zIsInitial` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_range_union_range_eq_top_of_isPushout` 📖	mathematical	`CategoryTheory.IsPushout` `CommRingCat` `instCategory`	`Subring.closure` `carrier` `CommRing.toRing` `commRing` `Set` `Set.instUnion` `Set.range` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier` `Top.top` `Subring` `Subring.instTop`	—	`isPushout_tensorProduct` `Subring.comap_map_eq_self_of_injective` `RingEquiv.injective` `RingHom.map_closure` `top_le_iff` `Subring.map_le_iff_le_comap` `Set.image_union` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Set.image_congr` `hom_comp` `CategoryTheory.IsPushout.inl_isoIsPushout_inv` `CategoryTheory.IsPushout.inr_isoIsPushout_inv` `hom_ofHom` `LE.le.trans` `le_top` `Eq.ge` `Algebra.TensorProduct.closure_range_union_range_eq_top`
`commRingCat_hasStrictTerminalObjects` 📖	mathematical	—	`CategoryTheory.Limits.HasStrictTerminalObjects` `CommRingCat` `instCategory`	—	`CategoryTheory.Limits.hasStrictTerminalObjects_of_terminal_is_strict` `hom_ext` `RingHom.ext` `RingHom.map_one` `RingHom.map_zero` `MulZeroClass.zero_mul` `one_mul`
`coproductCoconeIsColimit_desc` 📖	mathematical	—	`CategoryTheory.Limits.IsColimit.desc` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CommRingCat` `instCategory` `CategoryTheory.Limits.pair` `coproductCocone` `coproductCoconeIsColimit` `ofHom` `TensorProduct` `Int.instCommSemiring` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `AddCommGroup.toIntModule` `Ring.toAddCommGroup` `CommRing.toRing` `Algebra.TensorProduct.instCommRing` `Ring.toIntAlgebra` `CommRing.toCommSemiring` `AlgHom.toRingHom` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingPair.left` `CategoryTheory.Limits.WalkingPair.right` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Algebra.toModule` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.TensorProduct.lift` `Algebra.id` `RingHom.toIntAlgHom` `Hom.hom` `CategoryTheory.Limits.BinaryCofan.inl` `CategoryTheory.Limits.BinaryCofan.inr`	—	—
`coproductCocone_inl` 📖	mathematical	—	`CategoryTheory.Limits.BinaryCofan.inl` `CommRingCat` `instCategory` `coproductCocone` `ofHom` `carrier` `TensorProduct` `Int.instCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `AddCommGroup.toIntModule` `Ring.toAddCommGroup` `CommRing.toRing` `Algebra.TensorProduct.instCommRing` `Ring.toIntAlgebra` `CommRing.toCommSemiring` `AlgHom.toRingHom` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `AddGroup.int_smulCommClass` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DistribMulAction.toDistribSMul` `Int.instMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Module.toDistribMulAction` `Int.instSemiring` `Algebra.TensorProduct.includeLeft`	—	—
`coproductCocone_inr` 📖	mathematical	—	`CategoryTheory.Limits.BinaryCofan.inr` `CommRingCat` `instCategory` `coproductCocone` `ofHom` `carrier` `TensorProduct` `Int.instCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `AddCommGroup.toIntModule` `Ring.toAddCommGroup` `CommRing.toRing` `Algebra.TensorProduct.instCommRing` `Ring.toIntAlgebra` `CommRing.toCommSemiring` `AlgHom.toRingHom` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.includeRight`	—	—
`coproductCocone_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CommRingCat` `instCategory` `CategoryTheory.Limits.pair` `coproductCocone` `of` `TensorProduct` `Int.instCommSemiring` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `AddCommGroup.toIntModule` `Ring.toAddCommGroup` `CommRing.toRing` `Algebra.TensorProduct.instCommRing` `Ring.toIntAlgebra` `CommRing.toCommSemiring`	—	—
`coproductCocone_ι` 📖	mathematical	—	`CategoryTheory.Limits.Cocone.ι` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CommRingCat` `instCategory` `CategoryTheory.Limits.pair` `coproductCocone` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `of` `TensorProduct` `Int.instCommSemiring` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `AddCommGroup.toIntModule` `Ring.toAddCommGroup` `CommRing.toRing` `Algebra.TensorProduct.instCommRing` `Ring.toIntAlgebra` `CommRing.toCommSemiring` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Discrete.as` `ofHom` `RingHomClass.toRingHom` `AlgHom` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `AlgHom.funLike` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Algebra.TensorProduct.includeLeft` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.includeRight` `AlgHom.toRingHom`	—	—
`equalizer_ι_isLocalHom` 📖	mathematical	—	`IsLocalHom` `carrier` `CategoryTheory.Limits.limit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CommRingCat` `instCategory` `hasLimit` `small_subtype` `small_Pi` `CategoryTheory.Functor.obj` `CategoryTheory.types` `CategoryTheory.Functor.comp` `CategoryTheory.forget` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier` `UnivLE.small` `univLE_of_max` `UnivLE.self` `Set` `Set.instMembership` `CategoryTheory.Functor.sections` `CategoryTheory.Limits.WalkingParallelPair.zero` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Hom.hom` `CategoryTheory.Limits.limit.π`	—	`hasLimit` `small_subtype` `small_Pi` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.limMap_π` `CategoryTheory.NatIso.hom_app_isIso` `CategoryTheory.IsIso.comp_inv_eq` `CategoryTheory.Limits.limit.isoLimitCone_hom_π` `hasLimitsOfShape` `isLocalHom_comp` `isLocalHom_of_isIso` `CategoryTheory.IsIso.inv_isIso` `instIsLocalHomCarrierObjWalkingParallelPairFunctorConstPtEqualizerForkZeroParallelPairRingHomHomι` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Functor.map_isIso`
`equalizer_ι_isLocalHom'` 📖	mathematical	—	`IsLocalHom` `carrier` `CategoryTheory.Limits.limit` `Opposite` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Category.opposite` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CommRingCat` `instCategory` `hasLimit` `small_subtype` `small_Pi` `CategoryTheory.Functor.obj` `CategoryTheory.types` `CategoryTheory.Functor.comp` `CategoryTheory.forget` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier` `Opposite.small` `UnivLE.small` `univLE_of_max` `UnivLE.self` `Set` `Set.instMembership` `CategoryTheory.Functor.sections` `Opposite.op` `CategoryTheory.Limits.WalkingParallelPair.one` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Hom.hom` `CategoryTheory.Limits.limit.π`	—	`hasLimit` `small_subtype` `small_Pi` `Opposite.small` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.limit.isoLimitCone_inv_π` `equalizer_ι_isLocalHom` `isLocalHom_comp` `isLocalHom_of_isIso` `CategoryTheory.Iso.isIso_inv`
`instIsLocalHomCarrierObjWalkingParallelPairFunctorConstPtEqualizerForkZeroParallelPairRingHomHomι` 📖	mathematical	—	`IsLocalHom` `carrier` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CommRingCat` `instCategory` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.parallelPair` `equalizerFork` `CategoryTheory.Limits.WalkingParallelPair.zero` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `RingHom.instFunLike` `Hom.hom` `CategoryTheory.Limits.Fork.ι`	—	`RingHom.isUnit_map` `RingHom.map_mul` `RingHom.map_one` `isUnit_iff_exists_inv` `instIsDedekindFiniteMonoid`
`isPushout_iff_isPushout` 📖	mathematical	—	`CategoryTheory.IsPushout` `CommRingCat` `instCategory` `of` `ofHom` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.IsPushout`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits` `CategoryTheory.Limits.hasFiniteColimits_of_hasColimits` `Colimits.hasColimits_commRingCat` `isPushout_tensorProduct` `CategoryTheory.IsPushout.inl_isoPushout_hom` `CategoryTheory.IsPushout.inl_isoPushout_inv` `RingEquiv.map_mul'` `RingEquiv.map_add'` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Algebra.IsPushout.of_equiv` `TensorProduct.isScalarTower_left` `Algebra.TensorProduct.right_isScalarTower` `TensorProduct.isPushout` `RingHom.ext` `CategoryTheory.IsPushout.inr_isoPushout_hom` `CategoryTheory.IsPushout.inr_isoPushout_inv` `isPushout_of_isPushout`
`isPushout_of_isLocalization` 📖	mathematical	`RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `algebraMap`	`CategoryTheory.IsPushout` `CommRingCat` `instCategory` `of` `ofHom`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsScalarTower.of_algebraMap_eq'` `isPushout_iff_isPushout` `Algebra.isPushout_of_isLocalization`
`isPushout_of_isPushout` 📖	mathematical	—	`CategoryTheory.IsPushout` `CommRingCat` `instCategory` `of` `ofHom` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	`CategoryTheory.IsPushout.of_iso` `isPushout_tensorProduct` `Algebra.to_smulCommClass` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `hom_ext` `RingHom.ext` `Algebra.IsPushout.equiv_tmul` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `mul_one` `one_mul`
`isPushout_tensorProduct` 📖	mathematical	—	`CategoryTheory.IsPushout` `CommRingCat` `instCategory` `of` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `CommSemiring.toSemiring` `Algebra.TensorProduct.instCommRing` `ofHom` `algebraMap` `Algebra.TensorProduct.includeLeftRingHom` `AlgHom.toRingHom` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.includeRight`	—	`hom_ext` `RingHom.ext` `AlgHom.comp_algebraMap_of_tower` `IsScalarTower.left` `TensorProduct.isScalarTower`
`piFan_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cone.pt` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CommRingCat` `instCategory` `CategoryTheory.Discrete.functor` `piFan` `of` `Pi.commRing` `carrier` `commRing`	—	—
`prodFan_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cone.pt` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CommRingCat` `instCategory` `CategoryTheory.Limits.pair` `prodFan` `of` `carrier` `Prod.instCommRing` `commRing`	—	—
`pushoutCocone_inl` 📖	mathematical	—	`CategoryTheory.Limits.PushoutCocone.inl` `CommRingCat` `instCategory` `of` `ofHom` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `pushoutCocone` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Algebra.TensorProduct.instCommRing` `Algebra.TensorProduct.includeLeftRingHom`	—	—
`pushoutCocone_inr` 📖	mathematical	—	`CategoryTheory.Limits.PushoutCocone.inr` `CommRingCat` `instCategory` `of` `ofHom` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `pushoutCocone` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Algebra.TensorProduct.instCommRing` `AlgHom.toRingHom` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.includeRight`	—	—
`pushoutCocone_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.WalkingSpan` `CategoryTheory.Limits.WidePushoutShape.category` `CategoryTheory.Limits.WalkingPair` `CommRingCat` `instCategory` `CategoryTheory.Limits.span` `of` `ofHom` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `pushoutCocone` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Algebra.TensorProduct.instCommRing`	—	—
`subsingleton_of_isTerminal` 📖	mathematical	—	`carrier`	—	`Equiv.subsingleton_congr`

RingEquiv

Definitions

Name	Category	Theorems
`piEquivPi` 📖	CompOp	—

---

← Back to Index