Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.coverOfIsIso

{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  [P.ContainsIdentities] →
    [P.RespectsIso] →
      {X Y : AlgebraicGeometry.Scheme} →
        (f : X ⟶ Y) →
          [CategoryTheory.IsIso f] → AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) Y

An isomorphism X ⟶ Y is a P-cover of Y.

Defined in

Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Cited by

9 results in Mathlib

Foundations

Depth 111 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.MorphismProperty.ContainsIdentitiesCategoryTheory.MorphismProperty.RespectsIsoCategoryTheory.IsIso