Basic

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

Statistics

Metric	Count
Definitions toAddMagmaCatIso, toAddSemigrpIso, AddMagmaCat, hom, hom', carrier, instCategory, instCoeSortType, instConcreteCategoryAddHomCarrier, instInhabited, of, ofHom, str, AddSemigrp, hom, hom', carrier, hasForgetToAddMagmaCat, instCategory, instCoeSortType, instConcreteCategoryAddHomCarrier, instInhabited, of, ofHom, str, addMagmaCatIsoToAddEquiv, addSemigrpIsoToAddEquiv, magmaCatIsoToMulEquiv, semigrpIsoToMulEquiv, MagmaCat, hom, hom, hom', carrier, instCategory, instCoeSortType, instConcreteCategoryMulHomCarrier, instInhabited, of, ofHom, str, toMagmaCatIso, toSemigrpIso, hom, hom, hom', carrier, hasForgetToMagmaCat, instCategory, instCoeSortType, instConcreteCategoryMulHomCarrier, instInhabited, of, ofHom, str, addEquivIsoAddMagmaIso, addEquivIsoAddSemigrpIso, mulEquivIsoMagmaIso, mulEquivIsoSemigrpIso	59
Theorems toAddMagmaCatIso_hom, toAddMagmaCatIso_inv, toAddSemigrpIso_hom, toAddSemigrpIso_inv, ext, ext_iff, addEquiv_coe_eq, coe_comp, coe_id, coe_of, comp_apply, ext, ext_iff, forgetReflectsIsos, forget_map, hom_comp, hom_ext, hom_ext_iff, hom_id, hom_neg_apply, hom_ofHom, id_apply, neg_hom_apply, ofHom_apply, ofHom_comp, ofHom_hom, ofHom_id, ext, ext_iff, addEquiv_coe_eq, coe_comp, coe_id, coe_of, comp_apply, ext, ext_iff, forgetReflectsIsos, forget₂_full, hom_comp, hom_ext, hom_ext_iff, hom_id, hom_neg_apply, hom_ofHom, id_apply, neg_hom_apply, ofHom_apply, ofHom_comp, ofHom_hom, ofHom_id, ext, ext_iff, coe_comp, coe_id, coe_of, comp_apply, ext, ext_iff, forgetReflectsIsos, forget_map, hom_comp, hom_ext, hom_ext_iff, hom_id, hom_inv_apply, hom_ofHom, id_apply, inv_hom_apply, mulEquiv_coe_eq, ofHom_apply, ofHom_comp, ofHom_hom, ofHom_id, toMagmaCatIso_hom, toMagmaCatIso_inv, toSemigrpIso_hom, toSemigrpIso_inv, ext, ext_iff, coe_comp, coe_id, coe_of, comp_apply, ext, ext_iff, forgetReflectsIsos, forget_map, forget₂_full, hom_comp, hom_ext, hom_ext_iff, hom_id, hom_inv_apply, hom_ofHom, id_apply, inv_hom_apply, mulEquiv_coe_eq, ofHom_apply, ofHom_comp, ofHom_hom, ofHom_id	101
Total	160

AddEquiv

Definitions

Name	Category	Theorems
toAddMagmaCatIso 📖	CompOp	2 math math: toAddMagmaCatIso_inv, toAddMagmaCatIso_hom
toAddSemigrpIso 📖	CompOp	2 math math: toAddSemigrpIso_hom, toAddSemigrpIso_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toAddMagmaCatIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom AddMagmaCat AddMagmaCat.instCategory AddMagmaCat.of toAddMagmaCatIso AddMagmaCat.ofHom toAddHom	—	—
toAddMagmaCatIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv AddMagmaCat AddMagmaCat.instCategory AddMagmaCat.of toAddMagmaCatIso AddMagmaCat.ofHom toAddHom symm	—	—
toAddSemigrpIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom AddSemigrp AddSemigrp.instCategory AddSemigrp.of toAddSemigrpIso AddSemigrp.ofHom toAddHom AddSemigroup.toAdd	—	—
toAddSemigrpIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv AddSemigrp AddSemigrp.instCategory AddSemigrp.of toAddSemigrpIso AddSemigrp.ofHom toAddHom AddSemigroup.toAdd symm	—	—

