Inverse limits of schemes with affine transition maps

In this file, we develop API for inverse limits of schemes with affine transition maps, following EGA IV 8 and https://stacks.math.columbia.edu/tag/01YT.

theorem AlgebraicGeometry.Scheme.nonempty_of_isLimit {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I Scheme) (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofilteredOrEmpty I] [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] [∀ (i : I), Nonempty ↥(D.obj i)] [∀ (i : I), CompactSpace ↥(D.obj i)] : Nonempty ↥c.pt

Suppose we have a cofiltered diagram of nonempty quasi-compact schemes, whose transition maps are affine. Then the limit is also nonempty.

theorem AlgebraicGeometry.exists_mem_of_isClosed_of_nonempty {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I Scheme) (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofilteredOrEmpty I] [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] (Z : (i : I) → Set ↥(D.obj i)) (hZc : ∀ (i : I), IsClosed (Z i)) (hZne : ∀ (i : I), (Z i).Nonempty) (hZcpt : ∀ (i : I), IsCompact (Z i)) (hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom (D.map f).base)) (Z i) (Z i')) : ∃ (s : ↥c.pt), ∀ (i : I), (CategoryTheory.ConcreteCategory.hom (c.π.app i).base) s ∈ Z i

Suppose we have a cofiltered diagram of schemes whose transition maps are affine. The limit of a family of compatible nonempty quasicompact closed sets in the diagram is also nonempty.

theorem AlgebraicGeometry.exists_mem_of_isClosed_of_nonempty' {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I Scheme) (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofilteredOrEmpty I] [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] {j : I} (Z : (i : I) → (i ⟶ j) → Set ↥(D.obj i)) (hZc : ∀ (i : I) (hij : i ⟶ j), IsClosed (Z i hij)) (hZne : ∀ (i : I) (hij : i ⟶ j), (Z i hij).Nonempty) (hZcpt : ∀ (i : I) (hij : i ⟶ j), IsCompact (Z i hij)) (hstab : ∀ (i i' : I) (hi'i : i' ⟶ i) (hij : i ⟶ j), Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom (D.map hi'i).base)) (Z i' (CategoryTheory.CategoryStruct.comp hi'i hij)) (Z i hij)) : ∃ (s : ↥c.pt), ∀ (i : I) (hij : i ⟶ j), (CategoryTheory.ConcreteCategory.hom (c.π.app i).base) s ∈ Z i hij

A variant of exists_mem_of_isClosed_of_nonempty where the closed sets are only defined for the objects over a given j : I.

theorem AlgebraicGeometry.exists_map_eq_top {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I Scheme) (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I] [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] [∀ (i : I), CompactSpace ↥(D.obj i)] {i : I} (U : (D.obj i).Opens) (hU : (TopologicalSpace.Opens.map (c.π.app i).base).obj U = ⊤) : ∃ (j : I) (fji : j ⟶ i), (TopologicalSpace.Opens.map (D.map fji).base).obj U = ⊤

Let { Dᵢ } be a cofiltered diagram of compact schemes with affine transition maps. If U ⊆ Dⱼ contains the image of limᵢ Dᵢ ⟶ Dⱼ, then it contains the image of some Dₖ ⟶ Dⱼ.

noncomputable def AlgebraicGeometry.opensDiagram {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I Scheme) (i : I) (U : (D.obj i).Opens) : CategoryTheory.Functor (CategoryTheory.Over i) Scheme

Given a diagram { Dᵢ } of schemes and a open U ⊆ Dᵢ, this is the diagram of { Dⱼᵢ⁻¹ U }_{j ≤ i}.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.opensDiagram_map {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I Scheme) (i : I) (U : (D.obj i).Opens) {j k : CategoryTheory.Over i} (f : j ⟶ k) : (opensDiagram D i U).map f = Scheme.Hom.resLE (D.map f.left) ((TopologicalSpace.Opens.map (D.map k.hom).base).obj U) ((TopologicalSpace.Opens.map (D.map j.hom).base).obj U) ⋯

@[simp]

theorem AlgebraicGeometry.opensDiagram_obj {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I Scheme) (i : I) (U : (D.obj i).Opens) (j : CategoryTheory.Over i) : (opensDiagram D i U).obj j = ↑((TopologicalSpace.Opens.map (D.map j.hom).base).obj U)

noncomputable def AlgebraicGeometry.opensDiagramι {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I Scheme) (i : I) (U : (D.obj i).Opens) : opensDiagram D i U ⟶ (CategoryTheory.Over.forget i).comp D

The map Dⱼᵢ⁻¹ U ⟶ Dᵢ from the restricted diagram to the original diagram.

Equations

• AlgebraicGeometry.opensDiagramι D i U = { app := fun (j : CategoryTheory.Over i) => ((TopologicalSpace.Opens.map (D.map j.hom).base).obj U).ι, naturality := ⋯ }

@[simp]

theorem AlgebraicGeometry.opensDiagramι_app {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I Scheme) (i : I) (U : (D.obj i).Opens) (j : CategoryTheory.Over i) : (opensDiagramι D i U).app j = ((TopologicalSpace.Opens.map (D.map j.hom).base).obj U).ι

instance AlgebraicGeometry.instIsOpenImmersionAppOverSchemeOpensDiagramι {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I Scheme) (i : I) (U : (D.obj i).Opens) (j : CategoryTheory.Over i) : IsOpenImmersion ((opensDiagramι D i U).app j)

noncomputable def AlgebraicGeometry.opensCone {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I Scheme) (c : CategoryTheory.Limits.Cone D) (i : I) (U : (D.obj i).Opens) : CategoryTheory.Limits.Cone (opensDiagram D i U)

Given a diagram { Dᵢ } of schemes and a open U ⊆ Dᵢ, the preimage of U ⊆ Dᵢ under the map lim Dᵢ ⟶ Dᵢ is the limit of { Dⱼᵢ⁻¹ U }_{j ≤ i}. This is the underlying cone, and it is limiting as witnessed by isLimitOpensCone below.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.opensCone_π_app {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I Scheme) (c : CategoryTheory.Limits.Cone D) (i : I) (U : (D.obj i).Opens) (j : CategoryTheory.Over i) : (opensCone D c i U).π.app j = Scheme.Hom.resLE (c.π.app j.left) ((TopologicalSpace.Opens.map (D.map j.hom).base).obj U) ((TopologicalSpace.Opens.map (c.π.app i).base).obj U) ⋯

@[simp]

theorem AlgebraicGeometry.opensCone_pt {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I Scheme) (c : CategoryTheory.Limits.Cone D) (i : I) (U : (D.obj i).Opens) : (opensCone D c i U).pt = ↑((TopologicalSpace.Opens.map (c.π.app i).base).obj U)

noncomputable def AlgebraicGeometry.isLimitOpensCone {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I Scheme) (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I] (i : I) (U : (D.obj i).Opens) : CategoryTheory.Limits.IsLimit (opensCone D c i U)

Given a diagram { Dᵢ }_{i ∈ I} of schemes and a open U ⊆ Dᵢ, the preimage of U ⊆ Dᵢ under the map lim Dᵢ ⟶ Dᵢ is the limit of { Dⱼᵢ⁻¹ U }_{j ≤ i}.

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.instIsAffineHomMapOverSchemeOpensDiagram {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I Scheme) [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] {i : I} (U : (D.obj i).Opens) {j k : CategoryTheory.Over i} (f : j ⟶ k) : IsAffineHom ((opensDiagram D i U).map f)

theorem AlgebraicGeometry.isAffineHom_π_app {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I Scheme) (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I] [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] (i : I) : IsAffineHom (c.π.app i)

theorem AlgebraicGeometry.Scheme.compactSpace_of_isLimit {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I Scheme) (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I] [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] [∀ (i : I), CompactSpace ↥(D.obj i)] : CompactSpace ↥c.pt

Cofiltered Limits and Schemes of Finite Type

Given a cofiltered diagram D of quasi-compact S-schemes with affine transition maps, and another scheme X of finite type over S. Then the canonical map colim Homₛ(Dᵢ, X) ⟶ Homₛ(lim Dᵢ, X) is injective. In other words, for each pair of a : Homₛ(Dᵢ, X) and b : Homₛ(Dⱼ, X) that give rise to the same map Homₛ(lim Dᵢ, X), there exists a k with fᵢ : k ⟶ i and fⱼ : k ⟶ j such that D(fᵢ) ≫ a = D(fⱼ) ≫ b. This results is formalized in Scheme.exists_hom_hom_comp_eq_comp_of_locallyOfFiniteType.

We first reduce to the case i = j, and the goal is to reduce to the case where X and S are affine, where the result follows from commutative algebra.

To achieve this, we show that there exists some i₀ ⟶ i such that for each x, a x and b x are contained in the same component (i.e. given an open cover 𝒰ₛ of S, and 𝒰ₓ of X refining 𝒰ₛ, the range of x ↦ (a x, b x) falls in the diagonal part ⋃ᵢⱼ 𝒰ₓⱼ ×[𝒰ₛᵢ] 𝒰ₓⱼ). Then we may restrict to the sub-diagram over i₀ (which is cofinal because D is cofiltered), and check locally on X, reducing to the affine case.

For the actual implementation, we wrap i, a, b, the limit cone lim Dᵢ, and open covers of X and S into a structure ExistsHomHomCompEqCompAux for convenience.

See the injective part of (1) => (3) of https://stacks.math.columbia.edu/tag/01ZC.

structure AlgebraicGeometry.ExistsHomHomCompEqCompAux {I : Type u} [CategoryTheory.Category.{u, u} I] {S X : Scheme} (D : CategoryTheory.Functor I Scheme) (t : D ⟶ (CategoryTheory.Functor.const I).obj S) (f : X ⟶ S) : Type (u + 1)

(Implementation) An auxiliary structure used to prove Scheme.exists_hom_hom_comp_eq_comp_of_locallyOfFiniteType. See the section docstring.

• c : CategoryTheory.Limits.Cone D

  (Implementation) The limit cone. See the section docstring.

• hc : CategoryTheory.Limits.IsLimit self.c

  (Implementation) The limit cone is a limit. See the section docstring.

• i : I

  (Implementation) The index on which a and b lives. See the section docstring.

• a : D.obj self.i ⟶ X

  (Implementation) a. See the section docstring.

• ha : t.app self.i = CategoryTheory.CategoryStruct.comp self.a f
• b : D.obj self.i ⟶ X

  (Implementation) b. See the section docstring.

• hb : t.app self.i = CategoryTheory.CategoryStruct.comp self.b f
• hab : CategoryTheory.CategoryStruct.comp (self.c.π.app self.i) self.a = CategoryTheory.CategoryStruct.comp (self.c.π.app self.i) self.b
• 𝒰S : S.OpenCover

  (Implementation) An open cover on S. See the section docstring.

• h𝒰S (i : self.𝒰S.I₀) : IsAffine (self.𝒰S.X i)
• 𝒰X (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f self.𝒰S).I₀) : ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f self.𝒰S).X i).OpenCover

  (Implementation) A family of open covers refining 𝒰S. See the section docstring.

