Basic

📁 Source: Mathlib/Algebra/Category/CommAlgCat/Basic.lean

Statistics

Metric	Count
Definitions hom, hom, hom', algEquivOfIso, algebra, carrier, commRing, fullyFaithfulUliftFunctor, hasForgetToAlgCat, hasForgetToCommRingCat, instAlgebraObjForgetAlgHomCarrier, instCategory, instCoeSortType, instCommRingObjForgetAlgHomCarrier, instConcreteCategoryAlgHomCarrier, instInhabited, isoEquivAlgEquiv, isoMk, of, ofHom, ofIso, uliftFunctor, commAlgCatEquivUnder	23
Theorems ext, ext_iff, algEquivOfIso_apply, algEquivOfIso_symm_apply, coe_of, comp_apply, forget_map, forget_obj, forget₂_algCat_map, forget₂_algCat_obj, forget₂_commRingCat_map, forget₂_commRingCat_obj, hom_comp, hom_ext, hom_ext_iff, hom_id, hom_inv_apply, hom_ofHom, id_apply, instFaithfulUliftFunctor, instFullUliftFunctor, inv_hom_apply, isoEquivAlgEquiv_apply, isoEquivAlgEquiv_symm_apply, isoMk_hom, isoMk_inv, ofHom_apply, ofHom_comp, ofHom_hom, ofHom_id, reflectsIsomorphisms_forget, commAlgCatEquivUnder_counitIso, commAlgCatEquivUnder_functor_map, commAlgCatEquivUnder_functor_obj, commAlgCatEquivUnder_inverse_map, commAlgCatEquivUnder_inverse_obj_carrier, commAlgCatEquivUnder_unitIso, instHasColimitsCommAlgCat, instHasLimitsCommAlgCat	39
Total	62

CommAlgCat

Definitions

