Mathlib Map

Structures · Geometry

AlgebraicGeometry.IsSeparated

A morphism is separated if the diagonal map is a closed immersion.

Defined in
Mathlib.AlgebraicGeometry.Morphisms.Separated
Shape
One type argument · adds isClosedImmersion_diagonal
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by4

Forgetful instances

Every AlgebraicGeometry.IsSeparated is also a

Provided automatically by

Concrete types that are instances4

  • CategoryTheory.Limits.pullback
  • AlgebraicGeometry.Scheme.Opens.toScheme
  • AlgebraicGeometry.Spec
  • AlgebraicGeometry.Proj

How is a type an instance?

Loading the hierarchy index…

Assumed by34

Ancestors1