structure GRR.ChowRingData : Type 1

Chow-ring data: a commutative ℚ-algebra packaging the Chow ring A^*(X) ⊗ ℚ used in the Grothendieck-Riemann-Roch statement.

• Ring : Type
• instCommRing : CommRing self.Ring
• instAlgebra : Algebra ℚ self.Ring

structure GRR.ProperMorphismGRR : Type 1

Bundle of data needed for Grothendieck-Riemann-Roch along a proper morphism f : X → Y: Chow rings of X and Y, K-theory groups, derived/Chow pushforwards, Chern characters, and the relative Todd class.

• chowX : ChowRingData
• chowY : ChowRingData
• K0X : Type
• instK0X : AddCommGroup self.K0X
• K0Y : Type
• instK0Y : AddCommGroup self.K0Y
• derived_pushforward : self.K0X →+ self.K0Y
• chow_pushforward : self.chowX.Ring →ₗ[ℚ] self.chowY.Ring
• chern_character_X : self.K0X →+ self.chowX.Ring
• chern_character_Y : self.K0Y →+ self.chowY.Ring
• todd_class_relative : self.chowX.Ring

theorem GRR.grothendieck_riemann_roch (f : ProperMorphismGRR) (α : f.K0X) : f.chern_character_Y (f.derived_pushforward α) = f.chow_pushforward (f.chern_character_X α * f.todd_class_relative)

Grothendieck-Riemann-Roch: for a proper morphism f : X → Y, ch(f_! α) = f_*(ch(α) · td(T_f)) in the Chow ring of Y.

structure GRR.HRRData : Type 1

Data required for Hirzebruch-Riemann-Roch on a single smooth projective variety X: Chow ring, K-theory, Euler characteristic, degree map, Chern character, Todd class, and the explicit HRR equation χ(α) = deg(ch(α) · td(X)).

• chowX : ChowRingData
• K0X : Type
• instK0X : AddCommGroup self.K0X
• euler_char : self.K0X →+ ℤ
• degree : self.chowX.Ring →ₗ[ℚ] ℚ
• chern_character : self.K0X →+ self.chowX.Ring
• todd_class : self.chowX.Ring
• hrr_formula (α : self.K0X) : ↑(self.euler_char α) = self.degree (self.chern_character α * self.todd_class)

theorem GRR.hirzebruch_riemann_roch (X : HRRData) (α : X.K0X) : ↑(X.euler_char α) = X.degree (X.chern_character α * X.todd_class)

Hirzebruch-Riemann-Roch: χ(α) = deg(ch(α) · td(X)), obtained directly from the packaged hrr_formula.

theorem GRR.grr_trivial_todd (f : ProperMorphismGRR) (htd : f.todd_class_relative = 1) (α : f.K0X) : f.chern_character_Y (f.derived_pushforward α) = f.chow_pushforward (f.chern_character_X α)

Specialization of GRR when the relative Todd class is trivial: the Chern character commutes with proper pushforward, i.e. ch(f_! α) = f_*(ch(α)).