Basic

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

Statistics

Metric	Count
Definitions toUnder, toUnder, instAlgebraCarrierRightDiscretePUnit, instCoeSortUnderType, mkUnder, tensorProd, tensorProdIsoPushout, tensorProdObjIsoPushoutObj, toAlgHom	9
Theorems toUnder_hom_right_apply, toUnder_inv_right_apply, toUnder_trans, toUnder_comp, toUnder_right, mkUnder_ext, mkUnder_ext_iff, mkUnder_hom, mkUnder_right, pushout_inl_tensorProdObjIsoPushoutObj_inv_right, pushout_inl_tensorProdObjIsoPushoutObj_inv_right_assoc, pushout_inr_tensorProdObjIsoPushoutObj_inv_right, pushout_inr_tensorProdObjIsoPushoutObj_inv_right_assoc, tensorProdIsoPushout_app, tensorProd_map_right, toAlgHom_apply, toAlgHom_comp, toAlgHom_id	18
Total	27

AlgEquiv

Definitions

Name	Category	Theorems
toUnder 📖	CompOp	3 math math: toUnder_trans, toUnder_inv_right_apply, toUnder_hom_right_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toUnder_hom_right_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CommRingCat CommRingCat.instCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CommRingCat.mkUnder CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier CategoryTheory.CommaMorphism.right CategoryTheory.Iso.hom CategoryTheory.Under CategoryTheory.instCategoryUnder toUnder AlgEquiv instFunLike	—	—
toUnder_inv_right_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CommRingCat CommRingCat.instCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CommRingCat.mkUnder CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier CategoryTheory.CommaMorphism.right CategoryTheory.Iso.inv CategoryTheory.Under CategoryTheory.instCategoryUnder toUnder AlgEquiv instFunLike symm	—	—
toUnder_trans 📖	mathematical	—	toUnder trans CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing CommSemiring.toSemiring CategoryTheory.Iso.trans CategoryTheory.Under CommRingCat CommRingCat.instCategory CategoryTheory.instCategoryUnder CommRingCat.mkUnder	—	—

AlgHom

Definitions

Name	Category	Theorems
toUnder 📖	CompOp	9 math math: toUnder_comp, CommRingCat.Under.tensorProdEqualizer_ι, commAlgCatEquivUnder_counitIso, toUnder_right, commAlgCatEquivUnder_unitIso, CommRingCat.Under.equalizerFork_ι, commAlgCatEquivUnder_functor_map, CommRingCat.Under.equalizer_comp, CommRingCat.Under.equalizerFork'_ι

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toUnder_comp 📖	mathematical	—	toUnder comp CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing CommSemiring.toSemiring CategoryTheory.CategoryStruct.comp CategoryTheory.Under CommRingCat CommRingCat.instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryUnder CommRingCat.mkUnder	—	—
toUnder_right 📖	mathematical	—	DFunLike.coe CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CommRingCat CommRingCat.instCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CommRingCat.mkUnder CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier CategoryTheory.CommaMorphism.right toUnder AlgHom funLike	—	—

CommRingCat

Definitions