• h𝒰X (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f self.𝒰S).I₀) (j : (self.𝒰X i).I₀) : IsAffine ((self.𝒰X i).X j)

theorem AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_index {I : Type u} [CategoryTheory.Category.{u, u} I] {S X : Scheme} {D : CategoryTheory.Functor I Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S} [∀ (i : I), CompactSpace ↥(D.obj i)] [CategoryTheory.IsCofiltered I] [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] (A : ExistsHomHomCompEqCompAux D t f) : ∃ (i' : I) (hii' : i' ⟶ A.i), ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (D.map hii') (CategoryTheory.Limits.pullback.lift A.a A.b ⋯)).base) ⁻¹' (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X))ᶜ = ∅

def AlgebraicGeometry.ExistsHomHomCompEqCompAux.i' {I : Type u} [CategoryTheory.Category.{u, u} I] {S X : Scheme} {D : CategoryTheory.Functor I Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S} [∀ (i : I), CompactSpace ↥(D.obj i)] [CategoryTheory.IsCofiltered I] [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] (A : ExistsHomHomCompEqCompAux D t f) : I

(Implementation) The index i' such that a and b restricted onto i' maps into the diagonal components. See the section docstring.

Equations

• A.i' = ⋯.choose

def AlgebraicGeometry.ExistsHomHomCompEqCompAux.hii' {I : Type u} [CategoryTheory.Category.{u, u} I] {S X : Scheme} {D : CategoryTheory.Functor I Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S} [∀ (i : I), CompactSpace ↥(D.obj i)] [CategoryTheory.IsCofiltered I] [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] (A : ExistsHomHomCompEqCompAux D t f) : A.i' ⟶ A.i

