Atlas.AlgebraicGeometryI.code.CechSheafDataP1

def CechSheafDataP1.tateSetupP1 (k : Type) [Field k] :

The Tate duality setup for P¹ with its standard two-open cover: the ambient k-vector space is k itself with both subspaces equal to the top subspace.

Instances For

source

instance CechSheafDataP1.instFiniteDimensionalVTateSetupP1 (k : Type) [Field k] :

FiniteDimensional k (tateSetupP1 k).V

source

theorem CechSheafDataP1.finrank_cechH1_eq_zero (k : Type) [Field k] :

Module.finrank k (tateSetupP1 k).cechH1 = 0

For the standard two-open cover of P¹, the first Čech cohomology of the structure sheaf vanishes.

source

theorem CechSheafDataP1.finrank_dual_cechH0_eq_zero (k : Type) [Field k] :

Module.finrank k ↥(tateSetupP1 k).dual.cechH0 = 0

For the standard cover of P¹, the 0-th Čech cohomology of the dual setup also vanishes.

source

def CechSheafDataP1.P1 (k : Type) [Field k] :

CanonicalSheafCurves.SmoothCompleteCurve

The smooth complete curve P¹ constructed from the Čech data.

Instances For

source

theorem CechSheafDataP1.P1_genus (k : Type) [Field k] :

(P1 k).g = 0

The genus of P¹ is 0.

source

theorem CechSheafDataP1.P1_degK (k : Type) [Field k] :

(P1 k).degK = -2

The degree of the canonical bundle of P¹ is -2.

source

theorem CechSheafDataP1.P1_chi_O (k : Type) [Field k] :

(P1 k).χ (1, 0) = 1

The Euler characteristic of the structure sheaf of P¹ is 1.

source

theorem CechSheafDataP1.P1_chi_K (k : Type) [Field k] :

(P1 k).χ (1, -2) = -1

The Euler characteristic of the canonical bundle of P¹ is -1.

source

def CechSheafDataP1.cechSheafDataP1 (k : Type) [Field k] :

TateCechInfra.CechSheafData k

The packaged CechSheafData instance for P¹ with line bundle of degree 0, the structure sheaf, exhibiting Riemann–Roch for both O and K.

Instances For

source

theorem CechSheafDataP1.serre_duality_P1_from_cech_data (k : Type) [Field k] :

(cechSheafDataP1 k).h0_EK = (cechSheafDataP1 k).h1_E ∧ (cechSheafDataP1 k).h0_E = (cechSheafDataP1 k).h1_EK

Both forms of Serre duality hold on P¹ via the assembled Čech sheaf data.

source

theorem CechSheafDataP1.serre_duality_P1_h0K_eq_h1O (k : Type) [Field k] :

(cechSheafDataP1 k).h0_EK = (cechSheafDataP1 k).h1_E

One half of Serre duality for P¹: h⁰(K) = h¹(O).

source

theorem CechSheafDataP1.serre_duality_P1_h0O_eq_h1K (k : Type) [Field k] :

(cechSheafDataP1 k).h0_E = (cechSheafDataP1 k).h1_EK

The dual half of Serre duality for P¹: h⁰(O) = h¹(K).

source

theorem CechSheafDataP1.serre_duality_P1_full_chain (k : Type) [Field k] :

(cechSheafDataP1 k).h0_EK = (cechSheafDataP1 k).h1_E ∧ (cechSheafDataP1 k).h0_E = (cechSheafDataP1 k).h1_EK ∧ (P1 k).χ (1, 0) + (P1 k).χ (1, (P1 k).degK - 0) = 0

Full chain of Serre duality consequences for P¹: both duality identities and the Euler characteristic identity.

source

theorem CechSheafDataP1.cechSheafDataP1_nonvacuity (k : Type) [Field k] :

Nonempty (TateCechInfra.CechSheafData k)

The type CechSheafData k is nonempty, witnessed by the P¹ instance.

source

theorem CechSheafDataP1.cechSheafDataP1_values (k : Type) [Field k] :

(cechSheafDataP1 k).h0_E = 1 ∧ (cechSheafDataP1 k).h1_EK = 1 ∧ (cechSheafDataP1 k).deg = 0 ∧ (cechSheafDataP1 k).curve.g = 0 ∧ (cechSheafDataP1 k).curve.degK = -2

Concrete numerical values for the P¹ Čech sheaf data: h⁰(O) = 1, h¹(K) = 1, deg = 0, g = 0, degK = -2.

source

theorem CechSheafDataP1.cechSheafDataP1_cech_dimensions (k : Type) [Field k] :

Module.finrank k (cechSheafDataP1 k).setup.cechH1 = 0 ∧ Module.finrank k ↥(cechSheafDataP1 k).setup.dual.cechH0 = 0

Both the first Čech cohomology and the dual zeroth Čech cohomology vanish for P¹.

source

theorem CechSheafDataP1.serre_duality_P1_concrete_values (k : Type) [Field k] :

(cechSheafDataP1 k).h0_EK = 0 ∧ (cechSheafDataP1 k).h1_E = 0

Concrete values for the Serre duality identification on P¹: h⁰(K) = 0 and h¹(O) = 0.