NYLL
Module

Scheme_Modules_isFrameOn_sheafificationAdjunction_unit_iotaMulti.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isFrameOn_sheafificationAdjunction_unit_iotaMulti
28 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules is Frame On sheafification Adjunction unit iota Multi

Imports4
Imported by6

Declarations

def

uniquePowersetCardFin

L53 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.uniquePowersetCardFin
Documentation

The unique subset of Fin n of cardinality n, containing all indices.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
section ModuleLevel
open Set Set.powersetCard
Lean source · full declaration
def uniquePowersetCardFin (n : ℕ) : Unique (Set.powersetCard (Fin n) n)
  where
  default := Set.powersetCard.ofCard (n := n) (s := (Finset.univ : Finset (Fin n))) (by simp)
  uniq s := Subtype.ext (Finset.eq_univ_of_card _ (by
    rw [Fintype.card_fin]; exact Set.powersetCard.card_eq s))
lemma

exists_basis_exteriorPower_top

L61 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.exists_basis_exteriorPower_top
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
section ModuleLevel
open Set Set.powersetCard
variable {A : Type*} [CommRing A] {M : Type*} [AddCommGroup M] [Module A M] {n : ℕ}
Lean source · statement
lemma exists_basis_exteriorPower_top (b : Module.Basis (Fin n) A M) :
    ∃ B : Module.Basis (Set.powersetCard (Fin n) n) A (⋀[A]^n M), ∀ s, B s = exteriorPower.ιMulti
      A n b
lemma

exists_eq_smul_ιMulti

L74 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.exists_eq_smul_ιMulti
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
section ModuleLevel
open Set Set.powersetCard
variable {A : Type*} [CommRing A] {M : Type*} [AddCommGroup M] [Module A M] {n : ℕ}
Lean source · statement
lemma exists_eq_smul_ιMulti (b : Module.Basis (Fin n) A M) (x : ⋀[A]^n M) :
    ∃ r : A, x = r • exteriorPower.ιMulti A n b
lemma

smul_ιMulti_injective

L82 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.smul_ιMulti_injective
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
section ModuleLevel
open Set Set.powersetCard
variable {A : Type*} [CommRing A] {M : Type*} [AddCommGroup M] [Module A M] {n : ℕ}
Lean source · full declaration
lemma smul_ιMulti_injective (b : Module.Basis (Fin n) A M) :
    Function.Injective fun r : A => r • exteriorPower.ιMulti A n b := by
  let := uniquePowersetCardFin n
  obtain ⟨B, hB⟩ := exists_basis_exteriorPower_top b
  intro r r' h
  have h' := congrArg (fun y => B.repr y default) h
  simp only [← hB default] at h'
  simpa [Module.Basis.repr_self] using h'
abbrev

pre

L96 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.pre
Documentation

The presheaf exterior power of a module sheaf.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
variable {X : Scheme.{u}} (n : ℕ)
Lean source · statement
abbrev pre (M : X.Modules) : X.PresheafOfModules
def

toSh

L100 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.toSh
Documentation

The map from the exterior power of local sections to sections of the determinant sheaf.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
variable {X : Scheme.{u}} (n : ℕ)
Lean source · statement
def toSh (M : X.Modules) (W : X.Opens) :
    (⋀[Γ(X, W)]^n Γ(M, W)) → Γ(det n M, W)
lemma

toSh_add

