AlgebraicGeometry.exists_fg_subalgebra_isAffine_pullback_of_isAffine_pullback
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_isAffine_pullback_of_isAffine_pullback
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
open _root_.AlgebraicGeometry.SubalgebraStages inLean source · statement
theorem _root_.AlgebraicGeometry.exists_fg_subalgebra_isAffine_pullback_of_isAffine_pullback
{A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
{W : Scheme.{u}} (f : W ⟶ Spec (CommRingCat.of A₀)) [QuasiCompact f] [QuasiSeparated f]
[IsAffine (pullback f (Spec.map (CommRingCat.ofHom (algebraMap A₀ A))))] (s : Finset A) :
∃ (T : Subalgebra A₀ A), T.FG ∧ (↑s : Set A) ⊆ T ∧
IsAffine (pullback f (Spec.map (CommRingCat.ofHom (algebraMap A₀ ↥T))))