35.2 Descent data for… to 35.7 Descent of finiteness…

Section35.2 Descent data for quasi-coherent sheaves #

Section 35.2 of the Stacks Project, Tag 023A. 4 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 023B, a definition

Tag 023B in the Stacks Project.

AlgebraicGeometry.QuasicoherentDescentData, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherent/DescentData.lean, line 98.

Descent data for quasicoherent sheaves relative to a family f i : X i ⟶ S.

The underlying descent datum supplies the transition isomorphisms and their cocycle condition. Morphisms in this full subcategory are componentwise morphisms commuting with every transition isomorphism. For chosen binary and triple fibre products, Pseudofunctor.DescentData'.descentDataEquivalence is component-preserving and identifies this with the full subcategory of the source's fibre-product presentation on quasicoherent objects.

abbrev QuasicoherentDescentData {I : Type v} {S : Scheme.{u}} {X : I → Scheme.{u}}
    (f : ∀ i, X i ⟶ S)

Tag 023C, a lemma

Tag 023C in the Stacks Project.

AlgebraicGeometry.QuasicoherentDescentData.pullFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherent/DescentData.lean, line 123. The attribute's comment: “part (2), the pullback functor”.

Pullback along a morphism of families defines a functor on quasicoherent descent data.

Its underlying functor is Pseudofunctor.DescentData.pullFunctor; quasicoherence of its components follows from preservation of quasicoherence by pullback.

noncomputable def pullFunctor (Φ : 𝒰.HomOver 𝒱 g) :
    QuasicoherentDescentData 𝒱.f ⥤ QuasicoherentDescentData 𝒰.f

AlgebraicGeometry.QuasicoherentDescentData.pullFunctor_comp_ι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherent/DescentData.lean, line 135. The attribute's comment: “part (1), the pulled-back descent datum”.

After forgetting quasicoherence, pullFunctor is exactly the usual pullback functor on descent data. Thus its objects have components g_i^* F_{α(i)} and the pulled-back transition isomorphisms, and its action on morphisms is componentwise pullback.

theorem pullFunctor_comp_ι (Φ : 𝒰.HomOver 𝒱 g) :
    pullFunctor Φ ⋙ ObjectProperty.ι _ = ObjectProperty.ι _ ⋙
        Pseudofunctor.DescentData.pullFunctor modulePullbackPseudofunctor
          (f := 𝒱.f) (p := g) (f' := 𝒰.f) (α := Φ.s₀) (p' := Φ.h₀) Φ.w₀

AlgebraicGeometry.QuasicoherentDescentData.pullFunctorIsoOfEq, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherent/DescentData.lean, line 144. The attribute's comment: “part (3), functorial isomorphism when the maps of targets agree”.

Morphisms of families inducing the same morphism of targets give naturally isomorphic pullback functors on quasicoherent descent data.

