Basic

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

Statistics

Metric	Count
Definitions AlgCat, hom, hom, hom', adj, carrier, free, hasForgetToModule, hasForgetToRing, instAlgebraObjForgetAlgHomCarrier, instCategory, instCoeSortType, instConcreteCategoryAlgHomCarrier, instInhabited, instRingObjForgetAlgHomCarrier, isAlgebra, isRing, of, ofHom, toAlgebraIso, toAlgEquiv, algEquivIsoAlgebraIso	22
Theorems ext, ext_iff, coe_of, comp_apply, forget_map, forget_obj, forget_reflects_isos, forget₂_module_map, forget₂_module_obj, free_map, free_obj, hom_comp, hom_ext, hom_ext_iff, hom_id, hom_inv_apply, hom_ofHom, id_apply, instIsRightAdjointForgetAlgHomCarrier, inv_hom_apply, ofHom_apply, ofHom_comp, ofHom_hom, ofHom_id, toAlgebraIso_hom, toAlgebraIso_inv, toAlgEquiv_apply, toAlgEquiv_symm_apply, algEquivIsoAlgebraIso_hom, algEquivIsoAlgebraIso_inv	30
Total	52

AlgCat

Definitions

Name	Category	Theorems
adj 📖	CompOp	—
carrier 📖	CompOp	51 math math: hom_inv_apply, hom_inv_associator, hom_inv_rightUnitor, forget_obj, inv_hom_apply, forget_map, CommAlgCat.forget₂_algCat_map, id_apply, forget₂Ring_preservesLimitsOfSize, CSA.isSimple, hom_hom_associator, CategoryTheory.Iso.toAlgEquiv_symm_apply, forget_preservesLimits, forget₂Module_preservesLimitsOfSize, hom_hom_rightUnitor, BialgCat.forget₂_algebra_map, ModuleCat.MonModuleEquivalenceAlgebra.functor_obj_carrier, hom_inv_leftUnitor, CategoryTheory.Iso.toAlgEquiv_apply, coe_of, hom_hom_leftUnitor, hom_whiskerLeft, CommAlgCat.forget₂_algCat_obj, forget₂_module_obj, ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_mul, forget_preservesLimitsOfSize, BialgCat.MonoidalCategory.inducingFunctorData_μIso, instMonoidalCategory.tensorObj_carrier, instSmallSubtypeForallCarrierObjMemSubalgebraSectionsSubalgebra, forget₂Module_preservesLimits, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_isAddCommGroup, comp_apply, forget_reflects_isos, forget₂_module_map, CSA.fin_dim, QuadraticModuleCat.cliffordAlgebra_obj_carrier, hom_id, forget₂Ring_preservesLimits, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_carrier, hom_comp, hom_tensorHom, ModuleCat.MonModuleEquivalenceAlgebra.inverse_map_hom, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_isModule, CSA.isCentral, BialgCat.forget₂_algebra_obj, hom_whiskerRight, ofHom_apply, BialgCat.MonoidalCategory.inducingFunctorData_εIso, ofHom_hom, ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_one, instIsRightAdjointForgetAlgHomCarrier
free 📖	CompOp	2 math math: free_obj, free_map
hasForgetToModule 📖	CompOp	4 math math: forget₂Module_preservesLimitsOfSize, forget₂_module_obj, forget₂Module_preservesLimits, forget₂_module_map
hasForgetToRing 📖	CompOp	2 math math: forget₂Ring_preservesLimitsOfSize, forget₂Ring_preservesLimits
instAlgebraObjForgetAlgHomCarrier 📖	CompOp	—
instCategory 📖	CompOp	56 math math: hom_inv_apply, hom_inv_associator, hom_inv_rightUnitor, forget_obj, inv_hom_apply, forget_map, CommAlgCat.forget₂_algCat_map, id_apply, forget₂Ring_preservesLimitsOfSize, ofHom_comp, hom_hom_associator, CategoryTheory.Iso.toAlgEquiv_symm_apply, forget_preservesLimits, forget₂Module_preservesLimitsOfSize, hom_hom_rightUnitor, BialgCat.forget₂_algebra_map, ModuleCat.MonModuleEquivalenceAlgebra.functor_map_hom_apply, ModuleCat.MonModuleEquivalenceAlgebra.functor_obj_carrier, hom_inv_leftUnitor, CategoryTheory.Iso.toAlgEquiv_apply, free_obj, hom_hom_leftUnitor, hom_whiskerLeft, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_mon, ofHom_id, QuadraticModuleCat.cliffordAlgebra_map, CommAlgCat.forget₂_algCat_obj, algEquivIsoAlgebraIso_inv, AlgEquiv.toAlgebraIso_inv, forget₂_module_obj, forget_preservesLimitsOfSize, BialgCat.MonoidalCategory.inducingFunctorData_μIso, free_map, instSmallSubtypeForallCarrierObjMemSubalgebraSectionsSubalgebra, forget₂Module_preservesLimits, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_isAddCommGroup, comp_apply, forget_reflects_isos, forget₂_module_map, algEquivIsoAlgebraIso_hom, QuadraticModuleCat.cliffordAlgebra_obj_carrier, hom_id, forget₂Ring_preservesLimits, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_carrier, hom_comp, hom_tensorHom, ModuleCat.MonModuleEquivalenceAlgebra.inverse_map_hom, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_isModule, BialgCat.forget₂_algebra_obj, hom_whiskerRight, ofHom_apply, BialgCat.MonoidalCategory.inducingFunctorData_εIso, hasLimits, instIsRightAdjointForgetAlgHomCarrier, hasLimitsOfSize, AlgEquiv.toAlgebraIso_hom
instCoeSortType 📖	CompOp	—
instConcreteCategoryAlgHomCarrier 📖	CompOp	25 math math: hom_inv_apply, forget_obj, inv_hom_apply, forget_map, CommAlgCat.forget₂_algCat_map, id_apply, forget₂Ring_preservesLimitsOfSize, CategoryTheory.Iso.toAlgEquiv_symm_apply, forget_preservesLimits, forget₂Module_preservesLimitsOfSize, BialgCat.forget₂_algebra_map, CategoryTheory.Iso.toAlgEquiv_apply, CommAlgCat.forget₂_algCat_obj, forget₂_module_obj, forget_preservesLimitsOfSize, BialgCat.MonoidalCategory.inducingFunctorData_μIso, forget₂Module_preservesLimits, comp_apply, forget_reflects_isos, forget₂_module_map, forget₂Ring_preservesLimits, BialgCat.forget₂_algebra_obj, ofHom_apply, BialgCat.MonoidalCategory.inducingFunctorData_εIso, instIsRightAdjointForgetAlgHomCarrier
instInhabited 📖	CompOp	—
instRingObjForgetAlgHomCarrier 📖	CompOp	—
isAlgebra 📖	CompOp	45 math math: hom_inv_apply, hom_inv_associator, hom_inv_rightUnitor, forget_obj, inv_hom_apply, forget_map, CommAlgCat.forget₂_algCat_map, id_apply, forget₂Ring_preservesLimitsOfSize, hom_hom_associator, CategoryTheory.Iso.toAlgEquiv_symm_apply, forget_preservesLimits, forget₂Module_preservesLimitsOfSize, hom_hom_rightUnitor, BialgCat.forget₂_algebra_map, hom_inv_leftUnitor, CategoryTheory.Iso.toAlgEquiv_apply, hom_hom_leftUnitor, hom_whiskerLeft, CommAlgCat.forget₂_algCat_obj, forget₂_module_obj, ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_mul, forget_preservesLimitsOfSize, BialgCat.MonoidalCategory.inducingFunctorData_μIso, instMonoidalCategory.tensorObj_carrier, instSmallSubtypeForallCarrierObjMemSubalgebraSectionsSubalgebra, forget₂Module_preservesLimits, comp_apply, forget_reflects_isos, forget₂_module_map, CSA.fin_dim, hom_id, forget₂Ring_preservesLimits, hom_comp, hom_tensorHom, ModuleCat.MonModuleEquivalenceAlgebra.inverse_map_hom, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_isModule, CSA.isCentral, BialgCat.forget₂_algebra_obj, hom_whiskerRight, ofHom_apply, BialgCat.MonoidalCategory.inducingFunctorData_εIso, ofHom_hom, ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_one, instIsRightAdjointForgetAlgHomCarrier
isRing 📖	CompOp	47 math math: hom_inv_apply, hom_inv_associator, hom_inv_rightUnitor, forget_obj, inv_hom_apply, forget_map, CommAlgCat.forget₂_algCat_map, id_apply, forget₂Ring_preservesLimitsOfSize, CSA.isSimple, hom_hom_associator, CategoryTheory.Iso.toAlgEquiv_symm_apply, forget_preservesLimits, forget₂Module_preservesLimitsOfSize, hom_hom_rightUnitor, BialgCat.forget₂_algebra_map, hom_inv_leftUnitor, CategoryTheory.Iso.toAlgEquiv_apply, hom_hom_leftUnitor, hom_whiskerLeft, CommAlgCat.forget₂_algCat_obj, forget₂_module_obj, ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_mul, forget_preservesLimitsOfSize, BialgCat.MonoidalCategory.inducingFunctorData_μIso, instMonoidalCategory.tensorObj_carrier, instSmallSubtypeForallCarrierObjMemSubalgebraSectionsSubalgebra, forget₂Module_preservesLimits, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_isAddCommGroup, comp_apply, forget_reflects_isos, forget₂_module_map, CSA.fin_dim, hom_id, forget₂Ring_preservesLimits, hom_comp, hom_tensorHom, ModuleCat.MonModuleEquivalenceAlgebra.inverse_map_hom, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_isModule, CSA.isCentral, BialgCat.forget₂_algebra_obj, hom_whiskerRight, ofHom_apply, BialgCat.MonoidalCategory.inducingFunctorData_εIso, ofHom_hom, ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_one, instIsRightAdjointForgetAlgHomCarrier
of 📖	CompOp	13 math math: ofHom_comp, ModuleCat.MonModuleEquivalenceAlgebra.functor_map_hom_apply, coe_of, free_obj, ofHom_id, CommAlgCat.forget₂_algCat_obj, algEquivIsoAlgebraIso_inv, AlgEquiv.toAlgebraIso_inv, algEquivIsoAlgebraIso_hom, BialgCat.forget₂_algebra_obj, ofHom_apply, hom_ofHom, AlgEquiv.toAlgebraIso_hom
ofHom 📖	CompOp	11 math math: CommAlgCat.forget₂_algCat_map, ofHom_comp, BialgCat.forget₂_algebra_map, ofHom_id, QuadraticModuleCat.cliffordAlgebra_map, AlgEquiv.toAlgebraIso_inv, free_map, ofHom_apply, ofHom_hom, hom_ofHom, AlgEquiv.toAlgebraIso_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_of 📖	mathematical	—	carrier of	—	—
comp_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom AlgCat instCategory AlgHom CommRing.toCommSemiring Ring.toSemiring isRing isAlgebra AlgHom.funLike instConcreteCategoryAlgHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
forget_map 📖	mathematical	—	CategoryTheory.Functor.map AlgCat instCategory CategoryTheory.types CategoryTheory.forget AlgHom carrier CommRing.toCommSemiring Ring.toSemiring isRing isAlgebra AlgHom.funLike instConcreteCategoryAlgHomCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom	—	—
forget_obj 📖	mathematical	—	CategoryTheory.Functor.obj AlgCat instCategory CategoryTheory.types CategoryTheory.forget AlgHom carrier CommRing.toCommSemiring Ring.toSemiring isRing isAlgebra AlgHom.funLike instConcreteCategoryAlgHomCarrier	—	—
forget_reflects_isos 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms AlgCat instCategory CategoryTheory.types CategoryTheory.forget AlgHom carrier CommRing.toCommSemiring Ring.toSemiring isRing isAlgebra AlgHom.funLike instConcreteCategoryAlgHomCarrier	—	Equiv.left_inv Equiv.right_inv MonoidHom.map_mul' RingHom.map_add' AlgHom.commutes' CategoryTheory.Iso.isIso_hom
forget₂_module_map 📖	mathematical	—	CategoryTheory.Functor.map AlgCat instCategory ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.forget₂ AlgHom carrier CommRing.toCommSemiring Ring.toSemiring isRing isAlgebra AlgHom.funLike instConcreteCategoryAlgHomCarrier LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier hasForgetToModule ModuleCat.ofHom Ring.toAddCommGroup Algebra.toModule AlgHom.toLinearMap Hom.hom	—	—
forget₂_module_obj 📖	mathematical	—	CategoryTheory.Functor.obj AlgCat instCategory ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.forget₂ AlgHom carrier CommRing.toCommSemiring Ring.toSemiring isRing isAlgebra AlgHom.funLike instConcreteCategoryAlgHomCarrier LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier hasForgetToModule ModuleCat.of Ring.toAddCommGroup Algebra.toModule	—	—
free_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.types AlgCat instCategory free ofHom FreeAlgebra CommRing.toCommSemiring FreeAlgebra.instRing FreeAlgebra.instAlgebra Algebra.id DFunLike.coe Equiv AlgHom FreeAlgebra.instSemiring Ring.toSemiring EquivLike.toFunLike Equiv.instEquivLike FreeAlgebra.lift FreeAlgebra.ι	—	—
free_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types AlgCat instCategory free of FreeAlgebra CommRing.toCommSemiring FreeAlgebra.instRing FreeAlgebra.instAlgebra Algebra.id	—	—
hom_comp 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp AlgCat CategoryTheory.Category.toCategoryStruct instCategory AlgHom.comp carrier CommRing.toCommSemiring Ring.toSemiring isRing isAlgebra	—	—
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
hom_id 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id AlgCat CategoryTheory.Category.toCategoryStruct instCategory AlgHom.id carrier CommRing.toCommSemiring Ring.toSemiring isRing isAlgebra	—	—
hom_inv_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom AlgCat instCategory AlgHom CommRing.toCommSemiring Ring.toSemiring isRing isAlgebra 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 AlgCat instCategory AlgHom CommRing.toCommSemiring Ring.toSemiring isRing isAlgebra AlgHom.funLike instConcreteCategoryAlgHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
instIsRightAdjointForgetAlgHomCarrier 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint CategoryTheory.types AlgCat instCategory CategoryTheory.forget AlgHom carrier CommRing.toCommSemiring Ring.toSemiring isRing isAlgebra AlgHom.funLike instConcreteCategoryAlgHomCarrier	—	CategoryTheory.Adjunction.isRightAdjoint
inv_hom_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom AlgCat instCategory AlgHom CommRing.toCommSemiring Ring.toSemiring isRing isAlgebra AlgHom.funLike instConcreteCategoryAlgHomCarrier CategoryTheory.Iso.inv CategoryTheory.Iso.hom	—	CategoryTheory.Iso.hom_inv_id_apply
ofHom_apply 📖	mathematical	—	DFunLike.coe of carrier CategoryTheory.ConcreteCategory.hom AlgCat instCategory AlgHom CommRing.toCommSemiring Ring.toSemiring isRing isAlgebra AlgHom.funLike instConcreteCategoryAlgHomCarrier ofHom	—	—
ofHom_comp 📖	mathematical	—	ofHom AlgHom.comp CommRing.toCommSemiring Ring.toSemiring CategoryTheory.CategoryStruct.comp AlgCat CategoryTheory.Category.toCategoryStruct instCategory of	—	—
ofHom_hom 📖	mathematical	—	ofHom carrier isRing isAlgebra Hom.hom	—	—
ofHom_id 📖	mathematical	—	ofHom AlgHom.id CommRing.toCommSemiring Ring.toSemiring CategoryTheory.CategoryStruct.id AlgCat CategoryTheory.Category.toCategoryStruct instCategory of	—	—

