Determinant lines and first Chern classes

DerivedAlgGeo constructs exterior powers of module sheaves by sheafifying the objectwise exterior power presheaf. This file separates that construction from the remaining geometric assertion that the top exterior power of a fixed-rank locally free sheaf is invertible:

• Module.topExteriorPower R n is the actual top exterior power of the free rank-n R-module, and has rank one;
• Scheme.Modules.FiniteLocallyFreeData E n records a fixed-rank locally free atlas for a module sheaf;
• Scheme.Modules.DeterminantData E records that atlas together with a chosen global invertible sheaf realizing the descended top exterior power and an explicit tensor inverse;
• direct-sum and short-exact compatibility are expressed by explicit comparison isomorphisms, from which additivity of the resulting first Chern class follows;
• the coherent-sheaf API only applies to coherent objects carrying this explicit finite locally free determinant data. It deliberately does not claim that every coherent sheaf has a finite locally free resolution.

This is the same explicit-certificate design used for effective Cartier divisors: unsupported global existence claims do not hide behind typeclass inference, while downstream work gets a stable determinant/c₁ interface whose hypotheses are visible in theorem types.

structure AlgebraicGeometry.Scheme.Modules.FiniteLocallyFreeData {X : Scheme} (E : X.Modules) (n : ℕ) : Type (u + 1)

A fixed-rank locally free atlas for a module sheaf.

Unlike Mathlib's SheafOfModules.IsLocallyFree, this records one natural number n and requires every local free basis in the chosen cover to be indexed by Fin n.

• localGenerators : (have this := E; this).LocalGeneratorsData
• isLocallyFreeData : self.localGenerators.IsLocallyFreeData
• rankEquiv (i : self.localGenerators.I) : Nonempty ((self.localGenerators.generators i).I ≃ Fin n)

theorem AlgebraicGeometry.Scheme.Modules.FiniteLocallyFreeData.isLocallyFree {X : Scheme} {E : X.Modules} {n : ℕ} (D : E.FiniteLocallyFreeData n) : (have this := E; this).IsLocallyFree

Fixed-rank locally free data in particular proves upstream local freeness.

noncomputable def AlgebraicGeometry.Scheme.Modules.FiniteLocallyFreeData.ofIso {X : Scheme} {E F : X.Modules} {n : ℕ} (D : E.FiniteLocallyFreeData n) (e : E ≅ F) : F.FiniteLocallyFreeData n

Transport a fixed-rank locally free atlas across an isomorphism.

Equations

• D.ofIso e = { localGenerators := D.localGenerators.ofIso e, isLocallyFreeData := ⋯, rankEquiv := ⋯ }

theorem AlgebraicGeometry.Scheme.Modules.LineBundleData.isCoherent {X : Scheme} (L : LineBundleData X) : IsCoherent X L.line

The underlying sheaf of a line bundle is coherent.

noncomputable def AlgebraicGeometry.Scheme.Modules.LineBundleData.finiteLocallyFree {X : Scheme} (L : LineBundleData X) : L.line.FiniteLocallyFreeData 1

The rank-one locally free atlas carried by an invertible sheaf.

Equations

• L.finiteLocallyFree = { localGenerators := ⋯.choose, isLocallyFreeData := ⋯, rankEquiv := ⋯ }

noncomputable def AlgebraicGeometry.Scheme.Modules.LineBundleData.toPic {X : Scheme} (L : LineBundleData X) : Pic X

The Picard-group element represented by a line bundle with its recorded inverse.

Equations

• L.toPic = AlgebraicGeometry.Scheme.Modules.Pic.mkOfTensorInverse L.line L.inverse L.tensorInverseIso

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.LineBundleData.coe_toPic {X : Scheme} (L : LineBundleData X) : ↑L.toPic = PicardClass.mk L.line

theorem AlgebraicGeometry.Scheme.Modules.LineBundleData.toPic_eq_of_iso {X : Scheme} (L M : LineBundleData X) (e : L.line ≅ M.line) : L.toPic = M.toPic

Isomorphic line representatives determine the same Picard-group element.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.LineBundleData.toPic_dual {X : Scheme} (L : LineBundleData X) : L.dual.toPic = L.toPic⁻¹

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.LineBundleData.toPic_tensor {X : Scheme} (L M : LineBundleData X) : (L.tensor M).toPic = L.toPic * M.toPic

