Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.mk.noConfusion

{P : Sort u} →
  {toLocallyRingedSpace : AlgebraicGeometry.LocallyRingedSpace} →
    {local_affine :
        ∀ (x : ↑toLocallyRingedSpace.toTopCat),
          ∃ U R,
            Nonempty
              (toLocallyRingedSpace.restrict ⋯ ≅ AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op R))} →
      {toLocallyRingedSpace' : AlgebraicGeometry.LocallyRingedSpace} →
        {local_affine' :
            ∀ (x : ↑toLocallyRingedSpace'.toTopCat),
              ∃ U R,
                Nonempty
                  (toLocallyRingedSpace'.restrict ⋯ ≅
                    AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op R))} →
          { toLocallyRingedSpace := toLocallyRingedSpace, local_affine := local_affine } =
              { toLocallyRingedSpace := toLocallyRingedSpace', local_affine := local_affine' } →
            (toLocallyRingedSpace = toLocallyRingedSpace' → P) → P

Defined in

Mathlib.AlgebraicGeometry.Scheme

Cited by

1 results in Mathlib

Foundations

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