AlgebraicGeometry.Scheme.OrderedAffineCover.exists_forall_le_preimage_of_compactSpace
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_OrderedAffineCover_exists_forall_le_preimage_of_compactSpace
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe uLean source · statement
theorem _root_.AlgebraicGeometry.Scheme.OrderedAffineCover.exists_forall_le_preimage_of_compactSpace
{Y : Scheme.{u}} [CompactSpace Y] {n : ℕ} (X : Fin n → Scheme.{u}) (h : ∀ j, Y ⟶ X j)
(𝒰 : ∀ j, (X j).OrderedAffineCover) :
∃ (𝒲 : Y.OrderedAffineCover) (lam : ∀ j, 𝒲.ι → (𝒰 j).ι),
∀ (j : Fin n) (w : 𝒲.ι), 𝒲.U w ≤ (h j) ⁻¹ᵁ (𝒰 j).U (lam j w)