The Mukai class specialized to numerical K3 data

theorem AlgebraicGeometry.Numerical.K3.mukaiComp_one {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {V : NumericalVarietyData 2 A N} (hK3 : IsK3 V) (E : N) : V.mukaiComp E 1 = V.chComp E 1

theorem AlgebraicGeometry.Numerical.K3.mukaiComp_two {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {V : NumericalVarietyData 2 A N} (hK3 : IsK3 V) (E : N) : V.mukaiComp E 2 = V.chComp E 2 + (algebraMap ℚ A) ↑(V.rank E) * V.sqrtToddComp 2

theorem AlgebraicGeometry.Numerical.K3.degree_mukaiComp_two {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {V : NumericalVarietyData 2 A N} (hK3 : IsK3 V) (E : N) : V.ring.degree (V.mukaiComp E 2) = mukaiS V E

theorem AlgebraicGeometry.Numerical.K3.mukaiVector_fst_eq {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {V : NumericalVarietyData 2 A N} {Λ : Type u_1} [AddCommGroup Λ] (D : IntegralMukaiData V Λ) (E : N) : (D.mukaiVector E).1 = V.rank E

theorem AlgebraicGeometry.Numerical.K3.b_mukaiVector_snd_eq_degree {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {V : NumericalVarietyData 2 A N} {Λ : Type u_1} [AddCommGroup Λ] (D : IntegralMukaiData V Λ) (hK3 : IsK3 V) (E F : N) : ↑((D.b (D.mukaiVector E).2.1) (D.c₁ F)) = V.ring.degree (V.mukaiComp E 1 * V.chComp F 1)

theorem AlgebraicGeometry.Numerical.K3.mukaiVector_thd_eq_degree {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {V : NumericalVarietyData 2 A N} {Λ : Type u_1} [AddCommGroup Λ] (D : IntegralMukaiData V Λ) (hHRR : V.SatisfiesHRR) (hK3 : IsK3 V) (E : N) : ↑(D.mukaiVector E).2.2 = V.ring.degree (V.mukaiComp E 2)