structure ChowLemmaHelper.AffineCoverData (X : AlgebraicGeometry.Scheme) : Type (u + 1)

Data of a finite affine cover of a scheme X, together with closed immersions of each chart into an ambient affine space; used in the assembly of Chow's lemma.

• ι : Type u
• fintype : Fintype self.ι
• R : self.ι → CommRingCat
• f (i : self.ι) : AlgebraicGeometry.Spec (self.R i) ⟶ X
• isOpenImmersion (i : self.ι) : AlgebraicGeometry.IsOpenImmersion (self.f i)
• covers (x : ↥X) : ∃ (i : self.ι), x ∈ Set.range ⇑(self.f i)
• ambientRing : self.ι → CommRingCat
• embedding (i : self.ι) : AlgebraicGeometry.Spec (self.R i) ⟶ AlgebraicGeometry.Spec (self.ambientRing i)
• isClosedImmersion (i : self.ι) : AlgebraicGeometry.IsClosedImmersion (self.embedding i)

def ChowLemmaHelper.AffineCoverData.card {X : AlgebraicGeometry.Scheme} (c : AffineCoverData X) : ℕ

The number of charts in an AffineCoverData.

noncomputable def ChowLemmaHelper.AffineCoverData.toOpenCover {X : AlgebraicGeometry.Scheme} (c : AffineCoverData X) : X.OpenCover

Convert AffineCoverData into a Mathlib Scheme.OpenCover, forgetting the ambient embeddings.

@[implicit_reducible]

instance ChowLemmaHelper.instFintypeI₀SchemeToOpenCover {X : AlgebraicGeometry.Scheme} (c : AffineCoverData X) : Fintype c.toOpenCover.I₀

The underlying index type of the associated open cover is finite.

theorem ChowLemmaHelper.exists_affineCoverData (X : AlgebraicGeometry.Scheme) [CompactSpace ↥X] : Nonempty (AffineCoverData X)

Any quasi-compact scheme admits an AffineCoverData.

theorem ChowLemmaHelper.exists_affineCoverData_of_proper {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.IsProper f] : Nonempty (AffineCoverData X)

If f : X → S is proper, then X admits an AffineCoverData, since proper morphisms are in particular quasi-compact.