Reconstruction systems, in any dimension

A ReconstructionSystem picks reconstruction data for every coherent sheaf, compatibly with isomorphism and with short exact sequences, and thereby descends rank and the Chern-character components to K₀Ab (Coh X).

Nothing here mentions a dimension: the structure is stated over PairingContext D C d A for an arbitrary d.

Why this file exists

It was declared twice. HigherDimension/Hirzebruch.lean had it at d, and Surface/NumericalVariety.lean had it again at d = 2 -- eleven declarations, identical to the token across roughly eighty lines of code, differing only in line wrapping and two docstring phrasings. The surface case is the general case at d = 2, so it is now obtained rather than restated.

Placing it here rather than in HigherDimension/ is the point: a dimension-general structure does not belong in a namespace named for one range of dimensions, and Surface should not have to import HigherDimension to reach it.

Dimension-general descent through K₀(Coh X)

structure AlgebraicGeometry.RiemannRoch.ReconstructionSystem {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} {A : Type v} [CommRing A] [Algebra ℚ A] {P : IntersectionTheory.ChernCharacter.PairingContext D C d A} : Type (u + 1)

A compatible choice of reconstruction data for every coherent sheaf in dimension d.

• reconstruction (F : Coh X) : P.ReconstructionData F

  Reconstruction data for every coherent sheaf.

• rank_iso {F G : Coh X} (_e : F ≅ G) : (self.reconstruction F).rank = (self.reconstruction G).rank

  Rank is invariant under coherent-sheaf isomorphism.

• eulerPic_iso {F G : Coh X} (_e : F ≅ G) : (self.reconstruction F).twists.eulerPic = (self.reconstruction G).twists.eulerPic

  Twist Euler functions are invariant under coherent-sheaf isomorphism.

• rank_shortExact (S : CategoryTheory.ShortComplex (Coh X)) (_hS : S.ShortExact) : (self.reconstruction S.X₂).rank = (self.reconstruction S.X₁).rank + (self.reconstruction S.X₃).rank

  Rank is additive in a short exact sequence.

• eulerPic_shortExact (S : CategoryTheory.ShortComplex (Coh X)) (_hS : S.ShortExact) : (self.reconstruction S.X₂).twists.eulerPic = (self.reconstruction S.X₁).twists.eulerPic + (self.reconstruction S.X₃).twists.eulerPic

  Twist Euler functions are additive in a short exact sequence.

noncomputable def AlgebraicGeometry.RiemannRoch.ReconstructionSystem.rankInvariant {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} {A : Type v} [CommRing A] [Algebra ℚ A] {P : IntersectionTheory.ChernCharacter.PairingContext D C d A} (R : ReconstructionSystem) : CategoryTheory.K₀Ab (Coh X) →+ ℤ

Reconstructed rank as an additive coherent-sheaf invariant.

Equations

• R.rankInvariant = CategoryTheory.K₀Ab.liftOf (fun (F : AlgebraicGeometry.Coh X) => (R.reconstruction F).rank) ⋯

noncomputable def AlgebraicGeometry.RiemannRoch.ReconstructionSystem.chernCharacterInvariant {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} {A : Type v} [CommRing A] [Algebra ℚ A] {P : IntersectionTheory.ChernCharacter.PairingContext D C d A} {O : Coh X} (R : ReconstructionSystem) (RO : P.ReconstructionData O) (i : ℕ) : CategoryTheory.K₀Ab (Coh X) →+ ↥(P.ring.piece i)

The reconstructed i-th Chern-character component as an additive coherent-sheaf invariant valued in the certified graded piece.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.RiemannRoch.ReconstructionSystem.rankHom {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} {A : Type v} [CommRing A] [Algebra ℚ A] {P : IntersectionTheory.ChernCharacter.PairingContext D C d A} (R : ReconstructionSystem) : CategoryTheory.K₀Ab (Coh X) →+ ℤ

Reconstructed rank on K₀(Coh X).

Equations