(Implementation) The map from i' to i. See the section docstring.

Equations

• A.hii' = ⋯.choose

def AlgebraicGeometry.ExistsHomHomCompEqCompAux.g {I : Type u} [CategoryTheory.Category.{u, u} I] {S X : Scheme} {D : CategoryTheory.Functor I Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S} [∀ (i : I), CompactSpace ↥(D.obj i)] [CategoryTheory.IsCofiltered I] [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] (A : ExistsHomHomCompEqCompAux D t f) : D.obj A.i' ⟶ CategoryTheory.Limits.pullback f f

(Implementation) The map sending x to (a x, b x), which should fall in the diagonal component. See the section docstring.

Equations

• A.g = CategoryTheory.CategoryStruct.comp (D.map A.hii') (CategoryTheory.Limits.pullback.lift A.a A.b ⋯)

theorem AlgebraicGeometry.ExistsHomHomCompEqCompAux.range_g_subset {I : Type u} [CategoryTheory.Category.{u, u} I] {S X : Scheme} {D : CategoryTheory.Functor I Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S} [∀ (i : I), CompactSpace ↥(D.obj i)] [CategoryTheory.IsCofiltered I] [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] (A : ExistsHomHomCompEqCompAux D t f) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom A.g.base) ⊆ ↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X)

noncomputable def AlgebraicGeometry.ExistsHomHomCompEqCompAux.𝒰D₀ {I : Type u} [CategoryTheory.Category.{u, u} I] {S X : Scheme} {D : CategoryTheory.Functor I Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S} [∀ (i : I), CompactSpace ↥(D.obj i)] [CategoryTheory.IsCofiltered I] [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] (A : ExistsHomHomCompEqCompAux D t f) : (D.obj A.i').OpenCover

(Implementation) The covering of D(i') by the pullback of the diagonal components of X ×ₛ X. See the section docstring.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.ExistsHomHomCompEqCompAux.𝒰D {I : Type u} [CategoryTheory.Category.{u, u} I] {S X : Scheme} {D : CategoryTheory.Functor I Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S} [∀ (i : I), CompactSpace ↥(D.obj i)] [CategoryTheory.IsCofiltered I] [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] (A : ExistsHomHomCompEqCompAux D t f) : (D.obj A.i').OpenCover

(Implementation) An affine open cover refining 𝒰D₀. See the section docstring.

Equations

• A.𝒰D = CategoryTheory.Precoverage.ZeroHypercover.bind A.𝒰D₀ fun (x : A.𝒰D₀.I₀) => (A.𝒰D₀.X x).affineCover

def AlgebraicGeometry.ExistsHomHomCompEqCompAux.D' {I : Type u} [CategoryTheory.Category.{u, u} I] {S X : Scheme} {D : CategoryTheory.Functor I Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S} [∀ (i : I), CompactSpace ↥(D.obj i)] [CategoryTheory.IsCofiltered I] [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] (A : ExistsHomHomCompEqCompAux D t f) (j : A.𝒰D.I₀) : CategoryTheory.Functor (CategoryTheory.Over A.i') Scheme

