Module

Scheme_Modules_pullback_locally_mem_span_unit.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_pullback_locally_mem_span_unit

31 declarations indexed from sourceView source ↗

Module documentation

Local generation of a pulled-back module

Sections of a pullback module are locally spanned by images of sections under the adjunction unit.

Imports1

Mathlib.AlgebraicGeometry.Modules.Sheaf

Imported by3

abbrev

F

L48 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.F

Documentation

The pullback of the module sheaf E along ψ.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)

Lean source · statement

abbrev F : X.Modules

abbrev

res

L51 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.res

Documentation

Restrict a section of M along the open inclusion h.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)

Lean source · statement

abbrev res (M : X.Modules) {W' W : X.Opens} (h : W' ≤ W) : Γ(M, W) → Γ(M, W')

lemma

res_res

L55 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.res_res

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)
omit E in

Lean source · statement

lemma res_res (M : X.Modules) {W₁ W₂ W₃ : X.Opens} (h₂₁ : W₂ ≤ W₁) (h₃₂ : W₃ ≤ W₂) (y : Γ(M, W₁)) :
    res M h₃₂ (res M h₂₁ y) = res M (h₃₂.trans h₂₁) y

lemma

res_eq_map

L62 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.res_eq_map

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)
omit E in

Lean source · statement

lemma res_eq_map (M : X.Modules) {W' W : X.Opens} (f : W' ⟶ W) (y : Γ(M, W)) :
    M.presheaf.map f.op y = res M f.le y

lemma

res_smul

L67 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.res_smul

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)
omit E in

Lean source · statement

lemma res_smul (M : X.Modules) {W' W : X.Opens} (h : W' ≤ W) (r : Γ(X, W)) (y : Γ(M, W)) :
    res M h (r • y) = X.presheaf.map (homOfLE h).op r • res M h y

lemma

res_add

L72 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.res_add

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)
omit E in

Lean source · statement

lemma res_add (M : X.Modules) {W' W : X.Opens} (h : W' ≤ W) (y z : Γ(M, W)) :
    res M h (y + z) = res M h y + res M h z

lemma

res_zero

L76 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.res_zero

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)
omit E in

Lean source · statement

lemma res_zero (M : X.Modules) {W' W : X.Opens} (h : W' ≤ W) : res M h (0 : Γ(M, W)) = 0

def

eta

L80 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.eta

Documentation

Pull a section of E back along ψ using the unit of the pullback-pushforward adjunction.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)

Lean source · statement

def eta (U : Y.Opens) (e : Γ(E, U)) : Γ(F ψ E, ψ ⁻¹ᵁ U)

lemma

res_eta

L83 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.res_eta

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)

Lean source · statement

lemma res_eta {U U' : Y.Opens} (h : U' ≤ U) (e : Γ(E, U)) :
    res (F ψ E) (ψ.preimage_mono h) (eta ψ E U e) = eta ψ E U' (E.presheaf.map (homOfLE h).op e)

def

span₁

L92 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.span₁

Documentation

The module span over Γ(X, W) of restrictions to W of pullbacks of sections over U.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)

Lean source · statement

def span₁ (U : Y.Opens) (W : X.Opens) (j : W ≤ ψ ⁻¹ᵁ U) : Submodule Γ(X, W) Γ(F ψ
  E, W)

def

spanAll

L98 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.spanAll

Documentation

The module span of all sections obtained by pulling back sections of E and restricting them to W.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)

Lean source · statement

def spanAll (W : X.Opens) : Submodule Γ(X, W) Γ(F ψ E, W)

lemma

eta_res_mem_spanAll

L102 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.eta_res_mem_spanAll

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)

Lean source · statement

lemma eta_res_mem_spanAll {U : Y.Opens} {W : X.Opens} (j : W ≤ ψ ⁻¹ᵁ U) (e : Γ(E, U)) :
    res (F ψ E) j (eta ψ E U e) ∈ spanAll ψ E W

lemma

res_mem_spanAll

L106 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.res_mem_spanAll

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)

Lean source · statement

lemma res_mem_spanAll {W' W : X.Opens} (h : W' ≤ W) {y : Γ(F ψ E, W)} (hy : y ∈ spanAll ψ E W) :
    res (F ψ E) h y ∈ spanAll ψ E W'

lemma

res_mem_span₁

L117 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.res_mem_span₁

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)

Lean source · statement

