NYLL
Module

Scheme_Modules_nonempty_exteriorPower_free_iso_unit.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_exteriorPower_free_iso_unit
40 declarations indexed from sourceView source ↗

Module documentation

Top exterior powers of finite free module sheaves

The standard basis determines a top exterior form and an isomorphism from the top exterior power of a free module sheaf to the tensor unit.

Imports3
Imported by5

Declarations

instance

uniquePowersetCardFin

L40 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.exteriorPower.uniquePowersetCardFin
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace exteriorPower
open _root_.exteriorPower
open _root_.exteriorPower
variable (A : Type u) [CommRing A] (n : ℕ)
Lean source · full declaration
instance uniquePowersetCardFin : 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))
def

topForm

L46 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.exteriorPower.topForm
Documentation

The top exterior form determined by the standard basis.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace exteriorPower
open _root_.exteriorPower
open _root_.exteriorPower
variable (A : Type u) [CommRing A] (n : ℕ)
Lean source · statement
def topForm : ⋀[A]^n (Fin n → A)
abbrev

topBasis

L50 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.exteriorPower.topBasis
Documentation

The exterior power basis of the standard basis in top degree.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace exteriorPower
open _root_.exteriorPower
open _root_.exteriorPower
variable (A : Type u) [CommRing A] (n : ℕ)
Lean source · statement
abbrev topBasis : Module.Basis (Set.powersetCard (Fin n) n) A (⋀[A]^n (Fin n → A))
lemma

topBasis_apply

L53 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.exteriorPower.topBasis_apply
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace exteriorPower
open _root_.exteriorPower
open _root_.exteriorPower
variable (A : Type u) [CommRing A] (n : ℕ)
Lean source · statement
lemma topBasis_apply (s : Set.powersetCard (Fin n) n) : topBasis A n s = topForm A n
def

topEquiv

L58 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.exteriorPower.topEquiv
Documentation

Identify the top exterior power with the coefficient ring using its standard form.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace exteriorPower
open _root_.exteriorPower
open _root_.exteriorPower
variable (A : Type u) [CommRing A] (n : ℕ)
Lean source · statement
def topEquiv : ⋀[A]^n (Fin n → A) ≃ₗ[A] A
lemma

topEquiv_topForm

L61 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.exteriorPower.topEquiv_topForm
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace exteriorPower
open _root_.exteriorPower
open _root_.exteriorPower
variable (A : Type u) [CommRing A] (n : ℕ)
Lean source · statement
lemma topEquiv_topForm : topEquiv A n (topForm A n) = 1
lemma

topEquiv_symm_apply

L67 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.exteriorPower.topEquiv_symm_apply
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace exteriorPower
open _root_.exteriorPower
open _root_.exteriorPower
variable (A : Type u) [CommRing A] (n : ℕ)
Lean source · statement
lemma topEquiv_symm_apply (a : A) : (topEquiv A n).symm a = a • topForm A n
lemma

eq_topEquiv_smul_topForm

L72 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.exteriorPower.eq_topEquiv_smul_topForm
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace exteriorPower
open _root_.exteriorPower
open _root_.exteriorPower
variable (A : Type u) [CommRing A] (n : ℕ)
Lean source · statement
lemma eq_topEquiv_smul_topForm (x : ⋀[A]^n (Fin n → A)) : x = topEquiv A n x • topForm A n
lemma

exists_eq_smul_topForm

L76 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.exteriorPower.exists_eq_smul_topForm
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace exteriorPower
open _root_.exteriorPower
open _root_.exteriorPower
variable (A : Type u) [CommRing A] (n : ℕ)
Lean source · statement
lemma exists_eq_smul_topForm (x : ⋀[A]^n (Fin n → A)) : ∃ a : A, x = a • topForm A n
def

piPowAb

L88 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.PresheafOfModules.piPowAb
Documentation

The presheaf of tuples of regular functions with pointwise restriction.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
variable {C : Type*} [Category C] (R : Cᵒᵖ ⥤ CommRingCat.{u}) (n : ℕ)
Lean source · full declaration
def piPowAb : Cᵒᵖ ⥤ Ab.{u} where
  obj X := AddCommGrpCat.of (Fin n → R.obj X)
  map {X Y} f := AddCommGrpCat.ofHom (AddMonoidHom.compLeft (R.map f).hom.toAddMonoidHom (Fin n))
  map_id X := by ext v i; simp
  map_comp f g := by ext v i; simp
