Documentation

DerivedAlgGeo.AlgebraicGeometry.Modules.ExteriorPower.Restriction

Restriction and exterior powers #

This file compares restriction of a sheaf exterior power with the sheafification of the objectwise exterior power on the restricted site.

source
@[implicit_reducible]
def AlgebraicGeometry.Scheme.Modules.exteriorPowerRestrictionCategory {X : Scheme} :
CategoryTheory.Category.{u, u + 1} X.Modules
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def AlgebraicGeometry.Scheme.Modules.exteriorPowerOver {X : Scheme} (E : X.Modules) (U : X.Opens) (n : ℕ) :
    SheafOfModules (CategoryTheory.Sheaf.over X.ringCatSheaf U)

    On an open slice, sheafify the objectwise exterior power of the restricted sheaf.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def AlgebraicGeometry.Scheme.Modules.exteriorPowerOverMapIsoOfIso {X : Scheme} (U : X.Opens) {M N : SheafOfModules (CategoryTheory.Sheaf.over X.ringCatSheaf U)} (e : M ≅ N) (n : ℕ) :
      (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (CategoryTheory.Sheaf.over X.ringCatSheaf U).obj)).obj (PresheafOfModules.exteriorPower (CategoryTheory.Sheaf.over X.sheaf U).obj ((SheafOfModules.forget (CategoryTheory.Sheaf.over X.ringCatSheaf U)).obj M) n) ≅ (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (CategoryTheory.Sheaf.over X.ringCatSheaf U).obj)).obj (PresheafOfModules.exteriorPower (CategoryTheory.Sheaf.over X.sheaf U).obj ((SheafOfModules.forget (CategoryTheory.Sheaf.over X.ringCatSheaf U)).obj N) n)

      Sheafified exterior power on an open slice carries isomorphic module sheaves to isomorphic exterior powers.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def AlgebraicGeometry.Scheme.Modules.exteriorPowerOverMapIso {X : Scheme} {E F : X.Modules} (U : X.Opens) (e : SheafOfModules.over E U ≅ SheafOfModules.over F U) (n : ℕ) :
        E.exteriorPowerOver U n ≅ F.exteriorPowerOver U n

        Exterior power on an open slice carries isomorphic restricted sheaves to isomorphic exterior powers.

        Equations
        Instances For
          source
          noncomputable def AlgebraicGeometry.Scheme.Modules.topExteriorFreeOverIso {X : Scheme} (U : X.Opens) (n : ℕ) :
          (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (CategoryTheory.Sheaf.over X.ringCatSheaf U).obj)).obj (PresheafOfModules.exteriorPower (CategoryTheory.Sheaf.over X.sheaf U).obj ((SheafOfModules.forget (CategoryTheory.Sheaf.over X.ringCatSheaf U)).obj (SheafOfModules.free (ULift.{u, 0} (Fin n)))) n) ≅ SheafOfModules.unit (CategoryTheory.Sheaf.over X.ringCatSheaf U)

          On an open slice, the top exterior power of the free rank-n sheaf is the structure sheaf.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def AlgebraicGeometry.Scheme.Modules.overExteriorPowerPresheafIso {X : Scheme} (P : X.PresheafOfModules) (U : X.Opens) (n : ℕ) :
            (AlgebraicGeometry.Scheme.Modules.overPresheafFunctor✝ X U).obj (PresheafOfModules.exteriorPower X.presheaf P n) ≅ PresheafOfModules.exteriorPower (CategoryTheory.Sheaf.over X.sheaf U).obj ((AlgebraicGeometry.Scheme.Modules.overPresheafFunctor✝ X U).obj P) n

            Restricting an objectwise exterior-power presheaf is the objectwise exterior power of the restricted presheaf.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def AlgebraicGeometry.Scheme.Modules.exteriorPowerOverIso {X : Scheme} (E : X.Modules) (U : X.Opens) (n : ℕ) :
              SheafOfModules.over (E.exteriorPower n) U ≅ E.exteriorPowerOver U n

              Restriction of a sheaf exterior power agrees with the exterior power formed on the open slice.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For