Documentation Verification Report

LiftFunctor

📁 Source: FLT/Deformations/LiftFunctor.lean

Statistics

Metric	Count
Definitions `deformationFunctor`, `detConditionFunctor`, `flatFunctor`, `liftFunctor`, `narrowTraceConditionFunctor`, `repnFunctor`, `repnQuotFunctor`, `toFramedGaloisRep`, `toRepnQuot`, `toRepresentation`, `traceConditionFunctor`, `unramifiedFunctor`	12
Theorems `repnFunctor_map`, `toFramedGaloisRep_map`	2
Total	14

Deformation

Definitions

Name	Category	Theorems
`deformationFunctor` 📖	CompOp	1 math math: `isCorepresentable_deformationFunctor`
`detConditionFunctor` 📖	CompOp	—
`flatFunctor` 📖	CompOp	—
`liftFunctor` 📖	CompOp	—
`narrowTraceConditionFunctor` 📖	CompOp	—
`repnFunctor` 📖	CompOp	2 math math: `repnFunctor_map`, `toFramedGaloisRep_map`
`repnQuotFunctor` 📖	CompOp	1 math math: `isCorepresentable_deformationFunctor`
`toFramedGaloisRep` 📖	CompOp	1 math math: `toFramedGaloisRep_map`
`toRepnQuot` 📖	CompOp	—
`toRepresentation` 📖	CompOp	—
`traceConditionFunctor` 📖	CompOp	—
`unramifiedFunctor` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`repnFunctor_map` 📖	mathematical	—	`ProartinianCat.carrier` `ProartinianCat.commRing` `ProartinianCat.topologicalSpace` `ProartinianCat` `ProartinianCat.instCategory` `repnFunctor` `ProartinianCat.algebra` `ProartinianCat.Hom.hom`	—	—
`toFramedGaloisRep_map` 📖	mathematical	—	`toFramedGaloisRep` `ProartinianCat` `ProartinianCat.instCategory` `repnFunctor` `FramedGaloisRep.baseChange` `ProartinianCat.carrier` `ProartinianCat.commRing` `ProartinianCat.topologicalSpace` `IsLocalProartinianAlgebra.toIsTopologicalRing` `ProartinianCat.algebra` `ProartinianCat.isLocalProartinianAlgebra` `ProartinianCat.Hom.hom`	—	`IsLocalProartinianAlgebra.toIsTopologicalRing` `ProartinianCat.isLocalProartinianAlgebra` `FramedGaloisRep.baseChange_GL`

---

← Back to Index