NYLL
Module

Scheme_Modules_isIso_baseChangeHom_of_isAffineHom.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom
23 declarations indexed from sourceView source ↗

Module documentation

Base change for affine pushforward

The comparison is an isomorphism for locally trivial modules along an affine morphism.

Imports15
Imported by3

Declarations

theorem

isIso_of_isIso_moduleSpecΓFunctor_map

L61 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom.AlgebraicGeometry.Scheme.Modules.isIso_of_isIso_moduleSpecΓFunctor_map
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom
attribute [-simp] TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply
  TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply
  TwoChartCech.KerCoprod.ι0_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
theorem isIso_of_isIso_moduleSpecΓFunctor_map {A : Type u} [CommRing A]
    {M N : (Spec (CommRingCat.of A)).Modules}
    (hM : IsIso (Scheme.Modules.fromTildeΓ (R := .of A) M)) (hN : IsIso (Scheme.Modules.fromTildeΓ
      (R := .of A) N))
    (f : M ⟶ N) (hf : IsIso ((moduleSpecΓFunctor (R := .of A)).map f)) : IsIso f
lemma

app_presheaf_map

L83 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom.AlgebraicGeometry.Scheme.Modules.Hom.app_presheaf_map
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom
attribute [-simp] TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply
  TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply
  TwoChartCech.KerCoprod.ι0_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open scoped _root_.AlgebraicGeometry.Scheme.Modules.Hom in
Lean source · statement
lemma Hom.app_presheaf_map {X : Scheme.{u}} {F G : X.Modules} (η : F ⟶ G) {U V : X.Opens} (i : V ⟶
  U) (s : Γ(F, U)) :
    (η.app V).hom (F.presheaf.map i.op s) = G.presheaf.map i.op ((η.app U).hom s)
lemma

baseChangeHom_app_top_unit

L90 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom.AlgebraicGeometry.Scheme.Modules.baseChangeHom_app_top_unit
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom
attribute [-simp] TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply
  TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply
  TwoChartCech.KerCoprod.ι0_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
