Documentation Verification Report

OverClass

📁 Source: Mathlib/CategoryTheory/Comma/Over/OverClass.lean

Statistics

Metric	Count
Definitions `CanonicallyOverClass`, `over`, `instOverClass`, `toOverClass`, `HomIsOver`, `IsOverTower`, `asOver`, `OverClass`, `over`, `asOver`, `asOverHom`, `fromOver`, `hom`, `instOverClass`, `over`, `«term_↘_»`	16
Theorems `over_def`, `comp_over`, `asOver_hom`, `asOver_inv`, `asOverHom_comp`, `asOverHom_comp_assoc`, `asOverHom_id`, `asOverHom_inv`, `asOverHom_left`, `asOver_hom`, `asOver_left`, `fromOver_over`, `instHomIsOverHomAsIso`, `instHomIsOverHomOfInv`, `instHomIsOverInv`, `instHomIsOverInvAsIso`, `instHomIsOverInvOfHom`, `instIsIsoOverAsOverHom`, `comp_over`, `comp_over_assoc`, `homIsOver_of_isOverTower`, `instHomIsOverComp`, `instHomIsOverId`, `instHomIsOverLeftDiscretePUnit`, `instHomIsOverOfIsOverTower`, `instHomIsOverOfIsOverTower_1`, `instIsIsoOverInferInstanceOverClass`, `instIsOverTower`, `instIsOverTower_1`, `instIsOverTower_2`, `over_def`	31
Total	47

CategoryTheory

Definitions