instance

instModulePiPowAb

L94 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.PresheafOfModules.instModulePiPowAb
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
variable {C : Type*} [Category C] (R : Cᵒᵖ ⥤ CommRingCat.{u}) (n : ℕ)
Lean source · statement
instance instModulePiPowAb (X : Cᵒᵖ) :
    Module ((R ⋙ forget₂ CommRingCat RingCat).obj X) ((piPowAb R n).obj X)
def

piPow

L99 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.PresheafOfModules.piPow
Documentation

The module presheaf of tuples of regular functions.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
variable {C : Type*} [Category C] (R : Cᵒᵖ ⥤ CommRingCat.{u}) (n : ℕ)
Lean source · statement
def piPow : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat RingCat)
lemma

piPow_map_apply

L105 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.PresheafOfModules.piPow_map_apply
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
variable {C : Type*} [Category C] (R : Cᵒᵖ ⥤ CommRingCat.{u}) (n : ℕ)
Lean source · full declaration
lemma piPow_map_apply {X Y : Cᵒᵖ} (f : X ⟶ Y) (v : Fin n → R.obj X) (i : Fin n) :
    ((piPow R n).map f (show (piPow R n).obj X from v) : Fin n → R.obj Y) i = R.map f (v i) := rfl
lemma

piPow_map_basisFun

L108 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.PresheafOfModules.piPow_map_basisFun
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
variable {C : Type*} [Category C] (R : Cᵒᵖ ⥤ CommRingCat.{u}) (n : ℕ)
Lean source · full declaration
lemma piPow_map_basisFun {X Y : Cᵒᵖ} (f : X ⟶ Y) (j : Fin n) :
    ((piPow R n).map f (show (piPow R n).obj X from Pi.basisFun (R.obj X) (Fin n) j) :
      Fin n → R.obj Y) = Pi.basisFun (R.obj Y) (Fin n) j := by
  funext i
  rw [piPow_map_apply, Pi.basisFun_apply, Pi.basisFun_apply, Pi.single_apply, Pi.single_apply]
  split_ifs <;> simp
lemma

mapₗ_topForm

L117 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.PresheafOfModules.mapₗ_topForm
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
variable {C : Type*} [Category C] (R : Cᵒᵖ ⥤ CommRingCat.{u}) (n : ℕ)
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs in
open scoped Scheme_Modules_nonempty_exteriorPower_free_iso_unit.exteriorPower in
Lean source · statement
lemma mapₗ_topForm {X Y : Cᵒᵖ} (f : X ⟶ Y) :
    ExteriorPower.mapₗ n (piPow R n) f (exteriorPower.topForm (R.obj X) n) =
      exteriorPower.topForm (R.obj Y) n
lemma

topEquiv_mapₗ

L129 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.PresheafOfModules.topEquiv_mapₗ
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
variable {C : Type*} [Category C] (R : Cᵒᵖ ⥤ CommRingCat.{u}) (n : ℕ)
Lean source · statement
lemma topEquiv_mapₗ {X Y : Cᵒᵖ} (f : X ⟶ Y) (x : ⋀[R.obj X]^n (Fin n → R.obj X)) :
    exteriorPower.topEquiv (R.obj Y) n (ExteriorPower.mapₗ n (piPow R n) f x) =
      R.map f (exteriorPower.topEquiv (R.obj X) n x)
lemma

unit_map_apply

L147 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.PresheafOfModules.unit_map_apply
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
variable {C : Type*} [Category C] (R : Cᵒᵖ ⥤ CommRingCat.{u}) (n : ℕ)
Lean source · full declaration
lemma unit_map_apply {X Y : Cᵒᵖ} (f : X ⟶ Y) (a : R.obj X) :
    ((unit (R ⋙ forget₂ CommRingCat RingCat)).map f
      (show (unit (R ⋙ forget₂ CommRingCat RingCat)).obj X from a) : R.obj Y) = R.map f a := rfl
def

piPowTopHomAb

L152 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.PresheafOfModules.piPowTopHomAb
Documentation

