AlgebraicGeometry.DescentAction.effective_of_finiteEtale
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Descent.Proofs.DescentAction_effective_of_finiteEtale
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry OppositeLean source · statement
theorem _root_.AlgebraicGeometry.DescentAction.effective_of_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']
{X' : Scheme.{u}} {x' : X' ⟶ Spec (CommRingCat.of R')}
(A : DescentAction (Spec.map (CommRingCat.ofHom (algebraMap R R'))) x')
(haff : ∀ S : Finset X', ∃ U : X'.Opens, IsAffineOpen U ∧ ∀ x ∈ S, x ∈ U) :
A.Effective