Name	Category	Theorems
`CanonicallyOverClass` 📖	CompData	—
`HomIsOver` 📖	CompData	11 math math: `homIsOver_of_isOverTower`, `instHomIsOverComp`, `OverClass.instHomIsOverHomOfInv`, `OverClass.instHomIsOverInvAsIso`, `instHomIsOverOfIsOverTower`, `OverClass.instHomIsOverHomAsIso`, `instHomIsOverLeftDiscretePUnit`, `OverClass.instHomIsOverInv`, `instHomIsOverId`, `OverClass.instHomIsOverInvOfHom`, `instHomIsOverOfIsOverTower_1`
`IsOverTower` 📖	MathDef	3 math math: `instIsOverTower_1`, `instIsOverTower`, `instIsOverTower_2`
`OverClass` 📖	CompData	48 math math: `AlgebraicGeometry.AffineSpace.not_isIntegralHom`, `AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop`, `AlgebraicGeometry.Scheme.Hom.isOver_iff`, `AlgebraicGeometry.AffineSpace.map_over_assoc`, `AlgebraicGeometry.AffineSpace.homOverEquiv_symm_apply_coe`, `AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc`, `AlgebraicGeometry.Scheme.over_def`, `over_def`, `AlgebraicGeometry.Scheme.isCommMonObj_asOver_pullback`, `AlgebraicGeometry.Scheme.isMonHom_fst_id_right`, `AlgebraicGeometry.AffineSpace.reindex_over`, `AlgebraicGeometry.AffineSpace.map_over`, `AlgebraicGeometry.Scheme.instIsOverMapResidueFieldMapOverInferInstanceOverClass`, `OverClass.fromOver_over`, `AlgebraicGeometry.AffineSpace.instLocallyOfFinitePresentationOverSchemeInferInstanceOverClassOfFinite`, `AlgebraicGeometry.AffineSpace.instIsIsoSchemeOverInferInstanceOverClassOfIsEmpty`, `AlgebraicGeometry.AffineSpace.isOpenMap_over`, `AlgebraicGeometry.AffineSpace.hom_ext_iff`, `AlgebraicGeometry.AffineSpace.isPullback_map`, `AlgebraicGeometry.AffineSpace.homOfVector_over_assoc`, `AlgebraicGeometry.Scheme.Opens.over_def`, `AlgebraicGeometry.over_def`, `AlgebraicGeometry.AffineSpace.SpecIso_inv_over_assoc`, `AlgebraicGeometry.AffineSpace.instIsAffineHomOverSchemeInferInstanceOverClass`, `AlgebraicGeometry.Scheme.monObjAsOverPullback_mul`, `instIsIsoOverInferInstanceOverClass`, `AlgebraicGeometry.AffineSpace.instIsOverHomOfVectorOverSchemeInferInstanceOverClass`, `AlgebraicGeometry.Scheme.instIsOverFstOverInferInstanceOverClassId`, `AlgebraicGeometry.AffineSpace.isIntegralHom_over_iff_isEmpty`, `AlgebraicGeometry.Scheme.PartialMap.isOver_iff_eq_restrict`, `OverClass.asOver_hom`, `comp_over_assoc`, `AlgebraicGeometry.AffineSpace.homOfVector_over`, `CanonicallyOverClass.over_def`, `AlgebraicGeometry.AffineSpace.reindex_over_assoc`, `AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop`, `AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom`, `AlgebraicGeometry.AffineSpace.over_over`, `AlgebraicGeometry.Scheme.PartialMap.isOver_iff`, `AlgebraicGeometry.Scheme.instIsOverMapStalkMapOverInferInstanceOverClass`, `HomIsOver.comp_over`, `AlgebraicGeometry.Scheme.canonicallyOverPullback_over`, `AlgebraicGeometry.AffineSpace.SpecIso_inv_over`, `comp_over`, `AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over`, `AlgebraicGeometry.Scheme.monObjAsOverPullback_one`, `AlgebraicGeometry.AffineSpace.instSurjectiveOverSchemeInferInstanceOverClass`, `AlgebraicGeometry.Scheme.RationalMap.isOver_iff`
`instOverClass` 📖	CompOp	5 math math: `instIsOverTower_1`, `over_def`, `instIsOverTower`, `instIsIsoOverInferInstanceOverClass`, `AlgebraicGeometry.Scheme.Opens.instIsOverι`
`over` 📖	CompOp	48 math math: `AlgebraicGeometry.AffineSpace.not_isIntegralHom`, `AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop`, `AlgebraicGeometry.Scheme.Hom.isOver_iff`, `AlgebraicGeometry.AffineSpace.map_over_assoc`, `AlgebraicGeometry.AffineSpace.homOverEquiv_symm_apply_coe`, `AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc`, `AlgebraicGeometry.Scheme.over_def`, `over_def`, `AlgebraicGeometry.Scheme.isCommMonObj_asOver_pullback`, `AlgebraicGeometry.Scheme.isMonHom_fst_id_right`, `AlgebraicGeometry.AffineSpace.reindex_over`, `AlgebraicGeometry.AffineSpace.map_over`, `AlgebraicGeometry.Scheme.instIsOverMapResidueFieldMapOverInferInstanceOverClass`, `OverClass.fromOver_over`, `AlgebraicGeometry.AffineSpace.instLocallyOfFinitePresentationOverSchemeInferInstanceOverClassOfFinite`, `AlgebraicGeometry.AffineSpace.instIsIsoSchemeOverInferInstanceOverClassOfIsEmpty`, `AlgebraicGeometry.AffineSpace.isOpenMap_over`, `AlgebraicGeometry.AffineSpace.hom_ext_iff`, `AlgebraicGeometry.AffineSpace.isPullback_map`, `AlgebraicGeometry.AffineSpace.homOfVector_over_assoc`, `AlgebraicGeometry.Scheme.Opens.over_def`, `AlgebraicGeometry.over_def`, `AlgebraicGeometry.AffineSpace.SpecIso_inv_over_assoc`, `AlgebraicGeometry.AffineSpace.instIsAffineHomOverSchemeInferInstanceOverClass`, `AlgebraicGeometry.Scheme.monObjAsOverPullback_mul`, `instIsIsoOverInferInstanceOverClass`, `AlgebraicGeometry.AffineSpace.instIsOverHomOfVectorOverSchemeInferInstanceOverClass`, `AlgebraicGeometry.Scheme.instIsOverFstOverInferInstanceOverClassId`, `AlgebraicGeometry.AffineSpace.isIntegralHom_over_iff_isEmpty`, `AlgebraicGeometry.Scheme.PartialMap.isOver_iff_eq_restrict`, `OverClass.asOver_hom`, `comp_over_assoc`, `AlgebraicGeometry.AffineSpace.homOfVector_over`, `CanonicallyOverClass.over_def`, `AlgebraicGeometry.AffineSpace.reindex_over_assoc`, `AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop`, `AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom`, `AlgebraicGeometry.AffineSpace.over_over`, `AlgebraicGeometry.Scheme.PartialMap.isOver_iff`, `AlgebraicGeometry.Scheme.instIsOverMapStalkMapOverInferInstanceOverClass`, `HomIsOver.comp_over`, `AlgebraicGeometry.Scheme.canonicallyOverPullback_over`, `AlgebraicGeometry.AffineSpace.SpecIso_inv_over`, `comp_over`, `AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over`, `AlgebraicGeometry.Scheme.monObjAsOverPullback_one`, `AlgebraicGeometry.AffineSpace.instSurjectiveOverSchemeInferInstanceOverClass`, `AlgebraicGeometry.Scheme.RationalMap.isOver_iff`
`«term_↘_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_over` 📖	mathematical	—	`CategoryStruct.comp` `Category.toCategoryStruct` `over` `OverClass`	—	`HomIsOver.comp_over`
`comp_over_assoc` 📖	mathematical	—	`CategoryStruct.comp` `Category.toCategoryStruct` `over` `OverClass`	—	`Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comp_over`
`homIsOver_of_isOverTower` 📖	mathematical	—	`HomIsOver`	—	`comp_over` `comp_over_assoc`
`instHomIsOverComp` 📖	mathematical	—	`HomIsOver` `CategoryStruct.comp` `Category.toCategoryStruct`	—	`Category.assoc` `comp_over`
`instHomIsOverId` 📖	mathematical	—	`HomIsOver` `CategoryStruct.id` `Category.toCategoryStruct`	—	`Category.id_comp`
`instHomIsOverLeftDiscretePUnit` 📖	mathematical	—	`HomIsOver` `Comma.left` `Discrete` `discreteCategory` `Functor.id` `Functor.fromPUnit` `CommaMorphism.left` `OverClass.fromOver`	—	`Over.w`
`instHomIsOverOfIsOverTower` 📖	mathematical	—	`HomIsOver`	—	`homIsOver_of_isOverTower`
`instHomIsOverOfIsOverTower_1` 📖	mathematical	—	`HomIsOver`	—	`homIsOver_of_isOverTower`
`instIsIsoOverInferInstanceOverClass` 📖	mathematical	—	`IsIso` `over` `OverClass` `instOverClass`	—	`IsIso.id`
`instIsOverTower` 📖	mathematical	—	`IsOverTower` `instOverClass`	—	`comp_over` `instHomIsOverId`
`instIsOverTower_1` 📖	mathematical	—	`IsOverTower` `instOverClass`	—	`Category.comp_id`
`instIsOverTower_2` 📖	mathematical	—	`IsOverTower` `CanonicallyOverClass.instOverClass` `CanonicallyOverClass.toOverClass`	—	—
`over_def` 📖	mathematical	—	`over` `OverClass` `instOverClass` `CategoryStruct.id` `Category.toCategoryStruct`	—	—

