Module

PullbackLocalSection.lean

Nyll.SchemeTheory.Modules.PullbackLocalSection

15 declarations indexed from sourceView source ↗

Module documentation

Pullback of local module sections

The adjunction unit pulls sections back to inverse-image opens, compatibly with module operations, restriction maps, morphisms, and the counit.

Imports2

Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.Tactic.Ext

Imported by36

def

pullbackLocalSection

L39 ↗

AlgebraicGeometry.Scheme.Modules.pullbackLocalSection

Documentation

Pull a section of L over U back to the inverse image of U via the unit of the pullback-pushforward adjunction.

Source context 7 commands

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

universe u
open CategoryTheory TopologicalSpace Opposite
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (φ : X ⟶ Y)
section
variable {L : Y.Modules} {U : Y.Opens}

Lean source · statement

def pullbackLocalSection (s : Γ(L, U)) : Γ((Modules.pullback φ).obj L, φ ⁻¹ᵁ U)

lemma

pullbackLocalSection_def

L42 ↗

AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_def

Source context 7 commands

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

universe u
open CategoryTheory TopologicalSpace Opposite
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (φ : X ⟶ Y)
section
variable {L : Y.Modules} {U : Y.Opens}

Lean source · statement

lemma pullbackLocalSection_def (s : Γ(L, U)) :
    pullbackLocalSection φ s = ((Modules.pullbackPushforwardAdjunction φ).unit.app L).app U s

lemma

pullbackLocalSection_add

L45 ↗

AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add

Source context 7 commands

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

universe u
open CategoryTheory TopologicalSpace Opposite
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (φ : X ⟶ Y)
section
variable {L : Y.Modules} {U : Y.Opens}

Lean source · statement