noncomputable def pullFunctorIsoOfEq {g' : U ⟶ V} (Φ : 𝒰.HomOver 𝒱 g)
    (Φ' : 𝒰.HomOver 𝒱 g') (h : g = g') : pullFunctor Φ ≅ pullFunctor Φ'

Tag 023D, a definition

Tag 023D in the Stacks Project.

AlgebraicGeometry.canonicalDescentFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherent/DescentData.lean, line 168. The attribute's comment: “part (2)”.

The functor sending a quasicoherent module on S to its canonical descent datum relative to the family f i : X i ⟶ S.

noncomputable def canonicalDescentFunctor {I : Type v} {S : Scheme.{u}}
    {X : I → Scheme.{u}} (f : ∀ i, X i ⟶ S) :
    Functor (SheafOfModules.isQuasicoherent S.ringCatSheaf).FullSubcategory
      (QuasicoherentDescentData f)

AlgebraicGeometry.trivialDescentData, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherent/DescentData.lean, line 190. The attribute's comment: “part (1)”.

The trivial descent datum on a quasicoherent module, relative to the singleton family whose only morphism is the identity of the base scheme.

noncomputable abbrev trivialDescentData {S : Scheme.{u}}
    (M : (SheafOfModules.isQuasicoherent S.ringCatSheaf).FullSubcategory) :
    QuasicoherentDescentData (PreZeroHypercover.singleton.{0} (𝟙 S)).f

AlgebraicGeometry.trivialDescentComponentIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherent/DescentData.lean, line 210. The attribute's comment: “part (1), identity comparison”.

The sole component of the trivial descent datum is naturally isomorphic to the original quasicoherent module.

noncomputable def trivialDescentComponentIso {S : Scheme.{u}} :
    trivialDescentComponentFunctor (S := S) ≅
      (SheafOfModules.isQuasicoherent S.ringCatSheaf).ι

AlgebraicGeometry.pullTrivialDescentIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherent/DescentData.lean, line 288. The attribute's comment: “part (2), pullback of the trivial datum”.

Pulling the trivial descent datum back along a family gives, naturally in the quasicoherent module, its canonical descent datum for that family.

noncomputable def pullTrivialDescentIso {S : Scheme.{u}} (𝒰 : PreZeroHypercover.{v} S) :
    canonicalDescentFunctor (PreZeroHypercover.singleton.{0} (𝟙 S)).f ⋙
        QuasicoherentDescentData.pullFunctor (toTrivialFamily 𝒰) ≅
      canonicalDescentFunctor 𝒰.f

AlgebraicGeometry.QuasicoherentDescentData.IsEffective, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherent/DescentData.lean, line 320. The attribute's comment: “part (3)”.

A quasicoherent descent datum is effective if it is isomorphic to the canonical descent datum of a quasicoherent module on the target.

abbrev IsEffective (D : QuasicoherentDescentData f) : Prop

Tag 023E, a lemma

Tag 023E in the Stacks Project.

Stacks.Descent.isEffective_zariski, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherent/ZariskiEssSurj.lean, line 1215. The attribute's comment: “zariski_effectivity”.

The effectivity half of Stacks 023E. Every quasi-coherent descent datum for a family of open immersions whose images cover the target is effective. This is Stacks.Descent.isEffective_of_essSurj_zariski with its standing essential-surjectivity hypothesis discharged by Stacks.Descent.essSurj_toDescentData_zariski; the full faithfulness half is Stacks.Descent.nonempty_fullyFaithful_canonicalDescentFunctor_zariski.

theorem isEffective_zariski {S : Scheme.{u}} {I : Type v} {Y : I → Scheme.{u}}
    (f : ∀ i, Y i ⟶ S) [∀ i, IsOpenImmersion (f i)] (hf : ⨆ i, (f i).opensRange = ⊤)
    (D : QuasicoherentDescentData f) : D.IsEffective

Stacks.Descent.nonempty_fullyFaithful_canonicalDescentFunctor_zariski, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherent/ZariskiGluing.lean, line 522. The attribute's comment: “zariski_full_faithfulness”.

The full faithfulness half of Stacks 023E. For a family of open immersions whose images cover the target, the canonical descent functor of Stacks 023D on quasi-coherent modules is fully faithful.

This is the full faithfulness clause of Stacks 023E; the effectivity clause is not proved here.

theorem nonempty_fullyFaithful_canonicalDescentFunctor_zariski
    (hf : ⨆ i, (f i).opensRange = ⊤) :
    Nonempty (canonicalDescentFunctor f).FullyFaithful

Sources

LeanAlgebraicGeometry.QuasicoherentDescentData · AlgebraicGeometry.QuasicoherentDescentData.pullFunctor · AlgebraicGeometry.QuasicoherentDescentData.pullFunctor_comp_ι · AlgebraicGeometry.QuasicoherentDescentData.pullFunctorIsoOfEq · AlgebraicGeometry.canonicalDescentFunctor · AlgebraicGeometry.trivialDescentData · AlgebraicGeometry.trivialDescentComponentIso · AlgebraicGeometry.pullTrivialDescentIso

Section35.3 Descent for modules #

Section 35.3 of the Stacks Project, Tag 023F. 12 tags here are carried by 27 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 023G, a definition

Tag 023G in the Stacks Project.

ModuleCat.DescentData, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Module/DescentData.lean, line 244. The attribute's comment: “descent data”.

A descent datum for modules for an R-algebra A.

The transition is bundled as an A ⊗[R] A-linear equivalence, and cocycle is the equality φ₁₂ ∘ φ₀₁ = φ₀₂.

structure DescentData

ModuleCat.DescentData.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Module/DescentData.lean, line 271. The attribute's comment: “morphisms”.

A morphism of module descent data is an A-linear map commuting with the transition isomorphisms.

structure Hom (D E : DescentData.{u, v, w} R A)

Tag 023H, a lemma

Tag 023H in the Stacks Project.

ModuleCat.exists_descentCosimplicialModuleFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/CechCosimplicialModule.lean, line 1103.

Stacks Lemma 023H. To a descent datum (N, φ) one can associate a cosimplicial module over the Čech algebra (A / R)_• by the rules N_n = N_{n, n} and N_•(β) = φᵐ_{β(n), m} ∘ N_{β, n}, functorially in the descent datum.

public theorem exists_descentCosimplicialModuleFunctor :
    ∃ F : DescentData.{u, v, w} R A ⥤ CechModule.{u, v, w} R A,
      IsDescentCosimplicialModuleFunctor R A F

ModuleCat.descentCosimplicialModuleFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/CechCosimplicialModule.lean, line 1120.

The functor which associates to a descent datum (N, φ) its cosimplicial module over the Čech algebra (A / R)_•. It is characterised by descentCosimplicialModuleFunctor_obj and descentCosimplicialModuleFunctor_map.

public noncomputable def descentCosimplicialModuleFunctor :
    DescentData.{u, v, w} R A ⥤ CechModule.{u, v, w} R A

Tag 023I, a lemma

Tag 023I in the Stacks Project.

ModuleCat.cechTensorModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/CanonicalCechTensorModule.lean, line 246. The attribute's comment: “tensor cosimplicial module”.

The Čech cosimplicial algebra tensored with M, together with its degreewise and cosimplicial-map specification.

public noncomputable def cechTensorModule (M : ModuleCat.{w} R) :
    {T : CechModule.{u, v, w} R A // IsCechTensorModule R A M T}

ModuleCat.canonicalDescent_cosimplicialModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/CanonicalCechTensorModule.lean, line 560. The attribute's comment: “canonical isomorphism”.

The cosimplicial module associated to a canonical descent datum is isomorphic to the Čech cosimplicial algebra tensored with its base module.

public theorem canonicalDescent_cosimplicialModule
    (M : ModuleCat.{w} R)
    (D : DescentData.{u, v, w} R A)
    (e : (A ⊗[R] M) ≃ₗ[A] D.module)
    (he : ∀ (a b : A) (m : M),
      D.transition ((e (a ⊗ₜ[R] m)) ⊗ₜ[R] b) =
        a ⊗ₜ[R] (show restrictModule R A D.module from
          e (b ⊗ₜ[R] m))) :
    Nonempty (((descentCosimplicialModuleFunctor R A).obj D) ≅
      (cechTensorModule R A M).1)

Tag 023J, a definition

Tag 023J in the Stacks Project.

ModuleCat.DescentData.IsEffective, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Module/DescentData.lean, line 310.

A module descent datum is effective if it is isomorphic to the canonical descent datum obtained by extending scalars from an R-module.

abbrev DescentData.IsEffective (R : Type u) (A : Type v) [CommRing R] [CommRing A]
    [Algebra R A] (D : DescentData.{u, v, w} R A) : Prop

Tag 023K, an equation

Tag 023K in the Stacks Project.

Stacks.Descent.augmentedDescentComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Module/AugmentedDescentComplex.lean, line 368. The attribute's comment: “the augmented complex 0 → M → A ⊗ M → A ⊗ A ⊗ M → ⋯”.

Equation 023K: the augmented descent complex 0 → M → A ⊗[R] M → A ⊗[R] A ⊗[R] M → ⋯ of the ring map R → A with coefficients in M. It is the alternating coface map complex of (A/R)• ⊗[R] M, augmented by M along m ↦ 1 ⊗ₜ m.

noncomputable def augmentedDescentComplex : CochainComplex (ModuleCat.{max u v} R) ℕ

Stacks.Descent.augmentedDescentComplexXIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Module/AugmentedDescentComplex.lean, line 387. The attribute's comment: “its degree-(n+1) term is A^{⊗(n+1)} ⊗_R M”.

The degree-(n + 1) term of the augmented descent complex is A^{⊗(n + 1)} ⊗[R] M.

noncomputable def augmentedDescentComplexXIso (n : ℕ) :
    ModuleCat.of R ((tensorPowerAlg R A n : Type u) ⊗[R] M) ≅
      (augmentedDescentComplex R A M).X (n + 1)

Tag 023L, a lemma

Tag 023L in the Stacks Project.

AlgebraicTopology.amitsurExtendedCochainComplex_acyclic_of_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Module/Amitsur.lean, line 151.

Stacks Lemma 023L. If R → A admits a section, then the extended Amitsur cochain complex with coefficients in any R-module M is exact.

theorem amitsurExtendedCochainComplex_acyclic_of_section
    (h : Nonempty (A →ₐ[R] R)) :
    (amitsurExtendedCochainComplex R A M).Acyclic

Tag 023M, a lemma

Tag 023M in the Stacks Project.

Stacks.Descent.amitsurExtendedCochainComplex_acyclic_of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Module/AmitsurAcyclic.lean, line 435. References: SGA 1 VIII (1.7), “affine case”.

Stacks Lemma 023M. For a faithfully flat algebra A over a commutative ring R and an arbitrary R-module M, the extended Amitsur cochain complex M → A ⊗[R] M → (A ⊗[R] A) ⊗[R] M → ⋯ is exact in every degree.

theorem amitsurExtendedCochainComplex_acyclic_of_faithfullyFlat [Module.FaithfullyFlat R A] :
    (amitsurExtendedCochainComplex R A M).Acyclic

AlgebraicTopology.amitsurExtendedCochainComplex_acyclic_of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/ModuleEquivalence/FaithfullyFlatAmitsur.lean, line 1259. References: SGA 1 VIII (1.7), “affine case”.

Stacks Lemma 023M, and Stacks Lemma 03OA. The extended Amitsur cochain complex of a faithfully flat algebra is exact for every module of coefficients. Exactness of the extended complex M → A ⊗[R] M → A ⊗[R] A ⊗[R] M → ⋯ says both that the unaugmented complex is exact in positive degrees and that its degree-zero cohomology is M, which is the form 03OA states.

theorem amitsurExtendedCochainComplex_acyclic_of_faithfullyFlat
    (R : Type u) (A : Type v) (M : Type w) [CommRing R] [CommRing A] [Algebra R A]
    [AddCommGroup M] [Module R M] [Module.FaithfullyFlat R A] :
    (amitsurExtendedCochainComplex R A M).Acyclic

ModuleCat.baseExtensionUnitEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Modules/EffectiveDescent.lean, line 364. The attribute's comment: “degrees −1 and 0”. References: SGA 1 VIII (1.7), “affine case”.

Stacks Project, Tag 023M in degrees −1 and 0. For a universally injective ring map the unit m ↦ 1 ⊗ m of the base-extension adjunction is an isomorphism of M onto the invariants of the base-extended descent datum.

Exactness of the extended cochain complex 0 → M → A ⊗[R] M → A ⊗[R] A ⊗[R] M → ⋯ at M is injectivity of the unit, and exactness at A ⊗[R] M says that the kernel of the next differential — which is ModuleCat.invariantSubmodule R A of the canonical descent datum on A ⊗[R] M — is the image of the unit. Together they are bijectivity of the unit onto the invariants. The source assumes R → A faithfully flat; faithful flatness is used only through universal injectivity (Tag 08WL), which is the hypothesis here.

noncomputable def baseExtensionUnitEquiv
    (h : Algebra.UniversallyInjective R A) (M : ModuleCat.{max u w} R) :
    M ≃ₗ[R] invariantSubmodule R A
      ((baseExtension.{u, u, w} R A).functor.obj M)

Tag 039W, a lemma

Tag 039W in the Stacks Project.

ModuleCat.DescentData.isEffective_iff_canonicalMap_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/EffectiveCriterion.lean, line 560.

A module descent datum is effective if and only if its canonical map from the base change of its zeroth cohomology is an isomorphism.

public theorem isEffective_iff_canonicalMap_bijective
    [Module.FaithfullyFlat R A] :
    IsEffective R A D ↔
      Function.Bijective (canonicalMap R A D)

Tag 039X, a lemma

Tag 039X in the Stacks Project.

ModuleCat.all_isEffective_of_faithfullyFlat_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/BaseChangeEffective.lean, line 49.

Stacks Project, Tag 039X. Let R → A be a faithfully flat ring map and let R → R' be faithfully flat, and set A' = R' ⊗[R] A. If all descent data for R' → A' are effective, then so are all descent data for R → A.

public theorem all_isEffective_of_faithfullyFlat_baseChange
    (R A R' : Type u) [CommRing R] [CommRing A] [CommRing R']
    [Algebra R A] [Algebra R R']
    (hA : (algebraMap R A).FaithfullyFlat)
    (_hR' : (algebraMap R R').FaithfullyFlat)
    (_h : ∀ D : DescentData.{u, u, w} R' (R' ⊗[R] A), D.IsEffective R' (R' ⊗[R] A)) :
    ∀ D : DescentData.{u, u, x} R A, D.IsEffective R A

Tag 023N, a proposition

Tag 023N in the Stacks Project.

ModuleCat.isEffectiveDescentMorphismForModules_of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Modules/FaithfullyFlatEffective.lean, line 95. The attribute's comment: “(2)”. References: SGA 1 VIII (1.6), “effectivity”; SGA 1 VIII (1.1), “affine case”; SGA 4½ Arcata (1.4.5), “affine case”; SGA 4½ Arcata (1.4), “module equivalence”.

Stacks 023N, part (2). For a faithfully flat ring map R → A, base extension M ↦ (A ⊗[R] M, can) is an equivalence from R-modules onto the category of descent data for modules along R → A.

theorem isEffectiveDescentMorphismForModules_of_faithfullyFlat :
    IsEffectiveDescentMorphismForModules.{u, u, w} R A

ModuleCat.baseExtension_essSurj_of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Modules/FaithfullyFlatEffective.lean, line 106. The attribute's comment: “(1)”. References: SGA 1 VIII (1.6), “effectivity”; SGA 1 VIII (1.1), “affine case, effectivity”; SGA 4½ Arcata (1.4.5), “ess. surj. (affine)”.

Stacks 023N, part (1). Every descent datum on modules along a faithfully flat ring map R → A is effective, that is, lies in the essential image of base extension.

theorem baseExtension_essSurj_of_faithfullyFlat :
    (baseExtension.{u, u, w} R A).functor.EssSurj

ModuleCat.DescentData.isEffective_of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Modules/FaithfullyFlatEffectiveDescent.lean, line 84. The attribute's comment: “effectivity of descent data”. References: SGA 1 VIII (1.1), “affine case”; SGA 1 VIII (1.6), “effectivity”; SGA 4½ Arcata (1.4.5), “ess. surj. (affine)”; SGA 4½ Arcata (1.4), “module case”.

Stacks 023N, part (1). Every descent datum for modules along a faithfully flat ring map R → A is effective: it is isomorphic, as a descent datum, to the canonical datum on the extension of scalars of an R-module.

public theorem DescentData.isEffective_of_faithfullyFlat
    (D : DescentData.{u, u, max u w} R A) : D.IsEffective R A

Stacks.Descent.faithfullyFlatInvariantsEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Modules/InvariantsInverseFunctor.lean, line 283. The attribute's comment: “(3)”. References: SGA 1 VIII (1.6), “more general”.

Stacks 023N, part (3). For a faithfully flat ring map R → A the functor M ↦ (A ⊗[R] M, can) from R-modules to descent data for modules along R → A is an equivalence whose inverse functor is (N, φ) ↦ H⁰(s(N_•)), the kernel of the descent complex. Only part (3) is registered here; part (2), that the functor is an equivalence, is ModuleCat.isEffectiveDescentMorphismForModules_of_faithfullyFlat.

def faithfullyFlatInvariantsEquivalence [Module.FaithfullyFlat R A] :
    ModuleCat.{max u w} R ≌ DescentData.{u, u, max u w} R A

Stacks.Descent.faithfullyFlatInvariantsEquivalence_inverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Modules/InvariantsInverseFunctor.lean, line 295. The attribute's comment: “(3)”.

Stacks 023N, part (3). The inverse functor of the equivalence of Stacks 023N is ModuleCat.pushforward, that is (N, φ) ↦ H⁰(s(N_•)).

theorem faithfullyFlatInvariantsEquivalence_inverse [Module.FaithfullyFlat R A] :
    (faithfullyFlatInvariantsEquivalence.{u, w} R A).inverse = pushforward R A

Tag 023O, a remark

Tag 023O in the Stacks Project.

PrimeSpectrum.faithfullyFlat_standardCoverAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/StandardCoverAlgebra.lean, line 230. The attribute's comment: “faithfully flat product”.

The product of the principal localizations of a standard cover is faithfully flat.

public theorem faithfullyFlat_standardCoverAlgebra
    (hf : PrimeSpectrum.IsStandardOpenCoverOfSpectrum f) :
    Module.FaithfullyFlat R (∀ i : Fin m, Localization.Away (f i))

PrimeSpectrum.standardCoverCechDegreeEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/StandardCoverAlgebra.lean, line 332. The attribute's comment: “degree-wise Čech algebra”.

In degree d, the Čech algebra of a standard cover is the product of the localizations at all (d + 1)-fold products of its covering elements.

public noncomputable def standardCoverCechDegreeEquiv (d : ℕ) :
    ((Arrow.mk (CommAlgCat.ofHom
      (Algebra.ofId R (∀ i : Fin m, Localization.Away (f i))))).cechConerve).obj
        (SimplexCategory.mk d) ≃ₐ[R]
      (∀ i : Fin (d + 1) → Fin m, Localization.Away (∏ j, f (i j)))

Declarations registered for the tag:

Stacks.Cohomology.Cech.isZero_cechCohomology_of_isStandardOpenCover, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/StandardCoverAlgebra.lean, line 341 (StacksFrontier): “Čech cohomology vanishing”.

Tag 039Y, a remark

Tag 039Y in the Stacks Project.

ModuleCat.descentDataEquivCartesianCechModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Module/CartesianCechEquivalence.lean, line 1274. The attribute's comment: “(2): descent data for A / R correspond to cartesian (A / R)_•-modules, through the cosimplicial module of a descent datum of Stacks 023H”.

Let A be an R-algebra. Descent data for A / R correspond to cartesian (A / R)_•-modules: the functor (N, φ) ↦ N_•, sending a descent datum to its cosimplicial module over the Čech algebra (A / R)_• (N_n = N_{n, n}, N_•(β) = φᵐ_{β(n), m} ∘ N_{β, n}), is an equivalence of categories between descent data and cartesian (A / R)_•-modules. Its inverse sends a cartesian module M to M_0 with the transition M_0 ⊗_R A ≅ M_1 ≅ A ⊗_R M_0 read off from the cartesian isomorphisms along the two cofaces ⦋0⦌ ⟶ ⦋1⦌ (ModuleCat.cartesianDescentDataFunctor). No flatness is assumed.

noncomputable def descentDataEquivCartesianCechModule :
    DescentData.{u, u, max u w} R A ≌ CartesianCechModule.{u, u, max u w} R A

CategoryTheory.Arrow.cechConerve_homotopyEquivalent_const_of_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Module/CechConerve.lean, line 118. The attribute's comment: “split_cech_homotopy”.

A split Čech conerve is homotopy equivalent to the constant cosimplicial object on the base. For commutative R-algebras this is the split Čech algebra (A/R)• and the constant algebra R.

theorem cechConerve_homotopyEquivalent_const_of_section
    {C : Type u} [Category.{v} C] (f : Arrow C)
    [∀ n : ℕ, HasWidePushout f.left (fun _ : Fin (n + 1) => f.right) fun _ => f.hom]
    (h : ∃ s : f.right ⟶ f.left, f.hom ≫ s = 𝟙 f.left) :
    ∃ a : f.cechConerve.op ⟶ ((CosimplicialObject.const C).obj f.left).op,
      SimplicialObject.homotopyEquivalences Cᵒᵖ a

CategoryTheory.CosimplicialModule.Cartesian, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Module/Cosimplicial.lean, line 74. The attribute's comment: “cartesian_module”.

A cosimplicial module is cartesian when every cosimplicial transition map induces an isomorphism after extension of scalars.

abbrev Cartesian (M : CosimplicialModule A) : Prop

CategoryTheory.CosimplicialModule.isEquivalence_cartesianBaseChange_of_homotopyEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Module/CosimplicialCartesian.lean, line 651. The attribute's comment: “(4): base change along a homotopy equivalence of cosimplicial algebras is an equivalence of the categories of cartesian modules”.

Stacks 039Y (4). If α : A_• ⟶ B_• is a homotopy equivalence of cosimplicial R-algebras, then the functor M_• ↦ M_• ⊗_{A_•} B_• is an equivalence of categories between the cartesian A_•-modules and the cartesian B_•-modules.

A homotopy equivalence is taken in the sense of Simplicial, Definition 019N, through the opposite category (cosimplicial homotopies being simplicial homotopies of the opposite objects, Simplicial, Lemma 019X), exactly as in Stacks 039Y (3) here (CategoryTheory.Arrow.cechConerve_homotopyEquivalent_const_of_section). The proof is the source's "triviality": base change along homotopic morphisms gives isomorphic functors (CategoryTheory.CosimplicialModule.nonempty_iso_cartesianBaseChange_of_homotopic), so a homotopy inverse β makes base change along α ≫ β and along β ≫ α isomorphic to the identities, and base change is functorial (CategoryTheory.CosimplicialModule.cartesianBaseChangeCompIso).

theorem isEquivalence_cartesianBaseChange_of_homotopyEquivalence (α : A ⟶ B)
    (hα : SimplicialObject.homotopyEquivalences (CommAlgCat.{v, u} R)ᵒᵖ (NatTrans.op α)) :
    (cartesianBaseChange.{u, v, w} α).IsEquivalence

ModuleCat.all_isEffective_of_faithfullyFlat_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/BaseChangeEffective.lean, line 49. The attribute's comment: “(1): descent data for A / R are effective once those for (R' ⊗ A) / R' are”.

