Module

ModulesBaseChangeHom.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesBaseChangeHom

13 declarations indexed from sourceView source ↗

Module documentation

Base change morphisms for module sheaves

Iterated pullback comparisons determine base change morphisms by adjunction, with compatibility formulas for units, counits, and sections.

Imports2

Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.CategoryTheory.Adjunction.Mates

Imported by18

def

pullbackTwoSquare

L34 ↗

AlgebraicGeometry.Scheme.Modules.pullbackTwoSquare

Documentation

The comparison between iterated pullbacks associated with the commutative square h.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Modules
variable {X T X' T' : Scheme.{u}} {π : X ⟶ T} {ψ : T' ⟶ T} {π' : X' ⟶ T'} {g' : X' ⟶ X}

Lean source · statement

def pullbackTwoSquare (h : g' ≫ π = π' ≫ ψ) :
    TwoSquare (pullback ψ) (pullback π) (pullback π') (pullback g')

def

baseChangeNatTrans

L40 ↗

AlgebraicGeometry.Scheme.Modules.baseChangeNatTrans

Documentation

The pullback-pushforward base change transformation, obtained as the mate of pullbackTwoSquare h.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Modules
variable {X T X' T' : Scheme.{u}} {π : X ⟶ T} {ψ : T' ⟶ T} {π' : X' ⟶ T'} {g' : X' ⟶ X}

Lean source · statement

def baseChangeNatTrans (h : g' ≫ π = π' ≫ ψ) :
    TwoSquare (pushforward π) (pullback g') (pullback ψ) (pushforward π')

def

baseChangeHom

L46 ↗

AlgebraicGeometry.Scheme.Modules.baseChangeHom

Documentation

The component at F of the base change transformation for the commutative square h.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Modules
variable {X T X' T' : Scheme.{u}} {π : X ⟶ T} {ψ : T' ⟶ T} {π' : X' ⟶ T'} {g' : X' ⟶ X}

Lean source · statement

def baseChangeHom (h : g' ≫ π = π' ≫ ψ) (F : X.Modules) :
    (pullback ψ).obj ((pushforward π).obj F) ⟶ (pushforward π').obj ((pullback g').obj F)

theorem

baseChangeNatTrans_app

L50 ↗

AlgebraicGeometry.Scheme.Modules.baseChangeNatTrans_app

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Modules
variable {X T X' T' : Scheme.{u}} {π : X ⟶ T} {ψ : T' ⟶ T} {π' : X' ⟶ T'} {g' : X' ⟶ X}

Lean source · statement

theorem baseChangeNatTrans_app (h : g' ≫ π = π' ≫ ψ) (F : X.Modules) :
    (baseChangeNatTrans h).natTrans.app F = baseChangeHom h F

theorem

baseChangeHom_naturality

L53 ↗

AlgebraicGeometry.Scheme.Modules.baseChangeHom_naturality

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Modules
variable {X T X' T' : Scheme.{u}} {π : X ⟶ T} {ψ : T' ⟶ T} {π' : X' ⟶ T'} {g' : X' ⟶ X}

Lean source · statement

theorem baseChangeHom_naturality (h : g' ≫ π = π' ≫ ψ) {F G : X.Modules} (φ : F ⟶ G) :
    (pullback ψ).map ((pushforward π).map φ) ≫ baseChangeHom h G =
      baseChangeHom h F ≫ (pushforward π').map ((pullback g').map φ)

theorem

baseChangeHom_counit

L58 ↗

AlgebraicGeometry.Scheme.Modules.baseChangeHom_counit

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Modules
variable {X T X' T' : Scheme.{u}} {π : X ⟶ T} {ψ : T' ⟶ T} {π' : X' ⟶ T'} {g' : X' ⟶ X}

Lean source · statement

