Basic

📁 Source: Mathlib/RingTheory/Morita/Basic.lean

Statistics

Metric	Count
Definitions IsMoritaEquivalent, MoritaEquivalence, eqv, ofAlgEquiv, refl, trans	6
Theorems cond, of_algEquiv, refl, trans, instAdditiveModuleCatFunctorEqv, linear	6
Total	12

IsMoritaEquivalent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cond 📖	mathematical	IsMoritaEquivalent	MoritaEquivalence	—	—
of_algEquiv 📖	mathematical	—	IsMoritaEquivalent	—	—
refl 📖	mathematical	—	IsMoritaEquivalent	—	—
trans 📖	—	IsMoritaEquivalent	—	—	Nonempty.map2 cond

MoritaEquivalence

Definitions

Name	Category	Theorems
eqv 📖	CompOp	3 math math: linear, instAdditiveModuleCatFunctorEqv, moritaEquivalenceMatrix_eqv
ofAlgEquiv 📖	CompOp	—
refl 📖	CompOp	—
trans 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instAdditiveModuleCatFunctorEqv 📖	mathematical	—	CategoryTheory.Functor.Additive ModuleCat ModuleCat.moduleCategory ModuleCat.instPreadditive CategoryTheory.Equivalence.functor eqv	—	CategoryTheory.Functor.additive_of_preserves_binary_products CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits ModuleCat.hasLimits Finite.of_fintype CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_functor CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_terminal_object ModuleCat.instHasZeroObject CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit ModuleCat.hasLimit small_subtype small_Pi CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self
linear 📖	mathematical	—	CategoryTheory.Functor.Linear CommSemiring.toSemiring ModuleCat ModuleCat.moduleCategory ModuleCat.instPreadditive ModuleCat.Algebra.instLinear CategoryTheory.Equivalence.functor eqv	—	—

(root)

Definitions

Name	Category	Theorems
IsMoritaEquivalent 📖	CompData	3 math math: IsMoritaEquivalent.matrix, IsMoritaEquivalent.refl, IsMoritaEquivalent.of_algEquiv
MoritaEquivalence 📖	CompData	1 math math: IsMoritaEquivalent.cond

---

← Back to Index