noncomputable def CohomologyP1.NonNeg (k : Type) [Field k] : Submodule k (ℤ →₀ k)

The submodule of finitely supported integer-indexed k-functions supported on ℤ_{≥0}, modelling the global sections of O(n) on one affine chart of P^1.

noncomputable def CohomologyP1.AtMost (k : Type) [Field k] (n : ℤ) : Submodule k (ℤ →₀ k)

The submodule of finitely supported integer-indexed k-functions supported on (-∞, n], modelling the other affine chart contribution to O(n) on P^1.

noncomputable def CohomologyP1.CechH0 (k : Type) [Field k] (n : ℤ) : Submodule k (ℤ →₀ k)

The Čech H^0(P^1, O(n)): the intersection of the two chart submodules NonNeg and AtMost n.

theorem CohomologyP1.cechH0_eq_supported (k : Type) [Field k] (n : ℤ) : CechH0 k n = Finsupp.supported k k (Set.Icc 0 n)

CechH0 k n equals the submodule supported on the integer interval [0, n].

theorem CohomologyP1.sum_eq_supported (k : Type) [Field k] (n : ℤ) : NonNeg k ⊔ AtMost k n = Finsupp.supported k k (Set.Ici 0 ∪ Set.Iic n)

The sum of the two chart submodules equals the submodule supported on Set.Ici 0 ∪ Set.Iic n.

theorem CohomologyP1.complement_union (n : ℤ) : (Set.Ici 0 ∪ Set.Iic n)ᶜ = Set.Ioo n 0

The set-theoretic complement of Ici 0 ∪ Iic n in ℤ is the open interval Ioo n 0.

theorem CohomologyP1.finrank_supported_eq_card (k : Type) [Field k] (S : Set ℤ) [Fintype ↑S] : Module.finrank k ↥(Finsupp.supported k k S) = Fintype.card ↑S

The k-dimension of the submodule of finsupps supported on a finite set S ⊆ ℤ equals the cardinality of S.

theorem CohomologyP1.finrank_H0_nonneg (k : Type) [Field k] (n : ℕ) : Module.finrank k ↥(CechH0 k ↑n) = n + 1

H^0(P^1, O(n)) = n + 1 for n ≥ 0.

theorem CohomologyP1.H1_vanishes_nonneg (k : Type) [Field k] (n : ℕ) : NonNeg k ⊔ AtMost k ↑n = ⊤

For n ≥ 0, the two chart submodules sum to the entire space, so H^1(P^1, O(n)) = 0.

theorem CohomologyP1.finrank_H1_nonneg (k : Type) [Field k] (n : ℕ) : Module.finrank k ((ℤ →₀ k) ⧸ NonNeg k ⊔ AtMost k ↑n) = 0

H^1(P^1, O(n)) = 0 for n ≥ 0.

theorem CohomologyP1.H0_vanishes_neg (k : Type) [Field k] (n : ℤ) (hn : n < 0) : CechH0 k n = ⊥

For n < 0, H^0(P^1, O(n)) = 0.

noncomputable def CohomologyP1.H1_equiv_supported_complement (k : Type) [Field k] (n : ℤ) : ((ℤ →₀ k) ⧸ NonNeg k ⊔ AtMost k n) ≃ₗ[k] ↥(Finsupp.supported k k (Set.Ioo n 0))

Linear equivalence between the cokernel of the Čech differential and the submodule supported on the missing integer range Set.Ioo n 0.

theorem CohomologyP1.finrank_H1_neg (k : Type) [Field k] (n : ℤ) : n < 0 → Module.finrank k ((ℤ →₀ k) ⧸ NonNeg k ⊔ AtMost k n) = (-n - 1).toNat

For n < 0, H^1(P^1, O(n)) has dimension (-n - 1).toNat.

theorem CohomologyP1.H0_O_neg1 (k : Type) [Field k] : CechH0 k (-1) = ⊥

H^0(P^1, O(-1)) = 0.

theorem CohomologyP1.finrank_H1_O_neg1 (k : Type) [Field k] : Module.finrank k ((ℤ →₀ k) ⧸ NonNeg k ⊔ AtMost k (-1)) = 0

H^1(P^1, O(-1)) = 0.

theorem CohomologyP1.finrank_H1_O_neg2 (k : Type) [Field k] : Module.finrank k ((ℤ →₀ k) ⧸ NonNeg k ⊔ AtMost k (-2)) = 1

H^1(P^1, O(-2)) is 1-dimensional (Serre duality dual to H^0(O)).