AddMagmaCat

Definitions

Name	Category	Theorems
carrier 📖	CompOp	16 math math: coe_id, forgetReflectsIsos, addEquiv_coe_eq, forget_map, ofHom_apply, coe_comp, coe_of, ext_iff, AddSemigrp.forget₂_full, hom_id, comp_apply, id_apply, neg_hom_apply, hom_comp, hom_neg_apply, ofHom_hom
instCategory 📖	CompOp	17 math math: coe_id, ofHom_comp, forgetReflectsIsos, AddEquiv.toAddMagmaCatIso_inv, forget_map, ofHom_apply, coe_comp, ext_iff, ofHom_id, AddSemigrp.forget₂_full, hom_id, comp_apply, id_apply, AddEquiv.toAddMagmaCatIso_hom, neg_hom_apply, hom_comp, hom_neg_apply
instCoeSortType 📖	CompOp	—
instConcreteCategoryAddHomCarrier 📖	CompOp	11 math math: coe_id, forgetReflectsIsos, forget_map, ofHom_apply, coe_comp, ext_iff, AddSemigrp.forget₂_full, comp_apply, id_apply, neg_hom_apply, hom_neg_apply
instInhabited 📖	CompOp	—
of 📖	CompOp	8 math math: ofHom_comp, addEquiv_coe_eq, AddEquiv.toAddMagmaCatIso_inv, ofHom_apply, coe_of, ofHom_id, AddEquiv.toAddMagmaCatIso_hom, hom_ofHom
ofHom 📖	CompOp	8 math math: ofHom_comp, addEquiv_coe_eq, AddEquiv.toAddMagmaCatIso_inv, ofHom_apply, ofHom_id, AddEquiv.toAddMagmaCatIso_hom, hom_ofHom, ofHom_hom
str 📖	CompOp	15 math math: coe_id, forgetReflectsIsos, addEquiv_coe_eq, forget_map, ofHom_apply, coe_comp, ext_iff, AddSemigrp.forget₂_full, hom_id, comp_apply, id_apply, neg_hom_apply, hom_comp, hom_neg_apply, ofHom_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addEquiv_coe_eq 📖	mathematical	—	Hom.hom of ofHom AddHomClass.toAddHom AddEquiv EquivLike.toFunLike AddEquiv.instEquivLike AddEquivClass.instAddHomClass AddEquiv.instAddEquivClass carrier str	—	AddEquivClass.instAddHomClass AddEquiv.instAddEquivClass
coe_comp 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom AddMagmaCat instCategory AddHom str AddHom.funLike instConcreteCategoryAddHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
coe_id 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom AddMagmaCat instCategory AddHom str AddHom.funLike instConcreteCategoryAddHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
coe_of 📖	mathematical	—	carrier of	—	—
comp_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom AddMagmaCat instCategory AddHom str AddHom.funLike instConcreteCategoryAddHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
ext 📖	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom AddMagmaCat instCategory AddHom str AddHom.funLike instConcreteCategoryAddHomCarrier	—	—	CategoryTheory.ConcreteCategory.hom_ext
ext_iff 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom AddMagmaCat instCategory AddHom str AddHom.funLike instConcreteCategoryAddHomCarrier	—	ext
forgetReflectsIsos 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms AddMagmaCat instCategory CategoryTheory.types CategoryTheory.forget AddHom carrier str AddHom.funLike instConcreteCategoryAddHomCarrier	—	Equiv.left_inv Equiv.right_inv AddHom.map_add' CategoryTheory.Iso.isIso_hom
forget_map 📖	mathematical	—	CategoryTheory.Functor.map AddMagmaCat instCategory CategoryTheory.types CategoryTheory.forget AddHom carrier str AddHom.funLike instConcreteCategoryAddHomCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom	—	—
hom_comp 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp AddMagmaCat CategoryTheory.Category.toCategoryStruct instCategory AddHom.comp carrier str	—	—
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
hom_id 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id AddMagmaCat CategoryTheory.Category.toCategoryStruct instCategory AddHom.id carrier str	—	—
hom_neg_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom AddMagmaCat instCategory AddHom str AddHom.funLike instConcreteCategoryAddHomCarrier 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 AddMagmaCat instCategory AddHom str AddHom.funLike instConcreteCategoryAddHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
neg_hom_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom AddMagmaCat instCategory AddHom str AddHom.funLike instConcreteCategoryAddHomCarrier CategoryTheory.Iso.inv CategoryTheory.Iso.hom	—	CategoryTheory.Iso.hom_inv_id_apply
ofHom_apply 📖	mathematical	—	DFunLike.coe of carrier CategoryTheory.ConcreteCategory.hom AddMagmaCat instCategory AddHom str AddHom.funLike instConcreteCategoryAddHomCarrier ofHom	—	—
ofHom_comp 📖	mathematical	—	ofHom AddHom.comp CategoryTheory.CategoryStruct.comp AddMagmaCat CategoryTheory.Category.toCategoryStruct instCategory of	—	—
ofHom_hom 📖	mathematical	—	ofHom carrier str Hom.hom	—	—
ofHom_id 📖	mathematical	—	ofHom AddHom.id CategoryTheory.CategoryStruct.id AddMagmaCat CategoryTheory.Category.toCategoryStruct instCategory of	—	—

