structure Proposition40.SmoothCompleteCurveCohData : Type (max (u + 1) (v + 1))

Abstract input data for Proposition 40: an abelian category CohSheaf of "coherent sheaves" on a smooth complete curve, a predicate selecting locally free objects, a degree function degree : CohSheaf → ℤ, an axiom that every short exact sequence has the same degree defect as one between locally free objects, and additivity of the degree on locally free short exact sequences.

• CohSheaf : Type u

  The ambient category of coherent sheaves.

• catInst : CategoryTheory.Category.{v, u} self.CohSheaf
• abelInst : CategoryTheory.Abelian self.CohSheaf
• IsLocallyFree : self.CohSheaf → Prop

  The predicate selecting locally free coherent sheaves.

• degree : self.CohSheaf → ℤ

  The degree function on coherent sheaves.

• reduce_to_locally_free (S : CategoryTheory.ShortComplex self.CohSheaf) [CategoryTheory.Mono S.f] [CategoryTheory.Epi S.g] : S.Exact → ∃ (S' : CategoryTheory.ShortComplex self.CohSheaf), CategoryTheory.Mono S'.f ∧ CategoryTheory.Epi S'.g ∧ S'.Exact ∧ self.IsLocallyFree S'.X₁ ∧ self.IsLocallyFree S'.X₂ ∧ self.IsLocallyFree S'.X₃ ∧ self.degree S.X₂ - self.degree S.X₁ - self.degree S.X₃ = self.degree S'.X₂ - self.degree S'.X₁ - self.degree S'.X₃

  Every short exact sequence admits a "locally free replacement" with the same degree defect deg(X₂) − deg(X₁) − deg(X₃).

• locally_free_additive (S : CategoryTheory.ShortComplex self.CohSheaf) [CategoryTheory.Mono S.f] [CategoryTheory.Epi S.g] : S.Exact → self.IsLocallyFree S.X₁ → self.IsLocallyFree S.X₂ → self.IsLocallyFree S.X₃ → self.degree S.X₂ = self.degree S.X₁ + self.degree S.X₃

  Degree is additive on short exact sequences whose terms are all locally free.

theorem Proposition40.degree_additive (D : SmoothCompleteCurveCohData) (S : CategoryTheory.ShortComplex D.CohSheaf) [CategoryTheory.Mono S.f] [CategoryTheory.Epi S.g] (hex : S.Exact) : D.degree S.X₂ = D.degree S.X₁ + D.degree S.X₃

Combining the two axioms in SmoothCompleteCurveCohData, the degree is additive on every short exact sequence, not just locally free ones.

def Proposition40.CohSESRelSet (D : SmoothCompleteCurveCohData) : Set (FreeAbelianGroup D.CohSheaf)

The set of "short exact sequence relations" inside the free abelian group on coherent sheaves: for every short exact sequence 0 → X₁ → X₂ → X₃ → 0 we get an element [X₂] − [X₁] − [X₃].

def Proposition40.CohSESRelSubgroup (D : SmoothCompleteCurveCohData) : AddSubgroup (FreeAbelianGroup D.CohSheaf)

The subgroup of the free abelian group on coherent sheaves generated by the short exact sequence relations.

@[reducible, inline]

abbrev Proposition40.K0Coh (D : SmoothCompleteCurveCohData) : Type u

The Grothendieck group K⁰(Coh(X)) of coherent sheaves: the free abelian group on coherent sheaves modulo the short exact sequence relations.

def Proposition40.K0Coh.classOf (D : SmoothCompleteCurveCohData) (ℱ : D.CohSheaf) : K0Coh D

The class [ℱ] ∈ K⁰(Coh(X)) of a coherent sheaf ℱ.

theorem Proposition40.K0Coh.ses_relation (D : SmoothCompleteCurveCohData) (S : CategoryTheory.ShortComplex D.CohSheaf) [CategoryTheory.Mono S.f] [CategoryTheory.Epi S.g] (hex : S.Exact) : classOf D S.X₂ = classOf D S.X₁ + classOf D S.X₃

In K⁰(Coh(X)), every short exact sequence gives the relation [X₂] = [X₁] + [X₃].

theorem Proposition40.degree_lift_ker_contains_relations (D : SmoothCompleteCurveCohData) : CohSESRelSubgroup D ≤ (FreeAbelianGroup.lift D.degree).ker

The lift of degree : CohSheaf → ℤ to a homomorphism on the free abelian group sends every short exact sequence relation to zero, so its kernel contains the SES relations subgroup.

def Proposition40.degreeMapK0 (D : SmoothCompleteCurveCohData) : K0Coh D →+ ℤ

The induced degree homomorphism δ : K⁰(Coh(X)) → ℤ.

theorem Proposition40.proposition_40_delta_on_class (D : SmoothCompleteCurveCohData) (ℱ : D.CohSheaf) : (degreeMapK0 D) (K0Coh.classOf D ℱ) = D.degree ℱ

Proposition 40 (computation on classes): the induced degree map sends [ℱ] to deg ℱ.

theorem Proposition40.proposition_40_delta_well_defined (D : SmoothCompleteCurveCohData) : ∃ (δ : K0Coh D →+ ℤ), ∀ (ℱ : D.CohSheaf), δ (K0Coh.classOf D ℱ) = D.degree ℱ

Proposition 40 (existence of δ): there exists a group homomorphism δ : K⁰(Coh(X)) → ℤ extending the degree of every coherent sheaf.

theorem Proposition40.degreeMapK0_ses (D : SmoothCompleteCurveCohData) (S : CategoryTheory.ShortComplex D.CohSheaf) [CategoryTheory.Mono S.f] [CategoryTheory.Epi S.g] (hex : S.Exact) : (degreeMapK0 D) (K0Coh.classOf D S.X₂) = (degreeMapK0 D) (K0Coh.classOf D S.X₁) + (degreeMapK0 D) (K0Coh.classOf D S.X₃)

The degree map δ : K⁰(Coh(X)) → ℤ itself satisfies the SES relation on classes.