CategoryTheory.CanonicallyOverClass

Definitions

Name	Category	Theorems
`instOverClass` 📖	CompOp	4 math math: `AlgebraicGeometry.Scheme.instIsOverMapResidueFieldMapOverInferInstanceOverClass`, `over_def`, `AlgebraicGeometry.Scheme.instIsOverMapStalkMapOverInferInstanceOverClass`, `CategoryTheory.instIsOverTower_2`
`toOverClass` 📖	CompOp	38 math math: `AlgebraicGeometry.AffineSpace.not_isIntegralHom`, `AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop`, `AlgebraicGeometry.Scheme.instIsOverFromSpecStalkOfMem`, `AlgebraicGeometry.AffineSpace.map_over_assoc`, `AlgebraicGeometry.AffineSpace.homOverEquiv_symm_apply_coe`, `AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc`, `AlgebraicGeometry.Scheme.isCommMonObj_asOver_pullback`, `AlgebraicGeometry.Scheme.isMonHom_fst_id_right`, `AlgebraicGeometry.AffineSpace.reindex_over`, `AlgebraicGeometry.AffineSpace.map_over`, `AlgebraicGeometry.AffineSpace.instLocallyOfFinitePresentationOverSchemeInferInstanceOverClassOfFinite`, `AlgebraicGeometry.AffineSpace.instIsIsoSchemeOverInferInstanceOverClassOfIsEmpty`, `AlgebraicGeometry.AffineSpace.isOpenMap_over`, `AlgebraicGeometry.AffineSpace.hom_ext_iff`, `AlgebraicGeometry.AffineSpace.isPullback_map`, `AlgebraicGeometry.AffineSpace.homOfVector_over_assoc`, `AlgebraicGeometry.Scheme.Opens.over_def`, `AlgebraicGeometry.AffineSpace.SpecIso_inv_over_assoc`, `AlgebraicGeometry.AffineSpace.instIsAffineHomOverSchemeInferInstanceOverClass`, `AlgebraicGeometry.Scheme.monObjAsOverPullback_mul`, `AlgebraicGeometry.AffineSpace.instIsOverHomOfVectorOverSchemeInferInstanceOverClass`, `AlgebraicGeometry.Scheme.instIsOverFstOverInferInstanceOverClassId`, `AlgebraicGeometry.AffineSpace.isIntegralHom_over_iff_isEmpty`, `AlgebraicGeometry.AffineSpace.homOfVector_over`, `over_def`, `AlgebraicGeometry.AffineSpace.reindex_over_assoc`, `AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop`, `AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom`, `AlgebraicGeometry.Scheme.Opens.instIsOverι`, `AlgebraicGeometry.AffineSpace.homOverEquiv_apply`, `AlgebraicGeometry.AffineSpace.over_over`, `AlgebraicGeometry.Scheme.canonicallyOverPullback_over`, `AlgebraicGeometry.AffineSpace.SpecIso_inv_over`, `AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over`, `AlgebraicGeometry.Scheme.monObjAsOverPullback_one`, `AlgebraicGeometry.instIsOverHomOfLE`, `AlgebraicGeometry.AffineSpace.instSurjectiveOverSchemeInferInstanceOverClass`, `CategoryTheory.instIsOverTower_2`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`over_def` 📖	mathematical	—	`CategoryTheory.over` `CategoryTheory.OverClass` `instOverClass` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `toOverClass`	—	—

