AlgebraicGeometry.Scheme.Pullback.v.proof_1
theorem AlgebraicGeometry.Scheme.Pullback.v.proof_1 :
∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
[inst : ∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g]
(i j : 𝒰.J),
CategoryTheory.Limits.HasPullback
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (𝒰.map i)) (𝒰.map j)
The theorem `AlgebraicGeometry.Scheme.Pullback.v.proof_1` states that, given schemes `X`, `Y`, `Z`, an open cover `𝒰` of `X`, morphisms `f : X ⟶ Z` and `g : Y ⟶ Z`, and for all `i` in `𝒰.J` if the pullback of the composition of `𝒰.map i` and `f` with `g` exists, then for any `i, j` in `𝒰.J`, the pullback of the composition of the first projection of the pullback of `f` and `g` and `𝒰.map i` with `𝒰.map j` also exists. Essentially, this theorem relates the pullback of certain morphisms with the pullbacks of related compositions and is a part of the algebraic geometry theory in the context of scheme theory.
More concisely: Given schemes X, Y, Z, an open cover 𝒰 of X, morphisms f : X ⟶ Z and g : Y ⟶ Z, if for all i in 𝒰.J, the pullback of the composition of 𝒰.map i ∘ f and g exists, then the pullback of the composition of the first projection of the pullback of f and g with 𝒰.map i and 𝒰.map j exists for all i, j in 𝒰.J.
|
AlgebraicGeometry.Scheme.Pullback.lift_comp_ι
theorem AlgebraicGeometry.Scheme.Pullback.lift_comp_ι :
∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
[inst : ∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g]
(i : 𝒰.J),
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.pullback.lift CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst
(AlgebraicGeometry.Scheme.Pullback.p2 𝒰 f g))
⋯)
((AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).ι i) =
CategoryTheory.Limits.pullback.fst
This theorem demonstrates that the map from `W ×[X] Uᵢ ⟶ Uᵢ ×[Z] Y ⟶ W` is equivalent to the first projection. Here, the first mapping is defined by the lift of `W ×[X] Uᵢ ⟶ Uᵢ` and `W ×[X] Uᵢ ⟶ W ⟶ Y`. The proof is completed by showing that both maps agree when restricted onto `Uⱼ ×[Z] Y`. In this case, both maps factor through `V j i` via `pullback_fst_ι_to_V`. The proof utilizes aspects of category theory, specifically pullbacks and composition of morphisms. In essence, the theorem relates the lift of a map to the pullback, showing that they lead to the same result under certain conditions.
More concisely: The map obtained by lifting `W ×[X] Uᵢ ⟶ Uᵢ` and composing with the first projection `Uᵢ ×[Z] Y ⟶ W` is equivalent to the first projection of `W ×[X] Uᵢ ⟶ Uᵢ ×[Z] Y`, under the given conditions.
|
AlgebraicGeometry.Scheme.Pullback.p_comm
theorem AlgebraicGeometry.Scheme.Pullback.p_comm :
∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
[inst : ∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g],
CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) f =
CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.p2 𝒰 f g) g
This theorem, `AlgebraicGeometry.Scheme.Pullback.p_comm`, states that for any three schemes `X`, `Y`, and `Z` in algebraic geometry, an open cover `𝒰` of `X`, and morphisms `f : X ⟶ Z` and `g : Y ⟶ Z`, if for every index `i` in `𝒰.J` we have a pullback of the composite of the map `𝒰.map i` with `f` and `g`, then the composition of the first projection `AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g` with `f` equals the composition of the second projection `AlgebraicGeometry.Scheme.Pullback.p2 𝒰 f g` with `g`. In effect, this theorem asserts the commutativity of the pullback square in the context of schemes in algebraic geometry.
More concisely: Given schemes X, Y, Z, an open cover 𝒰 of X, and morphisms f : X ⟶ Z and g : Y ⟶ Z, if the pullback squares commute for all i in 𝒰.J, then the diagram commutes: f ∘ AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g = g ∘ AlgebraicGeometry.Scheme.Pullback.p2 𝒰 f g.
|