lemma res_mem_span₁ {U U₁ : Y.Opens} {W W₁ : X.Opens} (hU : U ≤ U₁) (hW : W ≤ W₁) (j₁ : W₁ ≤ ψ
  ⁻¹ᵁ U₁)
    (j : W ≤ ψ ⁻¹ᵁ U) {y : Γ(F ψ E, W₁)} (hy : y ∈ span₁ ψ E U₁ W₁ j₁) :
    res (F ψ E) hW y ∈ span₁ ψ E U W j

def

locSpan

L135 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.locSpan

Documentation

The submodule of sections that lie in spanAll on a neighborhood of each point of W.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)

Lean source · full declaration

def locSpan (W : X.Opens) : Submodule Γ(X, W) Γ(F ψ E, W) where
  carrier := {y | ∀ x ∈ W, ∃ (W' : X.Opens) (i : W' ≤ W), x ∈ W' ∧ res (F ψ E) i y ∈ spanAll ψ E W'}
  zero_mem' := fun x hx => ⟨W, le_rfl, hx, by rw [res_zero]; exact zero_mem _⟩
  add_mem' := by
    intro y z hy hz x hx
    obtain ⟨W₁, i₁, hx₁, h₁⟩ := hy x hx
    obtain ⟨W₂, i₂, hx₂, h₂⟩ := hz x hx
    refine ⟨W₁ ⊓ W₂, inf_le_left.trans i₁, ⟨hx₁, hx₂⟩, ?_⟩
    rw [res_add]
    refine add_mem ?_ ?_
    · rw [← res_res (F ψ E) i₁ inf_le_left]; exact res_mem_spanAll ψ E _ h₁
    · rw [← res_res (F ψ E) i₂ inf_le_right]; exact res_mem_spanAll ψ E _ h₂
  smul_mem' := by
    intro r y hy x hx
    obtain ⟨W₁, i₁, hx₁, h₁⟩ := hy x hx
    refine ⟨W₁, i₁, hx₁, ?_⟩
    rw [res_smul]
    exact Submodule.smul_mem _ _ h₁

lemma

res_mem_locSpan

L154 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.res_mem_locSpan

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)

Lean source · statement

lemma res_mem_locSpan {W' W : X.Opens} (h : W' ≤ W) {y : Γ(F ψ E, W)} (hy : y ∈ locSpan ψ E W) :
    res (F ψ E) h y ∈ locSpan ψ E W'

lemma

eta_mem_locSpan

L162 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.eta_mem_locSpan

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)

Lean source · statement

lemma eta_mem_locSpan (U : Y.Opens) (e : Γ(E, U)) : eta ψ E U e ∈ locSpan ψ E (ψ ⁻¹ᵁ U)

lemma

map_eq_res

L186 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.map_eq_res

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)
omit E in

Lean source · statement

lemma map_eq_res (M : X.Modules) {W W' : (X.Opens)ᵒᵖ} (f : W ⟶ W') (y : Γ(M, W.unop)) :
    M.presheaf.map f y = res M f.unop.le y

def

locSpanAb

L191 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.locSpanAb

Documentation

The presheaf of abelian groups of locally generated sections of the pullback of E.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)

Lean source · full declaration

def locSpanAb : (X.Opens)ᵒᵖ ⥤ AddCommGrpCat.{u} where
  obj W := AddCommGrpCat.of (locSpan ψ E W.unop)
  map {W W'} f := AddCommGrpCat.ofHom (X := locSpan ψ E W.unop) (Y := locSpan ψ E W'.unop)
    { toFun := fun y => ⟨(F ψ E).presheaf.map f y.1, by
        rw [map_eq_res]; exact res_mem_locSpan ψ E f.unop.le y.2⟩
      map_zero' := Subtype.ext (map_zero _)
      map_add' := fun y z => Subtype.ext (map_add _ _ _) }
  map_id W := by
    ext y
    change (F ψ E).presheaf.map (𝟙 W) y.1 = y.1
    rw [CategoryTheory.Functor.map_id]
    rfl
  map_comp f g := by
    ext y
    change (F ψ E).presheaf.map (f ≫ g) y.1 = (F ψ E).presheaf.map g ((F ψ E).presheaf.map f y.1)
    rw [CategoryTheory.Functor.map_comp]
    rfl

lemma

locSpanAb_map_apply_val

L209 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.locSpanAb_map_apply_val

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)

Lean source · statement