L106 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.toSh_add
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
variable {X : Scheme.{u}} (n : ℕ)
Lean source · statement
lemma toSh_add (M : X.Modules) (W : X.Opens) (w w' : ⋀[Γ(X, W)]^n Γ(M, W)) :
    toSh n M W (w + w') = toSh n M W w + toSh n M W w'
lemma

toSh_zero

L112 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.toSh_zero
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
variable {X : Scheme.{u}} (n : ℕ)
Lean source · statement
lemma toSh_zero (M : X.Modules) (W : X.Opens) : toSh n M W 0 = 0
lemma

toSh_smul

L117 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.toSh_smul
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
variable {X : Scheme.{u}} (n : ℕ)
Lean source · statement
lemma toSh_smul (M : X.Modules) (W : X.Opens) (r : Γ(X, W)) (w : ⋀[Γ(X, W)]^n Γ(M, W)) :
    toSh n M W (r • w) = r • toSh n M W w
abbrev

res

L123 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.res
Documentation

Restriction of module sections along an inclusion of opens.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
variable {X : Scheme.{u}} (n : ℕ)
Lean source · statement
abbrev res (M : X.Modules) {W' W : X.Opens} (h : W' ≤ W) (s : Γ(M, W)) : Γ(M, W')
lemma

res_res

L126 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.res_res
Source context 21 commands

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

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

res_smul

L132 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.res_smul
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
variable {X : Scheme.{u}} (n : ℕ)
Lean source · statement
lemma res_smul (M : X.Modules) {W' W : X.Opens} (h : W' ≤ W) (r : Γ(X, W)) (s : Γ(M, W)) :
    res M h (r • s) = X.presheaf.map (homOfLE h).op r • res M h s
abbrev

preMap

L137 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.preMap
Documentation

Restriction of exterior powers of local sections through the presheaf exterior power.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
variable {X : Scheme.{u}} (n : ℕ)
Lean source · statement
abbrev preMap (M : X.Modules) {W W' : X.Opens} (j : W' ⟶ W)
    (w : ⋀[Γ(X, W)]^n Γ(M, W)) : ⋀[Γ(X, W')]^n Γ(M, W')
lemma

preMap_ιMulti

L141 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.preMap_ιMulti
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
variable {X : Scheme.{u}} (n : ℕ)
Lean source · full declaration
lemma preMap_ιMulti (M : X.Modules) {W W' : X.Opens} (j : W' ⟶ W) (m : Fin n → Γ(M, W)) :
    preMap n M j (exteriorPower.ιMulti _ n m) =
      exteriorPower.ιMulti _ n (fun k => (M.presheaf.map j.op : Γ(M, W) ⟶ _) (m k)) :=
  PresheafOfModules.exteriorPower_map_ιMulti n M.val j.op m
lemma

preMap_smul

L146 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.preMap_smul
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
variable {X : Scheme.{u}} (n : ℕ)
Lean source · statement
lemma preMap_smul (M : X.Modules) {W W' : X.Opens} (j : W' ⟶ W)
    (r : Γ(X, W)) (w : ⋀[Γ(X, W)]^n Γ(M, W)) :
    preMap n M j (r • w) = X.presheaf.map j.op r • preMap n M j w
lemma

preMap_zero

L151 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.preMap_zero
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
variable {X : Scheme.{u}} (n : ℕ)
Lean source · statement
lemma preMap_zero (M : X.Modules) {W W' : X.Opens} (j : W' ⟶ W) :
    preMap n M j (0 : ⋀[Γ(X, W)]^n Γ(M, W)) = 0
lemma

res_toSh

L155 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.res_toSh
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
variable {X : Scheme.{u}} (n : ℕ)
Lean source · statement
lemma res_toSh (M : X.Modules) {W' W : X.Opens} (h : W' ≤ W) (w : ⋀[Γ(X, W)]^n Γ(M, W)) :
    res (det n M) h (toSh n M W w) = toSh n M W' (preMap n M (homOfLE h) w)
lemma

toSh_locally_injective

L162 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.toSh_locally_injective
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
variable {X : Scheme.{u}} (n : ℕ)
Lean source · statement
lemma toSh_locally_injective (M : X.Modules) {W : X.Opens} (w w' : ⋀[Γ(X, W)]^n Γ(M, W))
    (h : toSh n M W w = toSh n M W w') (x : X) (hx : x ∈ W) :
    ∃ (V : X.Opens) (i : V ≤ W), x ∈ V ∧ preMap n M (homOfLE i) w = preMap n M (homOfLE i) w'
lemma

toSh_locally_surjective

L175 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.toSh_locally_surjective
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
variable {X : Scheme.{u}} (n : ℕ)
Lean source · statement
lemma toSh_locally_surjective (M : X.Modules) {W : X.Opens} (c : Γ(det n M, W)) (x : X) (hx : x ∈
  W) :
    ∃ (V : X.Opens) (i : V ≤ W), x ∈ V ∧ ∃ w : ⋀[Γ(X, V)]^n Γ(M, V), toSh n M V w = res (det n M)
      i c
abbrev

eRes

L191 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.eRes
Documentation

The chosen local frame restricted to a smaller open set.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
variable {X : Scheme.{u}} (n : ℕ)
section Wedge
variable {n} {M : X.Modules} {U : X.Opens} (e : Fin n → Γ(M, U))
Lean source · statement
abbrev eRes {W : X.Opens} (hW : W ≤ U) : Fin n → Γ(M, W)
def

wedge

L194 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.wedge
Documentation

The determinant section obtained by wedging the restricted local frame.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
variable {X : Scheme.{u}} (n : ℕ)
section Wedge
variable {n} {M : X.Modules} {U : X.Opens} (e : Fin n → Γ(M, U))
Lean source · statement
def wedge {W : X.Opens} (hW : W ≤ U) : Γ(det n M, W)
lemma

res_toSh_ιMulti

L197 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.res_toSh_ιMulti
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
variable {X : Scheme.{u}} (n : ℕ)
section Wedge
variable {n} {M : X.Modules} {U : X.Opens} (e : Fin n → Γ(M, U))
Lean source · statement
lemma res_toSh_ιMulti {W : X.Opens} (hW : W ≤ U) :
    res (det n M) hW (toSh n M U (exteriorPower.ιMulti _ n e)) = wedge e hW
lemma

res_wedge

L201 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.res_wedge
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
variable {X : Scheme.{u}} (n : ℕ)
section Wedge
variable {n} {M : X.Modules} {U : X.Opens} (e : Fin n → Γ(M, U))
Lean source · statement
lemma res_wedge {W W' : X.Opens} (hW : W ≤ U) (h : W' ≤ W) :
    res (det n M) h (wedge e hW) = wedge e (h.trans hW)
lemma

exists_basis_eq

L212 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.exists_basis_eq
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
variable {X : Scheme.{u}} (n : ℕ)
section Wedge
variable {n} {M : X.Modules} {U : X.Opens} (e : Fin n → Γ(M, U))
variable (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
  ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
include he in
Lean source · statement
lemma exists_basis_eq {W : X.Opens} (hW : W ≤ U) :
    ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W), (b : Fin n → Γ(M, W)) = eRes e hW
lemma

smul_wedge_injective

L218 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.smul_wedge_injective
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
variable {X : Scheme.{u}} (n : ℕ)
section Wedge
variable {n} {M : X.Modules} {U : X.Opens} (e : Fin n → Γ(M, U))
variable (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
  ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
include he in
Lean source · full declaration
lemma smul_wedge_injective {W : X.Opens} (hW : W ≤ U) :
    Function.Injective fun g : Γ(X, W) => g • wedge e hW := by
  intro g g' hgg'
  rw [← sub_eq_zero]
  have h0 : (g - g') • wedge e hW = 0 := by rw [sub_smul]; exact sub_eq_zero.mpr hgg'
  have h1 : toSh n M W ((g - g') • exteriorPower.ιMulti _ n (eRes e hW)) = toSh n M W 0 := by
    rw [toSh_smul, toSh_zero]; exact h0
  have key : ∀ x ∈ W, ∃ (V : X.Opens) (i : V ≤ W), x ∈ V ∧ X.presheaf.map (homOfLE i).op (g - g')
    = 0 := by
    intro x hx
    obtain ⟨V, i, hxV, hV⟩ := toSh_locally_injective n M _ _ h1 x hx
    refine ⟨V, i, hxV, ?_⟩
    rw [preMap_zero, preMap_smul, preMap_ιMulti] at hV
    obtain ⟨b, hb⟩ := exists_basis_eq e he (i.trans hW)
    have hfam : (fun k => (M.presheaf.map (homOfLE i).op : Γ(M, W) ⟶ _) (eRes e hW k)) = (b : Fin
      n → Γ(M, V)) := by
      rw [hb]; funext k; exact res_res M hW i (e k)
    rw [hfam] at hV
    exact smul_ιMulti_injective b (hV.trans (zero_smul _ _).symm)
  choose V hV using key
  refine X.sheaf.eq_of_locally_eq' (fun p : {x // x ∈ W} => V p.1 p.2) W
    (fun p => homOfLE (hV p.1 p.2).1) (fun x hx => Opens.mem_iSup.mpr ⟨⟨x, hx⟩, (hV x hx).2.1⟩) (g
      - g') 0
    (fun p => ?_)
  rw [map_zero]
  exact (hV p.1 p.2).2.2
lemma

smul_wedge_surjective

L246 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.smul_wedge_surjective
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
variable {X : Scheme.{u}} (n : ℕ)
section Wedge
variable {n} {M : X.Modules} {U : X.Opens} (e : Fin n → Γ(M, U))
variable (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
  ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
include he in
Lean source · full declaration
lemma smul_wedge_surjective {W : X.Opens} (hW : W ≤ U) :
    Function.Surjective fun g : Γ(X, W) => g • wedge e hW := by
  intro c
  have key : ∀ x ∈ W, ∃ (V : X.Opens) (i : V ≤ W), x ∈ V ∧ ∃ r : Γ(X, V),
      res (det n M) i c = r • wedge e (i.trans hW) := by
    intro x hx
    obtain ⟨V, i, hxV, w, hw⟩ := toSh_locally_surjective n M c x hx
    obtain ⟨b, hb⟩ := exists_basis_eq e he (i.trans hW)
    obtain ⟨r, hr⟩ := exists_eq_smul_ιMulti b w
    refine ⟨V, i, hxV, r, ?_⟩
    rw [← hw, hr, toSh_smul, hb]
    rfl
  choose V i hxV r hr using key
  let ι := {x // x ∈ W}
  let Vf : ι → X.Opens := fun p => V p.1 p.2
  have hcover : W ≤ iSup Vf := fun x hx => Opens.mem_iSup.mpr ⟨⟨x, hx⟩, hxV x hx⟩
  have hcompat : TopCat.Presheaf.IsCompatible X.sheaf.1 Vf (fun p => r p.1 p.2) := by
    intro p q
    rw [Subsingleton.elim (Opens.infLELeft (Vf p) (Vf q)) (homOfLE inf_le_left),
      Subsingleton.elim (Opens.infLERight (Vf p) (Vf q)) (homOfLE inf_le_right)]
    have hpq_p : Vf p ⊓ Vf q ≤ Vf p := inf_le_left
    have hpq_q : Vf p ⊓ Vf q ≤ Vf q := inf_le_right
    have hp : (X.presheaf.map (homOfLE hpq_p).op (r p.1 p.2) : Γ(X, Vf p ⊓ Vf q)) •
        wedge e (hpq_p.trans ((i p.1 p.2).trans hW)) = res (det n M) (hpq_p.trans (i p.1 p.2)) c
          := by
      rw [← res_wedge e ((i p.1 p.2).trans hW) hpq_p, ← res_smul, ← hr p.1 p.2, res_res]
    have hq : (X.presheaf.map (homOfLE hpq_q).op (r q.1 q.2) : Γ(X, Vf p ⊓ Vf q)) •
        wedge e (hpq_q.trans ((i q.1 q.2).trans hW)) = res (det n M) (hpq_q.trans (i q.1 q.2)) c
          := by
      rw [← res_wedge e ((i q.1 q.2).trans hW) hpq_q, ← res_smul, ← hr q.1 q.2, res_res]
    apply smul_wedge_injective e he (hpq_p.trans ((i p.1 p.2).trans hW))
    exact hp.trans hq.symm
  obtain ⟨g, hg, -⟩ := X.sheaf.existsUnique_gluing' Vf W (fun p => homOfLE (i p.1 p.2)) hcover
    (fun p => r p.1 p.2) hcompat
  refine ⟨show Γ(X, W) from g, ?_⟩
  let D : TopCat.Sheaf Ab X.toTopCat := ⟨(det n M).presheaf, (det n M).isSheaf⟩
  refine D.eq_of_locally_eq' Vf W (fun p => homOfLE (i p.1 p.2)) hcover _ c (fun p => ?_)
  change res (det n M) (i p.1 p.2) ((show Γ(X, W) from g) • wedge e hW) = res (det n M) (i p.1
    p.2) c
  rw [res_smul, res_wedge, hr p.1 p.2]
  congr 1
  exact hg p
theorem

isFrameOn_toSh_ιMulti

L290 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame.AlgebraicGeometry.Scheme.Modules.Ws31H1.isFrameOn_toSh_ιMulti
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
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
namespace Ws31H1
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
variable {X : Scheme.{u}} (n : ℕ)
section Wedge
variable {n} {M : X.Modules} {U : X.Opens} (e : Fin n → Γ(M, U))
variable (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
  ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
include he in
Lean source · statement
theorem isFrameOn_toSh_ιMulti :
    IsFrameOn (M := det n M) (toSh n M U (exteriorPower.ιMulti _ n e)) U
theorem

isFrameOn_sheafificationAdjunction_unit_iotaMulti

L302 ↗
AlgebraicGeometry.Scheme.Modules.isFrameOn_sheafificationAdjunction_unit_iotaMulti
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.SheafifiedExteriorFrame
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
Lean source · full declaration
theorem _root_.AlgebraicGeometry.Scheme.Modules.isFrameOn_sheafificationAdjunction_unit_iotaMulti
    {X : Scheme.{u}} {n : ℕ} {M : X.Modules} {U : X.Opens} (e : Fin n → Γ(M, U))
    (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
      ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i)) :
    Scheme.Modules.IsFrameOn (M := Scheme.Modules.det n M)
      (((PresheafOfModules.sheafificationAdjunction (𝟙 X.ringCatSheaf.obj)).unit.app
          ((Scheme.Modules.presheafExteriorPower X n).obj M.val)).app (op U)
        (show ((Scheme.Modules.presheafExteriorPower X n).obj M.val).obj (op U) from
          exteriorPower.ιMulti (M := Γ(M, U)) Γ(X, U) n e))
      U :=
  AlgebraicGeometry.Scheme.Modules.Ws31H1.isFrameOn_toSh_ιMulti e he

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