Name	Category	Theorems
algEquivOfIso 📖	CompOp	3 math math: algEquivOfIso_apply, algEquivOfIso_symm_apply, isoEquivAlgEquiv_apply
algebra 📖	CompOp	43 math math: instFaithfulFGAlgCatUliftFunctor, comp_apply, ofHom_hom, instEssentiallySmallFGAlgCat, braiding_hom_hom, inv_hom_apply, forget₂_commRingCat_obj, ofHom_apply, forget₂_algCat_map, algEquivOfIso_apply, algEquivOfIso_symm_apply, CommBialgCat.forget₂_commAlgCat_obj, commAlgCatEquivUnder_functor_obj, lift_unop_hom, binaryCofan_pt, fst_unop_hom, hom_comp, snd_unop_hom, hom_inv_apply, tensorHom_hom, coe_tensorObj, commAlgCatEquivUnder_counitIso, binaryCofan_inl, forget₂_algCat_obj, whiskerLeft_hom, forget_obj, whiskerRight_hom, commAlgCatEquivUnder_unitIso, braiding_inv_hom, associator_inv_hom, toUnit_unop_hom, forget_map, hom_id, instFullFGAlgCatUliftFunctor, reflectsIsomorphisms_forget, instFiniteTypeCarrierObjCommAlgCat, commAlgCatEquivUnder_functor_map, binaryCofan_inr, associator_hom_hom, CommBialgCat.forget₂_commAlgCat_map, Algebra.FiniteType.exists_fgAlgCatSkeleton, id_apply, forget₂_commRingCat_map
carrier 📖	CompOp	51 math math: instFaithfulFGAlgCatUliftFunctor, comp_apply, ofHom_hom, instEssentiallySmallFGAlgCat, coe_of, commBialgCatEquivComonCommAlgCat_unitIso_inv_app, braiding_hom_hom, inv_hom_apply, forget₂_commRingCat_obj, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, ofHom_apply, forget₂_algCat_map, algEquivOfIso_apply, algEquivOfIso_symm_apply, CommBialgCat.forget₂_commAlgCat_obj, commAlgCatEquivUnder_functor_obj, lift_unop_hom, binaryCofan_pt, fst_unop_hom, hom_comp, snd_unop_hom, hom_inv_apply, tensorHom_hom, coe_tensorObj, commAlgCatEquivUnder_counitIso, binaryCofan_inl, coe_tensorUnit, commAlgCatEquivUnder_inverse_obj_carrier, forget₂_algCat_obj, whiskerLeft_hom, forget_obj, whiskerRight_hom, commAlgCatEquivUnder_unitIso, braiding_inv_hom, associator_inv_hom, toUnit_unop_hom, forget_map, hom_id, instFullFGAlgCatUliftFunctor, reflectsIsomorphisms_forget, instFiniteTypeCarrierObjCommAlgCat, commBialgCatEquivComonCommAlgCat_inverse_obj, commAlgCatEquivUnder_functor_map, binaryCofan_inr, associator_hom_hom, CommBialgCat.forget₂_commAlgCat_map, Algebra.FiniteType.exists_fgAlgCatSkeleton, id_apply, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, forget₂_commRingCat_map, commBialgCatEquivComonCommAlgCat_counitIso_inv_app
commRing 📖	CompOp	48 math math: instFaithfulFGAlgCatUliftFunctor, comp_apply, ofHom_hom, instEssentiallySmallFGAlgCat, commBialgCatEquivComonCommAlgCat_unitIso_inv_app, braiding_hom_hom, inv_hom_apply, forget₂_commRingCat_obj, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, ofHom_apply, forget₂_algCat_map, algEquivOfIso_apply, algEquivOfIso_symm_apply, CommBialgCat.forget₂_commAlgCat_obj, commAlgCatEquivUnder_functor_obj, lift_unop_hom, binaryCofan_pt, fst_unop_hom, hom_comp, snd_unop_hom, hom_inv_apply, tensorHom_hom, coe_tensorObj, commAlgCatEquivUnder_counitIso, binaryCofan_inl, forget₂_algCat_obj, whiskerLeft_hom, forget_obj, whiskerRight_hom, commAlgCatEquivUnder_unitIso, braiding_inv_hom, associator_inv_hom, toUnit_unop_hom, forget_map, hom_id, instFullFGAlgCatUliftFunctor, reflectsIsomorphisms_forget, instFiniteTypeCarrierObjCommAlgCat, commBialgCatEquivComonCommAlgCat_inverse_obj, commAlgCatEquivUnder_functor_map, binaryCofan_inr, associator_hom_hom, CommBialgCat.forget₂_commAlgCat_map, Algebra.FiniteType.exists_fgAlgCatSkeleton, id_apply, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, forget₂_commRingCat_map, commBialgCatEquivComonCommAlgCat_counitIso_inv_app
fullyFaithfulUliftFunctor 📖	CompOp	—
hasForgetToAlgCat 📖	CompOp	2 math math: forget₂_algCat_map, forget₂_algCat_obj
hasForgetToCommRingCat 📖	CompOp	2 math math: forget₂_commRingCat_obj, forget₂_commRingCat_map
instAlgebraObjForgetAlgHomCarrier 📖	CompOp	—
instCategory 📖	CompOp	68 math math: instFaithfulFGAlgCatUliftFunctor, comp_apply, instEssentiallySmallFGAlgCat, commBialgCatEquivComonCommAlgCat_unitIso_inv_app, braiding_hom_hom, inv_hom_apply, forget₂_commRingCat_obj, instFaithfulUliftFunctor, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, ofHom_apply, instHasLimitsCommAlgCat, forget₂_algCat_map, algEquivOfIso_apply, isoMk_hom, algEquivOfIso_symm_apply, CommBialgCat.forget₂_commAlgCat_obj, commAlgCatEquivUnder_functor_obj, ofHom_id, lift_unop_hom, commBialgCatEquivComonCommAlgCat_functor_obj_unop_X, mul_op_of_unop_hom, binaryCofan_pt, isoEquivAlgEquiv_apply, fst_unop_hom, hom_comp, instIsMonHomOppositeCommAlgCatOpOfHomToAlgHomBialgHom, snd_unop_hom, hom_inv_apply, tensorHom_hom, coe_tensorObj, commAlgCatEquivUnder_counitIso, binaryCofan_inl, coe_tensorUnit, commAlgCatEquivUnder_inverse_obj_carrier, forget₂_algCat_obj, whiskerLeft_hom, forget_obj, whiskerRight_hom, instIsCommMonObjOppositeCommAlgCatXUnopMonObjCommBialgCatFunctorCommBialgCatEquivComonCommAlgCatOfIsCocommCarrier, commAlgCatEquivUnder_unitIso, braiding_inv_hom, associator_inv_hom, toUnit_unop_hom, forget_map, one_op_of_unop_hom, instHasColimitsCommAlgCat, isoEquivAlgEquiv_symm_apply, hom_id, instFullFGAlgCatUliftFunctor, commAlgCatEquivUnder_inverse_map, isoMk_inv, reflectsIsomorphisms_forget, instFiniteTypeCarrierObjCommAlgCat, commBialgCatEquivComonCommAlgCat_inverse_obj, commAlgCatEquivUnder_functor_map, binaryCofan_inr, associator_hom_hom, commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom, CommBialgCat.forget₂_commAlgCat_map, Algebra.FiniteType.exists_fgAlgCatSkeleton, instIsCommMonObjOppositeCommAlgCatOpOfOfIsCocomm, ofHom_comp, id_apply, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, commBialgCatEquivComonCommAlgCat_functor_map_unop_hom, forget₂_commRingCat_map, instFullUliftFunctor, commBialgCatEquivComonCommAlgCat_counitIso_inv_app
instCoeSortType 📖	CompOp	—
instCommRingObjForgetAlgHomCarrier 📖	CompOp	—
instConcreteCategoryAlgHomCarrier 📖	CompOp	16 math math: comp_apply, inv_hom_apply, forget₂_commRingCat_obj, ofHom_apply, forget₂_algCat_map, algEquivOfIso_apply, algEquivOfIso_symm_apply, CommBialgCat.forget₂_commAlgCat_obj, hom_inv_apply, forget₂_algCat_obj, forget_obj, forget_map, reflectsIsomorphisms_forget, CommBialgCat.forget₂_commAlgCat_map, id_apply, forget₂_commRingCat_map
instInhabited 📖	CompOp	—
isoEquivAlgEquiv 📖	CompOp	2 math math: isoEquivAlgEquiv_apply, isoEquivAlgEquiv_symm_apply
isoMk 📖	CompOp	4 math math: isoMk_hom, commAlgCatEquivUnder_unitIso, isoEquivAlgEquiv_symm_apply, isoMk_inv
of 📖	CompOp	23 math math: coe_of, commBialgCatEquivComonCommAlgCat_unitIso_inv_app, hom_ofHom, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, ofHom_apply, isoMk_hom, CommBialgCat.forget₂_commAlgCat_obj, ofHom_id, commBialgCatEquivComonCommAlgCat_functor_obj_unop_X, mul_op_of_unop_hom, binaryCofan_pt, isoEquivAlgEquiv_apply, instIsMonHomOppositeCommAlgCatOpOfHomToAlgHomBialgHom, commAlgCatEquivUnder_counitIso, commAlgCatEquivUnder_unitIso, one_op_of_unop_hom, isoEquivAlgEquiv_symm_apply, isoMk_inv, instIsCommMonObjOppositeCommAlgCatOpOfOfIsCocomm, ofHom_comp, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, commBialgCatEquivComonCommAlgCat_functor_map_unop_hom, commBialgCatEquivComonCommAlgCat_counitIso_inv_app
ofHom 📖	CompOp	19 math math: ofHom_hom, commBialgCatEquivComonCommAlgCat_unitIso_inv_app, hom_ofHom, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, ofHom_apply, isoMk_hom, ofHom_id, instIsMonHomOppositeCommAlgCatOpOfHomToAlgHomBialgHom, commAlgCatEquivUnder_counitIso, binaryCofan_inl, commAlgCatEquivUnder_unitIso, commAlgCatEquivUnder_inverse_map, isoMk_inv, binaryCofan_inr, CommBialgCat.forget₂_commAlgCat_map, ofHom_comp, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, commBialgCatEquivComonCommAlgCat_functor_map_unop_hom, commBialgCatEquivComonCommAlgCat_counitIso_inv_app
ofIso 📖	CompOp	—
uliftFunctor 📖	CompOp	2 math math: instFaithfulUliftFunctor, instFullUliftFunctor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algEquivOfIso_apply 📖	mathematical	—	DFunLike.coe AlgEquiv carrier CommRing.toCommSemiring CommSemiring.toSemiring commRing algebra AlgEquiv.instFunLike algEquivOfIso CategoryTheory.ConcreteCategory.hom CommAlgCat instCategory AlgHom AlgHom.funLike instConcreteCategoryAlgHomCarrier CategoryTheory.Iso.hom	—	—
algEquivOfIso_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv carrier CommRing.toCommSemiring CommSemiring.toSemiring commRing algebra AlgEquiv.instFunLike AlgEquiv.symm algEquivOfIso CategoryTheory.ConcreteCategory.hom CommAlgCat instCategory AlgHom AlgHom.funLike instConcreteCategoryAlgHomCarrier CategoryTheory.Iso.inv	—	—
coe_of 📖	mathematical	—	carrier of	—	—
comp_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom CommAlgCat instCategory AlgHom CommRing.toCommSemiring CommSemiring.toSemiring commRing algebra AlgHom.funLike instConcreteCategoryAlgHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
forget_map 📖	mathematical	—	CategoryTheory.Functor.map CommAlgCat instCategory CategoryTheory.types CategoryTheory.forget AlgHom carrier CommRing.toCommSemiring CommSemiring.toSemiring commRing algebra AlgHom.funLike instConcreteCategoryAlgHomCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom	—	—
forget_obj 📖	mathematical	—	CategoryTheory.Functor.obj CommAlgCat instCategory CategoryTheory.types CategoryTheory.forget AlgHom carrier CommRing.toCommSemiring CommSemiring.toSemiring commRing algebra AlgHom.funLike instConcreteCategoryAlgHomCarrier	—	—
forget₂_algCat_map 📖	mathematical	—	CategoryTheory.Functor.map CommAlgCat instCategory AlgCat AlgCat.instCategory CategoryTheory.forget₂ AlgHom carrier CommRing.toCommSemiring CommSemiring.toSemiring commRing algebra AlgHom.funLike instConcreteCategoryAlgHomCarrier AlgCat.carrier Ring.toSemiring AlgCat.isRing AlgCat.isAlgebra AlgCat.instConcreteCategoryAlgHomCarrier hasForgetToAlgCat AlgCat.ofHom CommRing.toRing Hom.hom	—	—
forget₂_algCat_obj 📖	mathematical	—	CategoryTheory.Functor.obj CommAlgCat instCategory AlgCat AlgCat.instCategory CategoryTheory.forget₂ AlgHom carrier CommRing.toCommSemiring CommSemiring.toSemiring commRing algebra AlgHom.funLike instConcreteCategoryAlgHomCarrier AlgCat.carrier Ring.toSemiring AlgCat.isRing AlgCat.isAlgebra AlgCat.instConcreteCategoryAlgHomCarrier hasForgetToAlgCat AlgCat.of CommRing.toRing	—	—
forget₂_commRingCat_map 📖	mathematical	—	CategoryTheory.Functor.map CommAlgCat instCategory CommRingCat CommRingCat.instCategory CategoryTheory.forget₂ AlgHom carrier CommRing.toCommSemiring CommSemiring.toSemiring commRing algebra AlgHom.funLike instConcreteCategoryAlgHomCarrier RingHom CommRingCat.carrier Semiring.toNonAssocSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier hasForgetToCommRingCat CommRingCat.ofHom RingHomClass.toRingHom AlgHomClass.toRingHomClass AlgHom.algHomClass Hom.hom	—	—
forget₂_commRingCat_obj 📖	mathematical	—	CategoryTheory.Functor.obj CommAlgCat instCategory CommRingCat CommRingCat.instCategory CategoryTheory.forget₂ AlgHom carrier CommRing.toCommSemiring CommSemiring.toSemiring commRing algebra AlgHom.funLike instConcreteCategoryAlgHomCarrier RingHom CommRingCat.carrier Semiring.toNonAssocSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier hasForgetToCommRingCat CommRingCat.of	—	—
hom_comp 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp CommAlgCat CategoryTheory.Category.toCategoryStruct instCategory AlgHom.comp carrier CommRing.toCommSemiring CommSemiring.toSemiring commRing algebra	—	—
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
hom_id 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id CommAlgCat CategoryTheory.Category.toCategoryStruct instCategory AlgHom.id carrier CommRing.toCommSemiring CommSemiring.toSemiring commRing algebra	—	—
hom_inv_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom CommAlgCat instCategory AlgHom CommRing.toCommSemiring CommSemiring.toSemiring commRing algebra AlgHom.funLike instConcreteCategoryAlgHomCarrier CategoryTheory.Iso.hom CategoryTheory.Iso.inv	—	CategoryTheory.Iso.inv_hom_id_apply
hom_ofHom 📖	mathematical	—	Hom.hom of ofHom	—	—
id_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom CommAlgCat instCategory AlgHom CommRing.toCommSemiring CommSemiring.toSemiring commRing algebra AlgHom.funLike instConcreteCategoryAlgHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
instFaithfulUliftFunctor 📖	mathematical	—	CategoryTheory.Functor.Faithful CommAlgCat instCategory uliftFunctor	—	CategoryTheory.Functor.FullyFaithful.faithful
instFullUliftFunctor 📖	mathematical	—	CategoryTheory.Functor.Full CommAlgCat instCategory uliftFunctor	—	CategoryTheory.Functor.FullyFaithful.full
inv_hom_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom CommAlgCat instCategory AlgHom CommRing.toCommSemiring CommSemiring.toSemiring commRing algebra AlgHom.funLike instConcreteCategoryAlgHomCarrier CategoryTheory.Iso.inv CategoryTheory.Iso.hom	—	CategoryTheory.Iso.hom_inv_id_apply
isoEquivAlgEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Iso CommAlgCat instCategory of AlgEquiv CommRing.toCommSemiring CommSemiring.toSemiring EquivLike.toFunLike Equiv.instEquivLike isoEquivAlgEquiv algEquivOfIso	—	—
isoEquivAlgEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv AlgEquiv CommRing.toCommSemiring CommSemiring.toSemiring CategoryTheory.Iso CommAlgCat instCategory of EquivLike.toFunLike Equiv.instEquivLike Equiv.symm isoEquivAlgEquiv isoMk	—	—
isoMk_hom 📖	mathematical	—	CategoryTheory.Iso.hom CommAlgCat instCategory of isoMk ofHom AlgHomClass.toAlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgEquiv AlgEquiv.instFunLike	—	—
isoMk_inv 📖	mathematical	—	CategoryTheory.Iso.inv CommAlgCat instCategory of isoMk ofHom AlgHomClass.toAlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgEquiv AlgEquiv.instFunLike AlgEquiv.symm	—	—
ofHom_apply 📖	mathematical	—	DFunLike.coe of carrier CategoryTheory.ConcreteCategory.hom CommAlgCat instCategory AlgHom CommRing.toCommSemiring CommSemiring.toSemiring commRing algebra AlgHom.funLike instConcreteCategoryAlgHomCarrier ofHom	—	—
ofHom_comp 📖	mathematical	—	ofHom AlgHom.comp CommRing.toCommSemiring CommSemiring.toSemiring CategoryTheory.CategoryStruct.comp CommAlgCat CategoryTheory.Category.toCategoryStruct instCategory of	—	—
ofHom_hom 📖	mathematical	—	ofHom carrier commRing algebra Hom.hom	—	—
ofHom_id 📖	mathematical	—	ofHom AlgHom.id CommRing.toCommSemiring CommSemiring.toSemiring CategoryTheory.CategoryStruct.id CommAlgCat CategoryTheory.Category.toCategoryStruct instCategory of	—	—
reflectsIsomorphisms_forget 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms CommAlgCat instCategory CategoryTheory.types CategoryTheory.forget AlgHom carrier CommRing.toCommSemiring CommSemiring.toSemiring commRing algebra AlgHom.funLike instConcreteCategoryAlgHomCarrier	—	Equiv.left_inv Equiv.right_inv MonoidHom.map_mul' RingHom.map_add' AlgHom.commutes' CategoryTheory.Iso.isIso_hom

