Mathlib Map

Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Cover.RelativeGluingData.functor

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

The schemes Xᵢ.

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

Around this declaration

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

AlgebraicGeometry.Scheme.Hom.normalizationDesc · cited by 10Hom.normalizationDescAlgebraicGeometry.Scheme.Cover.RelativeGluingData.natTrans · cited by 8RelativeGluingData.natTra…AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase · cited by 8RelativeGluingData.toBaseAlgebraicGeometry.Scheme.Cover.RelativeGluingData.glued · cited by 7RelativeGluingData.gluedAlgebraicGeometry.Scheme.Hom.normalizationDesc_comp · cited by 5Hom.normalizationDesc_compAlgebraicGeometry.Scheme.Cover.RelativeGluingData.ι_toBase · cited by 4RelativeGluingData.ι_toBa…AlgebraicGeometry.Scheme.Cover.ColimitGluingData.gluedCocone · cited by 4ColimitGluingData.gluedCo…AlgebraicGeometry.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.AffineZariskiSite.opensRange_relativeGluingData_map · cited by 1AffineZariskiSite.opensRa…AlgebraicGeometry.Scheme.Hom.fromNormalization_preimage · cited by 1Hom.fromNormalization_pre…AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι · cited by 1ColimitGluingData.fst_glu…AlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover_f · cited by 1RelativeGluingData.cover_fAlgebraicGeometry.Scheme.Cover.RelativeGluingData.equifibered · cited by 1RelativeGluingData.equifi…CategoryTheory.Category · cited by 32673CategoryTheory.CategoryCategoryTheory.Functor · cited by 16252CategoryTheory.FunctorAlgebraicGeometry.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…AlgebraicGeometry.Scheme.precoverage · cited by 336Scheme.precoverageAlgebraicGeometry.Scheme.OpenCover · cited by 207Scheme.OpenCoverAlgebraicGeometry.Scheme.Cover.LocallyDirected · cited by 63Cover.LocallyDirectedAlgebraicGeometry.Scheme.Cover.RelativeGluingData · cited by 12Cover.RelativeGluingDataRelativeGluingData.functorCITED BYCITES

Cites10

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

Cited by25

Results whose statement or proof uses this declaration.