The presheaf map from the top exterior power to its coefficient ring.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
variable {C : Type*} [Category C] (R : Cᵒᵖ ⥤ CommRingCat.{u}) (n : ℕ)
Lean source · full declaration
def piPowTopHomAb :
    ExteriorPower.presheafAb n (piPow R n) ⟶ (unit (R ⋙ forget₂ CommRingCat RingCat)).presheaf where
  app X := AddCommGrpCat.ofHom (X := ⋀[R.obj X]^n (Fin n → R.obj X)) (Y := R.obj X)
    (exteriorPower.topEquiv (R.obj X) n).toLinearMap.toAddMonoidHom
  naturality {X Y} f := by
    ext x
    exact topEquiv_mapₗ R n f x
def

piPowTopInvAb

L161 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.PresheafOfModules.piPowTopInvAb
Documentation

The presheaf map sending a coefficient to a multiple of the standard top form.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
variable {C : Type*} [Category C] (R : Cᵒᵖ ⥤ CommRingCat.{u}) (n : ℕ)
Lean source · full declaration
def piPowTopInvAb :
    (unit (R ⋙ forget₂ CommRingCat RingCat)).presheaf ⟶ ExteriorPower.presheafAb n (piPow R n) where
  app X := AddCommGrpCat.ofHom (X := R.obj X) (Y := ⋀[R.obj X]^n (Fin n → R.obj X))
    (LinearMap.toSpanSingleton (R.obj X) (⋀[R.obj X]^n (Fin n → R.obj X))
      (exteriorPower.topForm (R.obj X) n)).toAddMonoidHom
  naturality {X Y} f :=
    AddCommGrpCat.ext fun (a : R.obj X) =>
      ((ExteriorPower.mapₗ_smul n (piPow R n) f a
        (exteriorPower.topForm (R.obj X) n)).trans
          (congrArg (fun z : ⋀[R.obj Y]^n (Fin n → R.obj Y) => R.map f a • z)
            (mapₗ_topForm R n f))).symm
def

exteriorPowerPiPowIso

L174 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.PresheafOfModules.exteriorPowerPiPowIso
Documentation

The top exterior power of the tuple presheaf is the unit module presheaf.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
variable {C : Type*} [Category C] (R : Cᵒᵖ ⥤ CommRingCat.{u}) (n : ℕ)
Lean source · full declaration
def exteriorPowerPiPowIso :
    exteriorPower n (piPow R n) ≅ unit (R ⋙ forget₂ CommRingCat RingCat) where
  hom := homMk (piPowTopHomAb R n) (fun X r m =>
    map_smul (exteriorPower.topEquiv (R.obj X) n) (show R.obj X from r)
      (show ⋀[R.obj X]^n (Fin n → R.obj X) from m))
  inv := homMk (M₁ := unit _) (piPowTopInvAb R n) (fun X r a =>
    mul_smul (show R.obj X from r) (show R.obj X from a) (exteriorPower.topForm (R.obj X) n))
  hom_inv_id := by
    ext X : 1
    refine ModuleCat.hom_ext (LinearMap.ext fun x => ?_)
    exact (exteriorPower.eq_topEquiv_smul_topForm (R.obj X) n x).symm
  inv_hom_id := by
    ext X : 1
    refine ModuleCat.hom_ext (LinearMap.ext fun (a : R.obj X) => ?_)
    change exteriorPower.topEquiv (R.obj X) n (a • exteriorPower.topForm (R.obj X) n) = a
    rw [← exteriorPower.topEquiv_symm_apply, LinearEquiv.apply_symm_apply]
lemma

sum_app

L197 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.PresheafOfModules.sum_app
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace PresheafOfModules
open _root_.PresheafOfModules
open _root_.PresheafOfModules
Lean source · statement
lemma sum_app {C : Type*} [Category C] {R : Cᵒᵖ ⥤ RingCat.{u}} {M N : PresheafOfModules.{u} R}
    {ι : Type*} (s : Finset ι) (f : ι → (M ⟶ N)) (X : Cᵒᵖ) :
    (∑ i ∈ s, f i).app X = ∑ i ∈ s, (f i).app X
lemma

sum_val

L208 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.SheafOfModules.sum_val
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
namespace SheafOfModules
open _root_.SheafOfModules
open _root_.SheafOfModules
Lean source · statement
lemma sum_val {C : Type*} [Category C] {J : GrothendieckTopology C} {R : Sheaf J RingCat.{u}}
    {M N : SheafOfModules.{u} R} {ι : Type*} (s : Finset ι) (f : ι → (M ⟶ N)) :
    (∑ i ∈ s, f i).val = ∑ i ∈ s, (f i).val