Stacks Project, Tag 039X. Let R → A be a faithfully flat ring map and let R → R' be faithfully flat, and set A' = R' ⊗[R] A. If all descent data for R' → A' are effective, then so are all descent data for R → A.

public theorem all_isEffective_of_faithfullyFlat_baseChange
    (R A R' : Type u) [CommRing R] [CommRing A] [CommRing R']
    [Algebra R A] [Algebra R R']
    (hA : (algebraMap R A).FaithfullyFlat)
    (_hR' : (algebraMap R R').FaithfullyFlat)
    (_h : ∀ D : DescentData.{u, u, w} R' (R' ⊗[R] A), D.IsEffective R' (R' ⊗[R] A)) :
    ∀ D : DescentData.{u, u, x} R A, D.IsEffective R A

Sources

LeanModuleCat.DescentData · ModuleCat.DescentData.Hom · ModuleCat.exists_descentCosimplicialModuleFunctor · ModuleCat.descentCosimplicialModuleFunctor · ModuleCat.cechTensorModule · ModuleCat.canonicalDescent_cosimplicialModule · ModuleCat.DescentData.IsEffective · Stacks.Descent.augmentedDescentComplex

Section35.4 Descent for universally injective morphisms #

Section 35.4 of the Stacks Project, Tag 08WE. 23 tags here are carried by 39 declarations of the repository (all in StacksFrontier) and 10 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08WG, an equation

Tag 08WG in the Stacks Project.

Stacks.Descent.IsEqualizerDiagram, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/UniversallyInjective/EqualizerDiagram.lean, line 60. The attribute's comment: “the displayed diagram is an equalizer”.

The diagram A ⟶ B ⇉ C consisting of f : A ⟶ B and a parallel pair g₁, g₂ : B ⟶ C is an equalizer: the two composites f ≫ g₁ and f ≫ g₂ agree, and f is universal for that property, meaning that every e : A' ⟶ B equalizing g₁ and g₂ factors as e = d ≫ f for a unique d : A' ⟶ A.

structure IsEqualizerDiagram (f : A ⟶ B) (g₁ g₂ : B ⟶ C) : Prop

Tag 08WH, a definition

Tag 08WH in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.IsSplitEqualizer registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch35.lean, line 19 (StacksFrontier): “as a structure carrying h and i; 'is a split equalizer' is its Nonempty”.

Tag 08WK, a remark

Tag 08WK in the Stacks Project.

CategoryTheory.Functor.reflectsMonomorphisms_of_preservesFiniteLimits_of_reflectsZeroObjects, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/UniversallyInjective/Exactness.lean, line 59. The attribute's comment: “monomorphisms”.