AddMagmaCat.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	6 math math: AddMagmaCat.hom_ext_iff, AddMagmaCat.addEquiv_coe_eq, AddMagmaCat.hom_id, AddMagmaCat.hom_ofHom, AddMagmaCat.hom_comp, AddMagmaCat.ofHom_hom
hom' 📖	CompOp	1 math math: ext_iff

Theorems

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

AddSemigrp

Definitions

Name	Category	Theorems
carrier 📖	CompOp	17 math math: coe_id, addEquiv_coe_eq, hom_id, comp_apply, hom_comp, neg_hom_apply, hom_neg_apply, ofHom_apply, forget₂_full, AddMonCat.adjoinZero_obj_coe, coe_comp, id_apply, coe_of, ofHom_hom, AddMonCat.adjoinZero_map, forgetReflectsIsos, ext_iff
hasForgetToAddMagmaCat 📖	CompOp	1 math math: forget₂_full
instCategory 📖	CompOp	18 math math: coe_id, hom_id, comp_apply, hom_comp, neg_hom_apply, AddEquiv.toAddSemigrpIso_hom, hom_neg_apply, ofHom_apply, forget₂_full, AddMonCat.adjoinZero_obj_coe, coe_comp, ofHom_comp, id_apply, AddEquiv.toAddSemigrpIso_inv, AddMonCat.adjoinZero_map, forgetReflectsIsos, ofHom_id, ext_iff
instCoeSortType 📖	CompOp	—
instConcreteCategoryAddHomCarrier 📖	CompOp	10 math math: coe_id, comp_apply, neg_hom_apply, hom_neg_apply, ofHom_apply, forget₂_full, coe_comp, id_apply, forgetReflectsIsos, ext_iff
instInhabited 📖	CompOp	—
of 📖	CompOp	8 math math: addEquiv_coe_eq, AddEquiv.toAddSemigrpIso_hom, ofHom_apply, ofHom_comp, coe_of, AddEquiv.toAddSemigrpIso_inv, hom_ofHom, ofHom_id
ofHom 📖	CompOp	8 math math: addEquiv_coe_eq, AddEquiv.toAddSemigrpIso_hom, ofHom_apply, ofHom_comp, ofHom_hom, AddEquiv.toAddSemigrpIso_inv, hom_ofHom, ofHom_id
str 📖	CompOp	15 math math: coe_id, addEquiv_coe_eq, hom_id, comp_apply, hom_comp, neg_hom_apply, hom_neg_apply, ofHom_apply, forget₂_full, coe_comp, id_apply, ofHom_hom, AddMonCat.adjoinZero_map, forgetReflectsIsos, ext_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addEquiv_coe_eq 📖	mathematical	—	Hom.hom of ofHom AddHomClass.toAddHom AddEquiv AddSemigroup.toAdd EquivLike.toFunLike AddEquiv.instEquivLike AddEquivClass.instAddHomClass AddEquiv.instAddEquivClass carrier str	—	AddEquivClass.instAddHomClass AddEquiv.instAddEquivClass
coe_comp 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom AddSemigrp instCategory AddHom AddSemigroup.toAdd str AddHom.funLike instConcreteCategoryAddHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
coe_id 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom AddSemigrp instCategory AddHom AddSemigroup.toAdd str AddHom.funLike instConcreteCategoryAddHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
coe_of 📖	mathematical	—	carrier of	—	—
comp_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom AddSemigrp instCategory AddHom AddSemigroup.toAdd str AddHom.funLike instConcreteCategoryAddHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
ext 📖	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom AddSemigrp instCategory AddHom AddSemigroup.toAdd str AddHom.funLike instConcreteCategoryAddHomCarrier	—	—	CategoryTheory.ConcreteCategory.hom_ext
ext_iff 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom AddSemigrp instCategory AddHom AddSemigroup.toAdd str AddHom.funLike instConcreteCategoryAddHomCarrier	—	ext
forgetReflectsIsos 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms AddSemigrp instCategory CategoryTheory.types CategoryTheory.forget AddHom carrier AddSemigroup.toAdd str AddHom.funLike instConcreteCategoryAddHomCarrier	—	Equiv.left_inv Equiv.right_inv AddHom.map_add' CategoryTheory.Iso.isIso_hom
forget₂_full 📖	mathematical	—	CategoryTheory.Functor.Full AddSemigrp instCategory AddMagmaCat AddMagmaCat.instCategory CategoryTheory.forget₂ AddHom carrier AddSemigroup.toAdd str AddHom.funLike instConcreteCategoryAddHomCarrier AddMagmaCat.carrier AddMagmaCat.str AddMagmaCat.instConcreteCategoryAddHomCarrier hasForgetToAddMagmaCat	—	—
hom_comp 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp AddSemigrp CategoryTheory.Category.toCategoryStruct instCategory AddHom.comp carrier AddSemigroup.toAdd str	—	—
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
hom_id 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id AddSemigrp CategoryTheory.Category.toCategoryStruct instCategory AddHom.id carrier AddSemigroup.toAdd str	—	—
hom_neg_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom AddSemigrp instCategory AddHom AddSemigroup.toAdd str AddHom.funLike instConcreteCategoryAddHomCarrier 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 AddSemigrp instCategory AddHom AddSemigroup.toAdd str AddHom.funLike instConcreteCategoryAddHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
neg_hom_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom AddSemigrp instCategory AddHom AddSemigroup.toAdd str AddHom.funLike instConcreteCategoryAddHomCarrier CategoryTheory.Iso.inv CategoryTheory.Iso.hom	—	CategoryTheory.Iso.hom_inv_id_apply
ofHom_apply 📖	mathematical	—	DFunLike.coe of carrier CategoryTheory.ConcreteCategory.hom AddSemigrp instCategory AddHom AddSemigroup.toAdd str AddHom.funLike instConcreteCategoryAddHomCarrier ofHom	—	—
ofHom_comp 📖	mathematical	—	ofHom AddHom.comp AddSemigroup.toAdd CategoryTheory.CategoryStruct.comp AddSemigrp CategoryTheory.Category.toCategoryStruct instCategory of	—	—
ofHom_hom 📖	mathematical	—	ofHom carrier str Hom.hom	—	—
ofHom_id 📖	mathematical	—	ofHom AddHom.id AddSemigroup.toAdd CategoryTheory.CategoryStruct.id AddSemigrp CategoryTheory.Category.toCategoryStruct instCategory of	—	—

