AlgebraicGeometry.Scheme.OpenCover.fromGlued.proof_2
theorem AlgebraicGeometry.Scheme.OpenCover.fromGlued.proof_2 :
∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (a : 𝒰.gluedCover.diagram.L),
CategoryTheory.CategoryStruct.comp (𝒰.gluedCover.diagram.fst a) (𝒰.map (𝒰.gluedCover.diagram.fstFrom a)) =
CategoryTheory.CategoryStruct.comp (𝒰.gluedCover.diagram.snd a) (𝒰.map (𝒰.gluedCover.diagram.sndFrom a))
This theorem states that for any Algebraic Geometry Scheme `X` and any open cover `𝒰` of `X`, and for any pair `(i, j)` in the indexing category of the diagram formed by the glued cover of `𝒰`, the composition of the first morphism from `(i, j)` and the map of `𝒰` from `i` is equal to the composition of the second morphism from `(i, j)` and the map of `𝒰` from `j`. This is a property of the glueing process in the construction of the co-limit in category theory, which is an important concept in the theory of schemes in algebraic geometry.
More concisely: For any AlgebraicGeometry Scheme X and open cover U, and for any pair (i, j) in the indexing category of its glued cover, the composition of the first morphism from (i, j) and the map of U from i is equal to the composition of the second morphism from (i, j) and the map of U from j.
|
AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'_snd_snd
theorem AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'_snd_snd :
∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.J),
CategoryTheory.CategoryStruct.comp (𝒰.gluedCoverT' x y z)
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd) =
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst
The theorem `AlgebraicGeometry.Scheme.OpenCover.gluedCoverT'_snd_snd` states that for any algebraic scheme `X`, given an open cover `𝒰` of `X` and three elements `x`, `y`, `z` from the indexing set of the open cover, the composition of morphisms `gluedCoverT' 𝒰 x y z` and the composition of two `pullback.snd` is equal to the composition of two `pullback.fst`. In the language of category theory, this theorem relates to the commutativity of a certain diagram involving pullbacks in the category of algebraic schemes.
More concisely: For any algebraic scheme X, open cover 𝒰, and indices i, j, k from its indexing set, the diagram commutes: (gluedCoverT' 𝒰 i j k).pullback.snd ∘ (pullback.fst i).pullback.snd = pullback.fst i ∘ pullback.fst j.
In other words, the composition of the second projections through the pullbacks along the open cover elements i, j, and k is equal to the composition of the first projections.
|
AlgebraicGeometry.Scheme.OpenCover.ι_fromGlued
theorem AlgebraicGeometry.Scheme.OpenCover.ι_fromGlued :
∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.J),
CategoryTheory.CategoryStruct.comp (𝒰.gluedCover.ι x) 𝒰.fromGlued = 𝒰.map x
The theorem `AlgebraicGeometry.Scheme.OpenCover.ι_fromGlued` states that for any algebraic scheme `X` and any open cover `𝒰` of `X`, the composition of the immersion of `𝒰.J` into the glued scheme and the canonical morphism from the glued scheme to `X` is equal to the map of `𝒰.J` in the open cover `𝒰`. In other words, this theorem ensures the compatibility of local descriptions (given by `𝒰.map x`) with the global gluing construction, which is a crucial property in the theory of algebraic geometry.
More concisely: The composition of the immersion of an open cover's joint open subset into the glued scheme and the canonical morphism from the glued scheme to the original algebraic scheme is equal to the map of the joint open subset in the open cover.
|