theorem baseChangeHom_counit (h : g' ≫ π = π' ≫ ψ) (F : X.Modules) :
    (pullback π').map (baseChangeHom h F) ≫
        (pullbackPushforwardAdjunction π').counit.app ((pullback g').obj F) =
      (pullbackTwoSquare h).natTrans.app ((pushforward π).obj F) ≫
        (pullback g').map ((pullbackPushforwardAdjunction π).counit.app F)

theorem

unit_baseChangeHom

L66 ↗

AlgebraicGeometry.Scheme.Modules.unit_baseChangeHom

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Modules
variable {X T X' T' : Scheme.{u}} {π : X ⟶ T} {ψ : T' ⟶ T} {π' : X' ⟶ T'} {g' : X' ⟶ X}

Lean source · statement

theorem unit_baseChangeHom (h : g' ≫ π = π' ≫ ψ) (M : T.Modules) :
    (pullback ψ).map ((pullbackPushforwardAdjunction π).unit.app M) ≫ baseChangeHom h ((pullback
        π).obj M) =
      (pullbackPushforwardAdjunction π').unit.app ((pullback ψ).obj M) ≫
        (pushforward π').map ((pullbackTwoSquare h).natTrans.app M)

theorem

conjugateEquiv_pullbackCongr_hom

L78 ↗

AlgebraicGeometry.Scheme.Modules.conjugateEquiv_pullbackCongr_hom

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Modules
variable {X T X' T' : Scheme.{u}} {π : X ⟶ T} {ψ : T' ⟶ T} {π' : X' ⟶ T'} {g' : X' ⟶ X}
section adjoint
variable (π ψ π' g')

Lean source · statement

theorem conjugateEquiv_pullbackCongr_hom {Y Z : Scheme.{u}} {f g : Y ⟶ Z} (e : f = g) :
    conjugateEquiv (pullbackPushforwardAdjunction g) (pullbackPushforwardAdjunction f)
        (pullbackCongr e).hom =
      (pushforwardCongr e).inv

theorem

pushforwardCongr_symm_inv

L88 ↗

AlgebraicGeometry.Scheme.Modules.pushforwardCongr_symm_inv

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Modules
variable {X T X' T' : Scheme.{u}} {π : X ⟶ T} {ψ : T' ⟶ T} {π' : X' ⟶ T'} {g' : X' ⟶ X}
section adjoint
variable (π ψ π' g')

Lean source · statement

theorem pushforwardCongr_symm_inv {Y Z : Scheme.{u}} {f g : Y ⟶ Z} (e : f = g) :
    (pushforwardCongr e.symm).inv = (pushforwardCongr e).hom

theorem

conjugateEquiv_pullbackComp_hom

L93 ↗

AlgebraicGeometry.Scheme.Modules.conjugateEquiv_pullbackComp_hom

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Modules
variable {X T X' T' : Scheme.{u}} {π : X ⟶ T} {ψ : T' ⟶ T} {π' : X' ⟶ T'} {g' : X' ⟶ X}
section adjoint
variable (π ψ π' g')

Lean source · statement

theorem conjugateEquiv_pullbackComp_hom {W Y Z : Scheme.{u}} (f : W ⟶ Y) (g : Y ⟶ Z) :
    conjugateEquiv (pullbackPushforwardAdjunction (f ≫ g))
        ((pullbackPushforwardAdjunction g).comp (pullbackPushforwardAdjunction f)) (pullbackComp f
            g).hom =
      (pushforwardComp f g).inv

theorem

conjugateEquiv_pullbackTwoSquare

L102 ↗

AlgebraicGeometry.Scheme.Modules.conjugateEquiv_pullbackTwoSquare

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Modules
variable {X T X' T' : Scheme.{u}} {π : X ⟶ T} {ψ : T' ⟶ T} {π' : X' ⟶ T'} {g' : X' ⟶ X}
section adjoint
variable (π ψ π' g')

Lean source · statement

theorem conjugateEquiv_pullbackTwoSquare (h : g' ≫ π = π' ≫ ψ) :
    conjugateEquiv ((pullbackPushforwardAdjunction π).comp (pullbackPushforwardAdjunction g'))
        ((pullbackPushforwardAdjunction ψ).comp (pullbackPushforwardAdjunction π'))
        (pullbackTwoSquare h).natTrans =
      (pushforwardComp g' π).hom ≫ (pushforwardCongr h).hom ≫ (pushforwardComp π' ψ).inv

theorem

pullbackPushforwardAdjunction_homEquiv_baseChangeHom

L114 ↗

AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction_homEquiv_baseChangeHom

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Modules
variable {X T X' T' : Scheme.{u}} {π : X ⟶ T} {ψ : T' ⟶ T} {π' : X' ⟶ T'} {g' : X' ⟶ X}
section adjoint
variable (π ψ π' g')

Lean source · statement

theorem pullbackPushforwardAdjunction_homEquiv_baseChangeHom (h : g' ≫ π = π' ≫ ψ) (F : X.Modules) :
    (pullbackPushforwardAdjunction ψ).homEquiv _ _ (baseChangeHom h F) =
      (pushforward π).map ((pullbackPushforwardAdjunction g').unit.app F) ≫
        (pushforwardComp g' π).hom.app _ ≫ (pushforwardCongr h).hom.app _ ≫ (pushforwardComp π'
            ψ).inv.app _

theorem

unit_app_app_comp_baseChangeHom_app

L140 ↗

AlgebraicGeometry.Scheme.Modules.unit_app_app_comp_baseChangeHom_app

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Modules
variable {X T X' T' : Scheme.{u}} {π : X ⟶ T} {ψ : T' ⟶ T} {π' : X' ⟶ T'} {g' : X' ⟶ X}
section adjoint
variable (π ψ π' g')

Lean source · full declaration

theorem unit_app_app_comp_baseChangeHom_app (h : g' ≫ π = π' ≫ ψ) (F : X.Modules) (U : T.Opens) :
    ((pullbackPushforwardAdjunction ψ).unit.app ((pushforward π).obj F)).app U ≫
        (baseChangeHom h F).app (ψ ⁻¹ᵁ U) =
      ((pullbackPushforwardAdjunction g').unit.app F).app (π ⁻¹ᵁ U) ≫
        ((pullback g').obj F).presheaf.map
          (eqToHom (show (π' ≫ ψ) ⁻¹ᵁ U = (g' ≫ π) ⁻¹ᵁ U by rw [h])).op := by
  have e := congrArg (fun t => Scheme.Modules.Hom.app t U)
      (pullbackPushforwardAdjunction_homEquiv_baseChangeHom π ψ π' g' h F)
  simp only [Adjunction.homEquiv_unit, Scheme.Modules.Hom.comp_app] at e
  exact e

Module documentation

Base change morphisms for module sheaves

Declarations