AlgCat.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	17 math math: AlgCat.hom_inv_associator, AlgCat.hom_inv_rightUnitor, AlgCat.hom_ext_iff, AlgCat.hom_hom_associator, AlgCat.hom_hom_rightUnitor, ModuleCat.MonModuleEquivalenceAlgebra.functor_map_hom_apply, AlgCat.hom_inv_leftUnitor, AlgCat.hom_hom_leftUnitor, AlgCat.hom_whiskerLeft, AlgCat.forget₂_module_map, AlgCat.hom_id, AlgCat.hom_comp, AlgCat.hom_tensorHom, ModuleCat.MonModuleEquivalenceAlgebra.inverse_map_hom, AlgCat.hom_whiskerRight, AlgCat.ofHom_hom, AlgCat.hom_ofHom
hom' 📖	CompOp	1 math math: ext_iff

Theorems

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

AlgCat.Hom.Simps

Definitions

Name	Category	Theorems
hom 📖	CompOp	—

AlgEquiv

Definitions

Name	Category	Theorems
toAlgebraIso 📖	CompOp	3 math math: toAlgebraIso_inv, algEquivIsoAlgebraIso_hom, toAlgebraIso_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toAlgebraIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom AlgCat AlgCat.instCategory AlgCat.of toAlgebraIso AlgCat.ofHom AlgHomClass.toAlgHom CommRing.toCommSemiring Ring.toSemiring AlgEquiv instFunLike	—	—
toAlgebraIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv AlgCat AlgCat.instCategory AlgCat.of toAlgebraIso AlgCat.ofHom AlgHomClass.toAlgHom CommRing.toCommSemiring Ring.toSemiring AlgEquiv instFunLike symm	—	—

