NYLL
Module

PullbackFrame.lean

Nyll.SchemeTheory.Modules.PullbackFrame
27 declarations indexed from sourceView source ↗

Module documentation

Pullback preserves the property that multiplication by a section gives a bijection on sections over every open subset of a prescribed open.

Imports2
  • Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
  • Mathlib.AlgebraicGeometry.Modules.Sheaf
Imported by6

Declarations

instance

opensMap_final'

L45 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.opensMap_final'
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
Lean source · statement
instance opensMap_final' {X Y : Scheme.{u}} (f : X ⟶ Y) : (Opens.map f.base).Final
def

unitMod

L51 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.unitMod
Documentation

The unit sheaf of modules on a 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_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
variable {Z : Scheme.{u}}
Lean source · statement
def unitMod (Z : Scheme.{u}) : Z.Modules
abbrev

res

L54 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.res
Documentation

Restrict a module section along an inclusion of open subsets.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
variable {Z : Scheme.{u}}
Lean source · statement
abbrev res (N : Z.Modules) {W' W : Z.Opens} (h : W' ≤ W) (s : Γ(N, W)) : Γ(N, W')
abbrev

resTop

L58 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.resTop
Documentation

Restrict a global module section to an open subset.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
variable {Z : Scheme.{u}}
Lean source · statement
abbrev resTop (N : Z.Modules) (W : Z.Opens) (s : Γ(N, ⊤)) : Γ(N, W)
lemma

res_res

L61 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.res_res
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
variable {Z : Scheme.{u}}
Lean source · statement
lemma res_res (N : Z.Modules) {W₁ W₂ W₃ : Z.Opens} (h₂₁ : W₂ ≤ W₁) (h₃₂ : W₃ ≤ W₂) (s : Γ(N, W₁)) :
    res N h₃₂ (res N h₂₁ s) = res N (h₃₂.trans h₂₁) s
lemma

res_resTop

L67 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.res_resTop
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
variable {Z : Scheme.{u}}
Lean source · statement
lemma res_resTop (N : Z.Modules) {W W' : Z.Opens} (h : W' ≤ W) (s : Γ(N, ⊤)) :
    res N h (resTop N W s) = resTop N W' s
lemma

res_eq_map

L71 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.res_eq_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_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
variable {Z : Scheme.{u}}
Lean source · statement
lemma res_eq_map (N : Z.Modules) {W' W : Z.Opens} (f : W' ⟶ W) (s : Γ(N, W)) :
    N.presheaf.map f.op s = res N f.le s
lemma

res_smul

L75 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.res_smul
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
variable {Z : Scheme.{u}}
Lean source · statement
lemma res_smul (N : Z.Modules) {W' W : Z.Opens} (h : W' ≤ W) (r : Γ(Z, W)) (x : Γ(N, W)) :
    res N h (r • x) = Z.presheaf.map (homOfLE h).op r • res N h x
lemma

app_res

L79 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.app_res
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
variable {Z : Scheme.{u}}
Lean source · statement
lemma app_res {N N' : Z.Modules} (φ : N ⟶ N') {W' W : Z.Opens} (h : W' ≤ W) (s : Γ(N, W)) :
    φ.app W' (res N h s) = res N' h (φ.app W s)
def

smulHom

L87 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.smulHom
Documentation

The morphism from the unit module obtained by multiplying by a global section.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
variable {Z : Scheme.{u}}
Lean source · statement
def smulHom (N : Z.Modules) (s : Γ(N, ⊤)) : unitMod Z ⟶ N
lemma

smulHom_app_apply

L105 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.smulHom_app_apply
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
variable {Z : Scheme.{u}}
Lean source · full declaration
lemma smulHom_app_apply (N : Z.Modules) (s : Γ(N, ⊤)) (W : Z.Opens) (g : Γ(Z, W)) :
    (smulHom N s).app W (show Γ(unitMod Z, W) from g) = g • resTop N W s :=
  rfl
lemma

isIso_restrict_smulHom

L109 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.isIso_restrict_smulHom
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
variable {Z : Scheme.{u}}
Lean source · full declaration
lemma isIso_restrict_smulHom (N : Z.Modules) (s : Γ(N, ⊤)) {V : Z.Opens}
    (hs : ∀ W : Z.Opens, W ≤ V → Function.Bijective fun g : Γ(Z, W) => g • resTop N W s) :
    IsIso ((Modules.restrictFunctor V.ι).map (smulHom N s)) := by
  rw [Modules.Hom.isIso_iff_isIso_app]
  intro W
  change IsIso ((smulHom N s).app (V.ι ''ᵁ W))
  rw [ConcreteCategory.isIso_iff_bijective]
  exact hs (V.ι ''ᵁ W) (V.ι_image_le W)
lemma

isIso_pullback_smulHom

L118 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.isIso_pullback_smulHom
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
variable {Z : Scheme.{u}}
Lean source · full declaration
lemma isIso_pullback_smulHom (N : Z.Modules) (s : Γ(N, ⊤)) {V : Z.Opens}
    (hs : ∀ W : Z.Opens, W ≤ V → Function.Bijective fun g : Γ(Z, W) => g • resTop N W s) :
    IsIso ((Modules.pullback V.ι).map (smulHom N s)) :=
  (NatIso.isIso_map_iff (Modules.restrictFunctorIsoPullback V.ι) (smulHom N s)).mp
    (isIso_restrict_smulHom N s hs)
theorem

nativePushforwardRightAdjoint

L128 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.nativePushforwardRightAdjoint
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
variable {Z : Scheme.{u}}
section pullback
variable {X X' : Scheme.{u}} (p : X' ⟶ X) (M : X.Modules)
Lean source · statement
theorem nativePushforwardRightAdjoint :
    (SheafOfModules.pushforward.{u} p.toRingCatSheafHom).IsRightAdjoint
abbrev

F

L135 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.F
Documentation

The pullback of M along p.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
variable {Z : Scheme.{u}}
section pullback
variable {X X' : Scheme.{u}} (p : X' ⟶ X) (M : X.Modules)
attribute [local instance] nativePushforwardRightAdjoint
Lean source · statement
abbrev F : X'.Modules
def

eta

L138 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.eta
Documentation

The section of the pullback module induced by the pullback-pushforward adjunction unit.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
variable {Z : Scheme.{u}}
section pullback
variable {X X' : Scheme.{u}} (p : X' ⟶ X) (M : X.Modules)
attribute [local instance] nativePushforwardRightAdjoint
Lean source · statement
def eta (U : X.Opens) (m : Γ(M, U)) : Γ(F p M, p ⁻¹ᵁ U)
lemma

eta_smul

L141 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.eta_smul
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
variable {Z : Scheme.{u}}
section pullback
variable {X X' : Scheme.{u}} (p : X' ⟶ X) (M : X.Modules)
attribute [local instance] nativePushforwardRightAdjoint
Lean source · statement
lemma eta_smul (U : X.Opens) (r : Γ(X, U)) (m : Γ(M, U)) :
    eta p M U (r • m) = p.app U r • eta p M U m
lemma

res_eta

L145 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.res_eta
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
variable {Z : Scheme.{u}}
section pullback
variable {X X' : Scheme.{u}} (p : X' ⟶ X) (M : X.Modules)
attribute [local instance] nativePushforwardRightAdjoint
Lean source · statement
lemma res_eta {U U' : X.Opens} (h : U' ≤ U) (m : Γ(M, U)) :
    res (F p M) (p.preimage_mono h) (eta p M U m) = eta p M U' (res M h m)
lemma

isIso_pullback_pullback_smulHom

L152 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.isIso_pullback_pullback_smulHom
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
variable {Z : Scheme.{u}}
section pullback
variable {X X' : Scheme.{u}} (p : X' ⟶ X) (M : X.Modules)
attribute [local instance] nativePushforwardRightAdjoint
Lean source · full declaration
lemma isIso_pullback_pullback_smulHom (s : Γ(M, ⊤)) {V : X.Opens}
    (hs : ∀ W : X.Opens, W ≤ V → Function.Bijective fun g : Γ(X, W) => g • resTop M W s) :
    IsIso ((Modules.pullback (p ⁻¹ᵁ V).ι).map ((Modules.pullback p).map (smulHom M s))) := by
  have hfact : (p ⁻¹ᵁ V).ι ≫ p = (p ∣_ V) ≫ V.ι := (morphismRestrict_ι p V).symm
  let e : Modules.pullback p ⋙ Modules.pullback (p ⁻¹ᵁ V).ι ≅
      Modules.pullback V.ι ⋙ Modules.pullback (p ∣_ V) :=
    Modules.pullbackComp _ _ ≪≫ Modules.pullbackCongr hfact ≪≫ (Modules.pullbackComp _ _).symm
  have h1 : IsIso ((Modules.pullback V.ι ⋙ Modules.pullback (p ∣_ V)).map (smulHom M s)) := by
    change IsIso ((Modules.pullback (p ∣_ V)).map ((Modules.pullback V.ι).map (smulHom M s)))
    have := isIso_pullback_smulHom M s hs
    infer_instance
  exact (NatIso.isIso_map_iff e (smulHom M s)).mpr h1
def

unitIso

L166 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.unitIso
Documentation

The canonical identification of the pullback of the unit module with the unit module.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
variable {Z : Scheme.{u}}
section pullback
variable {X X' : Scheme.{u}} (p : X' ⟶ X) (M : X.Modules)
attribute [local instance] nativePushforwardRightAdjoint
Lean source · statement
def unitIso : (Modules.pullback p).obj (unitMod X) ≅ unitMod X'
lemma

unitIso_hom

L178 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.unitIso_hom
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
variable {Z : Scheme.{u}}
section pullback
variable {X X' : Scheme.{u}} (p : X' ⟶ X) (M : X.Modules)
attribute [local instance] nativePushforwardRightAdjoint
Lean source · statement
lemma unitIso_hom :
    (unitIso p).hom = SheafOfModules.pullbackObjUnitToUnit p.toRingCatSheafHom
lemma

unitIso_hom_comp_smulHom

L181 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.unitIso_hom_comp_smulHom
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
variable {Z : Scheme.{u}}
section pullback
variable {X X' : Scheme.{u}} (p : X' ⟶ X) (M : X.Modules)
attribute [local instance] nativePushforwardRightAdjoint
Lean source · statement
lemma unitIso_hom_comp_smulHom (s : Γ(M, ⊤)) :
    (unitIso p).hom ≫ smulHom (F p M) (eta p M ⊤ s) = (Modules.pullback p).map (smulHom M s)
lemma

smulHom_eta_eq

L221 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.smulHom_eta_eq
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
variable {Z : Scheme.{u}}
section pullback
variable {X X' : Scheme.{u}} (p : X' ⟶ X) (M : X.Modules)
attribute [local instance] nativePushforwardRightAdjoint
Lean source · statement
lemma smulHom_eta_eq (s : Γ(M, ⊤)) :
    smulHom (F p M) (eta p M ⊤ s) = (unitIso p).inv ≫ (Modules.pullback p).map (smulHom M s)
lemma

isIso_pullback_smulHom_eta

L225 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.isIso_pullback_smulHom_eta
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
variable {Z : Scheme.{u}}
section pullback
variable {X X' : Scheme.{u}} (p : X' ⟶ X) (M : X.Modules)
attribute [local instance] nativePushforwardRightAdjoint
Lean source · full declaration
lemma isIso_pullback_smulHom_eta (s : Γ(M, ⊤)) {V : X.Opens}
    (hs : ∀ W : X.Opens, W ≤ V → Function.Bijective fun g : Γ(X, W) => g • resTop M W s) :
    IsIso ((Modules.pullback (p ⁻¹ᵁ V).ι).map (smulHom (F p M) (eta p M ⊤ s))) := by
  rw [smulHom_eta_eq, CategoryTheory.Functor.map_comp]
  have := isIso_pullback_pullback_smulHom p M s hs
  infer_instance
lemma

image_preimage_eq

L233 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.image_preimage_eq
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
variable {Z : Scheme.{u}}
section pullback
variable {X X' : Scheme.{u}} (p : X' ⟶ X) (M : X.Modules)
attribute [local instance] nativePushforwardRightAdjoint
omit M in
Lean source · statement
lemma image_preimage_eq {W V : X'.Opens} (hW : W ≤ V) : V.ι ''ᵁ (V.ι ⁻¹ᵁ W) = W
theorem

main

L237 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_smul_unit_app_of_bijective_smul.AlgebraicGeometry.Scheme.Modules.FramePullback.main
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
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 FramePullback
variable {Z : Scheme.{u}}
section pullback
variable {X X' : Scheme.{u}} (p : X' ⟶ X) (M : X.Modules)
attribute [local instance] nativePushforwardRightAdjoint
Lean source · full declaration
theorem main (s : Γ(M, ⊤)) {V : X.Opens}
    (hs : ∀ W : X.Opens, W ≤ V → Function.Bijective fun g : Γ(X, W) => g • resTop M W s)
    (W' : X'.Opens) (hW' : W' ≤ p ⁻¹ᵁ V) :
    Function.Bijective fun g : X'.presheaf.obj (op W') => g • resTop (F p M) W' (eta p M ⊤ s) := by
  have h1 := isIso_pullback_smulHom_eta p M s hs
  have h2 : IsIso ((Modules.restrictFunctor (p ⁻¹ᵁ V).ι).map (smulHom (F p M) (eta p M ⊤ s))) :=
    (NatIso.isIso_map_iff (Modules.restrictFunctorIsoPullback (p ⁻¹ᵁ V).ι) _).mpr h1
  rw [Modules.Hom.isIso_iff_isIso_app] at h2
  have h3 : IsIso ((smulHom (F p M) (eta p M ⊤ s)).app ((p ⁻¹ᵁ V).ι ''ᵁ ((p ⁻¹ᵁ V).ι ⁻¹ᵁ W'))) :=
    h2 ((p ⁻¹ᵁ V).ι ⁻¹ᵁ W')
  rw [image_preimage_eq hW'] at h3
  exact (ConcreteCategory.bijective_of_isIso ((smulHom (F p M) (eta p M ⊤ s)).app W'))
theorem

bijective_smul_unit_app_of_bijective_smul

L256 ↗
AlgebraicGeometry.Scheme.Modules.bijective_smul_unit_app_of_bijective_smul
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_bijective_smul_unit_app_of_bijective_smul
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
Lean source · full declaration
theorem _root_.AlgebraicGeometry.Scheme.Modules.bijective_smul_unit_app_of_bijective_smul
    {X X' : Scheme.{u}} (p : X' ⟶ X) (M : X.Modules) (σ : Γ(M, ⊤)) {V : X.Opens}
    (hσ : ∀ W : X.Opens, W ≤ V →
      Function.Bijective fun g : Γ(X, W) =>
        g • (M.presheaf.map (homOfLE (le_top : W ≤ ⊤)).op σ : Γ(M, W)))
    (W' : X'.Opens) (hW' : W' ≤ p ⁻¹ᵁ V) :
    Function.Bijective fun g : Γ(X', W') =>
      g • (((Scheme.Modules.pullback p).obj M).presheaf.map (homOfLE (le_top : W' ≤ ⊤)).op
        ((((Scheme.Modules.pullbackPushforwardAdjunction p).unit.app M).app ⊤) σ) :
          Γ((Scheme.Modules.pullback p).obj M, W')) :=
  AlgebraicGeometry.Scheme.Modules.FramePullback.main p M σ hσ W' hW'

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