CommAlgCat.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	28 math math: CommAlgCat.ofHom_hom, commBialgCatEquivComonCommAlgCat_unitIso_inv_app, CommAlgCat.braiding_hom_hom, CommAlgCat.hom_ofHom, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, CommAlgCat.forget₂_algCat_map, CommAlgCat.lift_unop_hom, CommAlgCat.mul_op_of_unop_hom, CommAlgCat.fst_unop_hom, CommAlgCat.hom_comp, CommAlgCat.snd_unop_hom, CommAlgCat.tensorHom_hom, commAlgCatEquivUnder_counitIso, CommAlgCat.whiskerLeft_hom, CommAlgCat.whiskerRight_hom, commAlgCatEquivUnder_unitIso, CommAlgCat.braiding_inv_hom, CommAlgCat.associator_inv_hom, CommAlgCat.toUnit_unop_hom, CommAlgCat.one_op_of_unop_hom, CommAlgCat.hom_id, commAlgCatEquivUnder_functor_map, CommAlgCat.hom_ext_iff, CommAlgCat.associator_hom_hom, commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, CommAlgCat.forget₂_commRingCat_map, commBialgCatEquivComonCommAlgCat_counitIso_inv_app
hom' 📖	CompOp	1 math math: ext_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	hom'	—	—	—
ext_iff 📖	mathematical	—	hom'	—	ext

