Theorems · Definition · algebraic geometry

AlgebraicGeometry.SheafedSpace.GlueData.mk.noConfusion

{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {P : Sort u_1} →
      {toGlueData : CategoryTheory.GlueData (AlgebraicGeometry.SheafedSpace C)} →
        {f_open : ∀ (i j : toGlueData.J), AlgebraicGeometry.SheafedSpace.IsOpenImmersion (toGlueData.f i j)} →
          {toGlueData' : CategoryTheory.GlueData (AlgebraicGeometry.SheafedSpace C)} →
            {f_open' : ∀ (i j : toGlueData'.J), AlgebraicGeometry.SheafedSpace.IsOpenImmersion (toGlueData'.f i j)} →
              { toGlueData := toGlueData, f_open := f_open } = { toGlueData := toGlueData', f_open := f_open' } →
                (toGlueData ≍ toGlueData' → P) → P

Defined in

Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Cited by

1 results in Mathlib

Foundations

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