3 Set Theory

Chapter 3 of the Stacks Project, Set Theory, Tag 0007: the 7 sections of its 12 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 19 tags are carried by 48 declarations of the repository (all in StacksFrontier) and 1 registered declaration.

Section3.5 The hierarchy of sets#

Section 3.5 of the Stacks Project, Tag 000B. 1 tag here is carried by 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 000C, a lemma

Tag 000C in the Stacks Project.

Declarations registered for the tag:

Sources
LeanZFSet.exists_mem_vonNeumann

Section3.7 Cofinality#

Section 3.7 of the Stacks Project, Tag 000E. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05N2, a lemma

Tag 05N2 in the Stacks Project.

Ordinal.exists_factorization_of_mk_lt_cof, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/SetTheory/Cardinal/Cofinality.lean, line 78.

Stacks 05N2. Let β be an ordinal and (F_α)_{α < β} an ordinal-indexed direct system with colimit DirectLimit F f and canonical maps ι_α : F_α → DirectLimit F f, x ↦ ⟦⟨α, x⟩⟧. Let S be a set and φ : S → DirectLimit F f a function. If the cofinality of β exceeds the cardinality of S, then φ factors through a single stage: there are an α < β and a φ_α : S → F_α with ι_α ∘ φ_α = φ.

theorem exists_factorization_of_mk_lt_cof {β : Ordinal.{u}}
    {F : {α : Ordinal.{u} // α < β} → Type u}
    {T : ∀ ⦃i j : {α : Ordinal.{u} // α < β}⦄, i ≤ j → Sort v}
    (f : ∀ i j (h : i ≤ j), T h)
    [∀ ⦃i j : {α : Ordinal.{u} // α < β}⦄ (h : i ≤ j), FunLike (T h) (F i) (F j)]
    [DirectedSystem F (f · · ·)]
    {S : Type u} (φ : S → DirectLimit F f)
    (hcof : Cardinal.mk S < β.cof) :
    ∃ (i : {α : Ordinal.{u} // α < β}) (φi : S → F i),
      (fun s => (⟦⟨i, φi s⟩⟧ : DirectLimit F f)) = φ
Tag 05N3, a proposition

Tag 05N3 in the Stacks Project.

Cardinal.exists_ordinal_cof_gt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/SetTheory/Cardinal/Cofinality.lean, line 61.

Stacks 05N3. For every cardinal κ there is an ordinal α with κ < cf(α): the successor of the infinite cardinal κ ⊔ ℵ₀ is regular, so the ordinal it indexes has cofinality (κ ⊔ ℵ₀)⁺, which is strictly greater than κ.

theorem exists_ordinal_cof_gt (κ : Cardinal) : ∃ α : Ordinal, κ < α.cof
Sources
LeanOrdinal.exists_factorization_of_mk_lt_cof · Cardinal.exists_ordinal_cof_gt

Section3.8 Reflection principle#

Section 3.8 of the Stacks Project, Tag 000F. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 000G, a theorem

Tag 000G in the Stacks Project.

reflection_principle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/SetTheory/ZFC/Reflection.lean, line 328.

Stacks 000G — Reflection principle. Given a finite family of set-theory formulas φᵢ with n free variables and any set M₀, there is a limit ordinal α such that M₀ ⊆ V_α and for every parameter tuple in V_α and every i, the relativization φᵢ^{V_α} agrees with φᵢ on the full universe. Here V_ α = ZFSet.vonNeumann α is the von Neumann hierarchy from Mathlib.

theorem reflection_principle
    (n m : ℕ) (φ : Fin m → SetFormula n) (M₀ : ZFSet.{u}) :
    ∃ α : Ordinal.{u}, Order.IsSuccLimit α ∧ M₀ ⊆ V_ α ∧
      ∀ (x : Fin n → ZFSet),
        (∀ j, x j ∈ V_ α) →
        ∀ i : Fin m,
          (φ i).realizeIn (V_ α) x ↔ (φ i).realize x
Sources
Leanreflection_principle

Section3.9 Constructing categories of schemes#

Section 3.9 of the Stacks Project, Tag 000H. 11 tags here are carried by 33 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 000I, a lemma

Tag 000I in the Stacks Project.

AlgebraicGeometry.Scheme.size, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/Basic.lean, line 63.

The size of a scheme (Stacks tag 000I, Definition 3.9.2).

The size of a scheme S is the maximum of ℵ₀, the cardinality of the set of affine opens of S, and the supremum over affine opens U ⊆ S of the cardinality of the ring of sections Γ(S, U).

Every Section 3.9 size bound is stated in terms of this one cardinal, so the bounds compose.

noncomputable def Scheme.size (S : Scheme.{u}) : Cardinal.{u}
Tag 046U, an equation

Tag 046U in the Stacks Project.

Cardinal.stacksBound, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/SetTheory/Cardinal/SizeBound.lean, line 42.

Stacks 046U. The bound function Bound(κ) = max {κ ^ ℵ₀, κ⁺} on cardinals. Here Order.succ κ is the cardinal successor κ⁺.

noncomputable def Cardinal.stacksBound (κ : Cardinal) : Cardinal
Tag 000J, a lemma

Tag 000J in the Stacks Project.

AlgebraicGeometry.exists_size_cutoff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/Cutoff.lean, line 82.

For every set S₀ of schemes there is an uncountable strong limit cardinal κ of uncountable cofinality such that every member of S₀ has size below κ, that is, the collection Sch_κ = {S | size S < κ} contains S₀.

theorem exists_size_cutoff (S₀ : Set Scheme.{u}) [Small.{u} S₀] :
    ∃ κ : Cardinal.{u}, ℵ₀ < κ ∧ Cardinal.IsStrongPrelimit κ ∧ ℵ₀ < κ.ord.cof ∧
      ∀ S ∈ S₀, S.size < κ

AlgebraicGeometry.Scheme.size_lt_of_le_stacksBound, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/Cutoff.lean, line 95. The attribute's comment: “(2)”.

If S is an object of Sch_κ and T is a scheme of size at most Bound(size S), then T is an object of Sch_κ.

theorem Scheme.size_lt_of_le_stacksBound {κ : Cardinal.{u}} (hκ : ℵ₀ < κ)
    (hsl : Cardinal.IsStrongPrelimit κ) {S T : Scheme.{u}} (hS : S.size < κ)
    (hT : T.size ≤ Cardinal.stacksBound S.size) : T.size < κ

AlgebraicGeometry.Scheme.size_lt_of_le_stacksBound_iSup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/Cutoff.lean, line 103. The attribute's comment: “(3), (4)”.

Let F be an at most countable family of objects of Sch_κ. Then every scheme of size at most Bound(⨆ i, size (F i)) is an object of Sch_κ.

theorem Scheme.size_lt_of_le_stacksBound_iSup {κ : Cardinal.{u}} (hκ : ℵ₀ < κ)
    (hsl : Cardinal.IsStrongPrelimit κ) (hcof : ℵ₀ < κ.ord.cof) {ι : Type u}
    (hι : #ι ≤ ℵ₀) (F : ι → Scheme.{u}) (hF : ∀ i, (F i).size < κ) {X : Scheme.{u}}
    (hX : X.size ≤ Cardinal.stacksBound (⨆ i, (F i).size)) : X.size < κ
Tag 000P, a lemma

Tag 000P in the Stacks Project.

AlgebraicGeometry.Scheme.size_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/Affine.lean, line 164.

Stacks 000P. Let S be an affine scheme and R = Γ(S, 𝒪_S). Then size S = max ℵ₀ #R.

theorem Scheme.size_of_isAffine (S : Scheme.{u}) [IsAffine S] :
    S.size = max ℵ₀ #Γ(S, ⊤)
Tag 000Q, a lemma

Tag 000Q in the Stacks Project.

AlgebraicGeometry.Scheme.size_le_of_iSup_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/OpenCover.lean, line 250.

If S : I → X.Opens is an open cover of X indexed by a nonempty type I, then size X ≤ max #I (⨆ i, size (S i)).

theorem Scheme.size_le_of_iSup_eq_top {X : Scheme.{u}} {I : Type u} [Nonempty I]
    (S : I → X.Opens) (hcov : ⨆ i, S i = ⊤) :
    Scheme.size X ≤ max #I (⨆ i, Scheme.size (S i : Scheme))
Tag 04T6, a lemma

Tag 04T6 in the Stacks Project.

AlgebraicGeometry.Scheme.size_pullback_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/Pullback.lean, line 365.

Stacks 04T6. The size of a fibre product of schemes is bounded by the maximum of the sizes of the two factors.

theorem Scheme.size_pullback_le {X Y S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S) :
    Scheme.size (pullback f g) ≤ max (Scheme.size X) (Scheme.size Y)
Tag 04T7, a lemma

Tag 04T7 in the Stacks Project.

AlgebraicGeometry.Scheme.size_le_of_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/FiniteType.lean, line 238.

If f : X ⟶ S is locally of finite type and X is quasi-compact, then Scheme.size X ≤ Scheme.size S.

theorem Scheme.size_le_of_locallyOfFiniteType {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] [CompactSpace X] :
    Scheme.size X ≤ Scheme.size S
Tag 04VA, a lemma

Tag 04VA in the Stacks Project.

AlgebraicGeometry.Scheme.size_le_of_mono_quasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/Monomorphism.lean, line 345.

If f : X ⟶ Y is a quasi-compact monomorphism of schemes, then size X ≤ size Y.

theorem Scheme.size_le_of_mono_quasiCompact
    {X Y : Scheme.{u}} (f : X ⟶ Y) [Mono f] [QuasiCompact f] :
    X.size ≤ Y.size

AlgebraicGeometry.Scheme.size_le_of_mono_locallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/Monomorphism.lean, line 356.

If f : X ⟶ Y is a monomorphism of schemes which is locally of finite presentation, then size X ≤ size Y.

theorem Scheme.size_le_of_mono_locallyOfFinitePresentation
    {X Y : Scheme.{u}} (f : X ⟶ Y) [Mono f] [LocallyOfFinitePresentation f] :
    X.size ≤ Y.size
Tag 000R, a lemma

Tag 000R in the Stacks Project.

AlgebraicGeometry.Scheme.size_pullback_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/Cutoff.lean, line 123. The attribute's comment: “(1)”.

The fibre product of two objects of Sch_κ over any base, which need not lie in Sch_κ, is again an object of Sch_κ.

theorem Scheme.size_pullback_lt {X Y S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S)
    (hX : X.size < κ) (hY : Y.size < κ) : (pullback f g).size < κ

AlgebraicGeometry.Scheme.size_sigmaObj_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/Cutoff.lean, line 132. The attribute's comment: “(2)”.

If κ is uncountable of uncountable cofinality, the coproduct of an at most countable family of objects of Sch_κ is again an object of Sch_κ.

theorem Scheme.size_sigmaObj_lt (hκ : ℵ₀ < κ) (hcof : ℵ₀ < κ.ord.cof) {ι : Type u}
    (hι : #ι ≤ ℵ₀) (Y : ι → Scheme.{u}) (hY : ∀ i, (Y i).size < κ) : (∐ Y).size < κ

AlgebraicGeometry.Scheme.size_lt_of_mono_quasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/Cutoff.lean, line 150. The attribute's comment: “(8)”.

The source of a quasi-compact monomorphism into an object of Sch_κ is an object of Sch_κ.

theorem Scheme.size_lt_of_mono_quasiCompact {X Y : Scheme.{u}} (f : X ⟶ Y) [Mono f]
    [QuasiCompact f] (hY : Y.size < κ) : X.size < κ

AlgebraicGeometry.Scheme.size_lt_of_mono_locallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/Cutoff.lean, line 157. The attribute's comment: “(8)”.

The source of a monomorphism locally of finite presentation into an object of Sch_κ is an object of Sch_κ.

theorem Scheme.size_lt_of_mono_locallyOfFinitePresentation {X Y : Scheme.{u}} (f : X ⟶ Y)
    [Mono f] [LocallyOfFinitePresentation f] (hY : Y.size < κ) : X.size < κ

AlgebraicGeometry.Scheme.size_lt_of_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/Cutoff.lean, line 163. The attribute's comment: “(3)”.

The source of an open immersion into an object of Sch_κ is an object of Sch_κ.

theorem Scheme.size_lt_of_isOpenImmersion {U S : Scheme.{u}} (f : U ⟶ S)
    [IsOpenImmersion f] (hS : S.size < κ) : U.size < κ

AlgebraicGeometry.Scheme.size_lt_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/Cutoff.lean, line 169. The attribute's comment: “(4)”.

The source of a closed immersion into an object of Sch_κ is an object of Sch_κ.

theorem Scheme.size_lt_of_isClosedImmersion {T S : Scheme.{u}} (f : T ⟶ S)
    [IsClosedImmersion f] (hS : S.size < κ) : T.size < κ

AlgebraicGeometry.Scheme.size_lt_of_openCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/Cutoff.lean, line 179. The attribute's comment: “(6)”.

Let S be a scheme with an open covering S = ⋃ i, U i and let T be an object of Sch_κ such that the index type and every member of the covering are bounded by size(T) ^ ℵ₀. Then S is an object of Sch_κ.

theorem Scheme.size_lt_of_openCover (hκ : ℵ₀ < κ) (hsl : Cardinal.IsStrongPrelimit κ)
    {S : Scheme.{u}} {I : Type u} [Nonempty I] (U : I → S.Opens) (hcov : ⨆ i, U i = ⊤)
    {T : Scheme.{u}} (hT : T.size < κ) (hI : #I ≤ T.size ^ ℵ₀)
    (hU : ∀ i, (↑(U i) : Scheme.{u}).size ≤ T.size ^ ℵ₀) : S.size < κ

AlgebraicGeometry.Scheme.size_lt_of_locallyOfFiniteType_of_quasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/Cutoff.lean, line 204. The attribute's comment: “(5)”.

The source of a finite type morphism (locally of finite type and quasi-compact) into an object of Sch_κ is an object of Sch_κ.

theorem Scheme.size_lt_of_locallyOfFiniteType_of_quasiCompact {T S : Scheme.{u}} (f : T ⟶ S)
    [LocallyOfFiniteType f] [QuasiCompact f] (hS : S.size < κ) : T.size < κ

AlgebraicGeometry.Scheme.size_lt_of_locallyOfFiniteType_of_affineCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/Cutoff.lean, line 214. The attribute's comment: “(7)”.

Let f : T ⟶ S be locally of finite type with S an object of Sch_κ, and suppose T has an affine open covering indexed by a type of cardinality at most size(S) ^ ℵ₀. Then T is an object of Sch_κ.

theorem Scheme.size_lt_of_locallyOfFiniteType_of_affineCover (hκ : ℵ₀ < κ)
    (hsl : Cardinal.IsStrongPrelimit κ) {T S : Scheme.{u}} (f : T ⟶ S)
    [LocallyOfFiniteType f] {I : Type u} [Nonempty I] (V : I → T.affineOpens)
    (hcov : ⨆ i, (V i).1 = ⊤) (hI : #I ≤ S.size ^ ℵ₀) (hS : S.size < κ) : T.size < κ

AlgebraicGeometry.Scheme.size_lt_of_isAffine_of_mk_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/Cutoff.lean, line 228. The attribute's comment: “(9)”.

An affine scheme S whose ring of global sections has cardinality at most Bound(size T) = size(T) ^ ℵ₀ for some object T of Sch_κ is itself an object of Sch_κ.

theorem Scheme.size_lt_of_isAffine_of_mk_le (hκ : ℵ₀ < κ)
    (hsl : Cardinal.IsStrongPrelimit κ) {S T : Scheme.{u}} [IsAffine S] (hT : T.size < κ)
    (h : Cardinal.mk Γ(S, ⊤) ≤ T.size ^ ℵ₀) : S.size < κ

AlgebraicGeometry.Scheme.size_Spec_lt_of_mk_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/Cutoff.lean, line 241. The attribute's comment: “(9)”.

If #R ≤ Bound(size T) = size(T) ^ ℵ₀ for some object T of Sch_κ, then Spec R is an object of Sch_κ.

theorem Scheme.size_Spec_lt_of_mk_le (hκ : ℵ₀ < κ) (hsl : Cardinal.IsStrongPrelimit κ)
    (R : CommRingCat.{u}) {T : Scheme.{u}} (hT : T.size < κ)
    (h : Cardinal.mk R ≤ T.size ^ ℵ₀) : (Spec R).size < κ

AlgebraicGeometry.Scheme.size_Spec_lt_of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/Cutoff.lean, line 264. The attribute's comment: “(9)(b)”.

For an object Spec R of Sch_κ and a finite type R-algebra A, the scheme Spec A is an object of Sch_κ.

theorem Scheme.size_Spec_lt_of_finiteType (hκ : ℵ₀ < κ)
    (hsl : Cardinal.IsStrongPrelimit κ) (R A : Type u) [CommRing R] [CommRing A]
    [Algebra R A] [Algebra.FiniteType R A] (hR : (Spec (CommRingCat.of R)).size < κ) :
    (Spec (CommRingCat.of A)).size < κ

AlgebraicGeometry.Scheme.size_Spec_lt_of_isLocalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/Cutoff.lean, line 273. The attribute's comment: “(9)(c)”.

For an object Spec R of Sch_κ and a localization A of R at a submonoid, the scheme Spec A is an object of Sch_κ.

theorem Scheme.size_Spec_lt_of_isLocalization (hκ : ℵ₀ < κ)
    (hsl : Cardinal.IsStrongPrelimit κ) {R : Type u} [CommRing R] (M : Submonoid R)
    (A : Type u) [CommRing A] [Algebra R A] [IsLocalization M A]
    (hR : (Spec (CommRingCat.of R)).size < κ) : (Spec (CommRingCat.of A)).size < κ

AlgebraicGeometry.Scheme.size_Spec_lt_of_subring, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/Cutoff.lean, line 282. The attribute's comment: “(9)(e)”.

For an object Spec R of Sch_κ and a subring R' ⊆ R, the scheme Spec R' is an object of Sch_κ.

theorem Scheme.size_Spec_lt_of_subring (hκ : ℵ₀ < κ) (hsl : Cardinal.IsStrongPrelimit κ)
    {R : Type u} [CommRing R] (R' : Subring R)
    (hR : (Spec (CommRingCat.of R)).size < κ) : (Spec (CommRingCat.of R')).size < κ

AlgebraicGeometry.Scheme.size_sigmaObj_lt_of_lt_cof, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoproductCutoff.lean, line 65. The attribute's comment: “(2), index type below the cofinality”.

Stacks 000R (2) at an arbitrary index type. The coproduct of a family of objects of Sch_κ indexed by a type smaller than the cofinality of κ is again an object of Sch_κ.

The hypothesis on the index type is what bounds the supremum of the sizes; the index type's own cardinality is then below κ because the cofinality of an ordinal is at most the ordinal.

theorem Scheme.size_sigmaObj_lt_of_lt_cof (hκ : ℵ₀ < κ) {ι : Type u} (hι : #ι < κ.ord.cof)
    (Y : ι → Scheme.{u}) (hY : ∀ i, (Y i).size < κ) : (∐ Y).size < κ

AlgebraicGeometry.Scheme.size_sigmaObj_lt_of_forall_size_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoproductCutoff.lean, line 81. The attribute's comment: “(2), uniformly bounded family at an index type below the cutoff”.

Stacks 000R (2) for a family of uniformly bounded size. The coproduct of a family of objects of Sch_κ indexed by a type of cardinality below κ is again an object of Sch_κ as soon as the sizes of its members admit one bound below κ.

The cofinality hypothesis of AlgebraicGeometry.Scheme.size_sigmaObj_lt_of_lt_cof is there only to bound the supremum ⨆ i, size (Y i), and a uniform bound does that directly. This is the form needed by a family indexed by the points of a scheme of the site — a set of size below κ whose cardinality need not be below cof κ — whose members are cut out of affine opens of one fixed scheme, so that their sizes are bounded in terms of that one scheme's.

theorem Scheme.size_sigmaObj_lt_of_forall_size_le (hκ : ℵ₀ < κ) {ι : Type u} (hι : #ι < κ)
    (Y : ι → Scheme.{u}) (c : Cardinal.{u}) (hc : c < κ) (hY : ∀ i, (Y i).size ≤ c) :
    (∐ Y).size < κ

AlgebraicGeometry.BigFppfSite.contains_spec_tensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PrimeResidueFieldSite.lean, line 59. The attribute's comment: “(9), for a tensor product”.

The spectrum of a tensor product of two contained spectra is contained.

theorem contains_spec_tensorProduct (B : BigFppfSite.{u}) {R A C : Type u}
    [CommRing R] [CommRing A] [CommRing C] [Algebra R A] [Algebra R C]
    (hA : B.Contains (Spec (.of A))) (hC : B.Contains (Spec (.of C))) :
    B.Contains (Spec (.of (A ⊗[R] C)))

AlgebraicGeometry.BigFppfSite.contains_spec_algebraicClosure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PrimeResidueFieldSite.lean, line 69. The attribute's comment: “(9), for an algebraic closure”.

The spectrum of an algebraic closure of a contained field is contained.

theorem contains_spec_algebraicClosure (B : BigFppfSite.{u}) {K : Type u} [Field K]
    (hK : B.Contains (Spec (.of K))) :
    B.Contains (Spec (.of (AlgebraicClosure K)))

AlgebraicGeometry.BigFppfSite.contains_spec_residueField_atPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PrimeResidueFieldSite.lean, line 78. The attribute's comment: “(9), for the residue field of a prime”.

The spectrum of the residue field of a prime of a contained spectrum is contained.

theorem contains_spec_residueField_atPrime (B : BigFppfSite.{u}) {A : Type u} [CommRing A]
    (hA : B.Contains (Spec (.of A))) (p : Ideal A) [p.IsPrime] :
    B.Contains (Spec (.of (IsLocalRing.ResidueField (Localization.AtPrime p))))

AlgebraicGeometry.BigFppfSite.contains_spec_algebraicClosure_residueField_tensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PrimeResidueFieldSite.lean, line 93. The attribute's comment: “(9), for the algebraic closure of the residue field of a prime of a tensor product”.

For algebras A and C over R whose spectra are objects of the site and a prime 𝔰 of A ⊗_R C, the spectrum of an algebraic closure of the residue field of 𝔰 is an object of the site.

theorem contains_spec_algebraicClosure_residueField_tensorProduct (B : BigFppfSite.{u})
    {R A C : Type u} [CommRing R] [CommRing A] [CommRing C] [Algebra R A] [Algebra R C]
    (hA : B.Contains (Spec (.of A))) (hC : B.Contains (Spec (.of C)))
    (s : Ideal (A ⊗[R] C)) [s.IsPrime] :
    B.Contains (Spec (.of (AlgebraicClosure
      (IsLocalRing.ResidueField (Localization.AtPrime s)))))
Tag 0AHK, a lemma

Tag 0AHK in the Stacks Project.

AlgebraicGeometry.Scheme.size_le_of_fpqc_factorsThrough, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/Coverings.lean, line 287.

Stacks 0AHK. Let f : X ⟶ Y be a morphism of schemes. If there is an fpqc covering {g j : Y' j ⟶ Y} of Y such that every g j factors through f, then Y.size ≤ X.size.

theorem Scheme.size_le_of_fpqc_factorsThrough {X Y : Scheme} (f : X ⟶ Y)
    {J : Type*} (Y' : J → Scheme) (g : ∀ j, Y' j ⟶ Y)
    (hcov : IsFpqcCovering Y' g)
    (hfac : ∀ j, ∃ h : Y' j ⟶ X, h ≫ f = g j) :
    Scheme.size Y ≤ Scheme.size X
Tag 0AHL, a lemma

Tag 0AHL in the Stacks Project.

exists_fppf_refinement_schemeSize_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Size/Coverings.lean, line 409.

Stacks 0AHL. Every fppf covering 𝒞 of a scheme X is refined by an fppf covering 𝒲 of X indexed in the universe of X whose total space is small: the coproduct of the members of 𝒲 satisfies Scheme.size (∐ 𝒲.X) ≤ Scheme.size X.

theorem exists_fppf_refinement_schemeSize_le (X : Scheme.{u}) (𝒞 : FppfCovering.{v} X) :
    ∃ 𝒲 : FppfCovering.{u} X,
      𝒲.IsRefinement 𝒞 ∧ Scheme.size (∐ 𝒲.X) ≤ Scheme.size X
Sources
LeanAlgebraicGeometry.Scheme.size · Cardinal.stacksBound · AlgebraicGeometry.exists_size_cutoff · AlgebraicGeometry.Scheme.size_lt_of_le_stacksBound · AlgebraicGeometry.Scheme.size_lt_of_le_stacksBound_iSup · AlgebraicGeometry.Scheme.size_of_isAffine · AlgebraicGeometry.Scheme.size_le_of_iSup_eq_top · AlgebraicGeometry.Scheme.size_pullback_le

Section3.10 Sets with group action#

Section 3.10 of the Stacks Project, Tag 000T. 2 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 000U, a lemma

Tag 000U in the Stacks Project.

Sk_of_le_power_aleph0, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/GroupTheory/GroupAction/SizeCutoff.lean, line 286. The attribute's comment: “(2)”.

Stacks 000U (2). For an admissible cutoff κ, if S is an object of G-Sets_α and T is a G-set with size T ≤ Bound(size S) = size(S) ^ ℵ₀, then T is an object of G-Sets_α. This is condition B2 of AdmissibleBound read through Sk.

theorem Sk_of_le_power_aleph0 {G : Type u} {κ : Cardinal.{u}} (hκ : AdmissibleBound G κ)
    {S T : Type u} (hS : Sk G κ S) (hT : gsetSize G T ≤ gsetSize G S ^ ℵ₀) : Sk G κ T

exists_admissibleBound, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/GroupTheory/GroupAction/SizeCutoff.lean, line 299.

Stacks 000U. For every group G and every family S₀ of G-sets there is a cardinal κ which is an admissible cutoff for G and for which every member of S₀, as well as the left regular G-set {}_G G, is an object of G-Sets_α; moreover G-Sets_α is closed under G-sets of size at most Bound of the size of one of its objects.

Cardinal.IsStrongPrelimit κ records that κ is a limit cardinal, the counterpart of the source's "α is a limit ordinal"; it is also what gives condition B2 of AdmissibleBound.

theorem exists_admissibleBound (G : Type u) {ι : Type u} (S₀ : ι → Type u) :
    ∃ κ : Cardinal.{u}, Cardinal.IsStrongPrelimit κ ∧ AdmissibleBound G κ ∧
      Sk G κ G ∧ (∀ i, Sk G κ (S₀ i)) ∧
      ∀ S T : Type u, Sk G κ S → gsetSize G T ≤ gsetSize G S ^ ℵ₀ → Sk G κ T
Tag 000V, a lemma

Tag 000V in the Stacks Project.

Sk_leftRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/GroupTheory/GroupAction/SizeCutoff.lean, line 181. The attribute's comment: “(1)”.

Stacks 000V (1). The left regular G-set {}_G G is an object of G-Sets_α, since its size is max {ℵ₀, #G}, which is below the cutoff by B1.

theorem Sk_leftRegular (G : Type u) [Group G] (κ : Cardinal.{u})
    (hκ : AdmissibleBound G κ) :
    Sk G κ G

Sk_prod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/GroupTheory/GroupAction/SizeCutoff.lean, line 189. The attribute's comment: “(2)”.

Stacks 000V (2). The product S × T of two G-sets below the cutoff, with the diagonal G-action, is again below it: #(S × T) = #S * #T ≤ max {max {#S, #T}, ℵ₀} < κ.

theorem Sk_prod (G : Type u) [Group G] (κ : Cardinal.{u})
    (hκ : AdmissibleBound G κ) (S T : Type u) [MulAction G S] [MulAction G T]
    (hS : Sk G κ S) (hT : Sk G κ T) :
    Sk G κ (S × T)

Sk_sum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/GroupTheory/GroupAction/SizeCutoff.lean, line 199. The attribute's comment: “(2)”.

Stacks 000V (2). The coproduct S ⊕ T of two G-sets below the cutoff, with the disjoint-union G-action, is again below it: #(S ⊕ T) = #S + #T ≤ max {max {#S, #T}, ℵ₀} < κ.

theorem Sk_sum (G : Type u) [Group G] (κ : Cardinal.{u})
    (hκ : AdmissibleBound G κ) (S T : Type u) [MulAction G S] [MulAction G T]
    (hS : Sk G κ S) (hT : Sk G κ T) :
    Sk G κ (S ⊕ T)

Sk_fibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/GroupTheory/GroupAction/SizeCutoff.lean, line 209. The attribute's comment: “(2)”.

Stacks 000V (2). For G-sets S, T, R below the cutoff and equivariant maps f : S → R, h : T → R, the fibre product S ×_R T = {p : S × T // f p.1 = h p.2} is below the cutoff, being a subtype of S × T.

theorem Sk_fibreProduct (G : Type u) [Group G] (κ : Cardinal.{u})
    (hκ : AdmissibleBound G κ) (S T R : Type u)
    [MulAction G S] [MulAction G T] [MulAction G R]
    (hS : Sk G κ S) (hT : Sk G κ T)
    (f : S → R) (h : T → R) :
    Sk G κ { p : S × T // f p.1 = h p.2 }

Sk_pushout, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/GroupTheory/GroupAction/SizeCutoff.lean, line 222. The attribute's comment: “(2)”.

Stacks 000V (2). For G-sets S, T, R below the cutoff and equivariant maps f : R → S, h : R → T, the pushout of S ← R → T is below the cutoff, being a quotient of S ⊕ T. The pushout is modelled as the quotient of S ⊕ T by the equivalence relation generated by inl (f r) ~ inr (h r).

theorem Sk_pushout (G : Type u) [Group G] (κ : Cardinal.{u})
    (hκ : AdmissibleBound G κ) (S T R : Type u)
    [MulAction G S] [MulAction G T] [MulAction G R]
    (hS : Sk G κ S) (hT : Sk G κ T)
    (f : R → S) (h : R → T) :
    Sk G κ
      (Quotient
        (Relation.EqvGen.setoid
          (fun a b : S ⊕ T =>
            ∃ r : R, a = Sum.inl (f r) ∧ b = Sum.inr (h r))))

Sk_sigma, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/GroupTheory/GroupAction/SizeCutoff.lean, line 239. The attribute's comment: “(2)”.

Stacks 000V (2). For an at-most-countable index type ι and a family of G-sets S i below the cutoff, the coproduct Σ i, S i with the fibrewise G-action is below the cutoff: #(Σ i, S i) = Σ i, #(S i) ≤ #ι * ⨆ i, #(S i), and a supremum of at most ℵ₀ many cardinals below κ is below κ because κ.ord has uncountable cofinality (B3).

theorem Sk_sigma (G : Type u) [Group G] (κ : Cardinal.{u})
    (hκ : AdmissibleBound G κ) (ι : Type u) (hι : #ι ≤ ℵ₀)
    (S : ι → Type u) [∀ i, MulAction G (S i)] (hS : ∀ i, Sk G κ (S i)) :
    Sk G κ (Σ i, S i)

Sk_pi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/GroupTheory/GroupAction/SizeCutoff.lean, line 256. The attribute's comment: “(2)”.

Stacks 000V (2). For an at-most-countable index type ι and a family of G-sets S i below the cutoff, the product Π i, S i with the pointwise G-action is below the cutoff: writing s = ⨆ i, #(S i), which is below κ by B3, one has #(Π i, S i) = Π i, #(S i) ≤ s ^ #ι ≤ s ^ ℵ₀ < κ by B2. If s = 0 the bound is instead the trivial s ^ #ι ≤ 1 < ℵ₀ < κ.

theorem Sk_pi (G : Type u) [Group G] (κ : Cardinal.{u})
    (hκ : AdmissibleBound G κ) (ι : Type u) (hι : #ι ≤ ℵ₀)
    (S : ι → Type u) [∀ i, MulAction G (S i)] (hS : ∀ i, Sk G κ (S i)) :
    Sk G κ (∀ i, S i)

Sk_subtype, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/GroupTheory/GroupAction/SizeCutoff.lean, line 276. The attribute's comment: “(3)”.

Stacks 000V (3). For a G-set U below the cutoff and a G-stable subset O ⊆ U, the induced G-set on {x : U // x ∈ O} is below the cutoff, being a subtype of U.

theorem Sk_subtype (G : Type u) [Group G] (κ : Cardinal.{u})
    (hκ : AdmissibleBound G κ) (U : Type u) [MulAction G U]
    (hU : Sk G κ U) (O : Set U) :
    Sk G κ { x : U // x ∈ O }
Sources
LeanSk_of_le_power_aleph0 · exists_admissibleBound · Sk_leftRegular · Sk_prod · Sk_sum · Sk_fibreProduct · Sk_pushout · Sk_sigma

Section3.11 Coverings of a site#

Section 3.11 of the Stacks Project, Tag 000W. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 000X, a lemma

Tag 000X in the Stacks Project.

exists_covBounded_isSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Pretopology/SmallSubsite.lean, line 296.

Stacks 000X. Let IsCov be a site on C and let Cov₀ be a set-sized family of coverings in it. Then there are a cardinal κ and a limit ordinal α such that the coverings in IsCov whose index set has cardinality at most κ again form a site, contain Cov₀, and every covering in IsCov is combinatorially equivalent to one of them. One may take κ = ℵ₀ ⊔ κ₀ ⊔ κ_rep, with κ₀ bounding the index sets of Cov₀ and κ_rep bounding those of a system of combinatorial representatives, and α = ω.

theorem exists_covBounded_isSite
    {C : Type u} [Category.{v} C]
    (IsCov : Covering.{u, v, max u v} C → Prop)
    (hSite : IsSite IsCov)
    (Cov₀ : Set (Covering.{u, v, max u v} C))
    [hSmall : Small.{max u v} Cov₀]
    (hCov₀ : ∀ 𝒰 ∈ Cov₀, IsCov 𝒰) :
    ∃ (κ : Cardinal.{max u v}) (α : Ordinal.{max u v}),
      Order.IsSuccLimit α ∧
      (∀ 𝒰 ∈ Cov₀, CovBounded IsCov κ 𝒰) ∧
      IsSite (CovBounded IsCov κ) ∧
      (∀ 𝒰 : Covering C, IsCov 𝒰 →
        ∃ 𝒰' : Covering C,
          CovBounded IsCov κ 𝒰' ∧ Covering.CombEquiv 𝒰 𝒰')
Sources
Leanexists_covBounded_isSite

Section3.12 Abelian categories and injectives#

Section 3.12 of the Stacks Project, Tag 000Z. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0010, a lemma

Tag 0010 in the Stacks Project.

exists_small_abelian_subcategory_with_enough_injectives, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Abelian/SmallSubcategory.lean, line 126.

Stacks 0010. Let 𝒜 be an abelian category with enough injectives and A : S → 𝒜 a family of objects. There is an object property P whose full subcategory 𝒜' = P.FullSubcategory has a set of objects, contains every A s, and admits an abelian structure for which the inclusion P.ι is additive and exact, 𝒜' has enough injectives, and an object of 𝒜' is injective there if and only if it is injective in 𝒜.

theorem exists_small_abelian_subcategory_with_enough_injectives (A : S → 𝒜) :
    ∃ (P : ObjectProperty 𝒜),
      Small.{max v w} P.FullSubcategory ∧
      (∀ s, P (A s)) ∧
      ∃ (_ : Abelian P.FullSubcategory),
        P.ι.Additive ∧
        Nonempty (PreservesFiniteLimits P.ι) ∧
        Nonempty (PreservesFiniteColimits P.ι) ∧
        EnoughInjectives P.FullSubcategory ∧
        ∀ X : P.FullSubcategory, Injective X ↔ Injective (P.ι.obj X)
Sources
Leanexists_small_abelian_subcategory_with_enough_injectives

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.