A left exact functor between abelian categories which reflects zero objects reflects monomorphisms.

theorem reflectsMonomorphisms_of_preservesFiniteLimits_of_reflectsZeroObjects
    (F : A ⥤ B) [PreservesFiniteLimits F]
    (hF : ∀ X, IsZero (F.obj X) → IsZero X) : F.ReflectsMonomorphisms

CategoryTheory.Functor.reflectsEpimorphisms_of_preservesFiniteColimits_of_reflectsZeroObjects, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/UniversallyInjective/Exactness.lean, line 68. The attribute's comment: “epimorphisms”.

A right exact functor between abelian categories which reflects zero objects reflects epimorphisms.

theorem reflectsEpimorphisms_of_preservesFiniteColimits_of_reflectsZeroObjects
    (F : A ⥤ B) [PreservesFiniteColimits F]
    (hF : ∀ X, IsZero (F.obj X) → IsZero X) : F.ReflectsEpimorphisms

ModuleCat.extendScalars_isZero_iff_of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/UniversallyInjective/Exactness.lean, line 83. The attribute's comment: “faithfully flat extension of scalars detects zero objects”. References: EGA IV (2.2.7), “special case”.

Extension of scalars along a faithfully flat ring homomorphism detects zero modules.

theorem extendScalars_isZero_iff_of_faithfullyFlat (f : R →+* S)
    (hf : f.FaithfullyFlat) (M : ModuleCat.{u} R) :
    IsZero ((ModuleCat.extendScalars f).obj M) ↔ IsZero M

ModuleCat.extendScalars_reflectsMonomorphisms_of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/UniversallyInjective/Exactness.lean, line 95. The attribute's comment: “faithfully flat extension of scalars reflects monomorphisms”. References: SGA 1 IV (2.1), “special case”; SGA 4½ Arcata (1.4.2), “Clause (i), special case”.

Extension of scalars along a faithfully flat ring homomorphism reflects monomorphisms.

theorem extendScalars_reflectsMonomorphisms_of_faithfullyFlat (f : R →+* S)
    (hf : f.FaithfullyFlat) :
    (ModuleCat.extendScalars.{u, u, u} f).ReflectsMonomorphisms

ModuleCat.extendScalars_reflectsEpimorphisms_of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/UniversallyInjective/Exactness.lean, line 105. The attribute's comment: “faithfully flat extension of scalars reflects epimorphisms”. References: SGA 1 IV (2.1), “special case”.

Extension of scalars along a faithfully flat ring homomorphism reflects epimorphisms.

theorem extendScalars_reflectsEpimorphisms_of_faithfullyFlat (f : R →+* S)
    (hf : f.FaithfullyFlat) :
    (ModuleCat.extendScalars.{u, u, u} f).ReflectsEpimorphisms

Declarations registered for the tag:

ModuleCat.preservesFiniteLimits_extendScalars_of_flat registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Descent/UniversallyInjective/Exactness.lean, line 47 (StacksFrontier): “exactness of extension of scalars”. References: EGA 0 (20.6.21), “partial”.

Tag 08WL, a definition

Tag 08WL in the Stacks Project.

Algebra.UniversallyInjective, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/UniversallyInjective/Defs.lean, line 45.

A ring map R → S is universally injective as a map of R-modules: for every R-module Q, the map (Algebra.linearMap R S) ⊗ id_Q is injective.

def Algebra.UniversallyInjective (R : Type u) [CommRing R] (S : Type u) [CommRing S]
    [Algebra R S] : Prop

Tag 08WM, an example

Tag 08WM in the Stacks Project.

UniversallyInjective.of_split, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/UniversallyInjective/Defs.lean, line 51. The attribute's comment: “module maps”.

A split injection of modules is universally injective.

theorem UniversallyInjective.of_split
    {R : Type u} [CommRing R]
    {M N : Type v} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N]
    (f : M →ₗ[R] N) (g : N →ₗ[R] M) (h : g.comp f = LinearMap.id) :
    UniversallyInjective f

Algebra.UniversallyInjective.of_split, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/UniversallyInjective/Defs.lean, line 62. The attribute's comment: “ring maps”.

A split ring map is universally injective.

