AlgebraicGeometry.DescentAction.effective_of_finiteEtale_of_forall_orbit
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Descent.Proofs
namespace DescentAction_effective_of_finiteEtale_of_forall_orbit
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry OppositeLean source · statement
theorem _root_.AlgebraicGeometry.DescentAction.effective_of_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']
{X' : Scheme.{u}} {x' : X' ⟶ Spec (CommRingCat.of R')}
(A : DescentAction (Spec.map (CommRingCat.ofHom (algebraMap R R'))) 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 → A.act r ∈ U) :
A.Effective