AddSemigrp.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	7 math math: AddSemigrp.addEquiv_coe_eq, AddSemigrp.hom_id, AddSemigrp.hom_comp, AddSemigrp.hom_ext_iff, AddSemigrp.ofHom_hom, AddSemigrp.hom_ofHom, AddMonCat.adjoinZero_map
hom' 📖	CompOp	1 math math: ext_iff

Theorems

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

CategoryTheory.Iso

Definitions

Name	Category	Theorems
addMagmaCatIsoToAddEquiv 📖	CompOp	—
addSemigrpIsoToAddEquiv 📖	CompOp	—
magmaCatIsoToMulEquiv 📖	CompOp	—
semigrpIsoToMulEquiv 📖	CompOp	—

MagmaCat

Definitions

Name	Category	Theorems
carrier 📖	CompOp	16 math math: coe_comp, Semigrp.forget₂_full, id_apply, mulEquiv_coe_eq, coe_id, ofHom_apply, hom_inv_apply, ext_iff, ofHom_hom, forget_map, inv_hom_apply, hom_comp, forgetReflectsIsos, hom_id, comp_apply, coe_of
instCategory 📖	CompOp	17 math math: coe_comp, Semigrp.forget₂_full, MulEquiv.toMagmaCatIso_hom, id_apply, coe_id, ofHom_apply, hom_inv_apply, ext_iff, forget_map, MulEquiv.toMagmaCatIso_inv, inv_hom_apply, hom_comp, forgetReflectsIsos, ofHom_id, hom_id, comp_apply, ofHom_comp
instCoeSortType 📖	CompOp	—
instConcreteCategoryMulHomCarrier 📖	CompOp	11 math math: coe_comp, Semigrp.forget₂_full, id_apply, coe_id, ofHom_apply, hom_inv_apply, ext_iff, forget_map, inv_hom_apply, forgetReflectsIsos, comp_apply
instInhabited 📖	CompOp	—
of 📖	CompOp	8 math math: MulEquiv.toMagmaCatIso_hom, mulEquiv_coe_eq, ofHom_apply, MulEquiv.toMagmaCatIso_inv, hom_ofHom, ofHom_id, coe_of, ofHom_comp
ofHom 📖	CompOp	8 math math: MulEquiv.toMagmaCatIso_hom, mulEquiv_coe_eq, ofHom_apply, ofHom_hom, MulEquiv.toMagmaCatIso_inv, hom_ofHom, ofHom_id, ofHom_comp
str 📖	CompOp	15 math math: coe_comp, Semigrp.forget₂_full, id_apply, mulEquiv_coe_eq, coe_id, ofHom_apply, hom_inv_apply, ext_iff, ofHom_hom, forget_map, inv_hom_apply, hom_comp, forgetReflectsIsos, hom_id, comp_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_comp 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom MagmaCat instCategory MulHom str MulHom.funLike instConcreteCategoryMulHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
coe_id 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom MagmaCat instCategory MulHom str MulHom.funLike instConcreteCategoryMulHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
coe_of 📖	mathematical	—	carrier of	—	—
comp_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom MagmaCat instCategory MulHom str MulHom.funLike instConcreteCategoryMulHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
ext 📖	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom MagmaCat instCategory MulHom str MulHom.funLike instConcreteCategoryMulHomCarrier	—	—	CategoryTheory.ConcreteCategory.hom_ext
ext_iff 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom MagmaCat instCategory MulHom str MulHom.funLike instConcreteCategoryMulHomCarrier	—	ext
forgetReflectsIsos 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms MagmaCat instCategory CategoryTheory.types CategoryTheory.forget MulHom carrier str MulHom.funLike instConcreteCategoryMulHomCarrier	—	Equiv.left_inv Equiv.right_inv MulHom.map_mul' CategoryTheory.Iso.isIso_hom
forget_map 📖	mathematical	—	CategoryTheory.Functor.map MagmaCat instCategory CategoryTheory.types CategoryTheory.forget MulHom carrier str MulHom.funLike instConcreteCategoryMulHomCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom	—	—
hom_comp 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp MagmaCat CategoryTheory.Category.toCategoryStruct instCategory MulHom.comp carrier str	—	—
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
hom_id 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id MagmaCat CategoryTheory.Category.toCategoryStruct instCategory MulHom.id carrier str	—	—
hom_inv_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom MagmaCat instCategory MulHom str MulHom.funLike instConcreteCategoryMulHomCarrier 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 MagmaCat instCategory MulHom str MulHom.funLike instConcreteCategoryMulHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
inv_hom_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom MagmaCat instCategory MulHom str MulHom.funLike instConcreteCategoryMulHomCarrier CategoryTheory.Iso.inv CategoryTheory.Iso.hom	—	CategoryTheory.Iso.hom_inv_id_apply
mulEquiv_coe_eq 📖	mathematical	—	Hom.hom of ofHom MulHomClass.toMulHom MulEquiv EquivLike.toFunLike MulEquiv.instEquivLike MulEquivClass.instMulHomClass MulEquiv.instMulEquivClass carrier str	—	MulEquivClass.instMulHomClass MulEquiv.instMulEquivClass
ofHom_apply 📖	mathematical	—	DFunLike.coe of carrier CategoryTheory.ConcreteCategory.hom MagmaCat instCategory MulHom str MulHom.funLike instConcreteCategoryMulHomCarrier ofHom	—	—
ofHom_comp 📖	mathematical	—	ofHom MulHom.comp CategoryTheory.CategoryStruct.comp MagmaCat CategoryTheory.Category.toCategoryStruct instCategory of	—	—
ofHom_hom 📖	mathematical	—	ofHom carrier str Hom.hom	—	—
ofHom_id 📖	mathematical	—	ofHom MulHom.id CategoryTheory.CategoryStruct.id MagmaCat CategoryTheory.Category.toCategoryStruct instCategory of	—	—