theorem Algebra.UniversallyInjective.of_split
    (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
    (g : S →+* R) (h : g.comp (algebraMap R S) = RingHom.id R) :
    Algebra.UniversallyInjective R S

Tag 08WN, an example

Tag 08WN in the Stacks Project.

Algebra.UniversallyInjective.pi_localizationAway, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/UniversallyInjective/Localization.lean, line 107.

A family of principal localizations covering Spec R yields a universally injective canonical map from R to their product.

theorem Algebra.UniversallyInjective.pi_localizationAway
    {R : Type u} [CommRing R] {ι : Type u} (f : ι → R)
    (hspan : Ideal.span (Set.range f) = ⊤) :
    Algebra.UniversallyInjective R (∀ i : ι, Localization.Away (f i))

Tag 08WP, a lemma

Tag 08WP in the Stacks Project.

Declarations registered for the tag:

faithfullyFlat_universallyInjective, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Descent/UniversallyInjective/Defs.lean, line 73 (StacksFrontier).

Tag 08WQ, a definition

Tag 08WQ in the Stacks Project.

CharacterModule.dualFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/CharacterModule/Duality.lean, line 55.

The contravariant functor M ↦ M^∨ = Hom_ℤ(M, ℚ/ℤ) on modules over a commutative ring, acting on a linear map by precomposition (CharacterModule.dual).

noncomputable def dualFunctor (R : Type u) [CommRing R] :
    (ModuleCat.{u} R)ᵒᵖ ⥤ ModuleCat.{u} R

Tag 08WR, a lemma

Tag 08WR in the Stacks Project.

Declarations registered for the tag:

CharacterModule.dual_exact, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Descent/UniversallyInjective/CharacterModule.lean, line 61 (StacksFrontier): “exactness”.
CharacterModule.dual_surjective_iff_injective registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Descent/UniversallyInjective/CharacterModule.lean, line 63 (StacksFrontier): “reflection of injections”.
CharacterModule.dual_injective_iff_surjective registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Descent/UniversallyInjective/CharacterModule.lean, line 66 (StacksFrontier): “reflection of surjections”.

Tag 08WS, a remark

Tag 08WS in the Stacks Project.

CharacterModule.dual_map_conj_homEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/UniversallyInjective/TensorHomAdjunction.lean, line 74. The attribute's comment: “naturality of the adjunction isomorphism”.

Stacks 08WS. The adjunction isomorphism C(• ⊗_R •) ≅ Hom_R(•, C(•)) is natural in both variables: conjugating C(f ⊗ g) by it gives φ ↦ C(g) ∘ φ ∘ f.

theorem dual_map_conj_homEquiv (f : M₁ →ₗ[R] M₁') (g : M₂ →ₗ[R] M₂') :
    homEquiv.symm.toLinearMap ∘ₗ dual (TensorProduct.map f g) ∘ₗ homEquiv.toLinearMap =
      LinearMap.compRight R (dual g) ∘ₗ LinearMap.lcomp R (CharacterModule M₂') f

CharacterModule.isSplitCoequalizer_dual_rTensor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/UniversallyInjective/TensorHomAdjunction.lean, line 178. The attribute's comment: “split coequalizers of character modules are preserved by tensoring inside C”.

Stacks 08WS, the corollary of the adjunction. If C(M) ⇉ C(N) → C(P) is a split coequalizer diagram of R-modules, the arrows being the character-module duals of u, v : N → M and w : P → N, then so is C(M ⊗_R Q) ⇉ C(N ⊗_R Q) → C(P ⊗_R Q), for any R-module Q.

noncomputable def isSplitCoequalizer_dual_rTensor (u v : N →ₗ[R] M) (w : P →ₗ[R] N)
    (q : IsSplitCoequalizer (ModuleCat.ofHom (dual u)) (ModuleCat.ofHom (dual v))
      (ModuleCat.ofHom (dual w))) :
    IsSplitCoequalizer (ModuleCat.ofHom (dual (u.rTensor Q)))
      (ModuleCat.ofHom (dual (v.rTensor Q))) (ModuleCat.ofHom (dual (w.rTensor Q)))

Declarations registered for the tag:

CharacterModule.homEquiv registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Descent/UniversallyInjective/TensorHomAdjunction.lean, line 222 (StacksFrontier): “adjunction isomorphism”. References: SGA 5 IIIB (5.2), “5.2.1 with K = B = Z”.
CharacterModule.homEquiv_symm_apply_apply_apply registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Descent/UniversallyInjective/TensorHomAdjunction.lean, line 225 (StacksFrontier): “the displayed formula for the isomorphism”.

Tag 08WU, a lemma

Tag 08WU in the Stacks Project.

universallyInjective_iff_dual_splitSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/UniversallyInjective/CharacterModule.lean, line 91.

A module map is universally injective exactly when its character-module dual admits a linear section.

theorem universallyInjective_iff_dual_splitSurjective
    {R : Type u} [CommRing R]
    {M N : Type v} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N]
    (f : M →ₗ[R] N) :
    UniversallyInjective f ↔
      ∃ s : CharacterModule M →ₗ[R] CharacterModule N,
        (CharacterModule.dual f).comp s = LinearMap.id

Tag 08WV, a remark

Tag 08WV in the Stacks Project.

exists_functorialCharacterModuleSplitting, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/UniversallyInjective/CharacterModule.lean, line 128.

A universally injective map admits a section after applying the character module functor, and the section obtained on C(P ⊗ -) by postcomposition is a splitting functorial in the module P.

theorem exists_functorialCharacterModuleSplitting
    {R : Type u} [CommRing R]
    {M N : Type v} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
    (f : M →ₗ[R] N) (hf : UniversallyInjective f) :
    ∃ g : CharacterModule M →ₗ[R] CharacterModule N,
      CharacterModule.dual f ∘ₗ g = LinearMap.id ∧
      (∀ (P : Type v) [AddCommGroup P] [Module R P],
        CharacterModule.dual (LinearMap.lTensor P f) ∘ₗ
            functorialCharacterModuleSection g P =
          LinearMap.id) ∧
      ∀ (P Q : Type v) [AddCommGroup P] [Module R P]
        [AddCommGroup Q] [Module R Q] (h : P →ₗ[R] Q),
        functorialCharacterModuleSection g P ∘ₗ
            CharacterModule.dual (LinearMap.rTensor M h) =
          CharacterModule.dual (LinearMap.rTensor N h) ∘ₗ
            functorialCharacterModuleSection g Q

Tag 08WX, an equation

Tag 08WX in the Stacks Project.

ModuleCat.DescentData, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Module/DescentData.lean, line 244. The attribute's comment: “the cocycle condition, as the cocycle field”.

A descent datum for modules for an R-algebra A.

The transition is bundled as an A ⊗[R] A-linear equivalence, and cocycle is the equality φ₁₂ ∘ φ₀₁ = φ₀₂.

structure DescentData

Tag 08WY, a definition

Tag 08WY in the Stacks Project.

ModuleCat.baseExtension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Module/BaseExtension.lean, line 236. The attribute's comment: “the functor”.

Stacks Project, Tag 08WY. The base-extension functor from R-modules to descent data for modules along R → A, bundled with its canonical objectwise description.

def baseExtension : BaseExtension.{u, v, w} R A

ModuleCat.IsDescentMorphismForModules, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Module/BaseExtension.lean, line 252. The attribute's comment: “descent morphism”.

Stacks Project, Tag 08WY. An algebra map is a descent morphism for modules when its base-extension functor is fully faithful.

abbrev IsDescentMorphismForModules : Prop

ModuleCat.IsEffectiveDescentMorphismForModules, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Module/BaseExtension.lean, line 260. The attribute's comment: “effective descent morphism”. References: SGA 4 Vbis (2.4.10), “modules over a ring map”; SGA 4 Vbis (2.2.2), “modules over rings”.

Stacks Project, Tag 08WY. An algebra map is an effective descent morphism for modules when its base-extension functor is an equivalence of categories.

abbrev IsEffectiveDescentMorphismForModules : Prop

Tag 08WZ, a lemma

Tag 08WZ in the Stacks Project.

ModuleCat.DescentData.isSplitEqualizer_descentComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Module/SplitEqualizer.lean, line 457.

Stacks Project, Tag 08WZ. The canonically associated diagram is a split equalizer of A-modules.

theorem isSplitEqualizer_descentComparison
    (D : DescentData.{u, v, w} R A) :
    Nonempty (IsSplitEqualizer
      (ModuleCat.ofHom (transition12AfterUnitHom R A D))
      (ModuleCat.ofHom (rightUnitBaseChangeHom R A D))
      (ModuleCat.ofHom (descentComparisonHom R A D)))

ModuleCat.DescentData.isSplitEqualizer_inverseTransitionUnitHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Module/TransitionSplitEqualizer.lean, line 602.

Stacks Project, Tag 08WZ. For a descent datum (M, θ) relative to R → S, the diagram
      θ ∘ (1 ⊗ δ₀¹)                    (θ ⊗ δ₂²) ∘ (1 ⊗ δ₀²)
  M ---------------> M ⊗_{S, δ₁¹} S₂ ========================> M ⊗_{S, δ₁₂¹} S₃
                                            1 ⊗ δ₁²
is a split equalizer of S-modules. Here M ⊗_{S, δ₁¹} S₂ = N ⊗[R] A and M ⊗_{S, δ₁₂¹} S₃ = (N ⊗[R] A) ⊗[R] A, on which S acts through the last tensor factor, and θ is inverseTransition, the inverse of the transition isomorphism; see the module docstring for the identifications. The auxiliary maps are 1 ⊗ σ₀⁰ and 1 ⊗ σ₀¹, see inverseTransitionUnitSplitEqualizer.

theorem isSplitEqualizer_inverseTransitionUnitHom (D : DescentData.{u, v, w} R A) :
    Nonempty (IsSplitEqualizer (inverseTransition01AfterUnitHom D) (middleUnitInsertionHom D)
      (inverseTransitionUnitHom D))

Tag 08X1, a lemma

Tag 08X1 in the Stacks Project.

ModuleCat.DescentData.isSplitCoequalizer_characterModule_descentComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Module/SplitEqualizer.lean, line 523.

Stacks Project, Tag 08X1. Character duality turns the descent equalizer into a split coequalizer.

theorem isSplitCoequalizer_characterModule_descentComparison
    (D : DescentData.{u, v, w} R A) :
    Nonempty (IsSplitCoequalizer
      (ModuleCat.ofHom (CharacterModule.dual (transition12AfterUnitHom R A D)))
      (ModuleCat.ofHom (CharacterModule.dual (rightUnitBaseChangeHom R A D)))
      (ModuleCat.ofHom (CharacterModule.dual (descentComparisonHom R A D))))

Tag 08X3, a lemma

Tag 08X3 in the Stacks Project.

Stacks.Descent.isSplitEqualizerTensorInsertOne, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Module/TensorPowerSplitEqualizer.lean, line 83.

Stacks Project, Tag 08X3. The diagram S₁ --δ¹₁--> S₂ ⇉ S₃ of tensor powers of A over R, whose parallel arrows are δ²₂ and δ²₁, is a split equalizer of commutative R-algebras. Its splittings are the codegeneracy maps σ⁰₀ and σ¹₀.

noncomputable def isSplitEqualizerTensorInsertOne :
    IsSplitEqualizer (tensorInsertOne R A 1 2) (tensorInsertOne R A 1 1)
      (tensorInsertOne R A 0 1)

Tag 08X5, a definition

Tag 08X5 in the Stacks Project.

ModuleCat.pushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Module/Pushforward.lean, line 78.

Pushforward sends a module descent datum to the equalizer of its two pullbacks to A ⊗[R] A.

def pushforward : DescentData.{u, v, w} R A ⥤ ModuleCat.{w} R

Tag 08X7, a lemma

Tag 08X7 in the Stacks Project.

ModuleCat.tensorPushforwardComparison_tmul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Modules/TensorEqualizer/Comparison.lean, line 302. The attribute's comment: “comparison formula”.

Under tensor symmetry, the first arrow applies the descent transition to the unit pullback of the scalar multiple of an invariant section.

public theorem tensorPushforwardComparison_tmul
    (D : DescentData.{u, v, w} R A)
    (a : A) (m : invariantSubmodule R A D) :
    tensorPushforwardComparison R A D (a ⊗ₜ[R] m) =
      D.transitionRestrictScalars R A
        ((a • (m.1 : restrictModule R A D.module)) ⊗ₜ[R] (1 : A))

ModuleCat.tensorPushforwardComparison_condition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Modules/TensorEqualizer/Comparison.lean, line 320. The attribute's comment: “fork condition”.

The base-changed inclusion equalizes the two pullbacks of a descent datum.

public theorem tensorPushforwardComparison_condition
    (D : DescentData.{u, v, w} R A) :
    ModuleCat.ofHom (tensorPushforwardComparison R A D) ≫
        ModuleCat.ofHom (DescentData.transition12AfterUnitHom R A D) =
      ModuleCat.ofHom (tensorPushforwardComparison R A D) ≫
        ModuleCat.ofHom (DescentData.rightUnitBaseChangeHom R A D)

ModuleCat.tensorPushforward_isEqualizer, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Modules/TensorEqualizer/Equalizer.lean, line 536. The attribute's comment: “equalizer”.

For a universally injective ring map, the displayed diagram of A-modules is an equalizer. The middle and right objects and both parallel arrows use the canonical identifications from the descent datum.

public noncomputable def tensorPushforward_isEqualizer
    (h : Stacks.UniversalInjectivity.LocalizationCriteria.UniversallyInjective.{u}
      (Algebra.linearMap R A))
    (D : DescentData.{u, v, w} R A) :
    CategoryTheory.Limits.IsLimit
      (CategoryTheory.Limits.Fork.ofι
        (ModuleCat.ofHom (tensorPushforwardComparison R A D))
        (tensorPushforwardComparison_condition R A D))

Tag 08XA, a theorem

Tag 08XA in the Stacks Project.

ModuleCat.isDescentMorphismForModules_iff_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Modules/EffectiveDescent.lean, line 689. The attribute's comment: “descent morphism”.

A ring map is a descent morphism for modules exactly when it is universally injective.

public theorem isDescentMorphismForModules_iff_universallyInjective :
    IsDescentMorphismForModules.{u, u, w} R A ↔
      Algebra.UniversallyInjective R A

ModuleCat.isEffectiveDescentMorphismForModules_iff_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Modules/EffectiveDescent.lean, line 697. The attribute's comment: “effective descent morphism”.

A ring map is an effective descent morphism for modules exactly when it is universally injective.

public theorem isEffectiveDescentMorphismForModules_iff_universallyInjective :
    IsEffectiveDescentMorphismForModules.{u, u, w} R A ↔
      Algebra.UniversallyInjective R A

Tag 08XC, a lemma

Tag 08XC in the Stacks Project.

Declarations registered for the tag:

Module.Flat.iff_characterModule_injective registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch35.lean, line 24 (StacksFrontier): “Mathlib proves the equivalence, under [Small.{v} R]”. References: SGA 4 V (1.2), “(ii) ⇒ (i)”.
Module.Flat.iff_characterModule_baer registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch35.lean, line 26 (StacksFrontier): “universe-free form, with Module.Baer.injective”. References: SGA 4 V (1.2), “(ii) ⇒ (i)”.

Tag 08XD, a theorem

Tag 08XD in the Stacks Project.

Module.finite_iff_baseChange_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Modules/BaseChangeFiniteness.lean, line 53. The attribute's comment: “finite”. References: EGA IV (2.5.2), “(i), affine case”; EGA IV (2.5.4), “(i), affine case”; SGA 1 VIII (1.11), “finite type”; SGA 4½ Arcata (1.4.2), “(ii) finite type”.

Finite generation descends and ascends along a universally injective ring map.

theorem finite_iff_baseChange_of_universallyInjective
    {R : Type u} [CommRing R] {S : Type u} [CommRing S] [Algebra R S]
    (hRS : Algebra.UniversallyInjective R S)
    (M : Type v) [AddCommGroup M] [Module R M] :
    Module.Finite R M ↔ Module.Finite S (TensorProduct R S M)

Module.finitePresentation_iff_baseChange_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Modules/BaseChangeFiniteness.lean, line 213. The attribute's comment: “finite_presentation”. References: EGA IV (2.5.2), “(ii), affine case”; EGA IV (2.5.4), “(ii), affine case”; SGA 1 VIII (1.11), “finite presentation”; SGA 4½ Arcata (1.4.2), “(ii) finite presentation”.

Finite presentation descends and ascends along a universally injective ring map.

theorem finitePresentation_iff_baseChange_of_universallyInjective
    {R : Type u} [CommRing R] {S : Type u} [CommRing S] [Algebra R S]
    (hRS : Algebra.UniversallyInjective R S)
    (M : Type v) [AddCommGroup M] [Module R M] :
    Module.FinitePresentation R M ↔
    Module.FinitePresentation S (TensorProduct R S M)

Module.flat_iff_baseChange_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Modules/BaseChangeFlat.lean, line 204. The attribute's comment: “flat”.

Flatness descends and ascends along a universally injective ring map.

theorem flat_iff_baseChange_of_universallyInjective
    {R : Type u} [CommRing R] {S : Type u} [CommRing S] [Algebra R S]
    (hRS : Algebra.UniversallyInjective R S)
    (M : Type v) [AddCommGroup M] [Module R M] :
    Module.Flat R M ↔ Module.Flat S (TensorProduct R S M)

Module.faithfullyFlat_iff_baseChange_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Modules/BaseChangeFlat.lean, line 238. The attribute's comment: “faithfully_flat”. References: EGA 0 (6.6.3), “more general”.

Faithful flatness descends and ascends along a universally injective ring map.

theorem faithfullyFlat_iff_baseChange_of_universallyInjective
    {R : Type u} [CommRing R] {S : Type u} [CommRing S] [Algebra R S]
    (hRS : Algebra.UniversallyInjective R S)
    (M : Type v) [AddCommGroup M] [Module R M] :
    Module.FaithfullyFlat R M ↔ Module.FaithfullyFlat S (TensorProduct R S M)

Module.finite_projective_iff_baseChange_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Modules/BaseChangeProjective.lean, line 40. The attribute's comment: “finite_projective”.

Finite projectivity descends and ascends along a universally injective ring map.

theorem finite_projective_iff_baseChange_of_universallyInjective
    {R : Type u} [CommRing R] {S : Type u} [CommRing S] [Algebra R S]
    (hRS : Algebra.UniversallyInjective R S)
    (M : Type v) [AddCommGroup M] [Module R M] :
    (Module.Finite R M ∧ Module.Projective R M) ↔
      (Module.Finite S (TensorProduct R S M) ∧
        Module.Projective S (TensorProduct R S M))

Tag 08XE, a theorem

Tag 08XE in the Stacks Project.

Algebra.finiteType_iff_tensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Modules/AlgebraBaseChangeFiniteness.lean, line 53. The attribute's comment: “finite_type”. References: EGA IV (1.3.1), “special case”.

Stacks Project, Tag 08XE (finite type). Finite type descends along a universally injective ring map and is preserved by base change.

theorem finiteType_iff_tensorProduct
    (R S A : Type u) [CommRing R] [CommRing S] [CommRing A]
    [Algebra R S] [Algebra R A] (h : Algebra.UniversallyInjective R S) :
    Algebra.FiniteType R A ↔ Algebra.FiniteType S (A ⊗[R] S)

Algebra.finitePresentation_iff_baseChange_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Modules/AlgebraBaseChangeFiniteness.lean, line 146. The attribute's comment: “finite_presentation”.

Finite presentation of an algebra descends and ascends along a universally injective ring map.

theorem finitePresentation_iff_baseChange_of_universallyInjective
    {R : Type u} [CommRing R] {S : Type u} [CommRing S] [Algebra R S]
    (hRS : Algebra.UniversallyInjective R S)
    (A : Type u) [CommRing A] [Algebra R A] :
    Algebra.FinitePresentation R A ↔
      Algebra.FinitePresentation S (TensorProduct R S A)

Algebra.formallyUnramified_iff_tensorProduct_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Modules/AlgebraBaseChangeUnramified.lean, line 52. The attribute's comment: “formally_unramified”.

Formal unramifiedness descends and ascends along a universally injective base-ring map.

theorem formallyUnramified_iff_tensorProduct_of_universallyInjective
    (R S A : Type u) [CommRing R] [CommRing S] [CommRing A]
    [Algebra R S] [Algebra R A] (hRS : Algebra.UniversallyInjective R S) :
    Algebra.FormallyUnramified R A ↔
      Algebra.FormallyUnramified S (TensorProduct R A S)

Algebra.unramified_iff_baseChange_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Modules/AlgebraBaseChangeUnramified.lean, line 72. The attribute's comment: “unramified”.

Unramifiedness descends and ascends along a universally injective ring map.

theorem unramified_iff_baseChange_of_universallyInjective
    {R : Type u} [CommRing R] {S : Type u} [CommRing S] [Algebra R S]
    (hRS : Algebra.UniversallyInjective R S)
    (A : Type u) [CommRing A] [Algebra R A] :
    Algebra.Unramified R A ↔ Algebra.Unramified S (A ⊗[R] S)

Algebra.etale_iff_baseChange_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Modules/AlgebraBaseChangeUnramified.lean, line 91. The attribute's comment: “etale”.

Étaleness descends and ascends along a universally injective ring map.

theorem etale_iff_baseChange_of_universallyInjective
    {R : Type u} [CommRing R] {S : Type u} [CommRing S] [Algebra R S]
    (hRS : Algebra.UniversallyInjective R S)
    (A : Type u) [CommRing A] [Algebra R A] :
    Algebra.Etale R A ↔ Algebra.Etale S (TensorProduct R S A)

Sources

LeanStacks.Descent.IsEqualizerDiagram · CategoryTheory.IsSplitEqualizer · CategoryTheory.Functor.reflectsMonomorphisms_of_preservesFiniteLimits_of_reflectsZeroObjects · CategoryTheory.Functor.reflectsEpimorphisms_of_preservesFiniteColimits_of_reflectsZeroObjects · ModuleCat.extendScalars_isZero_iff_of_faithfullyFlat · ModuleCat.extendScalars_reflectsMonomorphisms_of_faithfullyFlat · ModuleCat.extendScalars_reflectsEpimorphisms_of_faithfullyFlat · ModuleCat.preservesFiniteLimits_extendScalars_of_flat

Section35.5 Fpqc descent of quasi-coherent sheaves #

Section 35.5 of the Stacks Project, Tag 023R. 2 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 023S, a lemma

Tag 023S in the Stacks Project.

AlgebraicGeometry.QuasicoherentDescentData.nonempty_fullyFaithful_canonicalDescentFunctor_standardFpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherent/StandardFpqc023S.lean, line 224. The attribute's comment: “full faithfulness”. References: SGA 1 VIII (1.1), “standard affine case”.

The full faithfulness half of [Stacks, Tag 023S]: let S be an affine scheme and let {f i : X i ⟶ S} be a standard fpqc covering of S in the sense of Stacks 022F. Then the functor from quasi-coherent O_S-modules to quasi-coherent descent data for the family is fully faithful.

The content is the unconditional …QuasicoherentDescentData.nonempty_fullyFaithful_canonicalDescentFunctor_of_mem_fpqcPrecoverage, which holds for an arbitrary fpqc covering family of an arbitrary scheme; all that is done here is to supply the covering hypothesis in the elementary form in which Stacks 022F states it, by AlgebraicGeometry.QuasicoherentDescentData.presieve₀_mem_fpqcPrecoverage_standardFpqc.

theorem nonempty_fullyFaithful_canonicalDescentFunctor_standardFpqc
    (𝒲 : PreZeroHypercover.{0} S) [Finite 𝒲.I₀] [∀ i, IsAffine (𝒲.X i)] [∀ i, Flat (𝒲.f i)]
    (hsurj : ⋃ i, Set.range (𝒲.f i) = Set.univ) :
    Nonempty (canonicalDescentFunctor 𝒲.f).FullyFaithful

AlgebraicGeometry.QuasicoherentDescentData.isEffective_standardFpqc_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherent/StandardFpqc023S.lean, line 245. The attribute's comment: “effectivity”. References: SGA 1 VIII (1.1), “standard affine case”; SGA 1 VIII (1.3), “Cor. 1.3, special case”.

The effectivity half of [Stacks, Tag 023S]: let S be an affine scheme and let {f i : X i ⟶ S} be a standard fpqc covering of S in the sense of Stacks 022F — a finite family of flat morphisms from affine schemes whose images cover S. Then every quasi-coherent descent datum for the family is effective, i.e. isomorphic to the canonical descent datum of a quasi-coherent module on S.

This is AlgebraicGeometry.QuasicoherentDescentData.isEffective_standardFpqc, whose base is literally of the form Spec R, transported to an arbitrary affine base along AlgebraicGeometry.Scheme.isoSpec. The transport runs in the vocabulary of Stacks.Descent.qcohPseudofunctor, where Stacks.Descent.essSurj_toDescentData_of_baseIso is available; see the implementation notes of this file.

theorem isEffective_standardFpqc_of_isAffine (𝒲 : PreZeroHypercover.{0} S) [Finite 𝒲.I₀]
    [∀ i, IsAffine (𝒲.X i)] [∀ i, Flat (𝒲.f i)]
    (hsurj : ⋃ i, Set.range (𝒲.f i) = Set.univ)
    (D : QuasicoherentDescentData 𝒲.f) : D.IsEffective

Tag 023T, a proposition

Tag 023T in the Stacks Project.

AlgebraicGeometry.nonempty_fullyFaithful_canonicalDescentFunctor', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FpqcHomSheafRefinement.lean, line 353. The attribute's comment: “the moreover assertion, full faithfulness”. References: SGA 1 VIII (1.1), “full faithfulness”.

For every fpqc covering family the functor from the quasi-coherent 𝒪_S-modules to the descent data with respect to that family is fully faithful.

theorem nonempty_fullyFaithful_canonicalDescentFunctor' {I : Type (u + 1)}
    {X : I → Scheme.{u}} (f : ∀ i, X i ⟶ S)
    (hfpqc : Presieve.ofArrows X f ∈ Scheme.fpqcPrecoverage.{u} S) :
    Nonempty (canonicalDescentFunctor f).FullyFaithful

AlgebraicGeometry.QuasicoherentDescentData.isEffective_fpqcPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherent/FpqcEffectiveUnconditional.lean, line 43. The attribute's comment: “effectivity, arbitrary fpqc covering family”. References: SGA 1 VIII (1.1), “effectivity”; SGA 4½ Arcata (1.4), “fpqc qcoh case”.

Every quasi-coherent descent datum for an fpqc covering family of an arbitrary scheme is effective, at an arbitrary index universe.

theorem isEffective_fpqcPrecoverage {S : Scheme.{u}} (𝒰 : PreZeroHypercover.{v} S)
    (h𝒰 : 𝒰.presieve₀ ∈ Scheme.fpqcPrecoverage.{u} S) (D : QuasicoherentDescentData 𝒰.f) :
    D.IsEffective

AlgebraicGeometry.QuasicoherentDescentData.isEquivalence_canonicalDescentFunctor_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherent/FpqcEffectiveUnconditional.lean, line 55. The attribute's comment: “both assertions in one statement: the canonical descent functor is an equivalence. The index universe is u + 1, fixed by the full-faithfulness half nonempty_fullyFaithful_canonicalDescentFunctor'; effectivity on its own is isEffective_fpqcPrecoverage above, at an arbitrary index universe”.

For an fpqc covering family of a scheme S, indexed in Type (u + 1), the canonical descent functor from the quasi-coherent 𝒪_S-modules to the descent data with respect to that family is an equivalence of categories.

theorem isEquivalence_canonicalDescentFunctor_fpqc {S : Scheme.{u}} {I : Type (u + 1)}
    {X : I → Scheme.{u}} (f : ∀ i, X i ⟶ S)
    (hfpqc : Presieve.ofArrows X f ∈ Scheme.fpqcPrecoverage.{u} S) :
    (canonicalDescentFunctor f).IsEquivalence

Sources

LeanAlgebraicGeometry.QuasicoherentDescentData.nonempty_fullyFaithful_canonicalDescentFunctor_standardFpqc · AlgebraicGeometry.QuasicoherentDescentData.isEffective_standardFpqc_of_isAffine · AlgebraicGeometry.nonempty_fullyFaithful_canonicalDescentFunctor' · AlgebraicGeometry.QuasicoherentDescentData.isEffective_fpqcPrecoverage · AlgebraicGeometry.QuasicoherentDescentData.isEquivalence_canonicalDescentFunctor_fpqc

Section35.6 Galois descent for quasi-coherent sheaves #

Section 35.6 of the Stacks Project, Tag 0CDQ. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0CDR, a lemma

Tag 0CDR in the Stacks Project.

Stacks.Descent.nonempty_equivalence_galoisDescentData_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherent/GaloisFieldExtension.lean, line 532.

Galois descent for quasi-coherent modules. For a finite Galois extension K/k with group G and a scheme X over k, the category of quasi-coherent 𝒪_X-modules is equivalent to the category of systems (ℱ, (φ_σ)_{σ ∈ G}) where ℱ is quasi-coherent on X_K, each φ_σ : ℱ ≅ f_σ^* ℱ is an isomorphism, and φ_(στ) = f_σ^*(φ_τ) ∘ φ_σ. Here f_σ = id_X × Spec σ.

theorem nonempty_equivalence_galoisDescentData_baseChange :
    Nonempty ((SheafOfModules.isQuasicoherent Z.left.ringCatSheaf).FullSubcategory ≌
      GaloisDescentData (K ≃ₐ[k] K) (baseChangeProjection k K Z)
        (baseChangeOverAction k K Z))

Tag 0D1V, a lemma

Tag 0D1V in the Stacks Project.

Stacks.Descent.nonempty_equivalence_galoisDescentData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherent/GaloisEquivalence.lean, line 968. References: SGA 4½ Arcata (1.5.1), “a), b), c) equivalence”.

