Theorems · Inductive type · algebraic geometry

AlgebraicGeometry.Scheme.GlueData

Type (u_1 + 1)

A family of gluing data consists of 1. An index type J 2. A scheme U i for each i : J. 3. A scheme V i j for each i j : J. (Note that this is J × J → Scheme rather than J → J → Scheme to connect to the limits library easier.) 4. An open immersion f i j : V i j ⟶ U i for each i j : ι. 5. A transition map t i j : V i j ⟶ V j i for each i j : ι. such that 6. f i i is an isomorphism. 7. t i i is the identity. 8. V i j ×[U i] V i k ⟶ V i j ⟶ V j i factors through V j k ×[U j] V j i ⟶ V j i via some t' : V i j ×[U i] V i k ⟶ V j k ×[U j] V j i. 9. t' i j k ≫ t' j k i ≫ t' k i j = 𝟙 _. We can then glue the schemes U i together by identifying V i j with V j i, such that the U i's are open subschemes of the glued space.

Defined in

Mathlib.AlgebraicGeometry.Gluing

Cited by

23 results in Mathlib

Foundations

Depth 0 from the axioms · uses no axioms