AlgebraicGeometry.exists_representableBy_of_representableBy_restrict_finiteEtale_of_forall_orbit
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry
universe u
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs in
open exists_representableBy_of_representableBy_restrict_finiteEtale_of_forall_orbit in
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite inLean source · statement
theorem exists_representableBy_of_representableBy_restrict_finiteEtale_of_forall_orbit
(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 : ∀ x : X', ∃ U : X'.Opens, IsAffineOpen U ∧
∀ r : ↑(pullback (x' ≫ Spec.map (CommRingCat.ofHom (algebraMap R R'))) (Spec.map
(CommRingCat.ofHom (algebraMap R R')))),
(pullback.fst (x' ≫ Spec.map (CommRingCat.ofHom (algebraMap R R'))) (Spec.map
(CommRingCat.ofHom (algebraMap R R')))) r = x →
(DescentAction.ofRepresentableBy (Spec.map (CommRingCat.ofHom (algebraMap R R'))) G x'
hX').act r ∈ 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')))