Galois descent for quasi-coherent modules. For a surjective finite étale morphism f : X ⟶ Y carrying an action of a finite group G over Y which identifies ∐_{σ : G} X with X ×_Y X, quasi-coherent modules on Y are the same thing as Galois descent systems on X.

theorem nonempty_equivalence_galoisDescentData [IsFinite f] [Etale f] [Surjective f] :
    Nonempty ((SheafOfModules.isQuasicoherent Y.ringCatSheaf).FullSubcategory ≌
      GaloisDescentData G f a)

Sources

LeanStacks.Descent.nonempty_equivalence_galoisDescentData_baseChange · Stacks.Descent.nonempty_equivalence_galoisDescentData

Section35.7 Descent of finiteness properties of modules #

Section 35.7 of the Stacks Project, Tag 05AY. 10 tags here are carried by 12 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05AZ, a lemma

Tag 05AZ in the Stacks Project.

Stacks.AlgebraicGeometry.FlatBaseChange.isFiniteType_of_pullback_fpqcCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FlatBaseChange/Descent.lean, line 362.

Stacks Project, Tag 05AZ. Let X be a scheme and M a quasi-coherent 𝒪_X-module. If {f i : 𝒰.X i ⟶ X} is an fpqc covering of X such that every pullback (f i)^* M is of finite type, then M is of finite type.