CommAlgCat.Hom.Simps

Definitions

Name	Category	Theorems
hom 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
commAlgCatEquivUnder 📖	CompOp	6 math math: commAlgCatEquivUnder_functor_obj, commAlgCatEquivUnder_counitIso, commAlgCatEquivUnder_inverse_obj_carrier, commAlgCatEquivUnder_unitIso, commAlgCatEquivUnder_inverse_map, commAlgCatEquivUnder_functor_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commAlgCatEquivUnder_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CommAlgCat CommRingCat.carrier CommRingCat.commRing CategoryTheory.Under CommRingCat CommRingCat.instCategory CommAlgCat.instCategory CategoryTheory.instCategoryUnder commAlgCatEquivUnder CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CommAlgCat.of CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CommRingCat.instAlgebraCarrierRightDiscretePUnit CommAlgCat.ofHom CommRingCat.toAlgHom CommRingCat.mkUnder CommAlgCat.carrier CommAlgCat.commRing CommAlgCat.algebra AlgHom.toUnder CommAlgCat.Hom.hom	—	—
commAlgCatEquivUnder_functor_map 📖	mathematical	—	CategoryTheory.Functor.map CommAlgCat CommRingCat.carrier CommRingCat.commRing CommAlgCat.instCategory CategoryTheory.Under CommRingCat CommRingCat.instCategory CategoryTheory.instCategoryUnder CategoryTheory.Equivalence.functor commAlgCatEquivUnder AlgHom.toUnder CommAlgCat.carrier CommAlgCat.commRing CommAlgCat.algebra CommAlgCat.Hom.hom	—	—
commAlgCatEquivUnder_functor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CommAlgCat CommRingCat.carrier CommRingCat.commRing CommAlgCat.instCategory CategoryTheory.Under CommRingCat CommRingCat.instCategory CategoryTheory.instCategoryUnder CategoryTheory.Equivalence.functor commAlgCatEquivUnder CommRingCat.mkUnder CommAlgCat.carrier CommAlgCat.commRing CommAlgCat.algebra	—	—
commAlgCatEquivUnder_inverse_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Under CommRingCat CommRingCat.instCategory CategoryTheory.instCategoryUnder CommAlgCat CommRingCat.carrier CommRingCat.commRing CommAlgCat.instCategory CategoryTheory.Equivalence.inverse commAlgCatEquivUnder CommAlgCat.ofHom CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CommRingCat.instAlgebraCarrierRightDiscretePUnit CommRingCat.toAlgHom	—	—
commAlgCatEquivUnder_inverse_obj_carrier 📖	mathematical	—	CommAlgCat.carrier CommRingCat.carrier CommRingCat.commRing CategoryTheory.Functor.obj CategoryTheory.Under CommRingCat CommRingCat.instCategory CategoryTheory.instCategoryUnder CommAlgCat CommAlgCat.instCategory CategoryTheory.Equivalence.inverse commAlgCatEquivUnder CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id	—	—
commAlgCatEquivUnder_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CommAlgCat CommRingCat.carrier CommRingCat.commRing CategoryTheory.Under CommRingCat CommRingCat.instCategory CommAlgCat.instCategory CategoryTheory.instCategoryUnder commAlgCatEquivUnder CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.id CategoryTheory.Functor.comp CommRingCat.mkUnder CommAlgCat.carrier CommAlgCat.commRing CommAlgCat.algebra AlgHom.toUnder CommAlgCat.Hom.hom CommAlgCat.of CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CommRingCat.instAlgebraCarrierRightDiscretePUnit CommAlgCat.ofHom CommRingCat.toAlgHom CommAlgCat.isoMk CategoryTheory.Functor.obj	—	—
instHasColimitsCommAlgCat 📖	mathematical	—	CategoryTheory.Limits.HasColimits CommAlgCat CommAlgCat.instCategory	—	CategoryTheory.Adjunction.has_colimits_of_equivalence CategoryTheory.Equivalence.isEquivalence_functor instHasColimitsOfSizeUnder CommRingCat.Colimits.hasColimits_commRingCat
instHasLimitsCommAlgCat 📖	mathematical	—	CategoryTheory.Limits.HasLimits CommAlgCat CommAlgCat.instCategory	—	CategoryTheory.Adjunction.has_limits_of_equivalence CategoryTheory.Equivalence.isEquivalence_functor CategoryTheory.Under.instHasLimits CommRingCat.hasLimits

---

← Back to Index