(Implementation) The diagram restricted to Over i'. See the section docstring.

Equations

• A.D' j = (CategoryTheory.Over.post D).comp ((CategoryTheory.Over.pullback (A.𝒰D.f j)).comp (CategoryTheory.Over.forget (A.𝒰D.X j)))

def AlgebraicGeometry.ExistsHomHomCompEqCompAux.c' {I : Type u} [CategoryTheory.Category.{u, u} I] {S X : Scheme} {D : CategoryTheory.Functor I Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S} [∀ (i : I), CompactSpace ↥(D.obj i)] [CategoryTheory.IsCofiltered I] [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] (A : ExistsHomHomCompEqCompAux D t f) (j : A.𝒰D.I₀) : CategoryTheory.Limits.Cone (A.D' j)

(Implementation) The limit cone restricted to Over i'. See the section docstring.

Equations

• A.c' j = ((CategoryTheory.Over.pullback (A.𝒰D.f j)).comp (CategoryTheory.Over.forget (A.𝒰D.X j))).mapCone ((CategoryTheory.Over.conePost D A.i').obj A.c)

def AlgebraicGeometry.ExistsHomHomCompEqCompAux.hc' {I : Type u} [CategoryTheory.Category.{u, u} I] {S X : Scheme} {D : CategoryTheory.Functor I Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S} [∀ (i : I), CompactSpace ↥(D.obj i)] [CategoryTheory.IsCofiltered I] [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] (A : ExistsHomHomCompEqCompAux D t f) (j : A.𝒰D.I₀) : CategoryTheory.Limits.IsLimit (A.c' j)