Name	Category	Theorems
instAlgebraCarrierRightDiscretePUnit 📖	CompOp	14 math math: tensorProd_map_right, toAlgHom_comp, pushout_inr_tensorProdObjIsoPushoutObj_inv_right_assoc, Under.tensorProdEqualizer_ι, toAlgHom_id, toAlgHom_apply, pushout_inl_tensorProdObjIsoPushoutObj_inv_right_assoc, commAlgCatEquivUnder_counitIso, pushout_inl_tensorProdObjIsoPushoutObj_inv_right, commAlgCatEquivUnder_unitIso, commAlgCatEquivUnder_inverse_map, Under.equalizerFork_ι, Under.equalizer_comp, pushout_inr_tensorProdObjIsoPushoutObj_inv_right
instCoeSortUnderType 📖	CompOp	—
mkUnder 📖	CompOp	19 math math: tensorProd_map_right, mkUnder_ext_iff, pushout_inr_tensorProdObjIsoPushoutObj_inv_right_assoc, AlgHom.toUnder_comp, commAlgCatEquivUnder_functor_obj, mkUnder_hom, AlgEquiv.toUnder_trans, Under.tensorProdEqualizer_ι, mkUnder_right, AlgEquiv.toUnder_inv_right_apply, pushout_inl_tensorProdObjIsoPushoutObj_inv_right_assoc, commAlgCatEquivUnder_counitIso, pushout_inl_tensorProdObjIsoPushoutObj_inv_right, AlgHom.toUnder_right, AlgEquiv.toUnder_hom_right_apply, commAlgCatEquivUnder_unitIso, Under.equalizer_comp, Under.equalizerFork'_ι, pushout_inr_tensorProdObjIsoPushoutObj_inv_right
tensorProd 📖	CompOp	8 math math: tensorProd_map_right, Under.instPreservesFiniteLimitsUnderTensorProdOfFlatCarrier, Under.instPreservesLimitsOfShapeUnderWalkingParallelPairTensorProdOfFlatCarrier, Under.tensorProdEqualizer_ι, Under.instPreservesLimitUnderDiscreteFunctorTensorProdOfFinite, tensorProdIsoPushout_app, Under.instPreservesFiniteProductsUnderTensorProd, Under.instPreservesLimitUnderWalkingParallelPairParallelPairTensorProdOfFlatCarrier
tensorProdIsoPushout 📖	CompOp	1 math math: tensorProdIsoPushout_app
tensorProdObjIsoPushoutObj 📖	CompOp	5 math math: pushout_inr_tensorProdObjIsoPushoutObj_inv_right_assoc, pushout_inl_tensorProdObjIsoPushoutObj_inv_right_assoc, pushout_inl_tensorProdObjIsoPushoutObj_inv_right, tensorProdIsoPushout_app, pushout_inr_tensorProdObjIsoPushoutObj_inv_right
toAlgHom 📖	CompOp	10 math math: tensorProd_map_right, toAlgHom_comp, Under.tensorProdEqualizer_ι, toAlgHom_id, toAlgHom_apply, commAlgCatEquivUnder_counitIso, commAlgCatEquivUnder_unitIso, commAlgCatEquivUnder_inverse_map, Under.equalizerFork_ι, Under.equalizer_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mkUnder_ext 📖	—	DFunLike.coe CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CommRingCat instCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id mkUnder carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring commRing RingHom.instFunLike instConcreteCategoryRingHomCarrier CategoryTheory.CommaMorphism.right	—	—	CategoryTheory.Under.UnderMorphism.ext hom_ext RingHom.ext
mkUnder_ext_iff 📖	mathematical	—	DFunLike.coe CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CommRingCat instCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id mkUnder carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring commRing RingHom.instFunLike instConcreteCategoryRingHomCarrier CategoryTheory.CommaMorphism.right	—	mkUnder_ext
mkUnder_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CommRingCat instCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id mkUnder ofHom carrier commRing algebraMap CommRing.toCommSemiring CommSemiring.toSemiring	—	—
mkUnder_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CommRingCat instCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id mkUnder of	—	—
pushout_inl_tensorProdObjIsoPushoutObj_inv_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Limits.pushout CategoryTheory.Comma.left of carrier commRing CategoryTheory.Comma.hom ofHom algebraMap CommRing.toCommSemiring CommSemiring.toSemiring 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 Colimits.hasColimits_commRingCat CategoryTheory.Limits.span mkUnder TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule instAlgebraCarrierRightDiscretePUnit Algebra.TensorProduct.instCommRing Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass CategoryTheory.Limits.pushout.inl CategoryTheory.CommaMorphism.right CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Under.pushout CategoryTheory.Iso.inv tensorProdObjIsoPushoutObj AlgHom.toRingHom NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra Algebra.TensorProduct.includeRight	—	Algebra.to_smulCommClass 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 AlgHomClass.toRingHomClass AlgHom.algHomClass CategoryTheory.IsPushout.inl_isoPushout_inv
pushout_inl_tensorProdObjIsoPushoutObj_inv_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.Limits.pushout CategoryTheory.Functor.obj CategoryTheory.Comma.left of carrier commRing CategoryTheory.Comma.hom ofHom algebraMap CommRing.toCommSemiring CommSemiring.toSemiring 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 Colimits.hasColimits_commRingCat CategoryTheory.Limits.span CategoryTheory.Limits.pushout.inl mkUnder TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule instAlgebraCarrierRightDiscretePUnit Algebra.TensorProduct.instCommRing Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass CategoryTheory.CommaMorphism.right CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Under.pushout CategoryTheory.Iso.inv tensorProdObjIsoPushoutObj AlgHom.toRingHom NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra Algebra.TensorProduct.includeRight	—	Algebra.to_smulCommClass 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 CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pushout_inl_tensorProdObjIsoPushoutObj_inv_right
pushout_inr_tensorProdObjIsoPushoutObj_inv_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct instCategory of carrier commRing CategoryTheory.Limits.pushout CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom ofHom algebraMap CommRing.toCommSemiring CommSemiring.toSemiring 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 Colimits.hasColimits_commRingCat CategoryTheory.Limits.span mkUnder TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule instAlgebraCarrierRightDiscretePUnit Algebra.TensorProduct.instCommRing Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass CategoryTheory.Limits.pushout.inr CategoryTheory.CommaMorphism.right CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Under.pushout CategoryTheory.Iso.inv tensorProdObjIsoPushoutObj Algebra.TensorProduct.includeLeftRingHom	—	Algebra.to_smulCommClass 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 CategoryTheory.IsPushout.inr_isoPushout_inv AlgHomClass.toRingHomClass AlgHom.algHomClass
pushout_inr_tensorProdObjIsoPushoutObj_inv_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct instCategory of carrier commRing CategoryTheory.Limits.pushout CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom ofHom algebraMap CommRing.toCommSemiring CommSemiring.toSemiring 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 Colimits.hasColimits_commRingCat CategoryTheory.Limits.span CategoryTheory.Limits.pushout.inr mkUnder TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule instAlgebraCarrierRightDiscretePUnit Algebra.TensorProduct.instCommRing Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass CategoryTheory.CommaMorphism.right CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Under.pushout CategoryTheory.Iso.inv tensorProdObjIsoPushoutObj Algebra.TensorProduct.includeLeftRingHom	—	Algebra.to_smulCommClass 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 CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pushout_inr_tensorProdObjIsoPushoutObj_inv_right
tensorProdIsoPushout_app 📖	mathematical	—	CategoryTheory.Iso.app CategoryTheory.Under CommRingCat instCategory CategoryTheory.instCategoryUnder tensorProd CategoryTheory.Under.pushout ofHom carrier commRing algebraMap CommRing.toCommSemiring CommSemiring.toSemiring 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 Colimits.hasColimits_commRingCat CategoryTheory.Limits.span tensorProdIsoPushout tensorProdObjIsoPushoutObj	—	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
tensorProd_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Discrete CategoryTheory.discreteCategory CommRingCat instCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id mkUnder TensorProduct carrier CommRing.toCommSemiring commRing CategoryTheory.Comma.right NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule instAlgebraCarrierRightDiscretePUnit Algebra.TensorProduct.instCommRing Algebra.TensorProduct.leftAlgebra Algebra.id CategoryTheory.Functor.map CategoryTheory.Under CategoryTheory.instCategoryUnder tensorProd ofHom RingHomClass.toRingHom AlgHom AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass Algebra.TensorProduct.map AlgHom.id toAlgHom	—	—
toAlgHom_apply 📖	mathematical	—	DFunLike.coe AlgHom carrier CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CommRingCat instCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CommRing.toCommSemiring commRing CommSemiring.toSemiring instAlgebraCarrierRightDiscretePUnit AlgHom.funLike toAlgHom CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring RingHom.instFunLike instConcreteCategoryRingHomCarrier CategoryTheory.CommaMorphism.right	—	—
toAlgHom_comp 📖	mathematical	—	toAlgHom CategoryTheory.CategoryStruct.comp CategoryTheory.Under CommRingCat instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryUnder AlgHom.comp carrier CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CommRing.toCommSemiring commRing CommSemiring.toSemiring instAlgebraCarrierRightDiscretePUnit	—	—
toAlgHom_id 📖	mathematical	—	toAlgHom CategoryTheory.CategoryStruct.id CategoryTheory.Under CommRingCat instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryUnder AlgHom.id carrier CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CommRing.toCommSemiring commRing CommSemiring.toSemiring instAlgebraCarrierRightDiscretePUnit	—	—

---

← Back to Index