• R.rankHom = R.rankInvariant

noncomputable def AlgebraicGeometry.RiemannRoch.ReconstructionSystem.chernCharacterHom {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} {A : Type v} [CommRing A] [Algebra ℚ A] {P : IntersectionTheory.ChernCharacter.PairingContext D C d A} {O : Coh X} (R : ReconstructionSystem) (RO : P.ReconstructionData O) (i : ℕ) : CategoryTheory.K₀Ab (Coh X) →+ A

The reconstructed i-th Chern-character component on K₀(Coh X).

Equations

• R.chernCharacterHom RO i = (P.ring.piece i).subtype.toAddMonoidHom.comp (R.chernCharacterInvariant RO i)

@[simp]

theorem AlgebraicGeometry.RiemannRoch.ReconstructionSystem.rankHom_class {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} {A : Type v} [CommRing A] [Algebra ℚ A] {P : IntersectionTheory.ChernCharacter.PairingContext D C d A} (R : ReconstructionSystem) (F : Coh X) : R.rankHom (CategoryTheory.K₀Ab.of F) = (R.reconstruction F).rank

@[simp]

theorem AlgebraicGeometry.RiemannRoch.ReconstructionSystem.chernCharacterHom_class {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} {A : Type v} [CommRing A] [Algebra ℚ A] {P : IntersectionTheory.ChernCharacter.PairingContext D C d A} {O : Coh X} (R : ReconstructionSystem) (RO : P.ReconstructionData O) (F : Coh X) (i : ℕ) : (R.chernCharacterHom RO i) (CategoryTheory.K₀Ab.of F) = IntersectionTheory.ChernCharacter.chernCharacterComponent RO (R.reconstruction F) i

theorem AlgebraicGeometry.RiemannRoch.ReconstructionSystem.chernCharacterHom_mem {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} {A : Type v} [CommRing A] [Algebra ℚ A] {P : IntersectionTheory.ChernCharacter.PairingContext D C d A} {O : Coh X} (R : ReconstructionSystem) (RO : P.ReconstructionData O) (E : CategoryTheory.K₀Ab (Coh X)) (i : ℕ) : (R.chernCharacterHom RO i) E ∈ P.ring.piece i

Every descended Chern-character component remains in its graded piece.

noncomputable def AlgebraicGeometry.RiemannRoch.ReconstructionSystem.intAlgebraMap {A : Type v} [CommRing A] [Algebra ℚ A] : ℤ →+ A

The rational algebra map restricted to integral ranks.

Equations

• AlgebraicGeometry.RiemannRoch.ReconstructionSystem.intAlgebraMap = { toFun := fun (r : ℤ) => (algebraMap ℚ A) ↑r, map_zero' := ⋯, map_add' := ⋯ }

theorem AlgebraicGeometry.RiemannRoch.ReconstructionSystem.chernCharacterHom_zero {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} {A : Type v} [CommRing A] [Algebra ℚ A] {P : IntersectionTheory.ChernCharacter.PairingContext D C d A} {O : Coh X} (R : ReconstructionSystem) (RO : P.ReconstructionData O) (E : CategoryTheory.K₀Ab (Coh X)) : (R.chernCharacterHom RO 0) E = (algebraMap ℚ A) ↑(R.rankHom E)

The descended zeroth Chern character is the algebra image of rank.

theorem AlgebraicGeometry.RiemannRoch.ReconstructionSystem.chernCharacterHom_add {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {D : Cohomology.FiniteCohomology k X} {C : D.LinearConnectingSystem} {d : ℕ} {A : Type v} [CommRing A] [Algebra ℚ A] {P : IntersectionTheory.ChernCharacter.PairingContext D C d A} {O : Coh X} (R : ReconstructionSystem) (RO : P.ReconstructionData O) (E F : CategoryTheory.K₀Ab (Coh X)) (i : ℕ) : (R.chernCharacterHom RO i) (E + F) = (R.chernCharacterHom RO i) E + (R.chernCharacterHom RO i) F