(Implementation) The limit cone restricted to Over i' is still a limit because the diagram is cofiltered. See the section docstring.

Equations

• A.hc' j = CategoryTheory.Limits.isLimitOfPreserves ((CategoryTheory.Over.pullback (A.𝒰D.f j)).comp (CategoryTheory.Over.forget (A.𝒰D.X j))) (CategoryTheory.Over.isLimitConePost A.i' A.hc)

theorem AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_eq {I : Type u} [CategoryTheory.Category.{u, u} I] {S X : Scheme} {D : CategoryTheory.Functor I Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S} [∀ (i : I), CompactSpace ↥(D.obj i)] [LocallyOfFiniteType f] [CategoryTheory.IsCofiltered I] [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] (A : ExistsHomHomCompEqCompAux D t f) [∀ (i : I), IsAffineHom (A.c.π.app i)] (j : A.𝒰D.I₀) : ∃ (k : I) (hki' : k ⟶ A.i'), CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ (D.map hki') A.𝒰D).f j) (CategoryTheory.CategoryStruct.comp (D.map (CategoryTheory.CategoryStruct.comp hki' A.hii')) A.a) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ (D.map hki') A.𝒰D).f j) (CategoryTheory.CategoryStruct.comp (D.map (CategoryTheory.CategoryStruct.comp hki' A.hii')) A.b)

theorem AlgebraicGeometry.Scheme.exists_hom_hom_comp_eq_comp_of_locallyOfFiniteType {I : Type u} [CategoryTheory.Category.{u, u} I] {S X : Scheme} (D : CategoryTheory.Functor I Scheme) (t : D ⟶ (CategoryTheory.Functor.const I).obj S) (f : X ⟶ S) (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : I), CompactSpace ↥(D.obj i)] [LocallyOfFiniteType f] [CategoryTheory.IsCofiltered I] [∀ (i : I), IsAffineHom (c.π.app i)] [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] {i : I} (a : D.obj i ⟶ X) (ha : t.app i = CategoryTheory.CategoryStruct.comp a f) {j : I} (b : D.obj j ⟶ X) (hb : t.app j = CategoryTheory.CategoryStruct.comp b f) (hab : CategoryTheory.CategoryStruct.comp (c.π.app i) a = CategoryTheory.CategoryStruct.comp (c.π.app j) b) : ∃ (k : I) (hik : k ⟶ i) (hjk : k ⟶ j), CategoryTheory.CategoryStruct.comp (D.map hik) a = CategoryTheory.CategoryStruct.comp (D.map hjk) b

Given a cofiltered diagram D of quasi-compact S-schemes with affine transition maps, and another scheme X of finite type over S. Then the canonical map colim Homₛ(Dᵢ, X) ⟶ Homₛ(lim Dᵢ, X) is injective.

In other words, for each pair of a : Homₛ(Dᵢ, X) and b : Homₛ(Dⱼ, X) that give rise to the same map Homₛ(lim Dᵢ, X), there exists a k with fᵢ : k ⟶ i and fⱼ : k ⟶ j such that D(fᵢ) ≫ a = D(fⱼ) ≫ b.

