def SerreDualityP1.residueShift : ℤ → ℤ

The residue shift i ↦ -1 - i realizing the duality at the index level.

theorem SerreDualityP1.residueShift_involutive : Function.Involutive residueShift

The residue shift is involutive: (-1 - (-1 - i)) = i.

theorem SerreDualityP1.residueShift_comp_self : residueShift ∘ residueShift = id

The composition residueShift ∘ residueShift equals the identity.

theorem SerreDualityP1.residueShift_injective : Function.Injective residueShift

The residue shift is injective (consequence of being involutive).

noncomputable def SerreDualityP1.shiftMap (k : Type u_1) [Field k] : (ℤ →₀ k) →ₗ[k] ℤ →₀ k

The k-linear map on ℤ →₀ k induced by the residue shift i ↦ -1 - i.

theorem SerreDualityP1.shiftMap_involutive (k : Type u_1) [Field k] : Function.Involutive ⇑(shiftMap k)

The shiftMap is involutive, inherited from residueShift.

noncomputable def SerreDualityP1.shiftEquiv (k : Type u_1) [Field k] : (ℤ →₀ k) ≃ₗ[k] ℤ →₀ k

The k-linear involution (ℤ →₀ k) ≃ₗ[k] (ℤ →₀ k) induced by the residue shift.

theorem SerreDualityP1.shiftEquiv_coe_eq (k : Type u_1) [Field k] : ↑(shiftEquiv k) = shiftMap k

The underlying linear map of shiftEquiv is shiftMap.

theorem SerreDualityP1.residueShift_image_Ioo (n : ℤ) : residueShift '' Set.Ioo n 0 = Set.Icc 0 (-2 - n)

The residue shift sends the open interval (n, 0) bijectively onto [0, -2 - n].

theorem SerreDualityP1.shiftMap_supported_Ioo (k : Type u_1) [Field k] (n : ℤ) : Submodule.map (shiftMap k) (Finsupp.supported k k (Set.Ioo n 0)) = Finsupp.supported k k (Set.Icc 0 (-2 - n))

shiftMap carries Laurent polynomials supported on (n, 0) to those supported on [0, -2 - n].

noncomputable def SerreDualityP1.shiftEquiv_supported (k : Type u_1) [Field k] (n : ℤ) : ↥(Finsupp.supported k k (Set.Ioo n 0)) ≃ₗ[k] ↥(Finsupp.supported k k (Set.Icc 0 (-2 - n)))

shiftEquiv restricted to supports on (n, 0) is a linear isomorphism onto supports on [0, -2 - n].

noncomputable def SerreDualityP1.serre_duality_P1 (k : Type) [Field k] (n : ℤ) (_hn : n < -1) : ((ℤ →₀ k) ⧸ CohomologyP1.NonNeg k ⊔ CohomologyP1.AtMost k n) ≃ₗ[k] ↥(CohomologyP1.CechH0 k (-2 - n))

Serre duality on ℙ¹ as a linear isomorphism: for n < -1, H¹(O(n)) ≅ H⁰(O(-2 - n)) via the residue shift.

theorem SerreDualityP1.serre_duality_finrank (k : Type) [Field k] (n : ℤ) (hn : n < -1) : Module.finrank k ((ℤ →₀ k) ⧸ CohomologyP1.NonNeg k ⊔ CohomologyP1.AtMost k n) = Module.finrank k ↥(CohomologyP1.CechH0 k (-2 - n))

The dimensional Serre duality on ℙ¹ for n < -1.

@[simp]

theorem SerreDualityP1.residueShift_zero : residueShift 0 = -1

residueShift 0 = -1.

@[simp]

theorem SerreDualityP1.residueShift_neg_one : residueShift (-1) = 0

residueShift (-1) = 0.

theorem SerreDualityP1.residueShift_add (i : ℤ) : residueShift i + i = -1

residueShift i + i = -1 by definition.

theorem SerreDualityP1.residueShift_antitone : Antitone residueShift

residueShift is antitone: a ≤ b implies -1 - b ≤ -1 - a.