Module

ModulesWedge.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesWedge

22 declarations indexed from sourceView source ↗

Module documentation

Exterior multiplication for module sheaves

Exterior-algebra multiplication by a vector induces natural maps on module presheaves and module sheaves through sheafification.

Imports3

Imported by3

def

mulₗ

L33 ↗

exteriorPower.mulₗ

Documentation

The exterior-algebra product as a bilinear map between the specified homogeneous degrees.

Source context 4 commands

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

universe u
open CategoryTheory MonoidalCategory
namespace exteriorPower
variable (R : Type u) [CommRing R] (M : Type u) [AddCommGroup M] [Module R M] (a b : ℕ)

Lean source · statement

def mulₗ : ⋀[R]^a M →ₗ[R] ⋀[R]^b M →ₗ[R] ⋀[R]^(a + b) M

lemma

mulₗ_apply_coe

L40 ↗

exteriorPower.mulₗ_apply_coe

Source context 4 commands

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

universe u
open CategoryTheory MonoidalCategory
namespace exteriorPower
variable (R : Type u) [CommRing R] (M : Type u) [AddCommGroup M] [Module R M] (a b : ℕ)

Lean source · statement

lemma mulₗ_apply_coe (x : ⋀[R]^a M) (y : ⋀[R]^b M) :
    ((mulₗ R M a b x y : ⋀[R]^(a + b) M) : ExteriorAlgebra R M) = x.1 * y.1

lemma

mulₗ_ιMulti_ιMulti

L43 ↗

exteriorPower.mulₗ_ιMulti_ιMulti

Source context 4 commands

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

universe u
open CategoryTheory MonoidalCategory
namespace exteriorPower
variable (R : Type u) [CommRing R] (M : Type u) [AddCommGroup M] [Module R M] (a b : ℕ)

Lean source · statement

lemma mulₗ_ιMulti_ιMulti (v : Fin a → M) (w : Fin b → M) :
    mulₗ R M a b (ιMulti R a v) (ιMulti R b w) = ιMulti R (a + b) (Fin.append v w)

lemma

comp_append

L49 ↗

exteriorPower.comp_append

Source context 6 commands

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

universe u
open CategoryTheory MonoidalCategory
namespace exteriorPower
variable (R : Type u) [CommRing R] (M : Type u) [AddCommGroup M] [Module R M] (a b : ℕ)
variable {R M} in
omit [AddCommGroup M] [Module R M] in

Lean source · statement

lemma comp_append {N : Type*} (f : M → N) (v : Fin a → M) (w : Fin b → M) :
    f ∘ Fin.append v w = Fin.append (f ∘ v) (f ∘ w)

lemma

map_mulₗ

L57 ↗

exteriorPower.map_mulₗ

Source context 6 commands

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

universe u
open CategoryTheory MonoidalCategory
namespace exteriorPower
variable (R : Type u) [CommRing R] (M : Type u) [AddCommGroup M] [Module R M] (a b : ℕ)
variable {R M} in
variable {R M} in

Lean source · statement

lemma map_mulₗ {N : Type u} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N)
    (x : ⋀[R]^a M) (y : ⋀[R]^b M) :
    map (a + b) f (mulₗ R M a b x y) = mulₗ R N a b (map a f x) (map b f y)

def

mulVec

L83 ↗

exteriorPower.mulVec

Documentation

Exterior multiplication by a vector, increasing homogeneous degree by one.

Source context 6 commands

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

universe u
open CategoryTheory MonoidalCategory
namespace exteriorPower
variable (R : Type u) [CommRing R] (M : Type u) [AddCommGroup M] [Module R M] (a b : ℕ)
variable {R M} in
variable {R M} in

Lean source · statement

def mulVec (n : ℕ) : ⋀[R]^n M →ₗ[R] M →ₗ[R] ⋀[R]^(n + 1) M

lemma

mulVec_apply

L86 ↗

exteriorPower.mulVec_apply

Source context 6 commands

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

universe u
open CategoryTheory MonoidalCategory
namespace exteriorPower
variable (R : Type u) [CommRing R] (M : Type u) [AddCommGroup M] [Module R M] (a b : ℕ)
variable {R M} in
variable {R M} in

Lean source · statement

lemma mulVec_apply (n : ℕ) (x : ⋀[R]^n M) (m : M) :
    mulVec R M n x m = mulₗ R M n 1 x ((oneEquiv R M).symm m)

lemma

mulVec_ιMulti

L89 ↗

exteriorPower.mulVec_ιMulti

Source context 6 commands

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

universe u
open CategoryTheory MonoidalCategory
namespace exteriorPower
variable (R : Type u) [CommRing R] (M : Type u) [AddCommGroup M] [Module R M] (a b : ℕ)
variable {R M} in
variable {R M} in

Lean source · full declaration

