Documentation

Hironaka.AnalyticSpace.CoherentQuotient

Coherence of the quotient by an ideal sheaf #

If π’ͺ_X is coherent and π’₯ is an ideal sheaf of finite type, the structure sheaf (π’ͺ_X/π’₯)|_{S(π’₯)} of the quotient space (QuotientSpace.quotientSpace) is coherent ([Fre17, Ch. V, 7.3]). This is how the coherence of the structure sheaf of a closed subspace, and in particular of a local model, follows from Oka's theorem, as in [BM97, (3.8)(3)].

The proof is the standard reduction of relations modulo π’₯ to relations in π’ͺ_X. Near a point z of the support, the entries F i j of a matrix of sections of the quotient are the classes of ambient sections a i j (the compatible-germ-family definition of the quotient sheaf), and π’₯ is generated by sections g₁, …, g_l. A vector c of classes is a relation of F at w iff, for lifts cΜƒ, Ξ£_j a_{ij} cΜƒ_j ∈ π’₯_w for every row i, i.e. iff cΜƒ extends to a relation (cΜƒ, -d) of the augmented matrix [A | diag(g)] (row i: a_{i1}, …, a_{ip} and g₁, …, g_l in its own block of columns). By coherence of π’ͺ_X the relations of the augmented matrix are generated near z by finitely many sections R_n; the classes of their first p components generate the relations of F at every point near z: their classes are relations because the remaining components exhibit Ξ£_j a_{ij} R_{n,j} as an element of π’₯, and every relation c lifts to a relation (cΜƒ, -d), a combination of the R_n, whose first components reduce to c. The identification of the stalk of the quotient at w with π’ͺ_{X,w}/π’₯_w enters only through the canonical stalk map π’ͺ_{X,w} β†’ π’ͺ_{Z,w} (surjective with kernel π’₯_w: stalkMap_surjective, ker_stalkMap_ΞΉ) and its compatibility with germs (stalkMap_ΞΉ_germ, germ_eq_stalkMap_ΞΉ_germ).

source
def AnalyticSpace.QuotientSpace.augCol (p q l : β„•) :
Fin p βŠ• Fin q Γ— Fin l ≃ Fin (p + q * l)

The columns of the augmented matrix [A | diag(g)]: Fin p βŠ• Fin q Γ— Fin l, flattened.

Equations
Instances For
    source
    def AnalyticSpace.QuotientSpace.augVec {R : Type u_1} {p q l : β„•} (c : Fin p β†’ R) (d : Fin q β†’ Fin l β†’ R) :
    Fin (p + q * l) β†’ R

    The augmented vector (c, d).

    Equations
    Instances For
      source
      theorem AnalyticSpace.QuotientSpace.augVec_inl {R : Type u_1} {p q l : β„•} (c : Fin p β†’ R) (d : Fin q β†’ Fin l β†’ R) (j : Fin p) :
      augVec c d ((augCol p q l) (Sum.inl j)) = c j
      source
      theorem AnalyticSpace.QuotientSpace.augVec_inr {R : Type u_1} {p q l : β„•} (c : Fin p β†’ R) (d : Fin q β†’ Fin l β†’ R) (t : Fin q Γ— Fin l) :
      augVec c d ((augCol p q l) (Sum.inr t)) = d t.1 t.2
      source
      def AnalyticSpace.QuotientSpace.augMat {R : Type u_1} {p q l : β„•} [CommRing R] (A : Fin q β†’ Fin p β†’ R) (g : Fin l β†’ R) :
      Fin q β†’ Fin (p + q * l) β†’ R

      The augmented matrix [A | diag(g)]: row i is A i followed by g in the i-th block of l columns and 0 in the other blocks.

      Equations
      Instances For
        source
        theorem AnalyticSpace.QuotientSpace.map_augMat {R : Type u_1} {S : Type u_2} {p q l : β„•} [CommRing R] [CommRing S] (f : R β†’+* S) (A : Fin q β†’ Fin p β†’ R) (g : Fin l β†’ R) (i : Fin q) (c : Fin (p + q * l)) :
        f (augMat A g i c) = augMat (fun (i : Fin q) (j : Fin p) => f (A i j)) (fun (m : Fin l) => f (g m)) i c
        source
        theorem AnalyticSpace.QuotientSpace.sum_augMat_mul {R : Type u_1} {p q l : β„•} [CommRing R] (A : Fin q β†’ Fin p β†’ R) (g : Fin l β†’ R) (v : Fin (p + q * l) β†’ R) (i : Fin q) :
        βˆ‘ c : Fin (p + q * l), augMat A g i c * v c = βˆ‘ j : Fin p, A i j * v ((augCol p q l) (Sum.inl j)) + βˆ‘ m : Fin l, g m * v ((augCol p q l) (Sum.inr (i, m)))
        source
        theorem AnalyticSpace.QuotientSpace.sum_map_augMat_mul {R : Type u_1} {S : Type u_2} {p q l : β„•} [CommRing R] [CommRing S] (Ο† : R β†’+* S) (A : Fin q β†’ Fin p β†’ R) (g : Fin l β†’ R) (v : Fin (p + q * l) β†’ S) (i : Fin q) :
        βˆ‘ c : Fin (p + q * l), Ο† (augMat A g i c) * v c = βˆ‘ j : Fin p, Ο† (A i j) * v ((augCol p q l) (Sum.inl j)) + βˆ‘ m : Fin l, Ο† (g m) * v ((augCol p q l) (Sum.inr (i, m)))

        The row sums of the augmented matrix after a ring homomorphism (the germ at a point).

        source
        theorem AnalyticSpace.QuotientSpace.isCoherent_quotientSpace (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.π’ͺ) (hX : Manifold.IsCoherent X.π’ͺ) :
        Manifold.IsCoherent (quotientSpace X J).π’ͺ

        The quotient (S(π’₯), (π’ͺ_X/π’₯)|_{S(π’₯)}) of a space with coherent structure sheaf by an ideal sheaf of finite type has coherent structure sheaf ([Fre17, Ch. V, 7.3]; [BM97, (3.8)(3)] for the local models).