AlgebraicGeometry.exists_fg_subalgebra_opens_preimage_eq_of_isCompact
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_opens_preimage_eq_of_isCompact
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe uLean source · statement
theorem _root_.AlgebraicGeometry.exists_fg_subalgebra_opens_preimage_eq_of_isCompact
{A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
{X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀)) [QuasiCompact f] [QuasiSeparated f]
(W : (pullback f (Spec.map (CommRingCat.ofHom (algebraMap A₀ A)))).Opens)
(hW : IsCompact (W : Set ↥(pullback f (Spec.map (CommRingCat.ofHom (algebraMap A₀ A)))))) (s :
Finset A) :
∃ (T : Subalgebra A₀ A), T.FG ∧ (↑s : Set A) ⊆ T ∧
∃ W₀ : (pullback f (Spec.map (CommRingCat.ofHom (algebraMap A₀ ↥T)))).Opens,
IsCompact (W₀ : Set ↥(pullback f (Spec.map (CommRingCat.ofHom (algebraMap A₀ ↥T))))) ∧
∀ q : pullback f (Spec.map (CommRingCat.ofHom (algebraMap A₀ A))) ⟶
pullback f (Spec.map (CommRingCat.ofHom (algebraMap A₀ ↥T))),
q ≫ pullback.fst f _ = pullback.fst f _ →
q ≫ pullback.snd f _ = pullback.snd f _ ≫ Spec.map (CommRingCat.ofHom T.val.toRingHom) →
q ⁻¹ᵁ W₀ = W