Module

Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma

19 declarations indexed from sourceView source ↗

Module documentation

Base change of module sections on affine schemes when the canonical tilde-to-module comparison is an isomorphism.

Imports4

Mathlib.AlgebraicGeometry.Modules.Tilde
Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesTildePullback
Nyll.AlgebraicCurves.Geometry.Sheaves.tilde_pullbackSpecIso_unit

Imported by5

abbrev

ΓR

L49 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma.AlgebraicGeometry.Scheme.Modules.AffineBC.ΓR

Documentation

The global sections functor for modules on an affine scheme.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
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
namespace AffineBC
variable {R S : CommRingCat.{u}} (φ : R ⟶ S)

Lean source · statement

abbrev ΓR : (Spec R).Modules ⥤ ModuleCat R

abbrev

pb

L52 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma.AlgebraicGeometry.Scheme.Modules.AffineBC.pb

Documentation

Pullback of modules along the morphism of affine schemes induced by φ.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
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
namespace AffineBC
variable {R S : CommRingCat.{u}} (φ : R ⟶ S)

Lean source · statement

abbrev pb : (Spec R).Modules ⥤ (Spec S).Modules

abbrev

pf

L56 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma.AlgebraicGeometry.Scheme.Modules.AffineBC.pf

Documentation

Pushforward of modules along the morphism of affine schemes induced by φ.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
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
namespace AffineBC
variable {R S : CommRingCat.{u}} (φ : R ⟶ S)

Lean source · statement

abbrev pf : (Spec S).Modules ⥤ (Spec R).Modules

abbrev

adj

L60 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma.AlgebraicGeometry.Scheme.Modules.AffineBC.adj

Documentation

The pullback and pushforward adjunction for the affine morphism.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
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
namespace AffineBC
variable {R S : CommRingCat.{u}} (φ : R ⟶ S)

Lean source · statement

abbrev adj : pb φ ⊣ pf φ

abbrev

ext

L63 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma.AlgebraicGeometry.Scheme.Modules.AffineBC.ext

Documentation

Extension of scalars along the ring homomorphism φ.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
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
namespace AffineBC
variable {R S : CommRingCat.{u}} (φ : R ⟶ S)

Lean source · statement

abbrev ext : ModuleCat R ⥤ ModuleCat S

abbrev

res

L65 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma.AlgebraicGeometry.Scheme.Modules.AffineBC.res

Documentation

Restriction of scalars along the ring homomorphism φ.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
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
namespace AffineBC
variable {R S : CommRingCat.{u}} (φ : R ⟶ S)

Lean source · statement

abbrev res : ModuleCat S ⥤ ModuleCat R

abbrev

adjER

L67 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma.AlgebraicGeometry.Scheme.Modules.AffineBC.adjER

Documentation

The extension and restriction of scalars adjunction.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
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
namespace AffineBC
variable {R S : CommRingCat.{u}} (φ : R ⟶ S)

Lean source · statement

abbrev adjER : ext φ ⊣ res φ

theorem

isIso_map

L69 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma.AlgebraicGeometry.Scheme.Modules.AffineBC.isIso_map

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
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
namespace AffineBC
variable {R S : CommRingCat.{u}} (φ : R ⟶ S)

Lean source · statement

theorem isIso_map {C D : Type*} [Category C] [Category D] (F : C ⥤ D) {X Y : C} (f : X ⟶ Y)
    [IsIso f] :
    IsIso (F.map f)

theorem

isIso_tilde_unit

L75 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma.AlgebraicGeometry.Scheme.Modules.AffineBC.isIso_tilde_unit

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
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
namespace AffineBC
variable {R S : CommRingCat.{u}} (φ : R ⟶ S)

Lean source · statement

theorem isIso_tilde_unit (N : ModuleCat.{u} R) : IsIso ((tilde.adjunction (R := R)).unit.app N)

def

unitΓ

L80 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma.AlgebraicGeometry.Scheme.Modules.AffineBC.unitΓ

Documentation

The global sections map induced by the unit of the pullback and pushforward adjunction.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
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
namespace AffineBC
variable {R S : CommRingCat.{u}} (φ : R ⟶ S)

Lean source · statement

def unitΓ (M : (Spec R).Modules) : (ΓR).obj M ⟶ (res φ).obj ((ΓR).obj ((pb φ).obj
    M))

def

baseChangeΓ

L85 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma.AlgebraicGeometry.Scheme.Modules.AffineBC.baseChangeΓ

Documentation

The base change map on global sections obtained by the scalar adjunction.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
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
namespace AffineBC
variable {R S : CommRingCat.{u}} (φ : R ⟶ S)

Lean source · statement

def baseChangeΓ (M : (Spec R).Modules) : (ext φ).obj ((ΓR).obj M) ⟶ (ΓR).obj ((pb
    φ).obj M)

theorem

baseChangeΓ_eq

L89 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma.AlgebraicGeometry.Scheme.Modules.AffineBC.baseChangeΓ_eq

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
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
namespace AffineBC
variable {R S : CommRingCat.{u}} (φ : R ⟶ S)