MagmaCat.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	6 math math: MagmaCat.hom_ext_iff, MagmaCat.mulEquiv_coe_eq, MagmaCat.ofHom_hom, MagmaCat.hom_ofHom, MagmaCat.hom_comp, MagmaCat.hom_id
hom' 📖	CompOp	1 math math: ext_iff

Theorems

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

MagmaCat.Hom.Simps

Definitions

Name	Category	Theorems
hom 📖	CompOp	—

MulEquiv

Definitions

Name	Category	Theorems
toMagmaCatIso 📖	CompOp	2 math math: toMagmaCatIso_hom, toMagmaCatIso_inv
toSemigrpIso 📖	CompOp	2 math math: toSemigrpIso_inv, toSemigrpIso_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toMagmaCatIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom MagmaCat MagmaCat.instCategory MagmaCat.of toMagmaCatIso MagmaCat.ofHom toMulHom	—	—
toMagmaCatIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv MagmaCat MagmaCat.instCategory MagmaCat.of toMagmaCatIso MagmaCat.ofHom toMulHom symm	—	—
toSemigrpIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom Semigrp Semigrp.instCategory Semigrp.of toSemigrpIso Semigrp.ofHom toMulHom Semigroup.toMul	—	—
toSemigrpIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv Semigrp Semigrp.instCategory Semigrp.of toSemigrpIso Semigrp.ofHom toMulHom Semigroup.toMul symm	—	—

