Documentation

Atlas.AlgebraicGeometryI.code.SheafCohomology

The "restriction to the cover" map for an A-module M: it sends m to the pair of its images in the localizations away from f and from g. This is the first map of the Čech complex for the two-element cover {D(f), D(g)}.

Instances For
    theorem SheafCohomology.locProductMap_injective {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {f g : A} (hfg : Ideal.span {f, g} = ) :

    Sheaf condition (separation/injectivity): if f, g generate the unit ideal, then the product of the two localization maps is injective. This is the H⁰ part of the Čech sheaf condition for {D(f), D(g)}.

    Flatness of localization at a single element: A[f⁻¹] is A-flat. This is essential for showing that taking cohomology commutes with localization.

    f becomes a unit in A[(fg)⁻¹].

    g becomes a unit in A[(fg)⁻¹].

    noncomputable def SheafCohomology.cechMapFromF (A : Type u_1) [CommRing A] (f g : A) :

    The restriction A[f⁻¹] → A[(fg)⁻¹] induced by the universal property of localization. This is one of the two Čech restriction maps for {D(f), D(g)}.

    Instances For
      noncomputable def SheafCohomology.cechMapFromG (A : Type u_1) [CommRing A] (f g : A) :

      The restriction A[g⁻¹] → A[(fg)⁻¹] induced by the universal property of localization.

      Instances For
        theorem SheafCohomology.cech_dsquared_zero (A : Type u_1) [CommRing A] (f g a : A) :

        The Čech differential d applied to an element of A coming from both A[f⁻¹] and A[g⁻¹] gives zero. This expresses d ∘ d = 0 at the H⁰ level.

        The Čech differential A[f⁻¹] × A[g⁻¹] → A[(fg)⁻¹], sending (s, t) ↦ s|_{D(fg)} - t|_{D(fg)}. Its cokernel is for the two-element cover.

        Instances For

          The restriction map from A[f⁻¹] agrees with algebraMap A _ on elements of A.

          The restriction map from A[g⁻¹] agrees with algebraMap A _ on elements of A.

          Sending the formal inverse of f in A[f⁻¹] into A[(fg)⁻¹] and multiplying by f yields 1.

          Sending the formal inverse of g in A[g⁻¹] into A[(fg)⁻¹] and multiplying by g yields 1.

          Iterated version of cechMapFromF_invSelf_mul: pushing f⁻ⁿ into A[(fg)⁻¹] and multiplying by fⁿ gives 1.

          Iterated version of cechMapFromG_invSelf_mul: pushing g⁻ⁿ into A[(fg)⁻¹] and multiplying by gⁿ gives 1.

          theorem SheafCohomology.cechMapFromF_mul_fgpow (A : Type u_1) [CommRing A] (f g c : A) (n : ) :

          Computation of the Čech restriction map from A[f⁻¹] on an element of the form c / fⁿ, cleared by (fg)ⁿ: the result is c · gⁿ.

          theorem SheafCohomology.cechMapFromG_mul_fgpow (A : Type u_1) [CommRing A] (f g c : A) (n : ) :

          Computation of the Čech restriction map from A[g⁻¹] on an element of the form c / gⁿ, cleared by (fg)ⁿ: the result is c · fⁿ.

          Vanishing of Čech for the structure sheaf on an affine open: if f, g generate the unit ideal of A, then the Čech differential A[f⁻¹] × A[g⁻¹] → A[(fg)⁻¹] is surjective. Equivalently, of the two-element cover by basic opens vanishes for the structure sheaf — the algebraic origin of affine acyclicity.

          @[reducible, inline]
          abbrev SheafCohomology.H0 (k : Type) [Field k] (n : ) :

          H⁰(ℙ¹, O(n)), realized concretely as the Čech H⁰ of degree n sections.

          Instances For
            @[reducible, inline]
            abbrev SheafCohomology.H1 (k : Type) [Field k] (n : ) :

            H¹(ℙ¹, O(n)), realized concretely as the quotient of Laurent series in one variable by the sum of "non-negative degree" and "degree ≤ n" subspaces.

            Instances For
              theorem SheafCohomology.finrank_H0_of_neg (k : Type) [Field k] (n : ) (hn : n < 0) :
              Module.finrank k (H0 k n) = 0

              H⁰(ℙ¹, O(n)) = 0 for n < 0: no global sections in negative degree.

              theorem SheafCohomology.finrank_H0_of_nonneg (k : Type) [Field k] (n : ) (hn : 0 n) :
              Module.finrank k (H0 k n) = (n + 1).toNat

              dim H⁰(ℙ¹, O(n)) = n + 1 for n ≥ 0: the global sections of O(n) are the homogeneous polynomials of degree n in two variables.

              theorem SheafCohomology.finrank_H1_of_nonneg (k : Type) [Field k] (n : ) (hn : 0 n) :
              Module.finrank k (H1 k n) = 0

              H¹(ℙ¹, O(n)) = 0 for n ≥ 0: higher cohomology of non-negative twists vanishes on ℙ¹.

              theorem SheafCohomology.finrank_H1_of_neg (k : Type) [Field k] (n : ) (hn : n < 0) :
              Module.finrank k (H1 k n) = (-n - 1).toNat

              dim H¹(ℙ¹, O(n)) = -n - 1 for n < 0: combinatorial count of Laurent terms of strictly negative degree above the cutoff n.

              theorem SheafCohomology.serre_duality_nonneg (k : Type) [Field k] (n : ) (hn : 0 n) :
              Module.finrank k (H1 k n) = Module.finrank k (H0 k (-2 - n))

              Serre duality on ℙ¹, non-negative case: dim H¹(O(n)) = dim H⁰(O(-2 - n)). For n ≥ 0 both sides vanish, confirming the duality. The canonical bundle on ℙ¹ is O(-2), so O(n)∨ ⊗ K = O(-2 - n).

              theorem SheafCohomology.serre_duality_neg (k : Type) [Field k] (n : ) (hn : n < 0) :
              Module.finrank k (H1 k n) = Module.finrank k (H0 k (-2 - n))

              Serre duality on ℙ¹, negative case: dim H¹(O(n)) = dim H⁰(O(-2 - n)). For n < 0, -2 - n may be ≥ 0 or = -1; both sub-cases give matching dimensions.

              theorem SheafCohomology.euler_characteristic (k : Type) [Field k] (n : ) :
              (Module.finrank k (H0 k n)) - (Module.finrank k (H1 k n)) = n + 1

              Euler characteristic of O(n) on ℙ¹: χ(O(n)) = h⁰(O(n)) - h¹(O(n)) = n + 1. This is the Riemann–Roch formula for line bundles on ℙ¹ (genus 0).