lemma pullbackLocalSection_add (s s' : Γ(L, U)) :
    pullbackLocalSection φ (s + s') = pullbackLocalSection φ s + pullbackLocalSection φ s'

lemma

pullbackLocalSection_zero

L49 ↗

AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero

Source context 7 commands

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

universe u
open CategoryTheory TopologicalSpace Opposite
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (φ : X ⟶ Y)
section
variable {L : Y.Modules} {U : Y.Opens}

Lean source · statement

lemma pullbackLocalSection_zero : pullbackLocalSection φ (0 : Γ(L, U)) = 0

lemma

pullbackLocalSection_neg

L52 ↗

AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg

Source context 7 commands

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

universe u
open CategoryTheory TopologicalSpace Opposite
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (φ : X ⟶ Y)
section
variable {L : Y.Modules} {U : Y.Opens}

Lean source · statement

lemma pullbackLocalSection_neg (s : Γ(L, U)) : pullbackLocalSection φ (-s) =
    -pullbackLocalSection φ s

lemma

pullbackLocalSection_sub

L56 ↗

AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub

Source context 7 commands

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

universe u
open CategoryTheory TopologicalSpace Opposite
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (φ : X ⟶ Y)
section
variable {L : Y.Modules} {U : Y.Opens}

Lean source · statement

lemma pullbackLocalSection_sub (s s' : Γ(L, U)) :
    pullbackLocalSection φ (s - s') = pullbackLocalSection φ s - pullbackLocalSection φ s'

lemma

pullbackLocalSection_sum

L60 ↗

AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sum

Source context 7 commands

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

universe u
open CategoryTheory TopologicalSpace Opposite
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (φ : X ⟶ Y)
section
variable {L : Y.Modules} {U : Y.Opens}

Lean source · statement

lemma pullbackLocalSection_sum {ι : Type*} (S : Finset ι) (s : ι → Γ(L, U)) :
    pullbackLocalSection φ (∑ i ∈ S, s i) = ∑ i ∈ S, pullbackLocalSection φ (s i)

lemma

pullbackLocalSection_smul

L64 ↗

AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_smul

Source context 7 commands

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

universe u
open CategoryTheory TopologicalSpace Opposite
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (φ : X ⟶ Y)
section
variable {L : Y.Modules} {U : Y.Opens}

Lean source · statement

lemma pullbackLocalSection_smul (g : Γ(Y, U)) (s : Γ(L, U)) :
    pullbackLocalSection φ (g • s) = φ.app U g • pullbackLocalSection φ s

lemma

map_pullbackLocalSection

L69 ↗

AlgebraicGeometry.Scheme.Modules.map_pullbackLocalSection

Source context 7 commands

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

universe u
open CategoryTheory TopologicalSpace Opposite
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (φ : X ⟶ Y)
section
variable {L : Y.Modules} {U : Y.Opens}

Lean source · statement

lemma map_pullbackLocalSection {V : Y.Opens} (i : V ⟶ U) (s : Γ(L, U)) :
    ((Modules.pullback φ).obj L).presheaf.map ((Opens.map φ.base).map i).op (pullbackLocalSection φ
        s) =
      pullbackLocalSection φ (L.presheaf.map i.op s)

lemma

map_homOfLE_pullbackLocalSection

L77 ↗

AlgebraicGeometry.Scheme.Modules.map_homOfLE_pullbackLocalSection

Source context 7 commands

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

universe u
open CategoryTheory TopologicalSpace Opposite
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (φ : X ⟶ Y)
section
variable {L : Y.Modules} {U : Y.Opens}

Lean source · full declaration

lemma map_homOfLE_pullbackLocalSection {V : Y.Opens} (hVU : V ≤ U) (s : Γ(L, U)) :
    ((Modules.pullback φ).obj L).presheaf.map
        (homOfLE (show φ ⁻¹ᵁ V ≤ φ ⁻¹ᵁ U from fun _ hx => hVU hx)).op (pullbackLocalSection φ s) =
      pullbackLocalSection φ (L.presheaf.map (homOfLE hVU).op s) :=
  map_pullbackLocalSection φ (homOfLE hVU) s

lemma

pullbackLocalSection_app

L83 ↗

AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_app

Source context 7 commands

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

universe u
open CategoryTheory TopologicalSpace Opposite
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (φ : X ⟶ Y)
section
variable {L : Y.Modules} {U : Y.Opens}

Lean source · statement

lemma pullbackLocalSection_app {L' : Y.Modules} (θ : L ⟶ L') (s : Γ(L, U)) :
    pullbackLocalSection φ (θ.app U s) = ((Modules.pullback φ).map θ).app (φ ⁻¹ᵁ U)
        (pullbackLocalSection φ s)

lemma

app_pullbackLocalSection

L92 ↗

AlgebraicGeometry.Scheme.Modules.app_pullbackLocalSection

Source context 7 commands

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

universe u
open CategoryTheory TopologicalSpace Opposite
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (φ : X ⟶ Y)
section
variable {L : Y.Modules} {U : Y.Opens}

Lean source · statement

lemma app_pullbackLocalSection {N : X.Modules} (g : (Modules.pullback φ).obj L ⟶ N) (s : Γ(L, U)) :
    g.app (φ ⁻¹ᵁ U) (pullbackLocalSection φ s) =
      (((Modules.pullbackPushforwardAdjunction φ).homEquiv L N g).app U s : Γ(N, φ ⁻¹ᵁ U))

lemma

homEquiv_symm_app_pullbackLocalSection

L98 ↗

AlgebraicGeometry.Scheme.Modules.homEquiv_symm_app_pullbackLocalSection

Source context 7 commands

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

universe u
open CategoryTheory TopologicalSpace Opposite
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (φ : X ⟶ Y)
section
variable {L : Y.Modules} {U : Y.Opens}

Lean source · statement

lemma homEquiv_symm_app_pullbackLocalSection {N : X.Modules} (k : L ⟶ (Modules.pushforward φ).obj N)
    (s : Γ(L, U)) :
    (((Modules.pullbackPushforwardAdjunction φ).homEquiv L N).symm k).app (φ ⁻¹ᵁ U)
        (pullbackLocalSection φ s) =
      (k.app U s : Γ(N, φ ⁻¹ᵁ U))

lemma

counit_app_pullbackLocalSection

L107 ↗

AlgebraicGeometry.Scheme.Modules.counit_app_pullbackLocalSection

Source context 5 commands

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

universe u
open CategoryTheory TopologicalSpace Opposite
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (φ : X ⟶ Y)

Lean source · statement

lemma counit_app_pullbackLocalSection {N : X.Modules} {U : Y.Opens} (n : Γ((Modules.pushforward
  φ).obj N, U)) :
    ((Modules.pullbackPushforwardAdjunction φ).counit.app N).app (φ ⁻¹ᵁ U) (pullbackLocalSection φ
        n) =
      (n : Γ(N, φ ⁻¹ᵁ U))

theorem

pullback_hom_ext

L118 ↗

AlgebraicGeometry.Scheme.Modules.pullback_hom_ext

Source context 5 commands

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

universe u
open CategoryTheory TopologicalSpace Opposite
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (φ : X ⟶ Y)

Lean source · statement

theorem pullback_hom_ext {L : Y.Modules} {N : X.Modules} {g₁ g₂ : (Modules.pullback φ).obj L ⟶ N}
    (h : ∀ (U : Y.Opens) (s : Γ(L, U)),
      g₁.app (φ ⁻¹ᵁ U) (pullbackLocalSection φ s) = g₂.app (φ ⁻¹ᵁ U) (pullbackLocalSection φ s)) :
    g₁ = g₂

Module documentation

Pullback of local module sections

Declarations