lemma mulVec_ιMulti (n : ℕ) (v : Fin n → M) (m : M) :
    mulVec R M n (ιMulti R n v) m = ιMulti R (n + 1) (Fin.append v (fun _ : Fin 1 => m)) := by
  rw [mulVec_apply, oneEquiv_symm_apply, mulₗ_ιMulti_ιMulti]

lemma

map_mulVec

L94 ↗

exteriorPower.map_mulVec

Source context 7 commands

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

universe u
open CategoryTheory MonoidalCategory
namespace exteriorPower
variable (R : Type u) [CommRing R] (M : Type u) [AddCommGroup M] [Module R M] (a b : ℕ)
variable {R M} in
variable {R M} in
variable {R M} in

Lean source · statement

lemma map_mulVec {N : Type u} [AddCommGroup N] [Module R N] (n : ℕ) (f : M →ₗ[R] N)
    (x : ⋀[R]^n M) (m : M) :
    map (n + 1) f (mulVec R M n x m) = mulVec R N n (map n f x) (f m)

lemma

mapₗ_mulVec

L112 ↗

PresheafOfModules.ExteriorPower.mapₗ_mulVec

Source context 6 commands

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

universe u
open CategoryTheory MonoidalCategory
namespace PresheafOfModules
variable {C : Type*} [Category C] {R : Cᵒᵖ ⥤ CommRingCat.{u}} (n : ℕ)
namespace ExteriorPower
variable (P : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))

Lean source · statement

lemma mapₗ_mulVec {X Y : Cᵒᵖ} (f : X ⟶ Y) (x : ⋀[R.obj X]^n (P.obj X)) (m : P.obj X) :
    mapₗ (n + 1) P f (exteriorPower.mulVec (R.obj X) (P.obj X) n x m) =
      exteriorPower.mulVec (R.obj Y) (P.obj Y) n (mapₗ n P f x) (P.map f m)

abbrev

mulVecObj

L148 ↗

PresheafOfModules.ExteriorPower.mulVecObj

Documentation

Exterior multiplication by a vector on the module of sections at an object.

Source context 5 commands

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

universe u
open CategoryTheory MonoidalCategory
namespace PresheafOfModules
variable {C : Type*} [Category C] {R : Cᵒᵖ ⥤ CommRingCat.{u}} (n : ℕ)
variable (P : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))

Lean source · statement

abbrev ExteriorPower.mulVecObj (X : Cᵒᵖ) :
    (exteriorPower n P).obj X →ₗ[R.obj X]
      (P.obj X →ₗ[R.obj X] (exteriorPower (n + 1) P).obj X)

def

wedgeVec

L155 ↗

PresheafOfModules.wedgeVec

Documentation

The morphism of module presheaves induced by exterior multiplication by a vector.

Source context 5 commands

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

universe u
open CategoryTheory MonoidalCategory
namespace PresheafOfModules
variable {C : Type*} [Category C] {R : Cᵒᵖ ⥤ CommRingCat.{u}} (n : ℕ)
variable (P : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))

Lean source · full declaration

def wedgeVec : exteriorPower n P ⊗ P ⟶ exteriorPower (n + 1) P where
  app X := ModuleCat.ofHom
    (X := (exteriorPower n P ⊗ P).obj X)
    (Y := (exteriorPower (n + 1) P).obj X)
    (TensorProduct.lift (ExteriorPower.mulVecObj n P X))
  naturality {X Y} f := by
    apply ModuleCat.MonoidalCategory.tensor_ext
    intro x m
    change exteriorPower.mulVec (R.obj Y) (P.obj Y) n
        (ExteriorPower.mapₗ n P f (show ⋀[R.obj X]^n (P.obj X) from x)) (P.map f m) =
      ExteriorPower.mapₗ (n + 1) P f
        (exteriorPower.mulVec (R.obj X) (P.obj X) n (show ⋀[R.obj X]^n (P.obj X) from x) m)
    exact (ExteriorPower.mapₗ_mulVec n P f _ m).symm

lemma

wedgeVec_app_tmul

L169 ↗

PresheafOfModules.wedgeVec_app_tmul

Source context 5 commands

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

universe u
open CategoryTheory MonoidalCategory
namespace PresheafOfModules
variable {C : Type*} [Category C] {R : Cᵒᵖ ⥤ CommRingCat.{u}} (n : ℕ)
variable (P : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))

Lean source · full declaration

lemma wedgeVec_app_tmul (X : Cᵒᵖ) (x : ⋀[R.obj X]^n (P.obj X)) (m : P.obj X) :
    ((wedgeVec n P).app X ((show (exteriorPower n P).obj X from x) ⊗ₜ[R.obj X] m) :
      ⋀[R.obj X]^(n + 1) (P.obj X)) = exteriorPower.mulVec (R.obj X) (P.obj X) n x m := rfl

lemma

wedgeVec_naturality

L174 ↗

PresheafOfModules.wedgeVec_naturality

Source context 6 commands

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