Lean source · statement

theorem baseChangeΓ_eq (M : (Spec R).Modules) :
    baseChangeΓ φ M = (ext φ).map (unitΓ φ M) ≫ (adjER φ).counit.app _

theorem

unitΓ_naturality

L93 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma.AlgebraicGeometry.Scheme.Modules.AffineBC.unitΓ_naturality

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
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
namespace AffineBC
variable {R S : CommRingCat.{u}} (φ : R ⟶ S)

Lean source · statement

theorem unitΓ_naturality {M M' : (Spec R).Modules} (g : M ⟶ M') :
    (ΓR).map g ≫ unitΓ φ M' = unitΓ φ M ≫ (res φ).map ((ΓR).map ((pb φ).map g))

theorem

baseChangeΓ_naturality

L110 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma.AlgebraicGeometry.Scheme.Modules.AffineBC.baseChangeΓ_naturality

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
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
namespace AffineBC
variable {R S : CommRingCat.{u}} (φ : R ⟶ S)

Lean source · statement

theorem baseChangeΓ_naturality {M M' : (Spec R).Modules} (g : M ⟶ M') :
    (ext φ).map ((ΓR).map g) ≫ baseChangeΓ φ M' = baseChangeΓ φ M ≫ (ΓR).map ((pb φ).map g)

def

UnitCompat

L125 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma.AlgebraicGeometry.Scheme.Modules.AffineBC.UnitCompat

Documentation

Compatibility of the affine pullback comparison with the units of the two adjunctions.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
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
namespace AffineBC
variable {R S : CommRingCat.{u}} (φ : R ⟶ S)

Lean source · statement

def UnitCompat (N : ModuleCat.{u} R) : Prop

theorem

unitΓ_tilde

L134 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma.AlgebraicGeometry.Scheme.Modules.AffineBC.unitΓ_tilde

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
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
namespace AffineBC
variable {R S : CommRingCat.{u}} (φ : R ⟶ S)

Lean source · statement

theorem unitΓ_tilde (N : ModuleCat.{u} R) (hunit : UnitCompat φ N) :
    (tilde.adjunction (R := R)).unit.app N ≫ unitΓ φ (tilde N) ≫ (res φ).map ((ΓR).map
      (tilde.pullbackSpecIso φ N).hom) =
      (adjER φ).unit.app N ≫ (res φ).map ((tilde.adjunction (R := S)).unit.app ((ext φ).obj N))

theorem

baseChangeΓ_tilde

L157 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma.AlgebraicGeometry.Scheme.Modules.AffineBC.baseChangeΓ_tilde

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
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
namespace AffineBC
variable {R S : CommRingCat.{u}} (φ : R ⟶ S)

Lean source · statement

theorem baseChangeΓ_tilde (N : ModuleCat.{u} R) (hunit : UnitCompat φ N) :
    (ext φ).map ((tilde.adjunction (R := R)).unit.app N) ≫
        baseChangeΓ φ (tilde N) ≫ (ΓR).map (tilde.pullbackSpecIso φ N).hom =
      (tilde.adjunction (R := S)).unit.app ((ext φ).obj N)

theorem

isIso_baseChangeΓ

L206 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma.AlgebraicGeometry.Scheme.Modules.AffineBC.isIso_baseChangeΓ

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
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
namespace AffineBC
variable {R S : CommRingCat.{u}} (φ : R ⟶ S)

Lean source · statement

theorem isIso_baseChangeΓ (M : (Spec R).Modules) [IsIso M.fromTildeΓ] (hunit : ∀ N, UnitCompat φ
    N) :
    IsIso (baseChangeΓ φ M)

theorem

isIso_baseChange_sections_of_isIso_fromTildeGamma

L240 ↗

AlgebraicGeometry.Scheme.Modules.isIso_baseChange_sections_of_isIso_fromTildeGamma

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_baseChange_sections_of_isIso_fromTildeGamma
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.AlgebraicGeometry.Scheme.Modules
    AlgebraicGeometry.Scheme.Modules in

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.isIso_baseChange_sections_of_isIso_fromTildeGamma
    {R S : CommRingCat.{u}} (φ : R ⟶ S) (M : (Spec R).Modules) (hM : IsIso M.fromTildeΓ) :
    IsIso (((ModuleCat.extendRestrictScalarsAdj φ.hom).homEquiv
        ((moduleSpecΓFunctor (R := R)).obj M)
        ((moduleSpecΓFunctor (R := S)).obj ((Scheme.Modules.pullback (Spec.map φ)).obj M))).symm
      ((moduleSpecΓFunctor (R := R)).map
          ((Scheme.Modules.pullbackPushforwardAdjunction (Spec.map φ)).unit.app M) ≫
        (Scheme.Modules.pushforwardSpecCompΓIso φ).hom.app ((Scheme.Modules.pullback (Spec.map
          φ)).obj M)))

Module documentation

Declarations