NYLL
Module

Scheme_Modules_nonempty_det_succ_iso_det_tensor_of_shortExact.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_det_succ_iso_det_tensor_of_shortExact
1 declaration indexed from sourceView source ↗

Module documentation

Determinants in a short exact sequence

For a locally free short exact complex with an invertible quotient, the determinant of the middle term is the determinant of the first term tensored with the quotient.

Imports11
Imported by4

Declarations

theorem

nonempty_det_succ_iso_det_tensor_of_shortExact

L67 ↗
AlgebraicGeometry.Scheme.Modules.nonempty_det_succ_iso_det_tensor_of_shortExact
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_det_succ_iso_det_tensor_of_shortExact
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.pushforwardCongr_inv_app_app_apply
    PresheafOfModules.pushforwardNatTrans_app_app_apply
    PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
    PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.nonempty_det_succ_iso_det_tensor_of_shortExact
    {X : Scheme.{u}} {n : ℕ} (S : ShortComplex X.Modules) (hS : S.ShortExact)
    (h₁ : Scheme.Modules.IsLocallyFreeOfRank n S.X₁) (h₂ : Scheme.Modules.IsLocallyFreeOfRank (n +
        1) S.X₂)
    (h₃ : Scheme.Modules.IsInvertible S.X₃) :
    Nonempty (Scheme.Modules.det (n + 1) S.X₂ ≅ Scheme.Modules.det n S.X₁ ⊗ S.X₃)

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