Module

Scheme_Modules_isInvertible_det_of_isLocallyFreeOfRank.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isInvertible_det_of_isLocallyFreeOfRank

1 declaration indexed from sourceView source ↗

Module documentation

Invertibility of determinants

The determinant of a locally free module sheaf of fixed rank is invertible.

Imports5

Imported by11

theorem

isInvertible_det_of_isLocallyFreeOfRank

L38 ↗

AlgebraicGeometry.Scheme.Modules.isInvertible_det_of_isLocallyFreeOfRank

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isInvertible_det_of_isLocallyFreeOfRank
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
    PresheafOfModules.pushforwardNatTrans_app_app_apply
    PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open CategoryTheory AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.isInvertible_det_of_isLocallyFreeOfRank {X :
  Scheme.{u}} {n : ℕ} {M : X.Modules}
    (hM : Scheme.Modules.IsLocallyFreeOfRank n M) :
    Scheme.Modules.IsInvertible (Scheme.Modules.det n M)

Module documentation

Invertibility of determinants

Declarations

isInvertible_det_of_isLocallyFreeOfRank