lemma baseChangeHom_app_top_unit {X X' T T' : Scheme.{u}}
    (π : X ⟶ T) (ψ : T' ⟶ T) (π' : X' ⟶ T') (g : X' ⟶ X)
    (h : g ≫ π = π' ≫ ψ) (F : X.Modules) (s : Γ((pushforward π).obj F, ⊤)) :
    (Scheme.Modules.baseChangeHom h F).app ⊤
        (((pullbackPushforwardAdjunction ψ).unit.app ((pushforward π).obj F)).app ⊤ s) =
      ((pullbackPushforwardAdjunction g).unit.app F).app ⊤ s
abbrev

resM

L111 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom.AlgebraicGeometry.Scheme.Modules.resM
Documentation

Restriction of a module section along an inclusion of opens.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom
attribute [-simp] TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply
  TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply
  TwoChartCech.KerCoprod.ι0_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section resM
variable {X : Scheme.{u}} (M : X.Modules)
Lean source · statement
abbrev resM {W W' : X.Opens} (h : W' ≤ W) : Γ(M, W) → Γ(M, W')
lemma

map_eq_resM

L116 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom.AlgebraicGeometry.Scheme.Modules.map_eq_resM
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom
attribute [-simp] TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply
  TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply
  TwoChartCech.KerCoprod.ι0_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section resM
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
Lean source · statement
lemma map_eq_resM {W W' : X.Opens} (i : W' ⟶ W) (s : Γ(M, W)) : M.presheaf.map i.op s = resM M i.le
  s
lemma

resM_resM

L120 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom.AlgebraicGeometry.Scheme.Modules.resM_resM
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom
attribute [-simp] TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply
  TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply
  TwoChartCech.KerCoprod.ι0_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section resM
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
Lean source · statement
lemma resM_resM {W W' W'' : X.Opens} (h : W' ≤ W) (h' : W'' ≤ W') (s : Γ(M, W)) :
    resM M h' (resM M h s) = resM M (h'.trans h) s
lemma

resM_refl

L126 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom.AlgebraicGeometry.Scheme.Modules.resM_refl
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom
attribute [-simp] TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply
  TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply
  TwoChartCech.KerCoprod.ι0_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section resM
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
Lean source · statement
lemma resM_refl {W : X.Opens} (h : W ≤ W) (s : Γ(M, W)) : resM M h s = s
lemma

presheaf_map_map_eq

L131 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom.AlgebraicGeometry.Scheme.Modules.presheaf_map_map_eq
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom
attribute [-simp] TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply
  TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply
  TwoChartCech.KerCoprod.ι0_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section resM
variable {X : Scheme.{u}} (M : X.Modules)
variable {M}
Lean source · statement
lemma presheaf_map_map_eq (M : X.Modules) {U V W : X.Opens} (a : V ⟶ U) (b : W ⟶ V) (c : W ⟶ U)
    (s : Γ(M, U)) : M.presheaf.map b.op (M.presheaf.map a.op s) = M.presheaf.map c.op s
theorem

prod_of_flat

L137 ↗
Module.Flat.prod_of_flat
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom
attribute [-simp] TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply
  TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply
  TwoChartCech.KerCoprod.ι0_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
theorem _root_.Module.Flat.prod_of_flat {R : Type u} [CommRing R] (M N : Type u)
  [AddCommGroup M] [Module R M]
    [AddCommGroup N] [Module R N] [Module.Flat R M] [Module.Flat R N] : Module.Flat R (M × N)
def

restrictScalarsSelfEquiv

L162 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom.AlgebraicGeometry.Scheme.Modules.restrictScalarsSelfEquiv
Documentation

The identity linear equivalence on the scalar-restricted coefficient module.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom
attribute [-simp] TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply
  TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply
  TwoChartCech.KerCoprod.ι0_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section bridge
variable {A : Type u} [CommRing A] (A' : Type u) [CommRing A'] [Algebra A A']
Lean source · statement
def restrictScalarsSelfEquiv :
    A' ≃ₗ[A'] ((ModuleCat.restrictScalars (CommRingCat.ofHom (algebraMap A A')).hom).obj
      (ModuleCat.of A' A'))
instance

(anonymous instance)

L167 ↗
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom
attribute [-simp] TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply
  TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply
  TwoChartCech.KerCoprod.ι0_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section bridge
variable {A : Type u} [CommRing A] (A' : Type u) [CommRing A'] [Algebra A A']
Lean source · statement
instance : IsScalarTower A A'
    ((ModuleCat.restrictScalars (CommRingCat.ofHom (algebraMap A A')).hom).obj (ModuleCat.of A'
      A'))
def

extendScalarsAlgebraMapEquiv

L175 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom.AlgebraicGeometry.Scheme.Modules.extendScalarsAlgebraMapEquiv
Documentation

The equivalence between the tensor and categorical scalar extensions.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom
attribute [-simp] TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply
  TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply
  TwoChartCech.KerCoprod.ι0_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section bridge
variable {A : Type u} [CommRing A] (A' : Type u) [CommRing A'] [Algebra A A']
Lean source · statement
def extendScalarsAlgebraMapEquiv (N : ModuleCat.{u} A) :
    (A' ⊗[A] N) ≃ₗ[A'] (ModuleCat.extendScalars (CommRingCat.ofHom (algebraMap A A')).hom).obj N
theorem

extendScalarsAlgebraMapEquiv_tmul

L180 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom.AlgebraicGeometry.Scheme.Modules.extendScalarsAlgebraMapEquiv_tmul
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom
attribute [-simp] TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply
  TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply
  TwoChartCech.KerCoprod.ι0_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section bridge
variable {A : Type u} [CommRing A] (A' : Type u) [CommRing A'] [Algebra A A']
Lean source · statement
theorem extendScalarsAlgebraMapEquiv_tmul (N : ModuleCat.{u} A) (a' : A') (n : N) :
    extendScalarsAlgebraMapEquiv (A := A) A' N (a' ⊗ₜ n) =
      ((a' : ((ModuleCat.restrictScalars (CommRingCat.ofHom (algebraMap A A')).hom).obj
        (ModuleCat.of A' A'))) ⊗ₜ[A] n :
        (ModuleCat.extendScalars (CommRingCat.ofHom (algebraMap A A')).hom).obj N)
abbrev

globalSectionsModule

L196 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom.AlgebraicGeometry.Scheme.Modules.globalSectionsModule
Documentation

Global sections of the pushforward as a module over the base ring.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom
attribute [-simp] TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply
  TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply
  TwoChartCech.KerCoprod.ι0_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section main
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (π : X ⟶ Spec (.of A))
Lean source · statement
abbrev globalSectionsModule (F : X.Modules) : ModuleCat A
def

globalSectionsEquiv

L200 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom.AlgebraicGeometry.Scheme.Modules.globalSectionsEquiv
Documentation

Global sections identified with sections of the original module.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom
attribute [-simp] TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply
  TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply
  TwoChartCech.KerCoprod.ι0_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section main
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (π : X ⟶ Spec (.of A))
Lean source · full declaration
def globalSectionsEquiv (F : X.Modules) :
    letI := moduleSectionsOfHom π F ⊤
    globalSectionsModule π F ≃ₗ[A] Γ(F, ⊤) :=
  let := moduleSectionsOfHom π F ⊤
  { toFun := fun s => (show Γ(F, ⊤) from s)
    invFun := fun s => (show globalSectionsModule π F from s)
    map_add' := fun _ _ => rfl
    map_smul' := fun a s => by
      change (show Γ(X, ⊤) from ((π.app ⊤).hom ((((Spec (CommRingCat.of A)).presheaf.map
          (homOfLE (le_top (a := ⊤))).op).hom) ((Scheme.ΓSpecIso (.of A)).inv.hom a)))) • (show
            Γ(F, ⊤) from s) =
        ((π.appLE ⊤ ⊤ le_top).hom ((Scheme.ΓSpecIso (.of A)).inv.hom a)) • (show Γ(F, ⊤) from s)
      congr 1
      have h1 : (homOfLE (le_top : (⊤ : (Spec (CommRingCat.of A)).Opens) ≤ ⊤)) = 𝟙 _ :=
        Subsingleton.elim _ _
      have e1 : (Spec (CommRingCat.of A)).presheaf.map (homOfLE (le_top (a := (⊤ : (Spec
        (CommRingCat.of A)).Opens)))).op = 𝟙 _ := by
        rw [h1, op_id, CategoryTheory.Functor.map_id]
      have e2 : π.appLE ⊤ ⊤ le_top = π.app ⊤ := Scheme.Hom.appLE_eq_app _
      rw [e2, e1]
      rfl
    left_inv := fun _ => rfl
    right_inv := fun _ => rfl }
abbrev

ΓMod

L225 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom.AlgebraicGeometry.Scheme.Modules.ΓMod
Documentation

The module of global sections of a module on an affine scheme.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom
attribute [-simp] TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply
  TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply
  TwoChartCech.KerCoprod.ι0_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section main
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (π : X ⟶ Spec (.of A))
Lean source · statement
abbrev ΓMod (N : (Spec (CommRingCat.of A)).Modules) : ModuleCat A
abbrev

φA

L231 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom.AlgebraicGeometry.Scheme.Modules.φA
Documentation

The coefficient algebra map as a morphism of commutative rings.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom
attribute [-simp] TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply
  TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply
  TwoChartCech.KerCoprod.ι0_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section main
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (π : X ⟶ Spec (.of A))
variable (A' : Type u) [CommRing A'] [Algebra A A']
Lean source · statement
abbrev φA : CommRingCat.of A ⟶ CommRingCat.of A'
lemma

specMap_eq

L234 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom.AlgebraicGeometry.Scheme.Modules.specMap_eq
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom
attribute [-simp] TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply
  TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply
  TwoChartCech.KerCoprod.ι0_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section main
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (π : X ⟶ Spec (.of A))
variable (A' : Type u) [CommRing A'] [Algebra A A']
Lean source · statement
lemma specMap_eq : Scheme.TwoAffineOpenCover.specMap A A' = Spec.map (φA (A := A) A')
theorem

exists_linearEquiv_tensor_ΓMod_pullback

L236 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom.AlgebraicGeometry.Scheme.Modules.exists_linearEquiv_tensor_ΓMod_pullback
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom
attribute [-simp] TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply
  TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply
  TwoChartCech.KerCoprod.ι0_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section main
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (π : X ⟶ Spec (.of A))
variable (A' : Type u) [CommRing A'] [Algebra A A']
Lean source · statement
theorem exists_linearEquiv_tensor_ΓMod_pullback (N : (Spec (CommRingCat.of A)).Modules)
    (hN : IsIso (Scheme.Modules.fromTildeΓ (R := .of A) N)) :
    ∃ σ : A' ⊗[A] (ΓMod N) ≃ₗ[A']
        ((moduleSpecΓFunctor (R := .of A')).obj ((Scheme.Modules.pullback (Spec.map (φA (A := A)
          A'))).obj N)),
      ∀ m : ΓMod N, σ ((1 : A') ⊗ₜ[A] m) =
        ((((pullbackPushforwardAdjunction (Spec.map (φA (A := A) A'))).unit.app N).app ⊤).hom m :)
theorem

exists_linearEquiv_ker_baseChange_cechDiff

L258 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom.AlgebraicGeometry.Scheme.Modules.exists_linearEquiv_ker_baseChange_cechDiff
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom
attribute [-simp] TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply
  TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply
  TwoChartCech.KerCoprod.ι0_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section main
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (π : X ⟶ Spec (.of A))
variable (A' : Type u) [CommRing A'] [Algebra A A']
Lean source · statement
theorem exists_linearEquiv_ker_baseChange_cechDiff (𝒱 : X.TwoAffineOpenCover) (F : X.Modules)
    (htriv : ∀ x : X, ∃ (V : X.Opens), x ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj F ≅
        SheafOfModules.unit V.toScheme.ringCatSheaf))
        :
    (Function.Surjective ((𝒱.pullback π A').sectionsOf
          (Limits.pullback.snd π (Scheme.TwoAffineOpenCover.specMap A A'))
          ((Scheme.Modules.pullback (Limits.pullback.fst π (Scheme.TwoAffineOpenCover.specMap A
            A'))).obj F)).cechDiff →
      Function.Surjective ((𝒱.sectionsOf π F).cechDiff.baseChange A')) ∧
    ∃ κ : LinearMap.ker ((𝒱.sectionsOf π F).cechDiff.baseChange A') ≃ₗ[A']
        LinearMap.ker ((𝒱.pullback π A').sectionsOf
          (Limits.pullback.snd π (Scheme.TwoAffineOpenCover.specMap A A'))
          ((Scheme.Modules.pullback (Limits.pullback.fst π (Scheme.TwoAffineOpenCover.specMap A
            A'))).obj F)).cechDiff,
      ∀ (x : (𝒱.sectionsOf π F).M0 × (𝒱.sectionsOf π F).M1)
        (hx : (1 : A') ⊗ₜ[A] x ∈ LinearMap.ker ((𝒱.sectionsOf π F).cechDiff.baseChange A')),
        (κ ⟨(1 : A') ⊗ₜ[A] x, hx⟩).1 =
          ((((Scheme.Modules.pullbackPushforwardAdjunction
              (Limits.pullback.fst π (Scheme.TwoAffineOpenCover.specMap A A'))).unit.app F).app
                𝒱.U0).hom x.1,
           (((Scheme.Modules.pullbackPushforwardAdjunction
              (Limits.pullback.fst π (Scheme.TwoAffineOpenCover.specMap A A'))).unit.app F).app
                𝒱.U1).hom x.2)
theorem

isIso_fromTildeΓ_pullback_pushforward

L363 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom.AlgebraicGeometry.Scheme.Modules.isIso_fromTildeΓ_pullback_pushforward
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom
attribute [-simp] TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply
  TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply
  TwoChartCech.KerCoprod.ι0_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section main
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (π : X ⟶ Spec (.of A))
variable (A' : Type u) [CommRing A'] [Algebra A A']
Lean source · statement
theorem isIso_fromTildeΓ_pullback_pushforward (F : X.Modules)
    (hF : IsIso (Scheme.Modules.fromTildeΓ (R := .of A) ((pushforward π).obj F))) :
    IsIso (Scheme.Modules.fromTildeΓ (R := .of A')
      ((Scheme.Modules.pullback (Spec.map (φA (A := A) A'))).obj ((pushforward π).obj F)))
theorem

affine_core

L377 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom.AlgebraicGeometry.Scheme.Modules.affine_core
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom
attribute [-simp] TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply
  TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply
  TwoChartCech.KerCoprod.ι0_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section main
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (π : X ⟶ Spec (.of A))
variable (A' : Type u) [CommRing A'] [Algebra A A']
Lean source · statement
theorem affine_core [IsAffine X] (F : X.Modules)
    (htriv : ∀ x : X, ∃ (V : X.Opens), x ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj F ≅
        SheafOfModules.unit V.toScheme.ringCatSheaf))
        :
    IsIso (Scheme.Modules.baseChangeHom
      (Limits.pullback.condition (f := π) (g := Scheme.TwoAffineOpenCover.specMap A A')) F)
theorem

isIso_baseChangeHom_of_isAffineHom

L466 ↗
AlgebraicGeometry.Scheme.Modules.isIso_baseChangeHom_of_isAffineHom
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_of_isAffineHom
attribute [-simp] TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply
  TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply
  TwoChartCech.KerCoprod.ι0_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
open _root_.AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.Scheme.Modules in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.isIso_baseChangeHom_of_isAffineHom
    {X T X' T' : Scheme.{u}} {π : X ⟶ T} {ψ : T' ⟶ T} {π' : X' ⟶ T'} {g' : X' ⟶ X}
    (hcart : IsPullback g' π' π ψ) [IsAffineHom π] (F : X.Modules)
    (htriv : ∀ x : X, ∃ (V : X.Opens), x ∈ V ∧
      Nonempty ((Scheme.Modules.pullback V.ι).obj F ≅
        SheafOfModules.unit V.toScheme.ringCatSheaf))
        :
    IsIso (Scheme.Modules.baseChangeHom hcart.w F)

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