theorem isFiniteType_of_pullback_fpqcCover {X : Scheme.{u}} (M : X.Modules) [M.IsQuasicoherent]
    (𝒰 : X.Cover.{v} Scheme.fpqcPrecoverage)
    (h : ∀ i, ((Scheme.Modules.pullback (𝒰.f i)).obj M).IsFiniteType) : M.IsFiniteType

Tag 09UB, a lemma

Tag 09UB in the Stacks Project.

AlgebraicGeometry.isFiniteType_of_isFiniteType_modulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/ModuleFiniteness/OpenFlatSurjective.lean, line 749.

Finite type of a sheaf of modules descends along an open, surjective, flat morphism of locally ringed spaces.

public theorem isFiniteType_of_isFiniteType_modulePullback
    {X Y : LocallyRingedSpace.{u}} (f : X ⟶ Y)
    (F : SheafOfModules.{u} (structureSheafRing Y.toRingedSpace))
    (hopen : IsOpenMap f.base) (hsurj : Function.Surjective f.base)
    (hflat : AlgebraicGeometry.IsFlat f.toShHom)
    (hF : ((modulePullback f.toShHom).obj F).IsFiniteType) :
    F.IsFiniteType

Tag 05B0, a lemma

Tag 05B0 in the Stacks Project.

AlgebraicGeometry.isFinitePresentation_of_pullback_fpqcCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Modules/FpqcFinitePresentation.lean, line 354. References: SGA 1 VIII (1.10), “finite presentation”.

A quasi-coherent module whose pullback to every member of an fpqc covering is finitely presented is itself finitely presented.

public theorem isFinitePresentation_of_pullback_fpqcCover
    {X : Scheme.{u}} (M : X.Modules) [M.IsQuasicoherent]
    (𝒰 : X.Cover.{v} Scheme.fpqcPrecoverage)
    (h : ∀ i, ((Scheme.Modules.pullback (𝒰.f i)).obj M).IsFinitePresentation) :
    M.IsFinitePresentation

Tag 082U, a lemma

Tag 082U in the Stacks Project.

AlgebraicGeometry.isCardinalGenerated_of_pullback_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/FittingGeneratorOpen/Descent.lean, line 142.

Being locally generated by r sections descends along an fpqc covering for quasi-coherent modules.