Semigrp

Definitions

Name	Category	Theorems
carrier 📖	CompOp	18 math math: hom_comp, hom_inv_apply, inv_hom_apply, mulEquiv_coe_eq, id_apply, hom_id, forget₂_full, ext_iff, comp_apply, forgetReflectsIsos, MonCat.adjoinOne_obj_coe, MonCat.adjoinOne_map, ofHom_hom, coe_id, ofHom_apply, forget_map, coe_comp, coe_of
hasForgetToMagmaCat 📖	CompOp	1 math math: forget₂_full
instCategory 📖	CompOp	19 math math: hom_comp, ofHom_comp, hom_inv_apply, inv_hom_apply, id_apply, hom_id, forget₂_full, ext_iff, comp_apply, forgetReflectsIsos, MonCat.adjoinOne_obj_coe, MonCat.adjoinOne_map, MulEquiv.toSemigrpIso_inv, ofHom_id, coe_id, MulEquiv.toSemigrpIso_hom, ofHom_apply, forget_map, coe_comp
instCoeSortType 📖	CompOp	—
instConcreteCategoryMulHomCarrier 📖	CompOp	11 math math: hom_inv_apply, inv_hom_apply, id_apply, forget₂_full, ext_iff, comp_apply, forgetReflectsIsos, coe_id, ofHom_apply, forget_map, coe_comp
instInhabited 📖	CompOp	—
of 📖	CompOp	8 math math: hom_ofHom, ofHom_comp, mulEquiv_coe_eq, MulEquiv.toSemigrpIso_inv, ofHom_id, MulEquiv.toSemigrpIso_hom, ofHom_apply, coe_of
ofHom 📖	CompOp	8 math math: hom_ofHom, ofHom_comp, mulEquiv_coe_eq, ofHom_hom, MulEquiv.toSemigrpIso_inv, ofHom_id, MulEquiv.toSemigrpIso_hom, ofHom_apply
str 📖	CompOp	16 math math: hom_comp, hom_inv_apply, inv_hom_apply, mulEquiv_coe_eq, id_apply, hom_id, forget₂_full, ext_iff, comp_apply, forgetReflectsIsos, MonCat.adjoinOne_map, ofHom_hom, coe_id, ofHom_apply, forget_map, coe_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_comp 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom Semigrp instCategory MulHom Semigroup.toMul str MulHom.funLike instConcreteCategoryMulHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
coe_id 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom Semigrp instCategory MulHom Semigroup.toMul str MulHom.funLike instConcreteCategoryMulHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
coe_of 📖	mathematical	—	carrier of	—	—
comp_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom Semigrp instCategory MulHom Semigroup.toMul str MulHom.funLike instConcreteCategoryMulHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
ext 📖	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom Semigrp instCategory MulHom Semigroup.toMul str MulHom.funLike instConcreteCategoryMulHomCarrier	—	—	CategoryTheory.ConcreteCategory.hom_ext
ext_iff 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom Semigrp instCategory MulHom Semigroup.toMul str MulHom.funLike instConcreteCategoryMulHomCarrier	—	ext
forgetReflectsIsos 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms Semigrp instCategory CategoryTheory.types CategoryTheory.forget MulHom carrier Semigroup.toMul str MulHom.funLike instConcreteCategoryMulHomCarrier	—	Equiv.left_inv Equiv.right_inv MulHom.map_mul' CategoryTheory.Iso.isIso_hom
forget_map 📖	mathematical	—	CategoryTheory.Functor.map Semigrp instCategory CategoryTheory.types CategoryTheory.forget MulHom carrier Semigroup.toMul str MulHom.funLike instConcreteCategoryMulHomCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom	—	—
forget₂_full 📖	mathematical	—	CategoryTheory.Functor.Full Semigrp instCategory MagmaCat MagmaCat.instCategory CategoryTheory.forget₂ MulHom carrier Semigroup.toMul str MulHom.funLike instConcreteCategoryMulHomCarrier MagmaCat.carrier MagmaCat.str MagmaCat.instConcreteCategoryMulHomCarrier hasForgetToMagmaCat	—	—
hom_comp 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp Semigrp CategoryTheory.Category.toCategoryStruct instCategory MulHom.comp carrier Semigroup.toMul str	—	—
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
hom_id 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id Semigrp CategoryTheory.Category.toCategoryStruct instCategory MulHom.id carrier Semigroup.toMul str	—	—
hom_inv_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom Semigrp instCategory MulHom Semigroup.toMul str MulHom.funLike instConcreteCategoryMulHomCarrier 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 Semigrp instCategory MulHom Semigroup.toMul str MulHom.funLike instConcreteCategoryMulHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
inv_hom_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom Semigrp instCategory MulHom Semigroup.toMul str MulHom.funLike instConcreteCategoryMulHomCarrier CategoryTheory.Iso.inv CategoryTheory.Iso.hom	—	CategoryTheory.Iso.hom_inv_id_apply
mulEquiv_coe_eq 📖	mathematical	—	Hom.hom of ofHom MulHomClass.toMulHom MulEquiv Semigroup.toMul EquivLike.toFunLike MulEquiv.instEquivLike MulEquivClass.instMulHomClass MulEquiv.instMulEquivClass carrier str	—	MulEquivClass.instMulHomClass MulEquiv.instMulEquivClass
ofHom_apply 📖	mathematical	—	DFunLike.coe of carrier CategoryTheory.ConcreteCategory.hom Semigrp instCategory MulHom Semigroup.toMul str MulHom.funLike instConcreteCategoryMulHomCarrier ofHom	—	—
ofHom_comp 📖	mathematical	—	ofHom MulHom.comp Semigroup.toMul CategoryTheory.CategoryStruct.comp Semigrp CategoryTheory.Category.toCategoryStruct instCategory of	—	—
ofHom_hom 📖	mathematical	—	ofHom carrier str Hom.hom	—	—
ofHom_id 📖	mathematical	—	ofHom MulHom.id Semigroup.toMul CategoryTheory.CategoryStruct.id Semigrp CategoryTheory.Category.toCategoryStruct instCategory of	—	—

