18.7. Properties of morphisms🔗

We have already seen two properties of morphisms in the previous section. Mathlib knows many properties of morphisms. Browsing the AlgebraicGeometry/Morphisms folder gives an overview. The properties are defined as type classes, so many basic proofs are automatic by inferInstance:

example (f : X ⟶ Z) (g : Y ⟶ Z) [IsProper f] :
    IsSeparated (pullback.snd f g) :=
  inferInstance

To unify the handling of the meta properties of these properties of morphisms, we rely on MorphismProperty. Any of the properties we have seen before can be viewed as a MorphismProperty by prepending @:

example : MorphismProperty Scheme :=
  @IsClosedImmersion

There exist meta properties for morphism properties, for example being stable under composition, base change, etc.

CategoryTheory.MorphismProperty.IsStableUnderComposition.{v, u} {C : Type u} [Category.{v, u} C]
  (P : MorphismProperty C) : Prop#check MorphismProperty.IsStableUnderComposition
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.{v, u} {C : Type u} [Category.{v, u} C]
  (P : MorphismProperty C) : Prop#check MorphismProperty.IsStableUnderBaseChange
CategoryTheory.MorphismProperty.RespectsIso.{v, u} {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) : Prop#check MorphismProperty.RespectsIso

and also some more technical ones:

CategoryTheory.MorphismProperty.HasOfPostcompProperty.{v, u} {C : Type u} [Category.{v, u} C]
  (W W' : MorphismProperty C) : Prop#check MorphismProperty.HasOfPostcompProperty

Besides properties of properties, we also use abstract constructions of properties.

CategoryTheory.MorphismProperty.universally.{v, u} {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) :
  MorphismProperty C#check MorphismProperty.universally
CategoryTheory.MorphismProperty.diagonal.{v, u} {C : Type u} [Category.{v, u} C] [HasPullbacks C]
  (P : MorphismProperty C) : MorphismProperty C#check MorphismProperty.diagonal
AlgebraicGeometry.topologically.{u}
  (P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop) : MorphismProperty Scheme#check topologically