CategoryTheory.Iso

Definitions

Name	Category	Theorems
toAlgEquiv 📖	CompOp	3 math math: toAlgEquiv_symm_apply, toAlgEquiv_apply, algEquivIsoAlgebraIso_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toAlgEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv AlgCat.carrier CommRing.toCommSemiring Ring.toSemiring AlgCat.isRing AlgCat.isAlgebra AlgEquiv.instFunLike toAlgEquiv CategoryTheory.ConcreteCategory.hom AlgCat AlgCat.instCategory AlgHom AlgHom.funLike AlgCat.instConcreteCategoryAlgHomCarrier hom	—	—
toAlgEquiv_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv AlgCat.carrier CommRing.toCommSemiring Ring.toSemiring AlgCat.isRing AlgCat.isAlgebra AlgEquiv.instFunLike AlgEquiv.symm toAlgEquiv CategoryTheory.ConcreteCategory.hom AlgCat AlgCat.instCategory AlgHom AlgHom.funLike AlgCat.instConcreteCategoryAlgHomCarrier inv	—	—

(root)

Definitions

Name	Category	Theorems
AlgCat 📖	CompData	56 math math: AlgCat.hom_inv_apply, AlgCat.hom_inv_associator, AlgCat.hom_inv_rightUnitor, AlgCat.forget_obj, AlgCat.inv_hom_apply, AlgCat.forget_map, CommAlgCat.forget₂_algCat_map, AlgCat.id_apply, AlgCat.forget₂Ring_preservesLimitsOfSize, AlgCat.ofHom_comp, AlgCat.hom_hom_associator, CategoryTheory.Iso.toAlgEquiv_symm_apply, AlgCat.forget_preservesLimits, AlgCat.forget₂Module_preservesLimitsOfSize, AlgCat.hom_hom_rightUnitor, BialgCat.forget₂_algebra_map, ModuleCat.MonModuleEquivalenceAlgebra.functor_map_hom_apply, ModuleCat.MonModuleEquivalenceAlgebra.functor_obj_carrier, AlgCat.hom_inv_leftUnitor, CategoryTheory.Iso.toAlgEquiv_apply, AlgCat.free_obj, AlgCat.hom_hom_leftUnitor, AlgCat.hom_whiskerLeft, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_mon, AlgCat.ofHom_id, QuadraticModuleCat.cliffordAlgebra_map, CommAlgCat.forget₂_algCat_obj, algEquivIsoAlgebraIso_inv, AlgEquiv.toAlgebraIso_inv, AlgCat.forget₂_module_obj, AlgCat.forget_preservesLimitsOfSize, BialgCat.MonoidalCategory.inducingFunctorData_μIso, AlgCat.free_map, AlgCat.instSmallSubtypeForallCarrierObjMemSubalgebraSectionsSubalgebra, AlgCat.forget₂Module_preservesLimits, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_isAddCommGroup, AlgCat.comp_apply, AlgCat.forget_reflects_isos, AlgCat.forget₂_module_map, algEquivIsoAlgebraIso_hom, QuadraticModuleCat.cliffordAlgebra_obj_carrier, AlgCat.hom_id, AlgCat.forget₂Ring_preservesLimits, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_carrier, AlgCat.hom_comp, AlgCat.hom_tensorHom, ModuleCat.MonModuleEquivalenceAlgebra.inverse_map_hom, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_isModule, BialgCat.forget₂_algebra_obj, AlgCat.hom_whiskerRight, AlgCat.ofHom_apply, BialgCat.MonoidalCategory.inducingFunctorData_εIso, AlgCat.hasLimits, AlgCat.instIsRightAdjointForgetAlgHomCarrier, AlgCat.hasLimitsOfSize, AlgEquiv.toAlgebraIso_hom
algEquivIsoAlgebraIso 📖	CompOp	2 math math: algEquivIsoAlgebraIso_inv, algEquivIsoAlgebraIso_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algEquivIsoAlgebraIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.types AlgEquiv CommRing.toCommSemiring Ring.toSemiring CategoryTheory.Iso AlgCat AlgCat.instCategory AlgCat.of algEquivIsoAlgebraIso AlgEquiv.toAlgebraIso	—	—
algEquivIsoAlgebraIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.types AlgEquiv CommRing.toCommSemiring Ring.toSemiring CategoryTheory.Iso AlgCat AlgCat.instCategory AlgCat.of algEquivIsoAlgebraIso CategoryTheory.Iso.toAlgEquiv	—	—

---

← Back to Index