AlgebraicGeometry.fpqc_SpecMap_pullback_fst_appTop
The affine base-change map induced on global sections is fpqc.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe u
variable {X S T : Scheme.{u}} (f : X ⟶ S) (g : T ⟶ S)
variable [IsAffine S] [IsAffine T] [QuasiCompact f] [QuasiSeparated f]
variable [Flat g] [Surjective g]Lean source · full declaration
theorem fpqc_SpecMap_pullback_fst_appTop :
(show CategoryTheory.MorphismProperty Scheme.{u} from
@Surjective ⊓ @Flat ⊓ @QuasiCompact) (Spec.map (pullback.fst f g).appTop) := by
have hg : Flat (Spec.map g.appTop) ∧ Surjective (Spec.map g.appTop) :=
(flat_and_surjective_SpecMap_iff g.appTop).mpr
((Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine g).mp
⟨inferInstance, inferInstance⟩)
let : Flat (Spec.map g.appTop) := hg.1
let : Surjective (Spec.map g.appTop) := hg.2
have h := isPullback_SpecMap_of_isPushout f.appTop g.appTop
(pullback.fst f g).appTop (pullback.snd f g).appTop
(isPushout_appTop_of_flat f g)
refine ⟨⟨?_, ?_⟩, inferInstance⟩
· exact (show CategoryTheory.MorphismProperty Scheme.{u} from @Surjective).of_isPullback
h.flip inferInstance
· exact (show CategoryTheory.MorphismProperty Scheme.{u} from @Flat).of_isPullback
h.flip inferInstance