CategoryTheory.CanonicallyOverClass.Simps

Definitions

Name	Category	Theorems
`over` 📖	CompOp	—

CategoryTheory.HomIsOver

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_over` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.over` `CategoryTheory.OverClass`	—	—

CategoryTheory.Iso

Definitions

Name	Category	Theorems
`asOver` 📖	CompOp	2 math math: `asOver_hom`, `asOver_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`asOver_hom` 📖	mathematical	—	`hom` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.OverClass.asOver` `asOver` `CategoryTheory.OverClass.asOverHom`	—	—
`asOver_inv` 📖	mathematical	—	`inv` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.OverClass.asOver` `asOver` `CategoryTheory.OverClass.asOverHom` `CategoryTheory.OverClass.instHomIsOverInvOfHom`	—	—

CategoryTheory.OverClass

Definitions

Name	Category	Theorems
`asOver` 📖	CompOp	15 math math: `AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_X`, `CategoryTheory.Iso.asOver_hom`, `AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_X`, `asOverHom_comp_assoc`, `AlgebraicGeometry.Scheme.isMonHom_fst_id_right`, `asOverHom_inv`, `asOverHom_id`, `instIsIsoOverAsOverHom`, `asOver_left`, `asOverHom_left`, `AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_f`, `asOver_hom`, `CategoryTheory.Iso.asOver_inv`, `AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_f`, `asOverHom_comp`
`asOverHom` 📖	CompOp	8 math math: `CategoryTheory.Iso.asOver_hom`, `asOverHom_comp_assoc`, `asOverHom_inv`, `asOverHom_id`, `instIsIsoOverAsOverHom`, `asOverHom_left`, `CategoryTheory.Iso.asOver_inv`, `asOverHom_comp`
`fromOver` 📖	CompOp	2 math math: `fromOver_over`, `CategoryTheory.instHomIsOverLeftDiscretePUnit`
`hom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`asOverHom_comp` 📖	mathematical	—	`asOverHom` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.instHomIsOverComp` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `asOver`	—	`CategoryTheory.instHomIsOverComp`
`asOverHom_comp_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Over` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.instCategoryOver` `asOver` `asOverHom` `CategoryTheory.instHomIsOverComp`	—	`CategoryTheory.instHomIsOverComp` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `asOverHom_comp`
`asOverHom_id` 📖	mathematical	—	`asOverHom` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.instHomIsOverId` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `asOver`	—	`CategoryTheory.instHomIsOverId`
`asOverHom_inv` 📖	mathematical	—	`asOverHom` `CategoryTheory.inv` `instHomIsOverInv` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `asOver` `instIsIsoOverAsOverHom`	—	`instHomIsOverInv` `instIsIsoOverAsOverHom` `asOverHom.congr_simp` `CategoryTheory.IsIso.hom_inv_id` `CategoryTheory.instHomIsOverComp`
`asOverHom_left` 📖	mathematical	—	`CategoryTheory.CommaMorphism.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `asOver` `asOverHom`	—	—
`asOver_hom` 📖	mathematical	—	`CategoryTheory.Comma.hom` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `asOver` `CategoryTheory.over` `CategoryTheory.OverClass`	—	—
`asOver_left` 📖	mathematical	—	`CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `asOver`	—	—
`fromOver_over` 📖	mathematical	—	`CategoryTheory.over` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.OverClass` `fromOver` `CategoryTheory.Comma.hom`	—	—
`instHomIsOverHomAsIso` 📖	mathematical	—	`CategoryTheory.HomIsOver` `CategoryTheory.Iso.hom` `CategoryTheory.asIso`	—	`CategoryTheory.comp_over`
`instHomIsOverHomOfInv` 📖	mathematical	—	`CategoryTheory.HomIsOver` `CategoryTheory.Iso.hom`	—	`CategoryTheory.comp_over`
`instHomIsOverInv` 📖	mathematical	—	`CategoryTheory.HomIsOver` `CategoryTheory.inv`	—	`CategoryTheory.comp_over`
`instHomIsOverInvAsIso` 📖	mathematical	—	`CategoryTheory.HomIsOver` `CategoryTheory.Iso.inv` `CategoryTheory.asIso`	—	`CategoryTheory.comp_over`
`instHomIsOverInvOfHom` 📖	mathematical	—	`CategoryTheory.HomIsOver` `CategoryTheory.Iso.inv`	—	`CategoryTheory.comp_over`
`instIsIsoOverAsOverHom` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `asOver` `asOverHom`	—	`CategoryTheory.isIso_of_reflects_iso` `CategoryTheory.Over.forget_reflects_iso`

CategoryTheory.OverClass.Simps

Definitions

Name	Category	Theorems
`over` 📖	CompOp	—

---

← Back to Index