abbrev

piPowPresheaf

L230 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.AlgebraicGeometry.Scheme.Modules.piPowPresheaf
Documentation

The tuple module presheaf on a scheme.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
Lean source · statement
abbrev piPowPresheaf : X.PresheafOfModules
abbrev

ringCatSheafAb

L233 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.AlgebraicGeometry.Scheme.Modules.ringCatSheafAb
Documentation

The structure sheaf viewed as a sheaf of abelian groups.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
Lean source · statement
abbrev ringCatSheafAb : Sheaf (Opens.grothendieckTopology X) AddCommGrpCat.{u}
def

piPowCone

L238 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.AlgebraicGeometry.Scheme.Modules.piPowCone
Documentation

The cone expressing tuples as the product of copies of the structure presheaf.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
Lean source · full declaration
def piPowCone :
    Cone (Discrete.functor (fun _ : Fin n => ringCatSheafAb X) ⋙ sheafToPresheaf _ _) where
  pt := (piPowPresheaf X n).presheaf
  π := Discrete.natTrans (fun i =>
    { app := fun V => AddCommGrpCat.ofHom (X := Fin n → (X.presheaf.obj V : Type u))
        (Y := (X.presheaf.obj V : Type u))
        (Pi.evalAddMonoidHom (fun _ : Fin n => (X.presheaf.obj V : Type u)) i.as)
      naturality := fun V W g => by ext v; rfl })
def

isLimitPiPowCone

L248 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.AlgebraicGeometry.Scheme.Modules.isLimitPiPowCone
Documentation

The tuple cone is a limit cone.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
Lean source · statement
def isLimitPiPowCone : IsLimit (piPowCone X n)
lemma

isSheaf_piPowPresheaf

L263 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.AlgebraicGeometry.Scheme.Modules.isSheaf_piPowPresheaf
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
Lean source · statement
lemma isSheaf_piPowPresheaf :
    Presheaf.IsSheaf (Opens.grothendieckTopology X) (piPowPresheaf X n).presheaf
def

piPow

L267 ↗
AlgebraicGeometry.Scheme.Modules.piPow
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
Lean source · full declaration
def _root_.AlgebraicGeometry.Scheme.Modules.piPow : X.Modules where
  val := piPowPresheaf X n
  isSheaf := isSheaf_piPowPresheaf X n
def

piPowπ

L274 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.AlgebraicGeometry.Scheme.Modules.piPowπ
Documentation

Projection from the tuple module to one coordinate.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
open _root_.AlgebraicGeometry.Scheme.Modules
Lean source · statement
def piPowπ (i : Fin n) : piPow X n ⟶ SheafOfModules.unit X.ringCatSheaf
lemma

piPowπ_apply

L282 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.AlgebraicGeometry.Scheme.Modules.piPowπ_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_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
open _root_.AlgebraicGeometry.Scheme.Modules
Lean source · full declaration
lemma piPowπ_apply (i : Fin n) (V : X.Opensᵒᵖ) (v : Fin n → (X.presheaf.obj V : Type u)) :
    ((piPowπ X n i).val.app V (show (piPow X n).val.obj V from v) : X.presheaf.obj V) = v i := rfl
def

piPowι

L286 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.AlgebraicGeometry.Scheme.Modules.piPowι
Documentation

Inclusion of a single coordinate into the tuple module.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
open _root_.AlgebraicGeometry.Scheme.Modules
Lean source · statement
def piPowι (i : Fin n) : SheafOfModules.unit X.ringCatSheaf ⟶ piPow X n
lemma

piPowι_apply

L305 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.AlgebraicGeometry.Scheme.Modules.piPowι_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_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
open _root_.AlgebraicGeometry.Scheme.Modules
Lean source · full declaration
lemma piPowι_apply (i : Fin n) (V : X.Opensᵒᵖ) (a : (X.presheaf.obj V : Type u)) :
    ((piPowι X n i).val.app V (show (SheafOfModules.unit X.ringCatSheaf).val.obj V from a) :
      Fin n → X.presheaf.obj V) = Pi.single i a := rfl
def

piPowBicone

L310 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.AlgebraicGeometry.Scheme.Modules.piPowBicone
Documentation

