Theorems · Theorem · algebraic geometry

AlgebraicGeometry.QuasiCompactCover.exists_hom

∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S)
  [P.RespectsLeft AlgebraicGeometry.IsOpenImmersion] [CompactSpace ↥S]
  [AlgebraicGeometry.QuasiCompactCover 𝒰.toPreZeroHypercover],
  ∃ 𝒱 f, Finite 𝒱.I₀ ∧ ∀ (j : 𝒱.cover.I₀), AlgebraicGeometry.IsOpenImmersion (f.h₀ j)

Defined in

Mathlib.AlgebraicGeometry.Cover.QuasiCompact

Cited by

1 results in Mathlib

Foundations

Depth 148 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.MorphismProperty.RespectsLeftCompactSpaceAlgebraicGeometry.QuasiCompactCover