structure K0Gen.SmoothCurveK0Data : Type 1

Axiomatic data for K^0(Coh X) of a smooth curve: a type of coherent sheaves with rank/degree invariants additive in short exact sequences, including the distinguished classes O_X (rank one, degree zero) and O_x (rank zero, degree one).

• CohSheaf : Type
• rank : self.CohSheaf → ℕ
• deg : self.CohSheaf → ℤ
• SES : self.CohSheaf → self.CohSheaf → self.CohSheaf → Prop
• O_X : self.CohSheaf
• O_x : self.CohSheaf
• O_X_rank : self.rank self.O_X = 1
• O_X_deg : self.deg self.O_X = 0
• O_x_rank : self.rank self.O_x = 0
• O_x_deg : self.deg self.O_x = 1
• rank_additive (A B C : self.CohSheaf) : self.SES A B C → self.rank B = self.rank A + self.rank C
• deg_additive (A B C : self.CohSheaf) : self.SES A B C → self.deg B = self.deg A + self.deg C

def K0Gen.sesRelations (X : SmoothCurveK0Data) : AddSubgroup (FreeAbelianGroup X.CohSheaf)

The subgroup of relations in the free abelian group generated by coherent sheaves imposed by short exact sequences 0 → A → B → C → 0, namely [A] + [C] − [B].

@[reducible, inline]

abbrev K0Gen.K0Coh (X : SmoothCurveK0Data) : Type

The Grothendieck group K^0(Coh X): free abelian group on coherent sheaves modulo short-exact-sequence relations.

def K0Gen.K0Coh.classOf (X : SmoothCurveK0Data) (F : X.CohSheaf) : K0Coh X

The class [F] ∈ K^0(Coh X) of a coherent sheaf F.

def K0Gen.rankDegToK0 (X : SmoothCurveK0Data) : ℤ × ℤ →+ K0Coh X

The map (r, d) ↦ r·[O_X] + d·[O_x] from ℤ × ℤ into K^0(Coh X).

theorem K0Gen.goal_179_lemma35_proved (X : SmoothCurveK0Data) : Function.Surjective ⇑(rankDegToK0 X)

Lemma 35 (Lec 24): on a smooth curve, O_X and O_x generate K^0(Coh X); i.e. the rank-degree map ℤ × ℤ → K^0(Coh X) is surjective.