Subfunctor

📁 Source: FLT/Deformations/Subfunctor.lean

Statistics

Metric	Count
Definitions `Subfunctor`, `Subfunctor`, `homOfLe`, `instCoeHeadObjToFunctor`, `obj`, `ofIsTerminal`, `toFunctor`, `ι`, `instCompleteLatticeSubfunctor`, `instPartialOrderSubfunctor`	10
Theorems `bot_obj`, `eq_top_iff_isIso`, `ext`, `ext_iff`, `homOfLe_app_coe`, `homOfLe_ι`, `homOfLe_ι_assoc`, `iInf_obj`, `iSup_min`, `iSup_obj`, `instIsIsoFunctorTypeιTop`, `instMonoFunctorTypeHomOfLe`, `instMonoFunctorTypeι`, `instNonempty`, `le_def`, `map`, `max_min`, `max_obj`, `min_obj`, `nat_trans_naturality`, `sInf_obj`, `sSup_obj`, `toFunctor_map_coe`, `toFunctor_obj`, `top_obj`, `ι_app`, `top_Subfunctor_obj`	27
Total	37

CategoryTheory

Definitions

Name	Category	Theorems
`Subfunctor` 📖	CompData	15 math math: `Subfunctor.instNonempty`, `Subfunctor.max_obj`, `Subfunctor.max_min`, `Subfunctor.sSup_obj`, `Subfunctor.eq_top_iff_isIso`, `Subfunctor.iSup_min`, `Subfunctor.min_obj`, `Subfunctor.le_def`, `Subfunctor.sInf_obj`, `Subfunctor.instIsIsoFunctorTypeιTop`, `Subfunctor.bot_obj`, `top_Subfunctor_obj`, `Subfunctor.iInf_obj`, `Subfunctor.top_obj`, `Subfunctor.iSup_obj`
`instCompleteLatticeSubfunctor` 📖	CompOp	13 math math: `Subfunctor.max_obj`, `Subfunctor.max_min`, `Subfunctor.sSup_obj`, `Subfunctor.eq_top_iff_isIso`, `Subfunctor.iSup_min`, `Subfunctor.min_obj`, `Subfunctor.sInf_obj`, `Subfunctor.instIsIsoFunctorTypeιTop`, `Subfunctor.bot_obj`, `top_Subfunctor_obj`, `Subfunctor.iInf_obj`, `Subfunctor.top_obj`, `Subfunctor.iSup_obj`
`instPartialOrderSubfunctor` 📖	CompOp	1 math math: `Subfunctor.le_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`top_Subfunctor_obj` 📖	mathematical	—	`Subfunctor.obj` `Subfunctor` `instCompleteLatticeSubfunctor`	—	`Subfunctor.top_obj`

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
`Subfunctor` 📖	CompOp	—

CategoryTheory.Subfunctor

Definitions

Name	Category	Theorems
`homOfLe` 📖	CompOp	4 math math: `homOfLe_app_coe`, `homOfLe_ι_assoc`, `homOfLe_ι`, `instMonoFunctorTypeHomOfLe`
`instCoeHeadObjToFunctor` 📖	CompOp	—
`obj` 📖	CompOp	17 math math: `toFunctor_obj`, `homOfLe_app_coe`, `max_obj`, `nat_trans_naturality`, `sSup_obj`, `min_obj`, `map`, `le_def`, `sInf_obj`, `bot_obj`, `toFunctor_map_coe`, `CategoryTheory.top_Subfunctor_obj`, `iInf_obj`, `ι_app`, `top_obj`, `iSup_obj`, `ext_iff`
`ofIsTerminal` 📖	CompOp	—
`toFunctor` 📖	CompOp	13 math math: `Deformation.isCorepresentable_deformationFunctor`, `toFunctor_obj`, `homOfLe_app_coe`, `nat_trans_naturality`, `Deformation.isCorepresentable_narrowSLiftFunctor`, `homOfLe_ι_assoc`, `homOfLe_ι`, `eq_top_iff_isIso`, `instIsIsoFunctorTypeιTop`, `toFunctor_map_coe`, `instMonoFunctorTypeHomOfLe`, `ι_app`, `instMonoFunctorTypeι`
`ι` 📖	CompOp	6 math math: `homOfLe_ι_assoc`, `homOfLe_ι`, `eq_top_iff_isIso`, `instIsIsoFunctorTypeιTop`, `ι_app`, `instMonoFunctorTypeι`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_obj` 📖	mathematical	—	`obj` `CategoryTheory.Subfunctor` `CategoryTheory.instCompleteLatticeSubfunctor`	—	—
`eq_top_iff_isIso` 📖	mathematical	—	`CategoryTheory.Subfunctor` `CategoryTheory.instCompleteLatticeSubfunctor` `toFunctor` `ι`	—	`instIsIsoFunctorTypeιTop` `ext`
`ext` 📖	—	`obj`	—	—	—
`ext_iff` 📖	mathematical	—	`obj`	—	`ext`
`homOfLe_app_coe` 📖	mathematical	`CategoryTheory.Subfunctor` `CategoryTheory.instPartialOrderSubfunctor`	`obj` `toFunctor` `homOfLe`	—	—
`homOfLe_ι` 📖	mathematical	`CategoryTheory.Subfunctor` `CategoryTheory.instPartialOrderSubfunctor`	`toFunctor` `homOfLe` `ι`	—	—
`homOfLe_ι_assoc` 📖	mathematical	`CategoryTheory.Subfunctor` `CategoryTheory.instPartialOrderSubfunctor`	`toFunctor` `homOfLe` `ι`	—	`homOfLe_ι`
`iInf_obj` 📖	mathematical	—	`obj` `CategoryTheory.Subfunctor` `CategoryTheory.instCompleteLatticeSubfunctor`	—	—
`iSup_min` 📖	mathematical	—	`CategoryTheory.Subfunctor` `CategoryTheory.instCompleteLatticeSubfunctor`	—	`ext` `iSup_obj`
`iSup_obj` 📖	mathematical	—	`obj` `CategoryTheory.Subfunctor` `CategoryTheory.instCompleteLatticeSubfunctor`	—	—
`instIsIsoFunctorTypeιTop` 📖	mathematical	—	`toFunctor` `CategoryTheory.Subfunctor` `CategoryTheory.instCompleteLatticeSubfunctor` `ι`	—	—
`instMonoFunctorTypeHomOfLe` 📖	mathematical	`CategoryTheory.Subfunctor` `CategoryTheory.instPartialOrderSubfunctor`	`toFunctor` `homOfLe`	—	—
`instMonoFunctorTypeι` 📖	mathematical	—	`toFunctor` `ι`	—	—
`instNonempty` 📖	mathematical	—	`CategoryTheory.Subfunctor`	—	—
`le_def` 📖	mathematical	—	`CategoryTheory.Subfunctor` `CategoryTheory.instPartialOrderSubfunctor` `obj`	—	—
`map` 📖	mathematical	—	`obj`	—	—
`max_min` 📖	mathematical	—	`CategoryTheory.Subfunctor` `CategoryTheory.instCompleteLatticeSubfunctor`	—	`ext`
`max_obj` 📖	mathematical	—	`obj` `CategoryTheory.Subfunctor` `CategoryTheory.instCompleteLatticeSubfunctor`	—	—
`min_obj` 📖	mathematical	—	`obj` `CategoryTheory.Subfunctor` `CategoryTheory.instCompleteLatticeSubfunctor`	—	—
`nat_trans_naturality` 📖	mathematical	—	`obj` `toFunctor`	—	—
`sInf_obj` 📖	mathematical	—	`obj` `CategoryTheory.Subfunctor` `CategoryTheory.instCompleteLatticeSubfunctor`	—	—
`sSup_obj` 📖	mathematical	—	`obj` `CategoryTheory.Subfunctor` `CategoryTheory.instCompleteLatticeSubfunctor`	—	—
`toFunctor_map_coe` 📖	mathematical	—	`obj` `toFunctor`	—	—
`toFunctor_obj` 📖	mathematical	—	`toFunctor` `obj`	—	—
`top_obj` 📖	mathematical	—	`obj` `CategoryTheory.Subfunctor` `CategoryTheory.instCompleteLatticeSubfunctor`	—	—
`ι_app` 📖	mathematical	—	`toFunctor` `ι` `obj`	—	—

---

← Back to Index