Representable

📁 Source: FLT/Deformations/Representable.lean

Statistics

Metric	Count
Definitions SLiftFunctor, narrowSLiftFunctor, narrowSLiftUniversalRing, narrowSLiftUniversalRingCorepresentableBy	4
Theorems isCorepresentable_deformationFunctor, isCorepresentable_narrowSLiftFunctor	2
Total	6
⚠️ With sorry isCorepresentable_deformationFunctor, isCorepresentable_narrowSLiftFunctor	2

Deformation

Definitions

Name	Category	Theorems
SLiftFunctor 📖	CompOp	—
narrowSLiftFunctor 📖	CompOp	—
narrowSLiftUniversalRing 📖	CompOp	—
narrowSLiftUniversalRingCorepresentableBy 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCorepresentable_deformationFunctor 📖 ⚠️	mathematical	—	ProartinianCat ProartinianCat.instCategory CategoryTheory.Subfunctor.toFunctor repnQuotFunctor deformationFunctor	—	—
isCorepresentable_narrowSLiftFunctor 📖 ⚠️	mathematical	ProartinianCat ProartinianCat.instCategory repnFunctor ProartinianCat.residueField CategoryTheory.Subfunctor.obj narrowSLiftFunctor	CategoryTheory.Subfunctor.toFunctor	—	—

---

← Back to Index