AlgebraicGeometry.exists_representableBy_of_representableBy_restrict_finiteEtale
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_representableBy_of_representableBy_restrict_finiteEtale
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry OppositeLean source · statement
theorem _root_.AlgebraicGeometry.exists_representableBy_of_representableBy_restrict_finiteEtale
(R : Type u) [CommRing R] (R' : Type u) [CommRing R'] [Algebra R R'] [Module.Finite R R']
[Algebra.Etale R R'] [Module.FaithfullyFlat R R']
(G : (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ Type (u + 1))
(hG : ∀ T : Over (Spec (CommRingCat.of R)), Presieve.IsSheafFor G (Presieve.singleton
((Over.mapPullbackAdj (Spec.map (CommRingCat.ofHom (algebraMap R R')))).counit.app T)))
{X' : Scheme.{u}} (x' : X' ⟶ Spec (CommRingCat.of R'))
(hX' : ((Over.map (Spec.map (CommRingCat.ofHom (algebraMap R R')))).op ⋙ G).RepresentableBy
(Over.mk x'))
(haff : ∀ S : Finset X', ∃ U : X'.Opens, IsAffineOpen U ∧ ∀ x ∈ S, x ∈ U) :
∃ (X : Scheme.{u}) (f : X ⟶ Spec (CommRingCat.of R)) (_ : G.RepresentableBy (Over.mk f))
(e : pullback f (Spec.map (CommRingCat.ofHom (algebraMap R R'))) ≅ X'),
e.hom ≫ x' = pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap R R')))