EssentiallySmall

📁 Source: Mathlib/Algebra/Category/FGModuleCat/EssentiallySmall.lean

Statistics

Metric	Count
Definitions FGModuleRepr, S, embed, instAddCommGroupRepr, instCategory, instCoeSortType, instModuleRepr, instSmallCategory, n, ofFinite, ofFiniteEquiv, repr	12
Theorems instFiniteRepr, instIsEquivalenceFGModuleCatEmbed, instEssentiallySmallFGModuleCat, instIsEquivalenceFGModuleCatUlift	4
Total	16

FGModuleRepr

Definitions

Name	Category	Theorems
S 📖	CompOp	—
embed 📖	CompOp	1 math math: instIsEquivalenceFGModuleCatEmbed
instAddCommGroupRepr 📖	CompOp	1 math math: instFiniteRepr
instCategory 📖	CompOp	—
instCoeSortType 📖	CompOp	—
instModuleRepr 📖	CompOp	1 math math: instFiniteRepr
instSmallCategory 📖	CompOp	1 math math: instIsEquivalenceFGModuleCatEmbed
n 📖	CompOp	—
ofFinite 📖	CompOp	—
ofFiniteEquiv 📖	CompOp	—
repr 📖	CompOp	1 math math: instFiniteRepr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFiniteRepr 📖	mathematical	—	Module.Finite repr CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupRepr instModuleRepr	—	Module.Finite.quotient Module.Finite.pi Finite.of_fintype Module.Finite.self
instIsEquivalenceFGModuleCatEmbed 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence FGModuleRepr instSmallCategory FGModuleCat CommRing.toRing CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG embed	—	CategoryTheory.Functor.Faithful.comp instFiniteRepr CategoryTheory.Functor.FullyFaithful.faithful FGModuleCat.instFaithfulUlift CategoryTheory.Functor.Full.comp CategoryTheory.Functor.FullyFaithful.full FGModuleCat.instFullUlift FGModuleCat.instFiniteCarrier Module.Finite.ulift RingHomCompTriple.ids RingHomInvPair.ids

(root)

Definitions

Name	Category	Theorems
FGModuleRepr 📖	CompData	1 math math: FGModuleRepr.instIsEquivalenceFGModuleCatEmbed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instEssentiallySmallFGModuleCat 📖	mathematical	—	CategoryTheory.EssentiallySmall FGModuleCat CommRing.toRing CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG	—	CategoryTheory.essentiallySmall_of_fully_faithful FGModuleCat.instFullUlift FGModuleCat.instFaithfulUlift FGModuleRepr.instIsEquivalenceFGModuleCatEmbed
instIsEquivalenceFGModuleCatUlift 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence FGModuleCat CommRing.toRing CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG FGModuleCat.ulift	—	FGModuleCat.instFaithfulUlift FGModuleCat.instFullUlift FGModuleCat.instFiniteCarrier Module.Finite.ulift FGModuleRepr.instFiniteRepr RingHomCompTriple.ids RingHomInvPair.ids

---

← Back to Index