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.

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.