structure AlgebraicGeometry.Scheme.Modules.DeterminantData {X : Scheme} (E : X.Modules) : Type (u + 1)

Determinant data for a finite locally free sheaf.

The topExteriorPower field is a chosen global descent of the algebraic local top exterior powers supplied by finiteLocallyFree. ExteriorDeterminantData strengthens this legacy interface by recording an isomorphism with the constructed sheaf exterior power.

• rank : ℕ
• finiteLocallyFree : E.FiniteLocallyFreeData self.rank
• topExteriorPower : LineBundleData X

structure AlgebraicGeometry.Scheme.Modules.ExteriorDeterminantData {X : Scheme} (E : X.Modules) extends E.DeterminantData : Type (u + 1)

Determinant data whose line is identified with the constructed top exterior power.

This is the target interface for determinant descent. DeterminantData remains available for existing numerical APIs which only need a chosen determinant line.

• rank : ℕ
• finiteLocallyFree : E.FiniteLocallyFreeData self.rank
• topExteriorPower : LineBundleData X
• topExteriorPowerIso : self.topExteriorPower.line ≅ E.exteriorPower self.rank

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.Modules.ExteriorDeterminantData.determinantData {X : Scheme} {E : X.Modules} (D : E.ExteriorDeterminantData) : E.DeterminantData

Forget the comparison with the constructed top exterior power.

Equations

• D.determinantData = D.toDeterminantData

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.Modules.DeterminantData.line {X : Scheme} {E : X.Modules} (D : E.DeterminantData) : X.Modules

The determinant line.

Equations

• D.line = D.topExteriorPower.line

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.Modules.DeterminantData.inverse {X : Scheme} {E : X.Modules} (D : E.DeterminantData) : X.Modules

The recorded inverse determinant line.

Equations

• D.inverse = D.topExteriorPower.inverse

theorem AlgebraicGeometry.Scheme.Modules.DeterminantData.isLocallyFree {X : Scheme} {E : X.Modules} (D : E.DeterminantData) : (have this := E; this).IsLocallyFree

Determinant data proves that the underlying sheaf is locally free.

noncomputable def AlgebraicGeometry.Scheme.Modules.DeterminantData.ofIso {X : Scheme} {E F : X.Modules} (D : E.DeterminantData) (e : E ≅ F) : F.DeterminantData

Transport determinant data across an isomorphism of finite locally free sheaves.

Equations

• D.ofIso e = { rank := D.rank, finiteLocallyFree := D.finiteLocallyFree.ofIso e, topExteriorPower := D.topExteriorPower }

noncomputable def AlgebraicGeometry.Scheme.Modules.DeterminantData.firstChernClass {X : Scheme} {E : X.Modules} (D : E.DeterminantData) : Pic X

The first Chern class of an explicitly determinant-equipped finite locally free sheaf.

Equations

• D.firstChernClass = D.topExteriorPower.toPic

noncomputable def AlgebraicGeometry.Scheme.Modules.DeterminantData.firstChernClassAdd {X : Scheme} {E : X.Modules} (D : E.DeterminantData) : Additive (Pic X)

Additive notation for the first Chern class.

Equations

• D.firstChernClassAdd = Additive.ofMul D.firstChernClass

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.DeterminantData.firstChernClass_ofIso {X : Scheme} {E F : X.Modules} (D : E.DeterminantData) (e : E ≅ F) : (D.ofIso e).firstChernClass = D.firstChernClass

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.DeterminantData.firstChernClassAdd_ofIso {X : Scheme} {E F : X.Modules} (D : E.DeterminantData) (e : E ≅ F) : (D.ofIso e).firstChernClassAdd = D.firstChernClassAdd

theorem AlgebraicGeometry.Scheme.Modules.DeterminantData.firstChernClass_eq_of_lineIso {X : Scheme} {E F : X.Modules} (D : E.DeterminantData) (D' : F.DeterminantData) (e : D.line ≅ D'.line) : D.firstChernClass = D'.firstChernClass

Two determinant packages with isomorphic determinant lines have the same first Chern class, independently of their chosen inverse representatives.

structure AlgebraicGeometry.Scheme.Modules.DirectSumDeterminantData {X : Scheme} (E F : X.Modules) : Type (u + 1)

Determinant compatibility data for a direct sum.

The comparison is explicit: constructing it geometrically is precisely compatibility of top exterior powers with direct sums.