Semigrp.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	7 math math: Semigrp.hom_comp, Semigrp.hom_ofHom, Semigrp.mulEquiv_coe_eq, Semigrp.hom_id, MonCat.adjoinOne_map, Semigrp.ofHom_hom, Semigrp.hom_ext_iff
hom' 📖	CompOp	1 math math: ext_iff

Theorems

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

Semigrp.Hom.Simps

Definitions

Name	Category	Theorems
hom 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
AddMagmaCat 📖	CompData	17 math math: AddMagmaCat.coe_id, AddMagmaCat.ofHom_comp, AddMagmaCat.forgetReflectsIsos, AddEquiv.toAddMagmaCatIso_inv, AddMagmaCat.forget_map, AddMagmaCat.ofHom_apply, AddMagmaCat.coe_comp, AddMagmaCat.ext_iff, AddMagmaCat.ofHom_id, AddSemigrp.forget₂_full, AddMagmaCat.hom_id, AddMagmaCat.comp_apply, AddMagmaCat.id_apply, AddEquiv.toAddMagmaCatIso_hom, AddMagmaCat.neg_hom_apply, AddMagmaCat.hom_comp, AddMagmaCat.hom_neg_apply
AddSemigrp 📖	CompData	18 math math: AddSemigrp.coe_id, AddSemigrp.hom_id, AddSemigrp.comp_apply, AddSemigrp.hom_comp, AddSemigrp.neg_hom_apply, AddEquiv.toAddSemigrpIso_hom, AddSemigrp.hom_neg_apply, AddSemigrp.ofHom_apply, AddSemigrp.forget₂_full, AddMonCat.adjoinZero_obj_coe, AddSemigrp.coe_comp, AddSemigrp.ofHom_comp, AddSemigrp.id_apply, AddEquiv.toAddSemigrpIso_inv, AddMonCat.adjoinZero_map, AddSemigrp.forgetReflectsIsos, AddSemigrp.ofHom_id, AddSemigrp.ext_iff
MagmaCat 📖	CompData	17 math math: MagmaCat.coe_comp, Semigrp.forget₂_full, MulEquiv.toMagmaCatIso_hom, MagmaCat.id_apply, MagmaCat.coe_id, MagmaCat.ofHom_apply, MagmaCat.hom_inv_apply, MagmaCat.ext_iff, MagmaCat.forget_map, MulEquiv.toMagmaCatIso_inv, MagmaCat.inv_hom_apply, MagmaCat.hom_comp, MagmaCat.forgetReflectsIsos, MagmaCat.ofHom_id, MagmaCat.hom_id, MagmaCat.comp_apply, MagmaCat.ofHom_comp
addEquivIsoAddMagmaIso 📖	CompOp	—
addEquivIsoAddSemigrpIso 📖	CompOp	—
mulEquivIsoMagmaIso 📖	CompOp	—
mulEquivIsoSemigrpIso 📖	CompOp	—

---

← Back to Index