NYLL
Module

Scheme_Modules_IsInvertible_exists_iso_toDescentData_of_isAffineHom_of_flat_of_surjective.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_iso_toDescentData_of_isAffineHom_of_flat_of_surjective
4 declarations indexed from sourceView source ↗

Module documentation

Descent of invertible modules along affine faithfully flat morphisms

Imports6
Imported by3

Declarations

theorem

isInvertible_of_iso

L50 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_iso_toDescentData_of_isAffineHom_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.InvDescAssembly.isInvertible_of_iso
Source context 19 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_iso_toDescentData_of_isAffineHom_of_flat_of_surjective
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply Algebra.DescentCofaces.i₂_apply Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul Algebra.DescentCofaces.c₁₃_tmul
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace InvDescAssembly
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
theorem isInvertible_of_iso {X : Scheme.{u}} {M N : X.Modules} (e : M ≅ N)
    (h : Scheme.Modules.IsInvertible M) : Scheme.Modules.IsInvertible N
theorem

isInvertible_of_forall_affineOpens

L56 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_iso_toDescentData_of_isAffineHom_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.InvDescAssembly.isInvertible_of_forall_affineOpens
Source context 19 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_iso_toDescentData_of_isAffineHom_of_flat_of_surjective
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply Algebra.DescentCofaces.i₂_apply Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul Algebra.DescentCofaces.c₁₃_tmul
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace InvDescAssembly
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
theorem isInvertible_of_forall_affineOpens {Y : Scheme.{u}} (L : Y.Modules)
    (h : ∀ U : Y.affineOpens,
      Scheme.Modules.IsInvertible ((Scheme.Modules.pullback (U : Y.Opens).ι).obj L)) :
    Scheme.Modules.IsInvertible L
def

affineOpensCover

L74 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_iso_toDescentData_of_isAffineHom_of_flat_of_surjective.AlgebraicGeometry.Scheme.Modules.InvDescAssembly.affineOpensCover
Documentation

The open cover of a scheme by all its affine open subsets.

Source context 19 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_iso_toDescentData_of_isAffineHom_of_flat_of_surjective
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
  Algebra.DescentCofaces.i₁_apply Algebra.DescentCofaces.i₂_apply Algebra.DescentCofaces.c₁₂_tmul
  Algebra.DescentCofaces.c₂₃_tmul Algebra.DescentCofaces.c₁₃_tmul
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace InvDescAssembly
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
def affineOpensCover (Y : Scheme.{u}) : Y.OpenCover
theorem

exists_iso_toDescentData_of_isAffineHom_of_flat_of_surjective

L99 ↗
AlgebraicGeometry.Scheme.Modules.IsInvertible.exists_iso_toDescentData_of_isAffineHom_of_flat_of_surjective
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicGeometry.Scheme.Modules.IsInvertible
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs in
open Scheme_Modules_IsInvertible_exists_iso_toDescentData_of_isAffineHom_of_flat_of_surjective in
open AlgebraicGeometry.Scheme.Modules.InvDescAssembly in
open _root_.CategoryTheory.Pseudofunctor.DescentData in
Lean source · full declaration
theorem exists_iso_toDescentData_of_isAffineHom_of_flat_of_surjective
    {Y Y' : Scheme.{u}} (q : Y' ⟶ Y) [IsAffineHom q] [Flat q] [Surjective q]
    (D : ((Scheme.Modules.pseudofunctor.{u}).comp Bicategory.Adj.forget₁).DescentData (fun _ : Unit
      => q))
    (hD : ∀ i, Scheme.Modules.IsInvertible (D.obj i)) :
    ∃ L : Y.Modules, Scheme.Modules.IsInvertible L ∧
      Nonempty ((((Scheme.Modules.pseudofunctor.{u}).comp Bicategory.Adj.forget₁).toDescentData
        (fun _ : Unit => q)).obj L ≅ D) := by
  have affineBaseChange : MorphismProperty.IsStableUnderBaseChange
      (fun {X Y : Scheme.{u}} (f : X ⟶ Y) => IsAffineHom f) :=
    isAffineHom_isStableUnderBaseChange
  obtain ⟨L, hL, e⟩ :=
    exists_iso_toDescentData_obj_of_isStackFor_of_forall_exists_iso_pullFunctor_obj
      (C := Scheme.{u}) ((Scheme.Modules.pseudofunctor.{u}).comp Bicategory.Adj.forget₁)
      (fun _ M => Scheme.Modules.IsInvertible M)
      (fun _ _ g M hM => hM.pullback g)
      (fun _ _ _ ⟨i⟩ hM => isInvertible_of_iso i hM)
      q (U := fun U : Y.affineOpens => ((U : Y.Opens) : Scheme.{u})) (fun U => (U : Y.Opens).ι)
      (AlgebraicGeometry.Scheme.Modules.isStackFor_openCover Y (affineOpensCover Y))
      (fun Z z => (AlgebraicGeometry.Scheme.Modules.isStackFor_openCover Z
        ((affineOpensCover Y).pullback₁ z)).isPrestackFor)
      (fun Z z M N hM hN => by
        have : IsAffineHom (pullback.snd q z) :=
          affineBaseChange.of_isPullback (IsPullback.of_hasPullback q z) inferInstance
        exact toDescentData_map_bijective_of_isAffineHom_of_flat_of_surjective
          (pullback.snd q z) M N hM hN)
      D
      (fun U => by
        have : IsAffine ((U : Y.Opens) : Scheme.{u}) := U.2
        have : IsAffineHom (pullback.snd q (U : Y.Opens).ι) :=
          affineBaseChange.of_isPullback
            (IsPullback.of_hasPullback q (U : Y.Opens).ι) inferInstance
        exact exists_iso_toDescentData_of_isAffine_of_isAffineHom_of_flat_of_surjective
          (pullback.snd q (U : Y.Opens).ι) _ (fun i => (hD i).pullback _))
  exact ⟨L, isInvertible_of_forall_affineOpens L hL, e⟩

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.