OAI/AlgebraicGeometry/SurfaceCones/ExteriorSheaf.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Localization of bilinear and alternating forms.

  1. lemma OAI.ActualExterior.targetUnits line 16
  2. def OAI.ActualExterior.liftLinear line 21

    Source documentation

    The localized linear-map universal property, linear in its input.

    def liftLinear : (M →ₗ[R] N) →ₗ[R] (M' →ₗ[S] N) where
…
  3. lemma OAI.ActualExterior.liftLinear_apply line 37
  4. def OAI.ActualExterior.liftBilinear line 41

    Source documentation

    Extend a bilinear form in both arguments.

    def liftBilinear (b : M →ₗ[R] M →ₗ[R] N) : M' →ₗ[S] M' →ₗ[S] N :=
…
  5. lemma OAI.ActualExterior.liftBilinear_apply line 44
  6. lemma OAI.ActualExterior.liftBilinear_isAlt line 48
  7. lemma OAI.ActualExterior.update_pair_zero line 72
  8. lemma OAI.ActualExterior.update_pair_one line 76
  9. def OAI.ActualExterior.alternatingToBilinear line 84
  10. lemma OAI.ActualExterior.alternatingToBilinear_isAlt line 91
  11. def OAI.ActualExterior.bilinearToAlternating line 98

    Source documentation

    Alternating bilinear maps expressed in the standard exterior universal-property format.

    def bilinearToAlternating (b : M →ₗ[R] M →ₗ[R] N) (hb : b.IsAlt) :
    M [⋀^Fin 2]→ₗ[R] N where
…
  12. lemma OAI.ActualExterior.bilinearToAlternating_apply line 122
  13. lemma OAI.ActualExterior.alternatingToBilinear_apply line 124
  14. lemma OAI.ActualExterior.bilinearToAlternating_alternatingToBilinear line 126
  15. def OAI.ActualExterior.liftAlternatingTwo line 140
  16. lemma OAI.ActualExterior.liftAlternatingTwo_apply line 144
  17. lemma OAI.ActualExterior.alternatingTwo_ext_localized line 154
  18. def OAI.ActualExterior.restrictAlternatingTwo line 188
  19. lemma OAI.ActualExterior.restrictAlternatingTwo_apply line 192
  20. def OAI.ActualExterior.localizationTwoMap line 196

    Source documentation

    Exterior vectors transform by the localization of their entries.

    def localizationTwoMap : (⋀[R]^2 M) →ₗ[R] (⋀[S]^2 N) :=
…
  21. lemma OAI.ActualExterior.localizationTwoMap_mk line 201
  22. def OAI.ActualExterior.localizationTwoInverse line 209
  23. lemma OAI.ActualExterior.localizationTwoInverse_mk line 214
  24. def OAI.ActualExterior.localizationTwoForward line 219
  25. lemma OAI.ActualExterior.localizationTwoForward_mk line 224
  26. lemma OAI.ActualExterior.localizationTwoInverse_forward line 229
  27. lemma OAI.ActualExterior.localizationTwoForward_inverse line 240
  28. def OAI.ActualExterior.localizationTwoEquiv line 250
  29. lemma OAI.ActualExterior.localizationTwoEquiv_comp line 255
  30. lemma OAI.ActualExterior.localizationTwoMap_isLocalized line 267
  31. def OAI.ActualExterior.scalarAlternating line 283
  32. def OAI.ActualExterior.powerMap line 320

    Source documentation

    Restriction of exterior vectors, using the given semilinear restriction maps of the module presheaf.

    def powerMap {X Y : Cᵒᵖ} (f : X ⟶ Y) :
    (M.obj X).exteriorPower n ⟶
      (ModuleCat.restrictScalars (R.map f).hom).obj ((M.obj Y).exteriorPower n) :=
…
  33. lemma OAI.ActualExterior.powerMap_ι line 325
  34. def OAI.ActualExterior.presheaf line 331

    Source documentation

    Objectwise exterior powers of the sections and their maps.

    def presheaf : PresheafOfModules.{u} (R ⋙ forget₂ _ _) where
…
  35. lemma OAI.ActualExterior.naturalityOnWedge line 370
  36. def OAI.ActualExterior.presheafMap line 402
  37. def OAI.ActualExterior.presheafFunctor line 411
  38. abbrev OAI.ActualExterior.schemeSheafification line 435
  39. def OAI.ActualExterior.sheafFunctor line 440

    Source documentation

    The sheaf of exterior powers.

    def sheafFunctor (X : Scheme.{u}) (n : ℕ) : X.Modules ⥤ X.Modules :=
…
  40. def OAI.ActualExterior.semilinearMap line 455
  41. lemma OAI.ActualExterior.semilinearMap_mk line 461
  42. lemma OAI.ActualExterior.semilinear_ext line 467

    Source documentation

    Extensionality for semilinear maps on the exterior power.

    lemma semilinear_ext {P : ModuleCat.{u} B} {a b : M.exteriorPower n →ₛₗ[φ] P}
    (h : ∀ z : Fin n → M, a (ModuleCat.exteriorPower.mk z) =
      b (ModuleCat.exteriorPower.mk z)) : a = b := by
…
  43. lemma OAI.ActualExterior.semilinearMap_left_inverse line 479
  44. def OAI.ActualExterior.semilinearEquiv line 498

    Source documentation

    exterior powers commute with semilinear coordinate isomorphisms, including all open-restriction coefficient-ring isomorphisms.

    def semilinearEquiv (f : M ≃ₛₗ[e.toRingHom] N) :
    M.exteriorPower n ≃ₛₗ[e.toRingHom] N.exteriorPower n where
…