Module

Scheme_IdealSheafData_IsInvertible_isInvertible_invModule.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_isInvertible_invModule

1 declaration indexed from sourceView source ↗

Module documentation

Invertibility of the inverse module of an ideal sheaf

The inverse module is the dual of the module associated to the invertible ideal sheaf.

Imports5

Imported by84

theorem

isInvertible_invModule

L54 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.isInvertible_invModule

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_isInvertible_invModule
attribute [-instance]
  PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ
  PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η
  PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.freeεIso_hom_app PresheafOfModules.freeμIso_hom_app
universe u
open CategoryTheory AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.isInvertible_invModule {X :
  AlgebraicGeometry.Scheme.{u}} {I : X.IdealSheafData} (hI : I.IsInvertible) :
    AlgebraicGeometry.Scheme.Modules.IsInvertible I.invModule

Module documentation

Invertibility of the inverse module of an ideal sheaf

Declarations

isInvertible_invModule