AlgebraicGeometry.exists_fg_subalgebra_hom_pullback_of_hom_pullback_of_locallyOfFinitePresentation
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits
open AlgebraicCurves.Geometry.Schemes.Proofs
exists_fg_subalgebra_hom_pullback_of_hom_pullback_of_locallyOfFinitePresentation
universe u
open _root_.AlgebraicGeometry.SubalgebraStagesLean source · statement
theorem exists_fg_subalgebra_hom_pullback_of_hom_pullback_of_locallyOfFinitePresentation
{A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
{X₁ X₂ : Scheme.{u}} (f₁ : X₁ ⟶ Spec (CommRingCat.of A₀)) (f₂ : X₂ ⟶ Spec (CommRingCat.of A₀))
[QuasiCompact f₁] [QuasiSeparated f₁] [LocallyOfFinitePresentation f₂]
(g : pullback f₁ (Spec.map (CommRingCat.ofHom (algebraMap A₀ A))) ⟶
pullback f₂ (Spec.map (CommRingCat.ofHom (algebraMap A₀ A))))
(hg : g ≫ pullback.snd f₂ _ = pullback.snd f₁ _) (s : Finset A) :
∃ (T : Subalgebra A₀ A), T.FG ∧ (↑s : Set A) ⊆ T ∧
∃ g₀ : pullback f₁ (Spec.map (CommRingCat.ofHom (algebraMap A₀ ↥T))) ⟶
pullback f₂ (Spec.map (CommRingCat.ofHom (algebraMap A₀ ↥T))),
g₀ ≫ pullback.snd f₂ _ = pullback.snd f₁ _ ∧
∀ (q₁ : pullback f₁ (Spec.map (CommRingCat.ofHom (algebraMap A₀ A))) ⟶
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₂ ≫ pullback.fst f₂ _ = pullback.fst f₂ _ →
q₂ ≫ pullback.snd f₂ _ = pullback.snd f₂ _ ≫ Spec.map (CommRingCat.ofHom T.val.toRingHom)
→
q₁ ≫ g₀ = g ≫ q₂