lemma locSpanAb_map_apply_val {W W' : (X.Opens)ᵒᵖ} (f : W ⟶ W') (y : locSpan ψ E
  W.unop) :
    ((locSpanAb ψ E).map f y).1 = (F ψ E).presheaf.map f y.1

instance

instModuleLocSpanAb

L213 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.instModuleLocSpanAb

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)

Lean source · statement

instance instModuleLocSpanAb (W : (X.Opens)ᵒᵖ) :
    Module (X.ringCatSheaf.obj.obj W) ((locSpanAb ψ E).obj W)

lemma

isSheaf_locSpanAb

L217 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.isSheaf_locSpanAb

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)

Lean source · statement

lemma isSheaf_locSpanAb : TopCat.Presheaf.IsSheaf (locSpanAb ψ E)

def

G

L239 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.G

Documentation

The module subsheaf of the pullback of E consisting of sections locally spanned by pulled-back sections.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)

Lean source · full declaration

def G : X.Modules where
  val :=
    letI := instModuleLocSpanAb ψ E
    PresheafOfModules.ofPresheaf (locSpanAb ψ E)
      (fun _W _W' f r m => Subtype.ext (Modules.map_smul (F ψ E) f.unop r m.1))
  isSheaf := isSheaf_locSpanAb ψ E

def

incl

L247 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.incl

Documentation

Include the module subsheaf of locally generated sections into the pullback module sheaf F.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)

Lean source · statement

def incl : G ψ E ⟶ F ψ E

lemma

incl_app_apply

L254 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.incl_app_apply

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)

Lean source · full declaration

lemma incl_app_apply (W : X.Opens) (y : locSpan ψ E W) :
    (incl ψ E).app W (show Γ(G ψ E, W) from y) = y.1 := rfl

instance

(anonymous instance)

L257 ↗

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)

Lean source · statement

instance : Mono (incl ψ E)

instance

(anonymous instance)

L265 ↗

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)

Lean source · statement

instance : Epi (incl ψ E)

instance

(anonymous instance)

L285 ↗

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)

Lean source · statement

instance : IsIso (incl ψ E)

lemma

mem_locSpan

L287 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.mem_locSpan

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)

Lean source · statement

lemma mem_locSpan (W : X.Opens) (y : Γ(F ψ E, W)) : y ∈ locSpan ψ E W

theorem

main

L292 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit.AlgebraicGeometry.Scheme.Modules.PullbackGen.main

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
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 PullbackGen
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules)

Lean source · statement

theorem main {W : X.Opens} (y : Γ(F ψ E, W)) {x : X} (hx : x ∈ W) {U₀ : Y.Opens} (hU₀ : ψ.base x
  ∈ U₀) :
    ∃ (U : Y.Opens) (W' : X.Opens) (i : W' ≤ W) (j : W' ≤ ψ ⁻¹ᵁ U), U ≤ U₀ ∧ x ∈ W' ∧
      res (F ψ E) i y ∈ span₁ ψ E U W' j

theorem

pullback_locally_mem_span_unit

L331 ↗

AlgebraicGeometry.Scheme.Modules.pullback_locally_mem_span_unit

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_pullback_locally_mem_span_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite

Lean source · full declaration

theorem _root_.AlgebraicGeometry.Scheme.Modules.pullback_locally_mem_span_unit
    {X Y : Scheme.{u}} (ψ : X ⟶ Y) (E : Y.Modules) {W : X.Opens}
    (y : Γ((Scheme.Modules.pullback ψ).obj E, W)) {x : X} (hx : x ∈ W)
    {U₀ : Y.Opens} (hU₀ : ψ.base x ∈ U₀) :
    ∃ (U : Y.Opens) (W' : X.Opens) (i : W' ≤ W) (j : W' ≤ ψ ⁻¹ᵁ U), U ≤ U₀ ∧ x ∈ W' ∧
      ((Scheme.Modules.pullback ψ).obj E).presheaf.map (homOfLE i).op y ∈
        Submodule.span Γ(X, W') (Set.range fun e : Γ(E, U) =>
          ((Scheme.Modules.pullback ψ).obj E).presheaf.map (homOfLE j).op
            ((((Scheme.Modules.pullbackPushforwardAdjunction ψ).unit.app E).app U e :
              Γ((Scheme.Modules.pullback ψ).obj E, ψ ⁻¹ᵁ U)))) :=
  AlgebraicGeometry.Scheme.Modules.PullbackGen.main ψ E y hx hU₀

Module documentation

Local generation of a pulled-back module

Declarations