Sections of the limit

Let D be a cofiltered diagram schemes with affine transition map. Consider the canonical map colim Γ(Dᵢ, ⊤) ⟶ Γ(lim Dᵢ, ⊤).

If D consists of quasicompact schemes, then this map is injective. More generally, we show that if s t : Γ(Dᵢ, U) have equal image in lim Dᵢ, then they are equal at some Γ(Dⱼ, Dⱼᵢ⁻¹U). See AlgebraicGeometry.exists_app_map_eq_map_of_isLimit.

If D consists of qcqs schemes, then this map is surjective. Specifically, we show that any s : Γ(lim Dᵢ, ⊤) comes from Γ(Dᵢ, ⊤) for some i. See AlgebraicGeometry.exists_appTop_π_eq_of_isLimit.

These two results imply that PreservesLimit D Scheme.Γ.rightOp, which is available as an instance.

theorem AlgebraicGeometry.exists_appTop_map_eq_zero_of_isAffine_of_isLimit {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I Scheme) (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I] [∀ (i : I), IsAffine (D.obj i)] (i : I) (s : ↑((D.obj i).presheaf.obj (Opposite.op ⊤))) (hs : (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0) : ∃ (j : I) (f : j ⟶ i), (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop (D.map f))) s = 0

theorem AlgebraicGeometry.exists_appTop_map_eq_zero_of_isLimit {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I Scheme) (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I] [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] {i : I} [CompactSpace ↥(D.obj i)] (s : ↑((D.obj i).presheaf.obj (Opposite.op ⊤))) (hs : (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0) : ∃ (j : I) (f : j ⟶ i), (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop (D.map f))) s = 0

theorem AlgebraicGeometry.exists_app_map_eq_zero_of_isLimit {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I Scheme) (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I] [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] {i : I} {U : (D.obj i).Opens} (hU : IsCompact ↑U) (s : ↑((D.obj i).presheaf.obj (Opposite.op U))) (hs : (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.app (c.π.app i) U)) s = 0) : ∃ (j : I) (f : j ⟶ i), (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.app (D.map f) U)) s = 0

theorem AlgebraicGeometry.exists_app_map_eq_map_of_isLimit {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I Scheme) (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I] [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] {i : I} {U : (D.obj i).Opens} (hU : IsCompact ↑U) (s t : ↑((D.obj i).presheaf.obj (Opposite.op U))) (hs : (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.app (c.π.app i) U)) s = (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.app (c.π.app i) U)) t) : ∃ (j : I) (f : j ⟶ i), (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.app (D.map f) U)) s = (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.app (D.map f) U)) t

theorem AlgebraicGeometry.exists_appTop_π_eq_of_isAffine_of_isLimit {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I Scheme) (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I] [∀ (i : I), IsAffine (D.obj i)] (s : ↑(c.pt.presheaf.obj (Opposite.op ⊤))) : ∃ (i : I) (t : ↑((D.obj i).presheaf.obj (Opposite.op ⊤))), (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) t = s

theorem AlgebraicGeometry.exists_appTop_π_eq_of_isLimit {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I Scheme) (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I] [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] (s : ↑(c.pt.presheaf.obj (Opposite.op ⊤))) [∀ (i : I), CompactSpace ↥(D.obj i)] [∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)] : ∃ (i : I) (t : ↑((D.obj i).presheaf.obj (Opposite.op ⊤))), s = (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) t

theorem AlgebraicGeometry.nonempty_isColimit_Γ_mapCocone {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I Scheme) (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I] [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] [∀ (i : I), CompactSpace ↥(D.obj i)] [∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)] : Nonempty (CategoryTheory.Limits.IsColimit (Scheme.Γ.mapCocone c.op))

instance AlgebraicGeometry.instPreservesLimitSchemeOppositeCommRingCatRightOpΓOfIsAffineHomMapOfCompactSpaceOfQuasiSeparatedSpaceCarrierCarrierObj {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I Scheme) [CategoryTheory.IsCofiltered I] [∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)] [∀ (i : I), CompactSpace ↥(D.obj i)] [∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)] : CategoryTheory.Limits.PreservesLimit D Scheme.Γ.rightOp