Over

📁 Source: Mathlib/AlgebraicGeometry/Over.lean

Statistics

Metric	Count
Definitions CanonicallyOver, IsOver, asOver, Over, asOver	5
Theorems isOver_iff	1
Total	6

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
CanonicallyOver 📖	CompOp	—
Over 📖	CompOp	1 math math: AlgebraicGeometry.instSubsingletonOverTerminalScheme
asOver 📖	CompOp	3 math math: isCommMonObj_asOver_pullback, monObjAsOverPullback_mul, monObjAsOverPullback_one

AlgebraicGeometry.Scheme.Hom

Definitions

Name	Category	Theorems
IsOver 📖	MathDef	14 math math: AlgebraicGeometry.Scheme.instIsOverFromSpecStalkOfMem, isOver_iff, AlgebraicGeometry.AffineSpace.homOverEquiv_symm_apply_coe, AlgebraicGeometry.instIsOverTerminalScheme, AlgebraicGeometry.Scheme.instIsOverMapResidueFieldMapOverInferInstanceOverClass, AlgebraicGeometry.Scheme.instIsOverMapStalkSpecializesCommRingCatPresheaf, AlgebraicGeometry.AffineSpace.instIsOverHomOfVectorOverSchemeInferInstanceOverClass, AlgebraicGeometry.Scheme.instIsOverFstOverInferInstanceOverClassId, AlgebraicGeometry.Scheme.Opens.instIsOverι, AlgebraicGeometry.AffineSpace.homOverEquiv_apply, AlgebraicGeometry.Scheme.instIsOverMapStalkMapOverInferInstanceOverClass, AlgebraicGeometry.Scheme.instIsOverMapHomCommRingCatResidueFieldCongr, AlgebraicGeometry.Scheme.Cover.Over.isOver_map, AlgebraicGeometry.instIsOverHomOfLE
asOver 📖	CompOp	5 math math: AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_X, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_X, AlgebraicGeometry.Scheme.isMonHom_fst_id_right, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver_f, AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOver_iff 📖	mathematical	—	IsOver CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.over CategoryTheory.OverClass	—	CategoryTheory.HomIsOver.comp_over

---

← Back to Index