universe u
open CategoryTheory MonoidalCategory
namespace PresheafOfModules
variable {C : Type*} [Category C] {R : Cᵒᵖ ⥤ CommRingCat.{u}} (n : ℕ)
variable (P : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat))
variable {P} in

Lean source · statement

lemma wedgeVec_naturality {Q : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat)} (φ : P ⟶ Q)
  :
    (exteriorPowerMap n φ ⊗ₘ φ) ≫ wedgeVec n Q = wedgeVec n P ≫ exteriorPowerMap (n + 1) φ

def

sheafifyValIso

L195 ↗

AlgebraicGeometry.Scheme.Modules.sheafifyValIso

Documentation

The canonical sheafification isomorphism for the underlying presheaf of a sheaf of modules.

Source context 4 commands

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

universe u
open CategoryTheory MonoidalCategory
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (n : ℕ)

Lean source · statement

def sheafifyValIso (M : X.Modules) : (Scheme.Modules.sheafify X).obj M.val ≅ M

lemma

sheafifyValIso_hom_naturality

L198 ↗

AlgebraicGeometry.Scheme.Modules.sheafifyValIso_hom_naturality

Source context 4 commands

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

universe u
open CategoryTheory MonoidalCategory
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (n : ℕ)

Lean source · statement

lemma sheafifyValIso_hom_naturality {M N : X.Modules} (φ : M ⟶ N) :
    (Scheme.Modules.sheafify X).map φ.val ≫ (sheafifyValIso N).hom = (sheafifyValIso M).hom ≫ φ

lemma

sheafifyValIso_inv_naturality

L204 ↗

AlgebraicGeometry.Scheme.Modules.sheafifyValIso_inv_naturality

Source context 4 commands

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

universe u
open CategoryTheory MonoidalCategory
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (n : ℕ)

Lean source · statement

lemma sheafifyValIso_inv_naturality {M N : X.Modules} (φ : M ⟶ N) :
    φ ≫ (sheafifyValIso N).inv = (sheafifyValIso M).inv ≫ (Scheme.Modules.sheafify X).map φ.val

lemma

det_eq

L209 ↗

AlgebraicGeometry.Scheme.Modules.det_eq

Source context 4 commands

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

universe u
open CategoryTheory MonoidalCategory
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (n : ℕ)

Lean source · statement

lemma det_eq (M : X.Modules) :
    Scheme.Modules.det n M = (Scheme.Modules.sheafify X).obj ((presheafExteriorPower X n).obj M.val)

lemma

exteriorPower_map_eq

L213 ↗

AlgebraicGeometry.Scheme.Modules.exteriorPower_map_eq

Source context 4 commands

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

universe u
open CategoryTheory MonoidalCategory
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (n : ℕ)

Lean source · statement

lemma exteriorPower_map_eq {M N : X.Modules} (φ : M ⟶ N) :
    (exteriorPower X n).map φ = (Scheme.Modules.sheafify X).map ((presheafExteriorPower X n).map
        φ.val)

def

wedgeVec

L219 ↗

AlgebraicGeometry.Scheme.Modules.wedgeVec

Documentation

Exterior multiplication by a local section, transported from presheaves through sheafification.

Source context 4 commands

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

universe u
open CategoryTheory MonoidalCategory
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (n : ℕ)

Lean source · statement

def wedgeVec (M : X.Modules) : Scheme.Modules.det n M ⊗ M ⟶ Scheme.Modules.det (n + 1)
  M

lemma

whiskerRight_exteriorPower_map_comp_wedgeVec

L226 ↗

AlgebraicGeometry.Scheme.Modules.whiskerRight_exteriorPower_map_comp_wedgeVec

Source context 4 commands

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

universe u
open CategoryTheory MonoidalCategory
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (n : ℕ)

Lean source · statement

lemma whiskerRight_exteriorPower_map_comp_wedgeVec {M N : X.Modules} (φ : M ⟶ N) :
    ((exteriorPower X n).map φ ▷ N) ≫ wedgeVec n N =
      (Scheme.Modules.det n M ◁ (sheafifyValIso N).inv) ≫
        Functor.LaxMonoidal.μ (Scheme.Modules.sheafify X) ((presheafExteriorPower X n).obj M.val)
            N.val ≫
          (Scheme.Modules.sheafify X).map
            (((presheafExteriorPower X n).map φ.val ▷ N.val) ≫ PresheafOfModules.wedgeVec n N.val)

lemma

wedgeVec_naturality

L239 ↗

AlgebraicGeometry.Scheme.Modules.wedgeVec_naturality

Source context 4 commands

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

universe u
open CategoryTheory MonoidalCategory
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} (n : ℕ)

Lean source · statement

lemma wedgeVec_naturality {M N : X.Modules} (φ : M ⟶ N) :
    ((exteriorPower X n).map φ ⊗ₘ φ) ≫ wedgeVec n N = wedgeVec n M ≫ (exteriorPower X (n + 1)).map φ

Module documentation

Exterior multiplication for module sheaves

Declarations