• left : E.DeterminantData
• right : F.DeterminantData
• sum : (E ⊞ F).DeterminantData
• lineIso : self.sum.line ≅ self.left.line.tensorObj self.right.line

theorem AlgebraicGeometry.Scheme.Modules.DirectSumDeterminantData.firstChernClass_eq_mul {X : Scheme} {E F : X.Modules} (D : E.DirectSumDeterminantData F) : D.sum.firstChernClass = D.left.firstChernClass * D.right.firstChernClass

Determinants turn direct sums into tensor products.

theorem AlgebraicGeometry.Scheme.Modules.DirectSumDeterminantData.firstChernClassAdd_eq_add {X : Scheme} {E F : X.Modules} (D : E.DirectSumDeterminantData F) : D.sum.firstChernClassAdd = D.left.firstChernClassAdd + D.right.firstChernClassAdd

Additive form of determinant compatibility with direct sums.

structure AlgebraicGeometry.Scheme.Modules.ShortExactDeterminantData {X : Scheme} (S : CategoryTheory.ShortComplex X.Modules) : Type (u + 1)

Determinant compatibility data for a short exact sequence.

• shortExact : S.ShortExact
• left : S.X₁.DeterminantData
• middle : S.X₂.DeterminantData
• right : S.X₃.DeterminantData
• lineIso : self.middle.line ≅ self.left.line.tensorObj self.right.line

theorem AlgebraicGeometry.Scheme.Modules.ShortExactDeterminantData.firstChernClass_eq_mul {X : Scheme} {S : CategoryTheory.ShortComplex X.Modules} (D : ShortExactDeterminantData S) : D.middle.firstChernClass = D.left.firstChernClass * D.right.firstChernClass

The determinant line of the middle term of a short exact sequence is the tensor product of the determinant lines of its ends.

theorem AlgebraicGeometry.Scheme.Modules.ShortExactDeterminantData.firstChernClassAdd_eq_add {X : Scheme} {S : CategoryTheory.ShortComplex X.Modules} (D : ShortExactDeterminantData S) : D.middle.firstChernClassAdd = D.left.firstChernClassAdd + D.right.firstChernClassAdd

First Chern classes are additive in determinant-equipped short exact sequences.

@[reducible, inline]

abbrev AlgebraicGeometry.Coh.DeterminantData {X : Scheme} (F : Coh X) : Type (u + 1)

Determinant data for a coherent sheaf whose underlying module sheaf is explicitly finite locally free of fixed rank. No instance asserts this for arbitrary coherent sheaves.

Equations

• F.DeterminantData = ((AlgebraicGeometry.Coh.ι X).obj F).DeterminantData

structure AlgebraicGeometry.Coh.ShortExactDeterminantData {X : Scheme} [IsLocallyNoetherian X] (S : CategoryTheory.ShortComplex (Coh X)) : Type (u + 1)

Determinant compatibility data for a short exact sequence of coherent sheaves.

• shortExact : S.ShortExact
• left : S.X₁.DeterminantData
• middle : S.X₂.DeterminantData
• right : S.X₃.DeterminantData
• lineIso : Scheme.Modules.DeterminantData.line self.middle ≅ (Scheme.Modules.DeterminantData.line self.left).tensorObj (Scheme.Modules.DeterminantData.line self.right)

noncomputable def AlgebraicGeometry.Coh.ShortExactDeterminantData.toModules {X : Scheme} [IsLocallyNoetherian X] {S : CategoryTheory.ShortComplex (Coh X)} (D : ShortExactDeterminantData S) : Scheme.Modules.ShortExactDeterminantData (S.map (ι X))

Forget a coherent determinant comparison to the ambient module-sheaf category.

Equations

• D.toModules = { shortExact := ⋯, left := D.left, middle := D.middle, right := D.right, lineIso := D.lineIso }

theorem AlgebraicGeometry.Coh.ShortExactDeterminantData.firstChernClassAdd_eq_add {X : Scheme} [IsLocallyNoetherian X] {S : CategoryTheory.ShortComplex (Coh X)} (D : ShortExactDeterminantData S) : Scheme.Modules.DeterminantData.firstChernClassAdd D.middle = Scheme.Modules.DeterminantData.firstChernClassAdd D.left + Scheme.Modules.DeterminantData.firstChernClassAdd D.right

First Chern classes are additive for coherent short exact sequences carrying explicit finite-locally-free determinant comparison data.