theorem isCardinalGenerated_of_pullback_fpqc {X : Scheme.{u}} (M : X.Modules)
    (hM : M.IsQuasicoherent) (r : ℕ) {I : Type v} (X' : I → Scheme.{u})
    (f : ∀ i, X' i ⟶ X)
    (hfpqc : Presieve.ofArrows X' f ∈ Scheme.fpqcPrecoverage X)
    (hgen : ∀ i, SheafOfModules.IsCardinalGenerated.{u}
      ((Scheme.Modules.pullback (f i)).obj M) (Cardinal.lift.{u, 0} r)) :
    SheafOfModules.IsCardinalGenerated.{u} M (Cardinal.lift.{u, 0} r)

Tag 05B1, a lemma

Tag 05B1 in the Stacks Project.

AlgebraicGeometry.isFlat_of_pullback_fpqc, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/ModuleFiniteness/Flat.lean, line 65.

A quasi-coherent module whose pullback to each member of an fpqc covering family is flat is itself flat.

public lemma isFlat_of_pullback_fpqc {S : Scheme.{u}} {I : Type v}
    {X : I → Scheme.{u}} (f : ∀ i, X i ⟶ S)
    (hfpqc : Presieve.ofArrows X f ∈ Scheme.fpqcPrecoverage S)
    (F : SheafOfModules.{u} (structureSheafRing S.toRingedSpace)) [F.IsQuasicoherent]
    (hF : ∀ i, SheafOfModules.IsFlat.{u, u, u, u} (O := (X i).toRingedSpace.sheaf)
      ((modulePullback (f i).toLRSHom.toShHom).obj F)) :
      SheafOfModules.IsFlat.{u, u, u, u} (O := S.toRingedSpace.sheaf) F

Tag 05B2, a lemma

Tag 05B2 in the Stacks Project.

AlgebraicGeometry.isFiniteLocallyFree_of_pullback_fpqcCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Modules/FiniteLocallyFreeDescent/Fpqc.lean, line 53. References: SGA 1 VIII (1.10), “finite locally free”.

Stacks Project, Tag 05B2. Let M be a quasi-coherent module on a scheme X and let 𝒰 be an fpqc covering of X. If the pullback of M to every member of 𝒰 is finite locally free, then M is finite locally free.

public theorem isFiniteLocallyFree_of_pullback_fpqcCover {X : Scheme.{u}} (M : X.Modules)
    [hqc : M.IsQuasicoherent] (𝒰 : X.Cover.{v} Scheme.fpqcPrecoverage)
    (h : ∀ i, SheafOfModules.IsFiniteLocallyFree.{u, u, u}
      ((Scheme.Modules.pullback (𝒰.f i)).obj M)) :
    SheafOfModules.IsFiniteLocallyFree.{u, u, u} M

Tag 05JZ, a lemma

Tag 05JZ in the Stacks Project.

AlgebraicGeometry.isLocallyProjective_of_pullback_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Modules/FpqcLocallyProjective.lean, line 191.

Stacks Project, Tag 05JZ. Local projectivity of a quasi-coherent module descends along an fpqc covering.

theorem isLocallyProjective_of_pullback_fpqc {X : Scheme.{u}} (F : X.Modules)
    (hF : F.IsQuasicoherent) {I : Type v} (X' : I → Scheme.{u}) (f : ∀ i, X' i ⟶ X)
    (hfpqc : Presieve.ofArrows X' f ∈ Scheme.fpqcPrecoverage X)
    (hprojective : ∀ i,
      Scheme.Modules.IsLocallyProjective ((Scheme.Modules.pullback (f i)).obj F)) :
    Scheme.Modules.IsLocallyProjective F

Tag 05VF, a remark

Tag 05VF in the Stacks Project.

Stacks.Examples.exists_faithfullyFlat_free_baseChange_directSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/LocallyFreeNotFpqcLocal.lean, line 326. The attribute's comment: “a countable direct sum of rank one locally free modules becomes free after a faithfully flat base change”.

Stacks 05VF. A countable direct sum of rank one locally free modules is projective and becomes free after a faithfully flat base change.

theorem exists_faithfullyFlat_free_baseChange_directSum {R : Type u} [CommRing R]
    (L : ℕ → Type u) [∀ n, AddCommGroup (L n)] [∀ n, Module R (L n)]
    (hL : ∀ n, Module.IsFiniteLocallyFreeOfRank R (L n) 1) :
    ∃ (S : Type u) (_ : CommRing S) (_ : Algebra R S),
      Module.Projective R (⨁ n, L n) ∧ Module.FaithfullyFlat R S ∧
        Module.Free S (S ⊗[R] (⨁ n, L n))

Stacks.Examples.exists_faithfullyFlat_free_baseChange_not_isLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Algebra/LocallyFreeNotFpqcLocal.lean, line 353. The attribute's comment: “being locally free does not descend along a faithfully flat ring map: a countable direct sum of rank one locally free modules which is not locally free still becomes free after the faithfully flat base change built here. That such a direct sum exists is Stacks 05WL, which the source cites and which is not formalized, so failure of local freeness is a hypothesis here and not a conclusion”.

Stacks 05VF. Being locally free does not descend along faithfully flat ring maps: a countable direct sum of rank one locally free modules which is not locally free still becomes free after a faithfully flat base change.

theorem exists_faithfullyFlat_free_baseChange_not_isLocallyFree {R : Type u} [CommRing R]
    (L : ℕ → Type u) [∀ n, AddCommGroup (L n)] [∀ n, Module R (L n)]
    (hL : ∀ n, Module.IsFiniteLocallyFreeOfRank R (L n) 1)
    (hM : ¬ Module.IsLocallyFree R (⨁ n, L n)) :
    ∃ (S : Type u) (_ : CommRing S) (_ : Algebra R S),
      Module.Projective R (⨁ n, L n) ∧ Module.FaithfullyFlat R S ∧
        Module.Free S (S ⊗[R] (⨁ n, L n)) ∧ ¬ Module.IsLocallyFree R (⨁ n, L n)

Tag 05B3, a lemma

Tag 05B3 in the Stacks Project.

AlgebraicGeometry.isFiniteType_iff_pushforward_isFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Finiteness/PushforwardFinite.lean, line 93.

A quasi-coherent module on the source of a finite morphism is of finite type if and only if its direct image is of finite type.

theorem isFiniteType_iff_pushforward_isFiniteType (f : X ⟶ Y) [IsFinite f] (F : X.Modules)
    [F.IsQuasicoherent] :
    F.IsFiniteType ↔ ((Scheme.Modules.pushforward f).obj F).IsFiniteType

Stacks.AlgebraicGeometry.FinitePushforwardCoherent.isFiniteType_pushforward_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FinitePushforwardCoherent/Basic.lean, line 147.

[Stacks, Tag 05B3]. A quasi-coherent module on the source of a finite morphism is of finite type if and only if its direct image is of finite type.

theorem isFiniteType_pushforward_iff [IsFinite f] [F.IsQuasicoherent] :
    F.IsFiniteType ↔ ((Scheme.Modules.pushforward f).obj F).IsFiniteType

Tag 05B4, a lemma

Tag 05B4 in the Stacks Project.

AlgebraicGeometry.isFinitePresentation_iff_pushforward_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/FinitePushforward.lean, line 69.

A quasi-coherent module on the source of a finite morphism of finite presentation is finitely presented if and only if its direct image is finitely presented.

public theorem isFinitePresentation_iff_pushforward_isFinitePresentation
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsFinite f]
    (hf : FinitePresentation f) (F : X.Modules) [F.IsQuasicoherent] :
    F.IsFinitePresentation ↔
      ((Scheme.Modules.pushforward f).obj F).IsFinitePresentation

Sources

LeanStacks.AlgebraicGeometry.FlatBaseChange.isFiniteType_of_pullback_fpqcCover · AlgebraicGeometry.isFiniteType_of_isFiniteType_modulePullback · AlgebraicGeometry.isFinitePresentation_of_pullback_fpqcCover · AlgebraicGeometry.isCardinalGenerated_of_pullback_fpqc · AlgebraicGeometry.isFlat_of_pullback_fpqc · AlgebraicGeometry.isFiniteLocallyFree_of_pullback_fpqcCover · AlgebraicGeometry.isLocallyProjective_of_pullback_fpqc · Stacks.Examples.exists_faithfullyFlat_free_baseChange_directSum

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

35.2 Descent data for… to 35.7 Descent of finiteness…

Section35.2 Descent data for quasi-coherent sheaves#

Tag 023B, a definition

Tag 023C, a lemma

Tag 023D, a definition

Tag 023E, a lemma

Sources

Section35.3 Descent for modules#

Tag 023G, a definition

Tag 023H, a lemma

Tag 023I, a lemma

Tag 023J, a definition

Tag 023K, an equation

Tag 023L, a lemma

Tag 023M, a lemma

Tag 039W, a lemma

Tag 039X, a lemma

Tag 023N, a proposition

Tag 023O, a remark

Tag 039Y, a remark

Sources

Section35.4 Descent for universally injective morphisms#

Tag 08WG, an equation

Tag 08WH, a definition

Tag 08WK, a remark

Tag 08WL, a definition

Tag 08WM, an example

Tag 08WN, an example

Tag 08WP, a lemma

Tag 08WQ, a definition

Tag 08WR, a lemma

Tag 08WS, a remark

Tag 08WU, a lemma

Tag 08WV, a remark

Tag 08WX, an equation

Tag 08WY, a definition

Tag 08WZ, a lemma

Tag 08X1, a lemma

Tag 08X3, a lemma

Tag 08X5, a definition

Tag 08X7, a lemma

Tag 08XA, a theorem

Tag 08XC, a lemma

Tag 08XD, a theorem

Tag 08XE, a theorem

Sources

Section35.5 Fpqc descent of quasi-coherent sheaves#

Tag 023S, a lemma

Tag 023T, a proposition

Sources

Section35.6 Galois descent for quasi-coherent sheaves#

Tag 0CDR, a lemma

Tag 0D1V, a lemma

Sources

Section35.7 Descent of finiteness properties of modules#

Tag 05AZ, a lemma

Tag 09UB, a lemma

Tag 05B0, a lemma

Tag 082U, a lemma

Tag 05B1, a lemma

Tag 05B2, a lemma

Tag 05JZ, a lemma

Tag 05VF, a remark

Tag 05B3, a lemma

Tag 05B4, a lemma

Sources

Section35.2 Descent data for quasi-coherent sheaves #

Section35.3 Descent for modules #

Section35.4 Descent for universally injective morphisms #

Section35.5 Fpqc descent of quasi-coherent sheaves #

Section35.6 Galois descent for quasi-coherent sheaves #

Section35.7 Descent of finiteness properties of modules #