Theorems · Theorem · algebraic geometry

AlgebraicGeometry.SheafedSpace.GlueData.mk.inj

∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  {toGlueData : CategoryTheory.GlueData (AlgebraicGeometry.SheafedSpace C)}
  {f_open : ∀ (i j : toGlueData.J), AlgebraicGeometry.SheafedSpace.IsOpenImmersion (toGlueData.f i j)}
  {toGlueData_1 : CategoryTheory.GlueData (AlgebraicGeometry.SheafedSpace C)}
  {f_open_1 : ∀ (i j : toGlueData_1.J), AlgebraicGeometry.SheafedSpace.IsOpenImmersion (toGlueData_1.f i j)},
  { toGlueData := toGlueData, f_open := f_open } = { toGlueData := toGlueData_1, f_open := f_open_1 } →
    toGlueData = toGlueData_1

Defined in

Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Cited by

1 results in Mathlib

Foundations

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