The bicone of coordinate projections and inclusions for the tuple module.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
open _root_.AlgebraicGeometry.Scheme.Modules
Lean source · full declaration
def piPowBicone :
    Bicone (fun _ : ULift.{u} (Fin n) => SheafOfModules.unit X.ringCatSheaf) where
  pt := piPow X n
  π j := piPowπ X n j.down
  ι j := piPowι X n j.down
  ι_π j j' := by
    refine SheafOfModules.hom_ext (PresheafOfModules.hom_ext fun V => ModuleCat.hom_ext
      (LinearMap.ext fun (a : X.presheaf.obj V) => ?_))
    by_cases h : j = j'
    · subst h
      rw [dite_eq_left rfl]
      change (Pi.single j.down a : Fin n → X.presheaf.obj V) j.down = a
      simp
    · rw [dite_eq_right h]
      have h' : j'.down ≠ j.down := fun e => h (ULift.ext e.symm)
      change (Pi.single j.down a : Fin n → X.presheaf.obj V) j'.down = (0 : X.presheaf.obj V)
      simp [h']
lemma

piPowBicone_total

L328 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.AlgebraicGeometry.Scheme.Modules.piPowBicone_total
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
open _root_.AlgebraicGeometry.Scheme.Modules
Lean source · statement
lemma piPowBicone_total :
    ∑ j : ULift.{u} (Fin n), (piPowBicone X n).π j ≫ (piPowBicone X n).ι j = 𝟙 (piPow X n)
def

isBilimitPiPowBicone

L341 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.AlgebraicGeometry.Scheme.Modules.isBilimitPiPowBicone
Documentation

The coordinate bicone is a biproduct.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
open _root_.AlgebraicGeometry.Scheme.Modules
Lean source · statement
def isBilimitPiPowBicone : (piPowBicone X n).IsBilimit
def

freeIsoPiPow

L345 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.AlgebraicGeometry.Scheme.Modules.freeIsoPiPow
Documentation

Identify the finite free module sheaf with tuples of regular functions.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
open _root_.AlgebraicGeometry.Scheme.Modules
Lean source · statement
def freeIsoPiPow : SheafOfModules.free.{u} (ULift.{u} (Fin n)) ≅ piPow X n
def

sheafificationUnitIso

L351 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.AlgebraicGeometry.Scheme.Modules.sheafificationUnitIso
Documentation

Identify the sheafification of the unit presheaf with the unit sheaf.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
open _root_.AlgebraicGeometry.Scheme.Modules
Lean source · statement
def sheafificationUnitIso :
    (PresheafOfModules.sheafification (𝟙 X.ringCatSheaf.obj)).obj (PresheafOfModules.unit _) ≅
      SheafOfModules.unit X.ringCatSheaf
def

exteriorPowerFreeIso

L359 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.AlgebraicGeometry.Scheme.Modules.exteriorPowerFreeIso
Documentation

The top exterior power of the finite free module sheaf is the unit sheaf.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
open _root_.AlgebraicGeometry.Scheme.Modules
Lean source · statement
def exteriorPowerFreeIso :
    (exteriorPower X n).obj (SheafOfModules.free.{u} (ULift.{u} (Fin n))) ≅
      SheafOfModules.unit X.ringCatSheaf
theorem

nonempty_exteriorPowerFreeIso

L367 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_exteriorPower_free_iso_unit.AlgebraicGeometry.Scheme.Modules.nonempty_exteriorPowerFreeIso
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
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
open TopologicalSpace
variable (X : Scheme.{u}) (n : ℕ)
open _root_.AlgebraicGeometry.Scheme.Modules
Lean source · statement
theorem nonempty_exteriorPowerFreeIso :
    Nonempty ((exteriorPower X n).obj (SheafOfModules.free.{u} (ULift.{u} (Fin n))) ≅
      SheafOfModules.unit X.ringCatSheaf)
theorem

nonempty_exteriorPower_free_iso_unit

L375 ↗
AlgebraicGeometry.Scheme.Modules.nonempty_exteriorPower_free_iso_unit
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_exteriorPower_free_iso_unit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry AlgebraicGeometry in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.nonempty_exteriorPower_free_iso_unit (X :
  Scheme.{u}) (n : ℕ) :
    Nonempty ((Scheme.Modules.exteriorPower X n).obj (SheafOfModules.free.{u} (ULift.{u} (Fin n))) ≅
      SheafOfModules.unit X.ringCatSheaf)

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