structure AlgebraicGeometry.Coh.TwoTermPerfectDeterminantData {X : Scheme} [IsLocallyNoetherian X] (F : Coh X) : Type (u + 1)

A coherent sheaf with an explicit two-term finite locally free resolution.

This is the available perfectness hypothesis in this file: no theorem manufactures such a resolution for an arbitrary coherent sheaf.

• resolution : CategoryTheory.ShortComplex (Coh X)
• shortExact : self.resolution.ShortExact
• targetIso : self.resolution.X₃ ≅ F
• left : self.resolution.X₁.DeterminantData
• middle : self.resolution.X₂.DeterminantData

noncomputable def AlgebraicGeometry.Coh.TwoTermPerfectDeterminantData.determinantLine {X : Scheme} [IsLocallyNoetherian X] {F : Coh X} (D : F.TwoTermPerfectDeterminantData) : Scheme.Modules.LineBundleData X

The determinant line of a two-term resolution is det(P₀) ⊗ det(P₁)⁻¹.

Equations

• D.determinantLine = D.middle.topExteriorPower.tensor D.left.topExteriorPower.dual

noncomputable def AlgebraicGeometry.Coh.TwoTermPerfectDeterminantData.firstChernClass {X : Scheme} [IsLocallyNoetherian X] {F : Coh X} (D : F.TwoTermPerfectDeterminantData) : Scheme.Modules.Pic X

First Chern class of a coherent sheaf carrying a two-term finite locally free resolution.

Equations

• D.firstChernClass = D.determinantLine.toPic

noncomputable def AlgebraicGeometry.Coh.TwoTermPerfectDeterminantData.firstChernClassAdd {X : Scheme} [IsLocallyNoetherian X] {F : Coh X} (D : F.TwoTermPerfectDeterminantData) : Additive (Scheme.Modules.Pic X)

Additive notation for the first Chern class of a two-term perfect object.

Equations

• D.firstChernClassAdd = Additive.ofMul D.firstChernClass

theorem AlgebraicGeometry.Coh.TwoTermPerfectDeterminantData.firstChernClass_eq {X : Scheme} [IsLocallyNoetherian X] {F : Coh X} (D : F.TwoTermPerfectDeterminantData) : D.firstChernClass = Scheme.Modules.DeterminantData.firstChernClass D.middle * (Scheme.Modules.DeterminantData.firstChernClass D.left)⁻¹

The resolution formula c₁(F) = c₁(P₀) - c₁(P₁).

noncomputable def AlgebraicGeometry.Coh.TwoTermPerfectDeterminantData.ofIso {X : Scheme} [IsLocallyNoetherian X] {F G : Coh X} (D : F.TwoTermPerfectDeterminantData) (e : F ≅ G) : G.TwoTermPerfectDeterminantData

Transport a two-term determinant resolution across an isomorphism of its target.

Equations

• D.ofIso e = { resolution := D.resolution, shortExact := ⋯, targetIso := D.targetIso ≪≫ e, left := D.left, middle := D.middle }

@[simp]

theorem AlgebraicGeometry.Coh.TwoTermPerfectDeterminantData.firstChernClass_ofIso {X : Scheme} [IsLocallyNoetherian X] {F G : Coh X} (D : F.TwoTermPerfectDeterminantData) (e : F ≅ G) : (D.ofIso e).firstChernClass = D.firstChernClass

structure AlgebraicGeometry.Coh.PerfectShortExactDeterminantData {X : Scheme} [IsLocallyNoetherian X] (S : CategoryTheory.ShortComplex (Coh X)) : Type (u + 1)

Determinant comparison data for a coherent short exact sequence whose terms carry two-term finite locally free resolutions.

• shortExact : S.ShortExact
• left : S.X₁.TwoTermPerfectDeterminantData
• middle : S.X₂.TwoTermPerfectDeterminantData
• right : S.X₃.TwoTermPerfectDeterminantData
• lineIso : self.middle.determinantLine.line ≅ self.left.determinantLine.line.tensorObj self.right.determinantLine.line

theorem AlgebraicGeometry.Coh.PerfectShortExactDeterminantData.firstChernClassAdd_eq_add {X : Scheme} [IsLocallyNoetherian X] {S : CategoryTheory.ShortComplex (Coh X)} (D : PerfectShortExactDeterminantData S) : D.middle.firstChernClassAdd = D.left.firstChernClassAdd + D.right.firstChernClassAdd

First Chern classes are additive for a perfect short exact comparison.