Mathlib Map

Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Cover.RelativeGluingData.glued

{S : AlgebraicGeometry.Scheme} →
  {𝒰 : S.OpenCover} →
    [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] →
      [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
        AlgebraicGeometry.Scheme.Cover.RelativeGluingData 𝒰 →
          [Small.{u, u_1} 𝒰.I₀] → [Quiver.IsThin 𝒰.I₀] → AlgebraicGeometry.Scheme

The glued scheme of a relative gluing datum is the colimit over the Xᵢ. For the structure map, see AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase and the isomorphisms with the preimages AlgebraicGeometry.Scheme.Cover.RelativeGluingData.isPullback_natTrans_ι_toBase.

Defined in
Mathlib.AlgebraicGeometry.RelativeGluing
Cited by
7 results in Mathlib
Foundations
Depth 199 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CategoryTheory.CategoryAlgebraicGeometry.Scheme.Cover.LocallyDirectedSmallQuiver.IsThin
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

AlgebraicGeometry.Scheme.Hom.normalization · cited by 41Hom.normalizationAlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase · cited by 8RelativeGluingData.toBaseAlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover · cited by 4RelativeGluingData.coverAlgebraicGeometry.Scheme.Cover.RelativeGluingData.preimage_toBase_eq_range_ι · cited by 2RelativeGluingData.preima…AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase_preimage_eq_opensRange_ι · cited by 2RelativeGluingData.toBase…AlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover_f · cited by 1RelativeGluingData.cover_fAlgebraicGeometry.Scheme.Cover.RelativeGluingData.isPullback_natTrans_ι_toBase · cited by 0RelativeGluingData.isPull…AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.colimitDesc_preimage · cited by 0PreservesLocalization.col…AlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover_I₀ · cited by 0RelativeGluingData.cover_…AlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover_X · cited by 0RelativeGluingData.cover_XCategoryTheory.Category · cited by 32673CategoryTheory.CategoryAlgebraicGeometry.Scheme · cited by 2540AlgebraicGeometry.SchemeCategoryTheory.PreZeroHypercover.I₀ · cited by 763PreZeroHypercover.I₀AlgebraicGeometry.IsOpenImmersion · cited by 476AlgebraicGeometry.IsOpenI…CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover · cited by 469ZeroHypercover.toPreZeroH…CategoryTheory.Limits.colimit · cited by 453Limits.colimitSmall · cited by 369SmallAlgebraicGeometry.Scheme.precoverage · cited by 336Scheme.precoverageAlgebraicGeometry.Scheme.OpenCover · cited by 207Scheme.OpenCoverAlgebraicGeometry.Scheme.Cover.LocallyDirected · cited by 63Cover.LocallyDirectedQuiver.IsThin · cited by 51Quiver.IsThinAlgebraicGeometry.Scheme.Cover.RelativeGluingData.functor · cited by 18RelativeGluingData.functorAlgebraicGeometry.Scheme.Cover.RelativeGluingData · cited by 12Cover.RelativeGluingDataRelativeGluingData.gluedCITED BYCITES

Cites13

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by10

Results whose statement or proof uses this declaration.