17.21 Symmetric and exterior… to 17.30 The de Rham complex

Section17.21 Symmetric and exterior powers#

Section 17.21 of the Stacks Project, Tag 01CF. 7 tags here are carried by 46 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01CF, the section

Tag 01CF in the Stacks Project.

SheafOfModules.ringedSpaceAlgebras, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/AlgebraBundleStalk.lean, line 424. The attribute's comment: “the construction of the three algebras themselves, for a sheaf of modules on a ringed space, which is the object the lemmas 01CG, 01CH, 01CJ, 01CK and 01CL of the section are statements about; the section has no finer tag for it”.

The tensor, exterior and symmetric algebras of a sheaf of modules on a ringed space, as the package Section 17.21 attaches to F: the three graded algebras, their three universal properties, the identification of the homogeneous pieces of T(F) with the tensor powers of F, the degree-zero identifications, the vanishing in negative degrees, the direct-sum presentation and the two quotient maps T(F) ⟶ ⋀(F) and T(F) ⟶ Sym(F). It is SheafOfModules.algebras, i.e. sheafifiedAlgebras, at the site of open subsets of X, so each of the three algebras is the degreewise sheafification of its sectionwise counterpart, which is the section's own construction.

noncomputable def ringedSpaceAlgebras (F : SheafOfModules.{w} (structureSheafRing X)) :
    TensorExteriorSymmetricAlgebras (Opens.grothendieckTopology X.carrier) F

Tag 01CG, a lemma

Tag 01CG in the Stacks Project.

SheafOfModules.exteriorPower_isSheafification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExteriorPowerComparison.lean, line 568. The attribute's comment: “exterior_power_sheafification: the exterior assertion, that ⋀ⁿ M is the sheafification of X ↦ ⋀ⁿ(M(X)), with the comparison pinned on wedges of degree-one local sections. The symmetric assertion is SheafOfModules.symmetricPower_isSheafification; the tag states those two and nothing else, so that pair is its covering set.”.

For a sheaf of modules M on a site with a sheaf of commutative rings O♯, and an exterior algebra A of M in the sense of Section 17.21, the degree-n exterior power A.piece n of M is the sheafification of the presheaf X ↦ ⋀ⁿ_{O♯(X)}(M(X)).

The presheaf is exhibited together with the sectionwise identification of its sections with ⋀ⁿ_{O♯(X)}(M(X)) and the comparison morphism to A.piece n; the two equation families fix the restriction maps and the comparison morphism on wedges of degree-one generators, and the last conjunct is the sheafification assertion.

theorem exteriorPower_isSheafification (n : ℕ) :
    ∃ P : PresheafOfModules.{w} (toRingCat J Osharp).obj,
      ∃ e : ∀ X : Cᵒᵖ, P.obj X ≃ₗ[(toRingCat J Osharp).obj.obj X]
          ⋀[(toRingCat J Osharp).obj.obj X]^n (M.val.obj X),
        ∃ cmp : P ⟶ (SheafOfModules.forget (toRingCat J Osharp)).obj (A.piece (n : ℤ)),
          (∀ (X Y : Cᵒᵖ) (f : X ⟶ Y) (s : Fin n → M.val.obj X)
              (x : ⋀[(toRingCat J Osharp).obj.obj X]^n (M.val.obj X))
              (y : ⋀[(toRingCat J Osharp).obj.obj Y]^n (M.val.obj Y)),
            ((x : ExteriorAlgebra ((toRingCat J Osharp).obj.obj X) (M.val.obj X)) =
                ExteriorAlgebra.ιMulti ((toRingCat J Osharp).obj.obj X) n s) →
            ((y : ExteriorAlgebra ((toRingCat J Osharp).obj.obj Y) (M.val.obj Y)) =
                ExteriorAlgebra.ιMulti ((toRingCat J Osharp).obj.obj Y) n
                  fun i => M.val.map f (s i)) →
            e Y (P.map f ((e X).symm x)) = y) ∧
          (∀ (X : Cᵒᵖ) (s : Fin n → M.val.obj X)
              (x : ⋀[(toRingCat J Osharp).obj.obj X]^n (M.val.obj X)),
            ((x : ExteriorAlgebra ((toRingCat J Osharp).obj.obj X) (M.val.obj X)) =
                ExteriorAlgebra.ιMulti ((toRingCat J Osharp).obj.obj X) n s) →
            Hom.app cmp X ((e X).symm x) =
              A.toPresheafGradedAlgebra.homogeneousProdLeft X n
                fun i => gen.val.app X (s i)) ∧
          IsIso ((sheafificationHomEquiv (𝟙 (toRingCat J Osharp).obj)).symm cmp)

SheafOfModules.symmetricPower_isSheafification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SymmetricPowerComparison.lean, line 411. The attribute's comment: “symmetric_power_sheafification”.

Tag 01CG. For a sheaf of modules M on a site with a sheaf of commutative rings O♯, and a symmetric algebra A of M in the sense of Section 17.21, the degree-n symmetric power A.piece n of M is the sheafification of the presheaf X ↦ Symⁿ_{O♯(X)}(M(X)).

The presheaf is exhibited together with the sectionwise identification of its sections with Symⁿ_{O♯(X)}(M(X)) and the comparison morphism to A.piece n; the two equation families fix the restriction maps and the comparison morphism on products of degree-one generators, and the last conjunct is the sheafification assertion.

The symmetric algebra is a hypothesis rather than a chosen term: Section 17.21 pins it only up to canonical isomorphism, and SheafOfModules.sectionwiseSymmetricAlgebra together with SheafOfModules.isSymmetricAlgebra_sectionwiseSymmetricAlgebra and SheafOfModules.GradedAlgebra.IsSymmetricAlgebra.comp_iso shows the hypothesis is satisfiable for every M.

theorem symmetricPower_isSheafification (n : ℕ) :
    ∃ P : PresheafOfModules.{w} (toRingCat J Osharp).obj,
      ∃ e : ∀ X : Cᵒᵖ, P.obj X ≃ₗ[(toRingCat J Osharp).obj.obj X]
          SymPow.symmetricPower n ((toRingCat J Osharp).obj.obj X) (M.val.obj X),
        ∃ cmp : P ⟶ (SheafOfModules.forget (toRingCat J Osharp)).obj (A.piece (n : ℤ)),
          (∀ (X Y : Cᵒᵖ) (f : X ⟶ Y) (s : Fin n → M.val.obj X)
              (x : SymPow.symmetricPower n ((toRingCat J Osharp).obj.obj X) (M.val.obj X))
              (y : SymPow.symmetricPower n ((toRingCat J Osharp).obj.obj Y) (M.val.obj Y)),
            ((x : SymmetricAlgebra ((toRingCat J Osharp).obj.obj X) (M.val.obj X)) =
                ∏ i : Fin n, SymmetricAlgebra.ι ((toRingCat J Osharp).obj.obj X)
                  (M.val.obj X) (s i)) →
            ((y : SymmetricAlgebra ((toRingCat J Osharp).obj.obj Y) (M.val.obj Y)) =
                ∏ i : Fin n, SymmetricAlgebra.ι ((toRingCat J Osharp).obj.obj Y)
                  (M.val.obj Y) (M.val.map f (s i))) →
            e Y (P.map f ((e X).symm x)) = y) ∧
          (∀ (X : Cᵒᵖ) (s : Fin n → M.val.obj X)
              (x : SymPow.symmetricPower n ((toRingCat J Osharp).obj.obj X) (M.val.obj X)),
            ((x : SymmetricAlgebra ((toRingCat J Osharp).obj.obj X) (M.val.obj X)) =
                ∏ i : Fin n, SymmetricAlgebra.ι ((toRingCat J Osharp).obj.obj X)
                  (M.val.obj X) (s i)) →
            Hom.app cmp X ((e X).symm x) =
              A.toPresheafGradedAlgebra.homogeneousProdLeft X n
                fun i => gen.val.app X (s i)) ∧
          IsIso ((sheafificationHomEquiv (𝟙 (toRingCat J Osharp).obj)).symm cmp)

Tag 01CH, a lemma

Tag 01CH in the Stacks Project.

SheafOfModules.symmetricAlgebra_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/AlgebraStalkUngraded.lean, line 536. The attribute's comment: “the ungraded symmetric assertion Sym(M)ₓ ≅ Sym(Mₓ), with the isomorphism pinned down by its values on germs of products of local sections in every degree. The tensor assertions are SheafOfModules.tensorPower_stalk and SheafOfModules.tensorAlgebra_stalk; the ungraded exterior assertion ⋀(M)ₓ ≅ ⋀(Mₓ) for a sheaf is SheafOfModules.exteriorAlgebra_stalk in StacksFrontier.Algebra.Category.ModuleCat.Sheaf.ExteriorStalkUngraded, and the degreewise exterior assertion is PresheafOfModules.extPowStalkEquivOfStalkIso. With those the three ungraded isomorphisms the source asserts are all proved”. References: EGA II (1.7.4), “(S(E))_s = S(E_s)”.

Tag 01CH, ungraded symmetric assertion. For a sheaf of modules M on a topological space with a sheaf of commutative rings O♯, a symmetric algebra A of M in the sense of Section 17.21, and a point x, there is a canonical isomorphism of O_x-modules

Sym(M)_x ≅ Sym_{O_x}(M_x),

where Sym(M) is the coproduct ∐ n, Symⁿ M of the homogeneous pieces of A.

It is canonical in the sense Tag 01CH means: its value is prescribed on the germ of every local section of the form s₀ ⋯ sₙ₋₁, in every degree n, namely the product of the germs of the sᵢ; such products span each symmetric power of the stalk (SymmetricAlgebra.symmetricPower_eq_span_prod_ι) and the symmetric powers span Sym(M_x) (SymmetricAlgebra.directSumSymmetricPowerEquiv), so no other linear map has that behaviour.

The symmetric algebra is a hypothesis rather than a chosen term because Section 17.21 pins it only up to canonical isomorphism; SheafOfModules.isSymmetricAlgebra_sectionwiseSymmetricAlgebra_val shows the hypothesis is satisfiable for every M, and SheafOfModules.TensorExteriorSymmetricAlgebras.symmetricAlgebraStalkEquiv discharges it from a package of the three algebras of Section 17.21.

The tag carries a clause comment: this declaration carries the ungraded symmetric assertion alone. The two tensor assertions are SheafOfModules.tensorPower_stalk and SheafOfModules.tensorAlgebra_stalk in StacksFrontier.Algebra.Category.ModuleCat.Sheaf.TensorPowerStalk. The ungraded exterior assertion ⋀(M)ₓ ≅ ⋀(Mₓ) for a sheaf is SheafOfModules.exteriorAlgebra_stalk in StacksFrontier.Algebra.Category.ModuleCat.Sheaf.ExteriorStalkUngraded, which is built from SheafOfModules.natStalkCoprodEquiv below exactly as this declaration is; the ungraded statement for a presheaf of modules, (⋀ F)ₓ ≅ ⋀(Fₓ), is PresheafOfModules.extAlgStalkRingEquiv in StacksFrontier.Algebra.Category.ModuleCat.Sheaf.ExteriorPowerStalk and the degreewise sheaf statement is PresheafOfModules.extPowStalkEquivOfStalkIso there.

theorem symmetricAlgebra_stalk (x : ↥X) :
    ∃ cmp : ↑(TopCat.Presheaf.stalk (∐ fun n : ℕ => A.piece (n : ℤ)).val.presheaf x)
        ≃ₗ[↑(TopCat.Presheaf.stalk Osharp.obj x)]
        SymmetricAlgebra ↑(TopCat.Presheaf.stalk Osharp.obj x)
          ↑(TopCat.Presheaf.stalk M.val.presheaf x),
      ∀ (n : ℕ) (U : Opens ↥X) (hx : x ∈ U) (s : Fin n → M.val.obj (op U)),
        cmp (TopCat.Presheaf.germ (∐ fun m : ℕ => A.piece (m : ℤ)).val.presheaf U x hx
            ((Sigma.ι (fun m : ℕ => A.piece (m : ℤ)) n).val.app (op U)
              (A.toPresheafGradedAlgebra.homogeneousProd (op U) n
                fun i => gen.val.app (op U) (s i)))) =
          ∏ i : Fin n, SymmetricAlgebra.ι ↑(TopCat.Presheaf.stalk Osharp.obj x)
            ↑(TopCat.Presheaf.stalk M.val.presheaf x)
            (TopCat.Presheaf.germ M.val.presheaf U x hx (s i))

PresheafOfModules.extPowStalkEquivOfStalkIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExteriorPowerStalk.lean, line 792. The attribute's comment: “the exterior assertion in each graded degree n: (⋀ⁿ M)ₓ ≅ ⋀ⁿ(Mₓ), with the isomorphism pinned by extPowStalkEquivOfStalkIso_germ_ιMulti as the map carrying the germ of a wedge of local sections to the wedge of their germs. The symmetric assertion is PresheafOfModules.symPowStalkEquivOfStalkIso. The graded-to-ungraded passage is not proved here; it is SheafOfModules.exteriorAlgebra_stalk in StacksFrontier.Algebra.Category.ModuleCat.Sheaf.ExteriorStalkUngraded, which is the ungraded ⋀(M)ₓ ≅ ⋀(Mₓ) that the source actually asserts.”. References: EGA 0 (4.1.5), “more general”.

The stalk of a sheafification of the sectionwise exterior powers. If φ exhibits Q as having the same stalks as the presheaf U ↦ ⋀ⁿ_{R(U)}(F(U)) — which the sheafification unit does, by PresheafOfModules.isIso_stalkFunctor_map_toSheafify — then the stalk of Q at x is ⋀ⁿ_{R_x}(F_x).

This is the form the exterior assertion of Stacks Tag 01CH is consumed in: the degree-n exterior power of a sheaf of modules on a ringed space is the sheafification of the sectionwise exterior powers, so taking Q to be that sheafification and φ its unit computes the stalk of ⋀ⁿ F. The isomorphism is pinned by extPowStalkEquivOfStalkIso_germ_ιMulti, which is the reason this and not an abstract uniqueness isomorphism is what the tag asserts.

noncomputable def extPowStalkEquivOfStalkIso (n : ℕ)
    {Q : PresheafOfModules.{u} (R ⋙ forget₂ CommRingCat.{u} RingCat.{u})}
    (φ : extPow n F ⟶ Q)
    (h : IsIso ((TopCat.Presheaf.stalkFunctor AddCommGrpCat.{u} x).map
      ((toPresheaf _).map φ))) :
    ↑(TopCat.Presheaf.stalk Q.presheaf x) ≃ₗ[↑(R.stalk x)]
      ⋀[↑(R.stalk x)]^n ↑(TopCat.Presheaf.stalk F.presheaf x)

SheafOfModules.exteriorAlgebra_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExteriorStalkUngraded.lean, line 346. The attribute's comment: “the ungraded exterior assertion ⋀(M)ₓ ≅ ⋀(Mₓ) — one of the three isomorphisms the source asserts — with the isomorphism pinned down by its values on germs of wedges of local sections in every degree. The ungraded symmetric assertion Sym(M)ₓ ≅ Sym(Mₓ) is SheafOfModules.symmetricAlgebra_stalk. The ungraded tensor assertion T(M)ₓ ≅ T(Mₓ) is not covered here. The degreewise clauses, which are this library's convention and not assertions of the source, are SheafOfModules.symmetricPower_stalk and PresheafOfModules.extPowStalkEquivOfStalkIso.”.

Tag 01CH, ungraded exterior assertion. For a sheaf of modules M on a topological space with a sheaf of commutative rings O♯, an exterior algebra A of M in the sense of Section 17.21, and a point x, there is a canonical isomorphism of O_x-modules

⋀(M)_x ≅ ⋀_{O_x}(M_x),

where ⋀(M) is the coproduct ∐ n, ⋀ⁿ M of the homogeneous pieces of A.

It is canonical in the sense Tag 01CH means: its value is prescribed on the germ of every local section of the form s₀ ∧ ⋯ ∧ s_{n-1}, in every degree n, namely the wedge of the germs of the sᵢ; such wedges span each exterior power of the stalk (ExteriorAlgebra.ιMulti_span_fixedDegree) and the exterior powers span ⋀(M_x) (ExteriorAlgebra.gradedAlgebra), so no other linear map has that behaviour.

The exterior algebra is a hypothesis rather than a chosen term because Section 17.21 pins it only up to canonical isomorphism; SheafOfModules.isExteriorAlgebra_sectionwiseExteriorAlgebra_val shows the hypothesis is satisfiable for every M, and SheafOfModules.TensorExteriorSymmetricAlgebras.exteriorAlgebraStalkEquiv discharges it from a package of the three algebras of Section 17.21.

theorem exteriorAlgebra_stalk (x : ↥X) :
    ∃ cmp : ↑(TopCat.Presheaf.stalk (∐ fun n : ℕ => A.piece (n : ℤ)).val.presheaf x)
        ≃ₗ[↑(TopCat.Presheaf.stalk Osharp.obj x)]
        ExteriorAlgebra ↑(TopCat.Presheaf.stalk Osharp.obj x)
          ↑(TopCat.Presheaf.stalk M.val.presheaf x),
      ∀ (n : ℕ) (U : Opens ↥X) (hx : x ∈ U) (s : Fin n → M.val.obj (op U)),
        cmp (TopCat.Presheaf.germ (∐ fun m : ℕ => A.piece (m : ℤ)).val.presheaf U x hx
            ((Sigma.ι (fun m : ℕ => A.piece (m : ℤ)) n).val.app (op U)
              (A.toPresheafGradedAlgebra.homogeneousProd (op U) n
                fun i => gen.val.app (op U) (s i)))) =
          ExteriorAlgebra.ιMulti ↑(TopCat.Presheaf.stalk Osharp.obj x) n
            fun i => TopCat.Presheaf.germ M.val.presheaf U x hx (s i)

SheafOfModules.symmetricPower_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SymmetricStalkSheaf.lean, line 431. The attribute's comment: “the symmetric assertion in each graded degree n: (Symⁿ M)ₓ ≅ Symⁿ(Mₓ), with the isomorphism pinned down by its values on germs of products of local sections. The ungraded Sym(M)ₓ ≅ Sym(Mₓ) is SheafOfModules.symmetricAlgebra_stalk; the exterior assertion in each degree is PresheafOfModules.extPowStalkEquivOfStalkIso and the ungraded ⋀(M)ₓ ≅ ⋀(Mₓ) is SheafOfModules.exteriorAlgebra_stalk; the tensor assertions are SheafOfModules.tensorPower_stalk and SheafOfModules.tensorAlgebra_stalk. The three assertions the source makes are the ungraded ones; the degreewise statements, this one included, are this library's clause convention”. References: EGA II (1.7.4), “partial”.

Tag 01CH, symmetric clause, in graded degree n. For a sheaf of modules M on a topological space with a sheaf of commutative rings O♯, a symmetric algebra A of M in the sense of Section 17.21, and a point x, there is a canonical isomorphism of O_x-modules

(Symⁿ M)_x ≅ Symⁿ_{O_x}(M_x).

It is canonical in the sense Tag 01CH means: its value is prescribed on the germ of every local section of the form s₀ ⋯ sₙ₋₁, namely the product of the germs of the sᵢ, and such products span the target (SymmetricAlgebra.symmetricPower_eq_span_prod_ι), so no other linear map has that behaviour.

The symmetric algebra is a hypothesis rather than a chosen term because Section 17.21 pins it only up to canonical isomorphism; SheafOfModules.isSymmetricAlgebra_sectionwiseSymmetricAlgebra_val shows the hypothesis is satisfiable for every M, and SheafOfModules.TensorExteriorSymmetricAlgebras.symmetricPowerStalkEquiv discharges it from a package of the three algebras of Section 17.21.

The tag carries a clause comment: this declaration carries the symmetric degreewise assertion alone. The ungraded symmetric assertion Sym(M)_x ≅ Sym(M_x) is proved from this one in StacksFrontier.Algebra.Category.ModuleCat.Sheaf.AlgebraStalkUngraded, and the two tensor assertions are SheafOfModules.tensorPower_stalk and SheafOfModules.tensorAlgebra_stalk in StacksFrontier.Algebra.Category.ModuleCat.Sheaf.TensorPowerStalk.

The exterior assertion in each graded degree is PresheafOfModules.extPowStalkEquivOfStalkIso in StacksFrontier.Algebra.Category.ModuleCat.Sheaf.ExteriorPowerStalk, pinned on germs of wedges of local sections by PresheafOfModules.extPowStalkEquivOfStalkIso_germ_ιMulti. It is stated there for a presheaf of modules together with a morphism out of the sectionwise exterior powers which is a stalk isomorphism — the form a sheafification presentation supplies — rather than in the bundled framing used here; SheafOfModules.exteriorPowerStalkEquiv in StacksFrontier.Algebra.Category.ModuleCat.Sheaf.ExteriorStalkUngraded is the bundled form, and SheafOfModules.exteriorAlgebra_stalk there is the ungraded exterior assertion. See the implementation notes of this file.

theorem symmetricPower_stalk (n : ℕ) (x : ↥X) :
    ∃ cmp : ↑(TopCat.Presheaf.stalk (A.piece (n : ℤ)).val.presheaf x)
        ≃ₗ[↑(TopCat.Presheaf.stalk Osharp.obj x)]
        SymPow.symmetricPower n ↑(TopCat.Presheaf.stalk Osharp.obj x)
          ↑(TopCat.Presheaf.stalk M.val.presheaf x),
      ∀ (U : Opens ↥X) (hx : x ∈ U) (s : Fin n → M.val.obj (op U)),
        (cmp (TopCat.Presheaf.germ (A.piece (n : ℤ)).val.presheaf U x hx
              (A.toPresheafGradedAlgebra.homogeneousProd (op U) n
                fun i => gen.val.app (op U) (s i))) :
            SymmetricAlgebra ↑(TopCat.Presheaf.stalk Osharp.obj x)
              ↑(TopCat.Presheaf.stalk M.val.presheaf x)) =
          ∏ i : Fin n, SymmetricAlgebra.ι ↑(TopCat.Presheaf.stalk Osharp.obj x)
            ↑(TopCat.Presheaf.stalk M.val.presheaf x)
            (TopCat.Presheaf.germ M.val.presheaf U x hx (s i))

SheafOfModules.tensorPower_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorPowerStalk.lean, line 986. The attribute's comment: “the tensor assertion in each graded degree n: (Tⁿ M)ₓ ≅ Tⁿ(Mₓ) for a sheaf of modules, with the isomorphism pinned down by its values on germs of ordered tensors of local sections. The ungraded T(M)ₓ ≅ T(Mₓ) is SheafOfModules.tensorAlgebra_stalk; the symmetric assertions are SheafOfModules.symmetricPower_stalk and SheafOfModules.symmetricAlgebra_stalk; the exterior assertion is not carried here”.

For a sheaf of modules M on a topological space with a sheaf of commutative rings O♯, a tensor algebra A of M in the sense of Section 17.21, and a point x, there is an isomorphism of O_x-modules

(Tⁿ M)ₓ ≅ Tⁿ_{O_x}(M_x)

sending the germ of every local section coming from an ordered tensor s₀ ⊗ ⋯ ⊗ s_{n-1} to the ordered tensor of the germs of the sᵢ.

theorem tensorPower_stalk (n : ℕ) (x : ↥X) :
    ∃ cmp : ↑(TopCat.Presheaf.stalk (A.piece (n : ℤ)).val.presheaf x)
        ≃ₗ[↑(TopCat.Presheaf.stalk Osharp.obj x)]
        TensorAlgebra.gradedPiece ↑(TopCat.Presheaf.stalk Osharp.obj x) n
          ↑(TopCat.Presheaf.stalk M.val.presheaf x),
      ∀ (U : Opens ↥X) (hx : x ∈ U) (s : Fin n → M.val.obj (op U)),
        cmp (TopCat.Presheaf.germ (A.piece (n : ℤ)).val.presheaf U x hx
              (PresheafOfModules.Hom.app (tensorAlgPieceIso A gen hA (n : ℤ)).hom.val (op U)
                (PresheafOfModules.Hom.app (PresheafOfModules.sheafifyUnit
                    (toRingCatMap (Opens.grothendieckTopology ↥X) (𝟙 Osharp.obj))
                    (PresheafOfModules.tensorPow n M.val)) (op U)
                  (TensorAlgebra.ιMultiPow
                    ((Osharp.obj ⋙ forget₂ CommRingCat.{u} RingCat.{u}).obj (op U)) n s)))) =
          TensorAlgebra.ιMultiPow ↑(TopCat.Presheaf.stalk Osharp.obj x) n
            fun i => TopCat.Presheaf.germ M.val.presheaf U x hx (s i)

SheafOfModules.tensorAlgebra_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorPowerStalk.lean, line 1065. The attribute's comment: “the ungraded tensor assertion T(M)ₓ ≅ T(Mₓ), with the isomorphism pinned down by its values on germs of ordered tensors of local sections in every degree. The degreewise (Tⁿ M)ₓ ≅ Tⁿ(Mₓ) is SheafOfModules.tensorPower_stalk; the symmetric assertions are SheafOfModules.symmetricPower_stalk and SheafOfModules.symmetricAlgebra_stalk; the exterior assertion is not carried here”.

For a sheaf of modules M on a topological space with a sheaf of commutative rings O♯, a tensor algebra A of M in the sense of Section 17.21, and a point x, there is an isomorphism of O_x-modules

T(M)ₓ ≅ T_{O_x}(M_x),

where T(M) is the coproduct ∐ n, Tⁿ M of the homogeneous pieces of A, sending the germ of every local section coming from an ordered tensor s₀ ⊗ ⋯ ⊗ s_{n-1}, in every degree n, to the ordered tensor of the germs of the sᵢ.

theorem tensorAlgebra_stalk (x : ↥X) :
    ∃ cmp : ↑(TopCat.Presheaf.stalk (∐ fun n : ℕ => A.piece (n : ℤ)).val.presheaf x)
        ≃ₗ[↑(TopCat.Presheaf.stalk Osharp.obj x)]
        TensorAlgebra ↑(TopCat.Presheaf.stalk Osharp.obj x)
          ↑(TopCat.Presheaf.stalk M.val.presheaf x),
      ∀ (n : ℕ) (U : Opens ↥X) (hx : x ∈ U) (s : Fin n → M.val.obj (op U)),
        cmp (TopCat.Presheaf.germ (∐ fun m : ℕ => A.piece (m : ℤ)).val.presheaf U x hx
            ((Sigma.ι (fun m : ℕ => A.piece (m : ℤ)) n).val.app (op U)
              (PresheafOfModules.Hom.app (tensorAlgPieceIso A gen hA (n : ℤ)).hom.val (op U)
                (PresheafOfModules.Hom.app (PresheafOfModules.sheafifyUnit
                    (toRingCatMap (Opens.grothendieckTopology ↥X) (𝟙 Osharp.obj))
                    (PresheafOfModules.tensorPow n M.val)) (op U)
                  (TensorAlgebra.ιMultiPow
                    ((Osharp.obj ⋙ forget₂ CommRingCat.{u} RingCat.{u}).obj (op U)) n s))))) =
          TensorAlgebra.ιMulti ↑(TopCat.Presheaf.stalk Osharp.obj x) n
            fun i => TopCat.Presheaf.germ M.val.presheaf U x hx (s i)

Tag 01CI, a lemma

Tag 01CI in the Stacks Project.

Stacks.PullbackExteriorAlgebra.exteriorAlgebraPullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExteriorAlgebraPullbackIso.lean, line 877. The attribute's comment: “pullback_exterior_algebra: the EXTERIOR algebra clause only; symmetric NOT proved”.

Stacks 01CI for the exterior algebra of a sheaf of modules. For a morphism of ringed spaces f : X ⟶ Y and a sheaf of 𝒪_Y-modules M, the pullback of the exterior algebra of M is canonically isomorphic to the exterior algebra of f^*M, degreewise and on the underlying direct-sum sheaf, compatibly with the products, the units and the degree-one generators.

This covers the exterior algebra clause of Tag 01CI only. The tensor-algebra clause is Stacks.PullbackAlgebra.pullbackTensorPieceIso and pullbackTensorSheafIso; the symmetric-algebra clause is not proved here. Both exterior algebras are given by their universal properties (SheafOfModules.GradedAlgebra.IsExteriorAlgebra) rather than by a construction, so nothing here depends on an unconstructed exterior algebra.

noncomputable def exteriorAlgebraPullbackIso (hA : IsExteriorAlgebra A ι)
    (hB : IsExteriorAlgebra B κ) : ExteriorAlgebraPullbackIso f A ι B κ

Stacks.PullbackExteriorAlgebra.exteriorAlgebraPullbackIso_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExteriorAlgebraPullbackIso.lean, line 892. The attribute's comment: “pullback_exterior_algebra: canonicality of the EXTERIOR algebra comparison only”.

The comparison of Stacks 01CI is unique. Compatibility with multiplication, with the unit and with the degree-one generators on the pullback-unit sections determines the comparison in every degree, and the restriction to the homogeneous summands then determines the comparison of the underlying direct-sum sheaves.

theorem exteriorAlgebraPullbackIso_unique (hA : IsExteriorAlgebra A ι)
    (hB : IsExteriorAlgebra B κ) (e : ExteriorAlgebraPullbackIso f A ι B κ) :
    e = exteriorAlgebraPullbackIso f A ι B κ hA hB

Stacks.PullbackAlgebra.pullbackTensorPieceIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PullbackAlgebraIso.lean, line 331. The attribute's comment: “the tensor algebra only. The exterior and symmetric algebras are NOT proved here; see the implementation notes for the two missing inputs.”.

The pullback of the degree-n piece of the tensor algebra of F is the degree-n piece of the tensor algebra of f^*F.

noncomputable def pullbackTensorPieceIso (n : ℕ) :
    (pullbackFunctor f).obj (S.tensor.piece (n : ℤ)) ≅ T.tensor.piece (n : ℤ)

Stacks.PullbackAlgebra.pullbackTensorSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PullbackAlgebraIso.lean, line 393. The attribute's comment: “the tensor algebra only, on the underlying direct-sum sheaf. The exterior and symmetric algebras are NOT proved here.”.

The pullback of the underlying direct-sum sheaf of the tensor algebra of F is the underlying direct-sum sheaf of the tensor algebra of f^*F.

noncomputable def pullbackTensorSheafIso :
    (pullbackFunctor f).obj S.tensorAlgebraSheaf ≅ T.tensorAlgebraSheaf

Stacks.RingedSpace.pullbackSymmetricPieceIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SymmetricPullback/Iso.lean, line 94. The attribute's comment: “symmetric algebra”. References: EGA II (1.7.5), “partial”.

Stacks 01CI for the symmetric algebra. For a morphism of ringed spaces f : X ⟶ Y and a sheaf of 𝒪_Y-modules F, the pullback of the degree-n symmetric power of F is the degree-n symmetric power of f^*F:

f^*(Symⁿ F) ≅ Symⁿ(f^*F).

The two symmetric algebras are given by their universal property, so this is a statement about the symmetric algebras and not about one construction of them.

noncomputable def pullbackSymmetricPieceIso (hA : IsSymmetricAlgebra A ι)
    (hB : IsSymmetricAlgebra B κ) (n : ℤ) :
    (pullbackFunctor f).obj (A.piece n) ≅ B.piece n

Stacks.RingedSpace.pullbackSymmetricPieceIsoOfRingedSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SymmetricPullback/Iso.lean, line 137. The attribute's comment: “symmetric algebra, at the constructed symmetric algebras”. References: EGA II (1.7.5), “partial”.

Stacks 01CI for the symmetric algebra, at the constructed symmetric algebras. For a morphism of ringed spaces f : X ⟶ Y and a sheaf of 𝒪_Y-modules F, the pullback of the degree-n symmetric power of F is the degree-n symmetric power of f^*F, both taken in SheafOfModules.ringedSpaceAlgebras.

noncomputable def pullbackSymmetricPieceIsoOfRingedSpace
    (G : SheafOfModules.{u} (structureRingSheaf Y)) (n : ℤ) :
    (pullbackFunctor f).obj ((SheafOfModules.ringedSpaceAlgebras Y G).symmetric.piece n) ≅
      (SheafOfModules.ringedSpaceAlgebras X
        ((pullbackFunctor f).obj G)).symmetric.piece n

Tag 01CJ, a lemma

Tag 01CJ in the Stacks Project.

SheafOfModules.ExtPresentation.epi_extDesc_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExteriorPresentationExact.lean, line 334. The attribute's comment: “exterior case, surjectivity clause: the second map of the sequence is an epimorphism, in every degree and with no exactness hypothesis. Exactness at the middle term is covered, by SheafOfModules.ExtPresentation.exteriorPresentation_exact below, which carries that clause and states the sequence of the source. The symmetric counterparts are SheafOfModules.SymPresentation.epi_symDesc_app and SheafOfModules.SymPresentation.symmetricPresentation_exact.”.

The surjectivity clause of Stacks Tag 01CJ for exterior powers. If p : M₁ ⟶ M is an epimorphism of sheaves of modules on a space, A' is an exterior algebra of M₁ and B' an exterior algebra of M, then the induced map ⋀ⁿ(M₁) ⟶ ⋀ⁿ(M) is an epimorphism in every degree. This is the clause ⟶ 0 of the sequence Tag 01CJ asserts.

The hypothesis n ≥ 1 of the source is not needed: the statement holds in degree 0 too, where both powers are the structure sheaf.

theorem epi_extDesc_app [Epi p] (n : ℕ) : Epi ((extDesc ι κ hA' hB' p).app (n : ℤ))

SheafOfModules.ExtPresentation.exteriorPresentation_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExteriorPresentationExact.lean, line 600. The attribute's comment: “exterior case, in full: the sequence M₂ ⊗ ⋀^k(M₁) ⟶ ⋀^{k+1}(M₁) ⟶ ⋀^{k+1}(M) ⟶ 0 is exact at the middle term and its second map is an epimorphism. The surjectivity clause alone, in every degree and with no exactness hypothesis, is SheafOfModules.ExtPresentation.epi_extDesc_app. With the symmetric pair SheafOfModules.SymPresentation.epi_symDesc_app and SheafOfModules.SymPresentation.symmetricPresentation_exact this completes the tag: the source states the two clauses for the symmetric and the exterior powers and nothing else.”.

Stacks Tag 01CJ for exterior powers. Let M₂ --q--> M₁ --p--> M ⟶ 0 be a presentation of a sheaf of modules on a topological space with a sheaf of commutative rings — p an epimorphism and the complex exact at M₁ — let A' be an exterior algebra of M₁ and B' one of M. Then for every k the three-term sequence

M₂ ⊗ ⋀^k(M₁) ⟶ ⋀^{k+1}(M₁) ⟶ ⋀^{k+1}(M) ⟶ 0

is exact at the middle term and its second map is an epimorphism, which is the exactness the source asserts in every degree n = k + 1 ≥ 1.

theorem exteriorPresentation_exact (hS : (ShortComplex.mk q p hqp).Exact) [Epi p] (k : ℕ) :
    (extComplex ι κ hA' hB' p q hqp k).Exact ∧
      Epi (extComplex ι κ hA' hB' p q hqp k).g

SheafOfModules.SymPresentation.epi_symDesc_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SymmetricPowerPresentation.lean, line 380. The attribute's comment: “symmetric case, surjectivity clause: the second map of the sequence is an epimorphism, in every degree and with no exactness hypothesis. Exactness at the middle term is covered, by SheafOfModules.SymPresentation.symmetricPresentation_exact in StacksFrontier.Algebra.Category.ModuleCat.Sheaf.SymmetricPresentationExact, which carries that clause and states the sequence of the source. The exterior case is covered too, by SheafOfModules.ExtPresentation.epi_extDesc_app and SheafOfModules.ExtPresentation.exteriorPresentation_exact in StacksFrontier.Algebra.Category.ModuleCat.Sheaf.ExteriorPresentationExact; those four declarations are the tag's covering set.”.

The surjectivity clause of Stacks Tag 01CJ for symmetric powers. If p : M₁ ⟶ M is an epimorphism of sheaves of modules on a space, A' is a symmetric algebra of M₁ and B' a symmetric algebra of M, then the induced map Symⁿ(M₁) ⟶ Symⁿ(M) is an epimorphism in every degree. This is the clause ⟶ 0 of the sequence Tag 01CJ asserts.

The hypothesis n ≥ 1 of the source is not needed: the statement holds in degree 0 too, where both powers are the structure sheaf.

theorem epi_symDesc_app [Epi p] (n : ℕ) : Epi ((symDesc ι κ hA' hB' p).app (n : ℤ))

SheafOfModules.SymPresentation.symmetricPresentation_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SymmetricPresentationExact.lean, line 528. The attribute's comment: “symmetric case, in full: the sequence M₂ ⊗ Sym^k(M₁) ⟶ Sym^{k+1}(M₁) ⟶ Sym^{k+1}(M) ⟶ 0 is exact at the middle term and its second map is an epimorphism. The surjectivity clause alone, in every degree and with no exactness hypothesis, is SheafOfModules.SymPresentation.epi_symDesc_app. The exterior case is covered too, by SheafOfModules.ExtPresentation.epi_extDesc_app and SheafOfModules.ExtPresentation.exteriorPresentation_exact in StacksFrontier.Algebra.Category.ModuleCat.Sheaf.ExteriorPresentationExact; those four declarations are the tag's covering set”. References: EGA 0 (19.5.1), “more general”.

Stacks Tag 01CJ for symmetric powers. Let M₂ --q--> M₁ --p--> M ⟶ 0 be a presentation of a sheaf of modules on a topological space with a sheaf of commutative rings — p an epimorphism and the complex exact at M₁ — let A' be a symmetric algebra of M₁ and B' one of M. Then for every k the three-term sequence

M₂ ⊗ Sym^k(M₁) ⟶ Sym^{k+1}(M₁) ⟶ Sym^{k+1}(M) ⟶ 0

is exact at the middle term and its second map is an epimorphism, which is the exactness the source asserts in every degree n = k + 1 ≥ 1.

The tag carries a clause comment: the surjectivity clause is also carried, at greater generality, by SheafOfModules.SymPresentation.epi_symDesc_app, and the exterior half of Tag 01CJ is not proved anywhere. See this file's implementation notes.

theorem symmetricPresentation_exact (hS : (ShortComplex.mk q p hqp).Exact) [Epi p] (k : ℕ) :
    (symComplex ι κ hA' hB' q p hqp k).Exact ∧ Epi (symComplex ι κ hA' hB' q p hqp k).g

SheafOfModules.exact_and_epi_symmetricPresentationShortComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SymmetricSituation/PowerExact.lean, line 791. The attribute's comment: “symmetric powers”.

Stacks Tag 01CJ, symmetric powers. Let M₂ --q--> M₁ --p--> M --> 0 be an exact sequence of sheaves of modules on a ringed site, and let n = 1 + k with k ≥ 0. Then

M₂ ⊗ Sym^k(M₁) ⟶ Symⁿ(M₁) ⟶ Symⁿ(M) ⟶ 0

is exact: the complex is exact at the middle term and its second map is an epimorphism.

theorem exact_and_epi_symmetricPresentationShortComplex (q : M₂ ⟶ M₁) (p : M₁ ⟶ M)
    (hqp : q ≫ p = 0) [Epi p] (hex : (ShortComplex.mk q p hqp).Exact)
    (k n : ℤ) (hk : 0 ≤ k) (hn : 1 + k = n) :
    (GradedAlgebra.symmetricPresentationShortComplex
        (isSymmetricAlgebra_sheafifiedSymmetricAlgebra J M₁)
        (isSymmetricAlgebra_sheafifiedSymmetricAlgebra J M).isUniversal.1
        q p hqp k n hn).Exact ∧
      Epi (GradedAlgebra.symmetricPresentationShortComplex
        (isSymmetricAlgebra_sheafifiedSymmetricAlgebra J M₁)
        (isSymmetricAlgebra_sheafifiedSymmetricAlgebra J M).isUniversal.1
        q p hqp k n hn).g

Tag 01CK, a lemma

Tag 01CK in the Stacks Project.

Stacks.SheafOfModules.isCoherent_exteriorPower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExteriorPowerCoherent.lean, line 297. The attribute's comment: “exterior powers of a coherent module, in positive degree”.

Each exterior power of positive degree of a coherent sheaf of modules on a ringed space is coherent. This is clause (4) of [Stacks, Tag 01CK] for the exterior powers. The kernel K of the quotient map Tⁿ(F) ⟶ ⋀ⁿ(F) is of finite type over each member of a cover presenting F finitely, by Tag 01BP; hence coherent by Tag 01BY (1), since it is a subsheaf of the coherent sheaf Tⁿ(F); hence ⋀ⁿ(F) is coherent by Tag 01BY (3).

theorem isCoherent_exteriorPower [_root_.SheafOfModules.IsCoherent F]
    (A : _root_.SheafOfModules.TensorExteriorSymmetricAlgebras
      (Opens.grothendieckTopology X.carrier) F) (n : ℕ) (hn : 0 < n) :
    _root_.SheafOfModules.IsCoherent (A.exteriorPower n)

Stacks.SheafOfModules.isFinitePresentation_exteriorPower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExteriorPowerFiniteType.lean, line 311. The attribute's comment: “exterior powers of a module of finite presentation”.

Each exterior power of a sheaf of modules of finite presentation on a ringed space is of finite presentation. The covering family is the one that presents F finitely; no degree needs a smaller open, because Stacks.SheafOfModules.exists_isFinite_presentation_exteriorPower_over presents every degree finitely over that same open. This is clause (3) of [Stacks, Tag 01CK] for the exterior powers.

theorem isFinitePresentation_exteriorPower [F.IsFinitePresentation] (n : ℕ) :
    (A.exteriorPower n).IsFinitePresentation

Stacks.SheafOfModules.isLocallyFree_symmetricPower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocallyFreePowers.lean, line 179. The attribute's comment: “symmetric powers of a locally free module”.

Each symmetric power of a locally free sheaf of modules is locally free. This is clause (6) of [Stacks, Tag 01CK] for the symmetric powers: a covering trivialising F with index types γ i trivialises Symⁿ F with index types the degree-n multidegrees in γ i.

theorem isLocallyFree_symmetricPower
    (A : _root_.SheafOfModules.TensorExteriorSymmetricAlgebras J F) (n : ℕ)
    [hF : F.IsLocallyFree] : (A.symmetricPower n).IsLocallyFree

Stacks.SheafOfModules.isLocallyFree_exteriorPower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocallyFreePowers.lean, line 190. The attribute's comment: “exterior powers of a locally free module”. References: SGA 6 X (6.1), “special case”.

Each exterior power of a locally free sheaf of modules is locally free. This is clause (6) of [Stacks, Tag 01CK] for the exterior powers: a covering trivialising F with index types γ i trivialises ⋀ⁿ F with index types the n-element subsets of γ i.

theorem isLocallyFree_exteriorPower
    (A : _root_.SheafOfModules.TensorExteriorSymmetricAlgebras J F) (n : ℕ)
    [hF : F.IsLocallyFree] : (A.exteriorPower n).IsLocallyFree

Stacks.SheafOfModules.isLocallyFree_tensorPower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocallyFreePowers.lean, line 268. The attribute's comment: “tensor powers of a locally free module”.

Each tensor power of a locally free sheaf of modules is locally free. This is clause (6) of [Stacks, Tag 01CK] for the tensor powers: a covering trivialising F with index types γ i trivialises Tⁿ F with index types the n-fold products of the γ i.

theorem isLocallyFree_tensorPower
    (A : _root_.SheafOfModules.TensorExteriorSymmetricAlgebras J F) (n : ℕ)
    [hF : F.IsLocallyFree] : (A.tensor.piece (n : ℤ)).IsLocallyFree

Stacks.SheafOfModules.nonempty_localGeneratorsData_symmetricPower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PowerLocalGenerators.lean, line 329. The attribute's comment: “symmetric powers of a module locally generated by sections”.

Each symmetric power of a sheaf of modules locally generated by sections on a ringed space is locally generated by sections. This is clause (1) of [Stacks, Tag 01CK] for the symmetric powers.

theorem nonempty_localGeneratorsData_symmetricPower
    (hF : Nonempty (F.LocalGeneratorsData.{u, u, u, u})) (n : ℕ) :
    Nonempty ((A.symmetricPower n).LocalGeneratorsData.{u, u, u, u})

Stacks.SheafOfModules.nonempty_localGeneratorsData_exteriorPower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PowerLocalGenerators.lean, line 338. The attribute's comment: “exterior powers of a module locally generated by sections”.

Each exterior power of a sheaf of modules locally generated by sections on a ringed space is locally generated by sections. This is clause (1) of [Stacks, Tag 01CK] for the exterior powers.

theorem nonempty_localGeneratorsData_exteriorPower
    (hF : Nonempty (F.LocalGeneratorsData.{u, u, u, u})) (n : ℕ) :
    Nonempty ((A.exteriorPower n).LocalGeneratorsData.{u, u, u, u})

Stacks.SheafOfModules.isFiniteType_symmetricPower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PowerLocalGenerators.lean, line 348. The attribute's comment: “symmetric powers of a module of finite type”. References: EGA II (1.7.7), “more general”.

Each symmetric power of a sheaf of modules of finite type on a ringed space is of finite type. This is clause (2) of [Stacks, Tag 01CK] for the symmetric powers: the covering is the one on which F is generated by finitely many sections, and the index type produced in degree n is the set of degree-n multidegrees in the given one, hence finite.

theorem isFiniteType_symmetricPower
    [hF : _root_.SheafOfModules.IsFiniteType.{u, u, u} F] (n : ℕ) :
    _root_.SheafOfModules.IsFiniteType.{u, u, u} (A.symmetricPower n)

Stacks.SheafOfModules.isFiniteType_exteriorPower', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PowerLocalGenerators.lean, line 361. The attribute's comment: “exterior powers of a module of finite type”.

Each exterior power of a sheaf of modules of finite type on a ringed space is of finite type. This is clause (2) of [Stacks, Tag 01CK] for the exterior powers. The primed name distinguishes it from Stacks.SheafOfModules.isFiniteType_exteriorPower, which assumes F of finite presentation and is therefore not this clause.

theorem isFiniteType_exteriorPower'
    [hF : _root_.SheafOfModules.IsFiniteType.{u, u, u} F] (n : ℕ) :
    _root_.SheafOfModules.IsFiniteType.{u, u, u} (A.exteriorPower n)

Stacks.SheafOfModules.isQuasicoherent_symmetricPower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/QuasicoherentAlgebras.lean, line 763. The attribute's comment: “symmetric powers of a quasi-coherent module”.

Each symmetric power of a quasi-coherent sheaf of modules on a ringed space is quasi-coherent. A presentation of the module over an open presents every symmetric power of it over that same open, by Stacks.SheafOfModules.nonempty_presentation_symmetricPower_over, so the covering family which presents the module presents the symmetric power too.

theorem isQuasicoherent_symmetricPower (n : ℕ) : (A.symmetricPower n).IsQuasicoherent

Stacks.SheafOfModules.isCoherent_symmetricPower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SymmetricPowerCoherent.lean, line 304. The attribute's comment: “symmetric powers of a coherent module, in positive degree”.

Each symmetric power of positive degree of a coherent sheaf of modules on a ringed space is coherent. This is clause (4) of [Stacks, Tag 01CK] for the symmetric powers. The sequence used is ⊕_{p < n - 1} Tⁿ(F) ⟶ Tⁿ(F) ⟶ Symⁿ(F) ⟶ 0, whose first term is coherent by Stacks.SheafOfModules.isCoherent_tensorPower and isCoherent_sigma, so that closure of coherence under cokernels finishes.

theorem isCoherent_symmetricPower [_root_.SheafOfModules.IsCoherent F]
    (A : _root_.SheafOfModules.TensorExteriorSymmetricAlgebras
      (Opens.grothendieckTopology X.carrier) F) (n : ℕ) (hn : 0 < n) :
    _root_.SheafOfModules.IsCoherent (A.symmetricPower n)

Stacks.SheafOfModules.isFinitePresentation_symmetricPower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SymmetricPowerFiniteType.lean, line 169. The attribute's comment: “symmetric powers of a module of finite presentation”. References: EGA II (1.7.7), “special case”.

Each symmetric power of a sheaf of modules of finite presentation on a ringed space is of finite presentation. This is clause (3) of [Stacks, Tag 01CK] for the symmetric powers. The covering family is the one that presents F finitely; no degree needs a smaller open, because Stacks.SheafOfModules.exists_isFinite_presentation_symmetricPower_over presents every degree finitely over that same open.

theorem isFinitePresentation_symmetricPower [F.IsFinitePresentation] (n : ℕ) :
    (A.symmetricPower n).IsFinitePresentation

Stacks.SheafOfModules.isCoherent_tensorPower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorPowerCoherent.lean, line 98. The attribute's comment: “tensor powers of a coherent module, in positive degree”.

Each tensor power of positive degree of a coherent sheaf of modules on a ringed space is coherent. This is clause (4) of [Stacks, Tag 01CK] for the tensor powers.

theorem isCoherent_tensorPower [_root_.SheafOfModules.IsCoherent F]
    (A : _root_.SheafOfModules.TensorExteriorSymmetricAlgebras
      (Opens.grothendieckTopology X.carrier) F) (n : ℕ) (hn : 0 < n) :
    _root_.SheafOfModules.IsCoherent (A.tensor.piece (n : ℤ))

Stacks.SheafOfModules.isFinitePresentation_tensorPower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorPowerFiniteType.lean, line 198. The attribute's comment: “tensor powers of a module of finite presentation”.

Each tensor power of a sheaf of modules of finite presentation on a ringed space is of finite presentation. This is clause (3) of [Stacks, Tag 01CK] for the tensor powers. The covering family is the one that presents F finitely; no degree needs a smaller open, because Stacks.SheafOfModules.exists_isFinite_presentation_tensorPiece_over presents every degree finitely over that same open.

theorem isFinitePresentation_tensorPower [F.IsFinitePresentation] (n : ℕ) :
    (A.tensor.piece (n : ℤ)).IsFinitePresentation

Stacks.SheafOfModules.nonempty_localGeneratorsData_tensorPower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorPowerLocalGenerators.lean, line 165. The attribute's comment: “tensor powers of a module locally generated by sections”.

Each tensor power of a sheaf of modules locally generated by sections on a ringed space is locally generated by sections, on the same covering.

theorem nonempty_localGeneratorsData_tensorPower
    (hF : Nonempty (F.LocalGeneratorsData.{t, t, t, t})) (n : ℕ) :
    Nonempty ((A.tensor.piece (n : ℤ)).LocalGeneratorsData.{t, t, t, t})

Stacks.SheafOfModules.isFiniteType_tensorPower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorPowerLocalGenerators.lean, line 173. The attribute's comment: “tensor powers of a module of finite type”.

Each tensor power of a sheaf of modules of finite type on a ringed space is of finite type.

theorem isFiniteType_tensorPower [hF : _root_.SheafOfModules.IsFiniteType.{t, t, t} F] (n : ℕ) :
    _root_.SheafOfModules.IsFiniteType.{t, t, t} (A.tensor.piece (n : ℤ))

Stacks.SheafOfModules.isQuasicoherent_tensorPower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorPowerPresentation.lean, line 548. The attribute's comment: “tensor powers of a quasi-coherent module”.

Each tensor power of a quasi-coherent sheaf of modules on a ringed space is quasi-coherent. This is clause (5) of Stacks Tag 01CK for the tensor powers. A presentation of F over an open presents Tⁿ(F) over that same open, by Stacks.SheafOfModules.nonempty_presentation_tensorPower_over, so the covering family which presents F presents each tensor power too.

theorem isQuasicoherent_tensorPower {X : AlgebraicGeometry.RingedSpace.{t, t}}
    (F : _root_.SheafOfModules.{t} (structureSheafRing X)) [F.IsQuasicoherent]
    (A : _root_.SheafOfModules.TensorExteriorSymmetricAlgebras
      (Opens.grothendieckTopology X.carrier) F) (n : ℕ) :
    (A.tensor.piece (n : ℤ)).IsQuasicoherent

Stacks.SheafOfModules.isQuasicoherent_exteriorPower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/ConstantRank.lean, line 123. The attribute's comment: “exterior powers of a quasi-coherent module”.

Each exterior power of a quasi-coherent sheaf of modules on a ringed space is quasi-coherent. A presentation of the module over an open presents every exterior power of it over that same open, by Stacks.SheafOfModules.nonempty_presentation_exteriorPower_over, so the covering family which presents the module presents the exterior power too.

theorem isQuasicoherent_exteriorPower {X : RingedSpace.{u, u}}
    (F : _root_.SheafOfModules.{u} (structureSheafRing X)) [F.IsQuasicoherent]
    (A : _root_.SheafOfModules.TensorExteriorSymmetricAlgebras
      (Opens.grothendieckTopology X.carrier) F) (n : ℕ) :
    (A.exteriorPower n).IsQuasicoherent

Stacks.SymGraded.isQuasicoherentPieces_of_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SymAlgebraQcohPieces/Basic.lean, line 408. The attribute's comment: “symmetric powers of a quasi-coherent module, at the encoding Stacks.SymGraded.schemeSymAlgebra”.

Every homogeneous piece of Sym(E) is quasi-coherent, for E a quasi-coherent module on an arbitrary scheme. This discharges the hypothesis Stacks.SymGraded.IsQuasicoherentPieces of Stacks.SymGraded.schemeSheafGradedAlgebra and of Stacks.SymGraded.schemeProjectiveBundle for a quasi-coherent module.

theorem isQuasicoherentPieces_of_isQuasicoherent {X : Scheme.{u}} (E : X.Modules)
    [E.IsQuasicoherent] : IsQuasicoherentPieces E

Stacks.SliceAlgebra.isQuasicoherent_sheafifiedSymmetricPiece, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SymmetricFree/Presentation.lean, line 157. The attribute's comment: “symmetric powers of a quasi-coherent module”.

Symmetric powers of a quasi-coherent module are quasi-coherent. For a quasi-coherent sheaf of modules F on a scheme X and n : ℕ, the degree-n piece of the symmetric algebra of F is quasi-coherent.

theorem SliceAlgebra.isQuasicoherent_sheafifiedSymmetricPiece (X : Scheme.{u})
    (F : X.Modules) [F.IsQuasicoherent] (n : ℕ) :
    ((sheafifiedSymmetricAlgebra (Opens.grothendieckTopology ↥X) F).piece
      (n : ℤ)).IsQuasicoherent

Tag 01CL, a lemma

Tag 01CL in the Stacks Project.

Stacks.SheafOfModules.isLocallyFree_symmetricAlgebraSheaf_of_isLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocallyFreeAlgebras.lean, line 147. The attribute's comment: “the symmetric algebra of a locally free module sheaf is locally free”. References: SGA 3 XXII (5.3.0), “partial”.

The symmetric algebra of a locally free sheaf of modules is locally free. The covering family is the one that trivialises F; no degree needs a smaller object of the site, because Stacks.SheafOfModules.symmetricPowerOverFreeIsoOfIsoFree trivialises every degree over that same object.

theorem isLocallyFree_symmetricAlgebraSheaf_of_isLocallyFree :
    A.symmetricAlgebraSheaf.IsLocallyFree

Stacks.SheafOfModules.isLocallyFree_exteriorAlgebraSheaf_of_isLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocallyFreeAlgebras.lean, line 162. The attribute's comment: “the exterior algebra of a locally free module sheaf is locally free”.

The exterior algebra of a locally free sheaf of modules is locally free. The covering family is the one that trivialises F, and Stacks.SheafOfModules.exteriorPowerOverFreeIsoOfIsoFree trivialises every degree over the same object of the site.

theorem isLocallyFree_exteriorAlgebraSheaf_of_isLocallyFree :
    A.exteriorAlgebraSheaf.IsLocallyFree

Stacks.SheafOfModules.isLocallyFree_tensorAlgebraSheaf_of_isLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocallyFreeAlgebras.lean, line 178. The attribute's comment: “the tensor algebra of a locally free module sheaf is locally free”.

The tensor algebra of a locally free sheaf of modules is locally free. The covering family is the one that trivialises F, and Stacks.SheafOfModules.exists_nonempty_iso_free_tensorPowerOver trivialises every degree over the same object of the site.

theorem isLocallyFree_tensorAlgebraSheaf_of_isLocallyFree :
    A.tensorAlgebraSheaf.IsLocallyFree

Stacks.SheafOfModules.isQuasicoherent_symmetricAlgebraSheaf_of_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/QuasicoherentAlgebras.lean, line 779. The attribute's comment: “the symmetric algebra of a quasi-coherent module sheaf is quasi-coherent”.

The symmetric algebra of a quasi-coherent sheaf of modules on a ringed space is quasi-coherent. The covering family is the one that presents F; no degree needs a smaller open, because Stacks.SheafOfModules.nonempty_presentation_symmetricPower_over presents every degree over that same open.

theorem isQuasicoherent_symmetricAlgebraSheaf_of_isQuasicoherent :
    A.symmetricAlgebraSheaf.IsQuasicoherent

Stacks.SheafOfModules.isQuasicoherent_exteriorAlgebraSheaf_of_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/QuasicoherentAlgebras.lean, line 788. The attribute's comment: “the exterior algebra of a quasi-coherent module sheaf is quasi-coherent”.

The exterior algebra of a quasi-coherent sheaf of modules on a ringed space is quasi-coherent.

theorem isQuasicoherent_exteriorAlgebraSheaf_of_isQuasicoherent :
    A.exteriorAlgebraSheaf.IsQuasicoherent

Stacks.SheafOfModules.isQuasicoherent_tensorAlgebraSheaf_of_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorPowerPresentation.lean, line 569. The attribute's comment: “the tensor algebra of a quasi-coherent module sheaf is quasi-coherent”.

The tensor algebra of a quasi-coherent sheaf of modules on a ringed space is quasi-coherent. This is the tensor assertion of Stacks Tag 01CL. The covering family is the one that presents F; no degree needs a smaller open, because Stacks.SheafOfModules.nonempty_presentation_tensorPower_over presents every degree over that same open.

theorem isQuasicoherent_tensorAlgebraSheaf_of_isQuasicoherent
    {X : AlgebraicGeometry.RingedSpace.{t, t}}
    (F : _root_.SheafOfModules.{t} (structureSheafRing X)) [F.IsQuasicoherent]
    (A : _root_.SheafOfModules.TensorExteriorSymmetricAlgebras
      (Opens.grothendieckTopology X.carrier) F) :
    A.tensorAlgebraSheaf.IsQuasicoherent

Sources

• Section 17.21, Tag 01CF
• AxiomMath/Stacks at 5ed82d14

LeanSheafOfModules.ringedSpaceAlgebras · SheafOfModules.exteriorPower_isSheafification · SheafOfModules.symmetricPower_isSheafification · SheafOfModules.symmetricAlgebra_stalk · PresheafOfModules.extPowStalkEquivOfStalkIso · SheafOfModules.exteriorAlgebra_stalk · SheafOfModules.symmetricPower_stalk · SheafOfModules.tensorPower_stalk

Section17.22 Internal Hom#

Section 17.22 of the Stacks Project, Tag 01CM. 8 tags here are carried by 24 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01CN, a lemma

Tag 01CN in the Stacks Project.

Stacks.SheafOfModules.internalHomTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/TensorAndDuals/InternalHom.lean, line 212. The attribute's comment: “canonical isomorphism”.

The sheaf-hom out of a tensor product is canonically the corresponding iterated sheaf-hom: ℋom(F ⊗ G, H) ≅ ℋom(F, ℋom(G, H)).

noncomputable def internalHomTensorIso
    (F G H : _root_.SheafOfModules.{u} (structureSheafRing X)) :
    sheafHomSpace X (((Tensor.sheafTensor ⟨X.presheaf, X.IsSheaf⟩).obj F).obj G) H ≅
      sheafHomSpace X F (sheafHomSpace X G H)

Stacks.SheafOfModules.internalHomTensorIso_hom_app_tmul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/TensorAndDuals/InternalHom.lean, line 228. The attribute's comment: “canonical characterization”.

The canonical sheaf-hom isomorphism is currying: on every open, its evaluation on two local sections agrees with evaluation on their pure tensor.

theorem internalHomTensorIso_hom_app_tmul
    (U : Opens X.carrier)
    (s : (sheafHomSpace X
      (((Tensor.sheafTensor ⟨X.presheaf, X.IsSheaf⟩).obj F).obj G) H).val.obj (op U))
    (f : F.val.obj (op U)) (g : G.val.obj (op U)) :
    evalNestedInternalHomSection X U
        ((internalHomTensorIso X F G H).hom.val.app (op U) s) f g =
      evalTensorHomSection X U s f g

Stacks.SheafOfModules.tensorHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/TensorAndDuals/InternalHom.lean, line 251. The attribute's comment: “morphism equivalence”.

Giving a morphism F ⊗ G ⟶ H is canonically equivalent to giving a morphism F ⟶ ℋom(G, H).

noncomputable def tensorHomEquiv
    (F G H : _root_.SheafOfModules.{u} (structureSheafRing X)) :
    (((Tensor.sheafTensor ⟨X.presheaf, X.IsSheaf⟩).obj F).obj G ⟶ H) ≃ (F ⟶ sheafHomSpace X G H)

Stacks.SheafOfModules.tensorHomEquiv_isTensorCurry, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/TensorAndDuals/InternalHom.lean, line 264. The attribute's comment: “morphism equivalence characterization”.

The forward direction of tensorHomEquiv is the canonical currying map.

theorem tensorHomEquiv_isTensorCurry
    (t : ((Tensor.sheafTensor ⟨X.presheaf, X.IsSheaf⟩).obj F).obj G ⟶ H) :
    IsTensorCurry X t (tensorHomEquiv X F G H t)

Stacks.SheafOfModules.internalHomTensorIso_natural_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/TensorAndDuals/InternalHom.lean, line 359. The attribute's comment: “functoriality in the first entry”.

The canonical isomorphism commutes with precomposition in its first argument.

theorem internalHomTensorIso_natural_left
    {F' : _root_.SheafOfModules.{u} (structureSheafRing X)} (f : F' ⟶ F) :
    (internalHomTensorIso X F G H).hom ≫ sheafHomMapLeft X f =
      sheafHomMapLeft X ((Functor.uncurry.obj (Tensor.sheafTensor ⟨X.presheaf, X.IsSheaf⟩)).map
        ((f, 𝟙 G) : (_, _) ⟶ (_, _))) ≫
        (internalHomTensorIso X F' G H).hom

Stacks.SheafOfModules.internalHomTensorIso_natural_middle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/TensorAndDuals/InternalHom.lean, line 371. The attribute's comment: “functoriality in the second entry”.

The canonical isomorphism commutes with precomposition in its second argument.

theorem internalHomTensorIso_natural_middle
    {G' : _root_.SheafOfModules.{u} (structureSheafRing X)} (g : G' ⟶ G) :
    (internalHomTensorIso X F G H).hom ≫ sheafHomMapRight X (sheafHomMapLeft X g) =
      sheafHomMapLeft X ((Functor.uncurry.obj (Tensor.sheafTensor ⟨X.presheaf, X.IsSheaf⟩)).map
        ((𝟙 F, g) : (_, _) ⟶ (_, _))) ≫
        (internalHomTensorIso X F G' H).hom

Stacks.SheafOfModules.internalHomTensorIso_natural_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/TensorAndDuals/InternalHom.lean, line 383. The attribute's comment: “functoriality in the third entry”.

The canonical isomorphism commutes with postcomposition in its target.

theorem internalHomTensorIso_natural_right
    {H' : _root_.SheafOfModules.{u} (structureSheafRing X)} (h : H ⟶ H') :
    sheafHomMapRight X h ≫ (internalHomTensorIso X F G H').hom =
      (internalHomTensorIso X F G H).hom ≫ sheafHomMapRight X (sheafHomMapRight X h)

Declarations registered for the tag:

• Stacks.SheafOfModules.internalHomTensorIso, declared in the repository, registered with add_to_stacks in StacksFrontier/Topology/Sheaves/Modules/TensorAndDuals/InternalHom.lean, line 399 (StacksFrontier): “canonical_iso”.
• Stacks.SheafOfModules.tensorHomEquiv, declared in the repository, registered with add_to_stacks in StacksFrontier/Topology/Sheaves/Modules/TensorAndDuals/InternalHom.lean, line 400 (StacksFrontier): “in_particular”.

Tag 01CO, a lemma

Tag 01CO in the Stacks Project.

sheafHom_leftExact_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SheafHomLeftExact.lean, line 353. The attribute's comment: “(1)”. References: EGA 0 (4.1.5), “special case”; EGA 0 (6.7.6), “partial”; SGA 4 IV (12.2), “partial”.

Left exactness of SheafHom in the first argument. Given an exact sequence F₂ --α--> F₁ --β--> F → 0 of O_X-modules (encoded as the exact ComposableArrows F₂ → F₁ → F → 0, whose final node forces β epi), and internal homs SheafHom(F,G), SheafHom(F₁,G), SheafHom(F₂,G) with induced precomposition maps β* = mβ, α* = mα (morphisms of O_X-modules), the induced sequence of O_X-modules 0 → SheafHom(F, G) --β*--> SheafHom(F₁, G) --α*--> SheafHom(F₂, G) is exact in SheafOfModules R (β* is mono and im β* = ker α*).

theorem sheafHom_leftExact_fst
    (F₂ F₁ F G : SheafOfModules.{v} (structureSheaf Rc)) (α : F₂ ⟶ F₁) (β : F₁ ⟶ F)
    (hin : (ComposableArrows.mk₃ α β (0 : F ⟶ 0)).Exact)
    (HF : SheafHom Rc F G) (HF₁ : SheafHom Rc F₁ G) (HF₂ : SheafHom Rc F₂ G)
    (mβ : HF.obj ⟶ HF₁.obj) (mα : HF₁.obj ⟶ HF₂.obj)
    (hmβ : SheafHom.IsPrecomp Rc β HF HF₁ mβ) (hmα : SheafHom.IsPrecomp Rc α HF₁ HF₂ mα) :
    (ComposableArrows.mk₃
      (0 : (0 : SheafOfModules.{v} (structureSheaf Rc)) ⟶ HF.obj) mβ mα).Exact

sheafHom_leftExact_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SheafHomLeftExact.lean, line 416. The attribute's comment: “(2)”. References: EGA 0 (4.1.5), “special case”; SGA 4 IV (12.2), “partial”; SGA 4 V (6.0), “6.0, special case”.

Left exactness of SheafHom in the second argument. Given an exact sequence 0 → G --u--> G₁ --v--> G₂ of O_X-modules (encoded as the exact ComposableArrows 0 → G → G₁ → G₂, whose first node forces u mono), and internal homs SheafHom(F,G), SheafHom(F,G₁), SheafHom(F,G₂) with induced postcomposition maps u_* = mu, v_* = mv (morphisms of O_X-modules), the induced sequence of O_X-modules 0 → SheafHom(F, G) --u_*--> SheafHom(F, G₁) --v_*--> SheafHom(F, G₂) is exact in SheafOfModules R (u_* is mono and im u_* = ker v_*).

theorem sheafHom_leftExact_snd
    (F G G₁ G₂ : SheafOfModules.{v} (structureSheaf Rc)) (u : G ⟶ G₁) (v : G₁ ⟶ G₂)
    (hin : (ComposableArrows.mk₃
      (0 : (0 : SheafOfModules.{v} (structureSheaf Rc)) ⟶ G) u v).Exact)
    (HG : SheafHom Rc F G) (HG₁ : SheafHom Rc F G₁) (HG₂ : SheafHom Rc F G₂)
    (mu : HG.obj ⟶ HG₁.obj) (mv : HG₁.obj ⟶ HG₂.obj)
    (hmu : SheafHom.IsPostcomp Rc u HG HG₁ mu) (hmv : SheafHom.IsPostcomp Rc v HG₁ HG₂ mv) :
    (ComposableArrows.mk₃
      (0 : (0 : SheafOfModules.{v} (structureSheaf Rc)) ⟶ HG.obj) mu mv).Exact

Tag 0A6F, a lemma

Tag 0A6F in the Stacks Project.

RingedSpaceModuleAdjunction.homSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Functors/Module/HomSheaf.lean, line 424. The attribute's comment: “the internal Hom sheaf, as a functor to modules over the target ring”.

The functor SheafHom_{𝒪₁}(𝒪₂, -) from 𝒪₁-modules to 𝒪₂-modules. On underlying presheaves it is the coextension of scalars Stacks.PresheafOfModules.CoextendScalars.coextFunMap.

noncomputable def homSheaf
    {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
    {𝒪₁ 𝒪₂ : CategoryTheory.Sheaf J RingCat.{u}}
    (α : 𝒪₁ ⟶ 𝒪₂) : SheafOfModules.{u} 𝒪₁ ⥤ SheafOfModules.{u} 𝒪₂

RingedSpaceModuleAdjunction.restrictScalarsHomAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Functors/Module/HomSheaf.lean, line 438. The attribute's comment: “the bifunctorial Hom identification”. References: SGA 4 IV (14.5), “adjunction i_* ⊣ i^!”.

Restriction of scalars along a homomorphism of sheaves of rings is left adjoint to the internal-Hom functor SheafHom_{𝒪₁}(𝒪₂, -).

noncomputable def restrictScalarsHomAdjunction
    {C : Type u} [Category.{u} C] {J : GrothendieckTopology C}
    {𝒪₁ 𝒪₂ : CategoryTheory.Sheaf J RingCat.{u}}
    (α : 𝒪₁ ⟶ 𝒪₂) :
    SheafOfModules.restrictScalars.{u} α ⊣ homSheaf α

Tag 01CP, a lemma

Tag 01CP in the Stacks Project.

Stacks.SheafOfModules.SheafHomStalk.injective_sheafHomStalkLinearMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SheafHomStalk.lean, line 903. The attribute's comment: “finite_type_injective”. References: EGA 0 (5.2.6), “partial”.

Injectivity half of Stacks 01CP. For F of finite type the canonical map from the stalk of the internal hom to the module of homomorphisms of the stalks is injective. Only local generation by finitely many sections is used, which is exactly LocalGenerators; the relations of a LocalPresentation are needed only for surjectivity.

This is injective_sheafHomStalkLinearMap_of_localGenerators, whose hypothesis is only that F has local generators at x, applied to the generators that finite type produces there.

theorem injective_sheafHomStalkLinearMap (H : SheafHom Rc F G) (x : X)
    [F.IsFiniteType] : Function.Injective (sheafHomStalkLinearMap H x)

Stacks.SheafOfModules.SheafHomStalk.sheafHomStalkLinearEquivOfFinitePresentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SheafHomStalk.lean, line 1130. The attribute's comment: “finite_presentation_isomorphism”.

Stacks Project, Tag 01CP. If F is of finite presentation, the canonical map from the stalk of SheafHom(F, G) at x to the module of O_{X,x}-linear maps from F_x to G_x is an isomorphism. The equivalence produced here is the canonical map sheafHomStalkLinearMap H x: its germ_apply field records that it sends the germ of a local homomorphism and the germ of a local section to the germ of the evaluation, and by sheafHomStalkLinearMap_unique that property determines it.

noncomputable def sheafHomStalkLinearEquivOfFinitePresentation
    (H : SheafHom Rc F G) (x : X) [F.IsFinitePresentation] :
    SheafHomStalkLinearEquiv Rc F G H x

Tag 0C6I, a lemma

Tag 0C6I in the Stacks Project.

Stacks.SheafHomPullback.pullbackSheafHomComparison_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/Recovery17/PullbackInternalHom.lean, line 814.

Stacks Project, Tag 0C6I. Let f : X ⟶ Y be a flat morphism of ringed spaces. If F is a finitely presented 𝒪_Y-module, then the canonical map f^* SheafHom(F, G) ⟶ SheafHom(f^*F, f^*G) is an isomorphism.

theorem pullbackSheafHomComparison_isIso
    {X Y : RingedSpace.{u, u}} (f : X ⟶ Y)
    (hf : AlgebraicGeometry.IsFlat f)
    (F G : SheafOfModules.{u} (structureSheafRing Y)) [F.IsFinitePresentation]
    (H : SheafHom Y.sheaf F G)
    (H' : SheafHom X.sheaf ((modulePullback f).obj F)
      ((modulePullback f).obj G))
    (comparison : PullbackSheafHomComparison f F G H H') :
    IsIso (pullbackSheafHomComparison f F G H H' comparison)

Tag 01CQ, a lemma

Tag 01CQ in the Stacks Project.

Stacks.SheafOfModules.sheafHom_locallyKernelFiniteCoproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SheafHomSlice.lean, line 732. The attribute's comment: “local kernel presentation”.

The internal hom out of a finitely presented module is locally the kernel of a map between finite direct sums of copies of the target.

theorem sheafHom_locallyKernelFiniteCoproduct [F.IsFinitePresentation] :
    ∀ x : X, ∃ U : Opens X, x ∈ U ∧ ∃ m n : ℕ,
      ∃ f : (∐ fun _ : Fin m => G.over U) ⟶ (∐ fun _ : Fin n => G.over U),
        Nonempty ((sheafHom 𝒪 h𝒪 F G).over U ≅ kernel f)

Stacks.SheafOfModules.sheafHom_isCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SheafHomSlice.lean, line 759. The attribute's comment: “coherence of internal Hom”.

The internal hom out of a finitely presented module into a coherent module is coherent.

theorem sheafHom_isCoherent [F.IsFinitePresentation] [IsCoherent G] :
    IsCoherent (sheafHom 𝒪 h𝒪 F G)

Stacks.SheafOfModules.InternalHom.exists_locally_isoKernel_sheafInternalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InternalHomCoherent/LocalKernel.lean, line 284. The attribute's comment: “local kernel presentation”.

The first clause of [Stacks, Tag 01CQ]. Let (Y, 𝒪_Y) be a ringed space and let F, G be 𝒪_Y-modules with F of finite presentation. Then SheafHom(F, G) is locally a kernel of a map between finite direct sums of copies of G: every point of Y has an open neighbourhood U for which SheafHom(F, G)|_U is the kernel of a morphism ∐_{i < m} G|_U ⟶ ∐_{j < n} G|_U.

theorem exists_locally_isoKernel_sheafInternalHom
    (F G : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf (spaceRingedSite O).O))
    [F.IsFinitePresentation] (y : Y) :
    ∃ U : Opens Y, y ∈ U ∧ ∃ (m n : ℕ)
      (f : (∐ fun _ : Fin m => G.over U) ⟶ (∐ fun _ : Fin n => G.over U)),
      Nonempty ((sheafInternalHom (spaceRingedSite O) F G).over U ≅ kernel f)

Stacks.SheafOfModules.InternalHom.isCoherent_sheafInternalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InternalHomCoherent/LocalKernel.lean, line 306. The attribute's comment: “coherence of internal Hom”.

The second clause of [Stacks, Tag 01CQ]. On a ringed space, the internal Hom from a module of finite presentation into a coherent module is coherent. This combines the first clause with the gluing step Stacks.SheafOfModules.isCoherent_of_locallyKernelFiniteCoproduct.

The coherence predicate here is the one of StacksFrontier/Algebra/Category/ModuleCat/Sheaf/Coherent.lean; for the one of Stacks Tag 01BW see isCoherent_sheafInternalHom', which is the same statement and is deliberately left untagged so that the tag is not counted twice.

theorem isCoherent_sheafInternalHom
    (F G : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf (spaceRingedSite O).O))
    [F.IsFinitePresentation] [Stacks.SheafOfModules.IsCoherent G] :
    Stacks.SheafOfModules.IsCoherent
      (sheafInternalHom (spaceRingedSite O) F G)

Stacks.AlgebraicGeometry.InternalHomLocalKernel.sheafHom_locallyKernelFiniteCoproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InternalHomLocalKernel/Basic.lean, line 375. The attribute's comment: “local kernel presentation”.

Stacks 01CQ, first assertion, for a ringed space. A sheaf Hom from a finitely presented module is locally the kernel of a map between finite direct sums of copies of the target.

theorem sheafHom_locallyKernelFiniteCoproduct
    (F G : _root_.SheafOfModules.{u}
      (structureSheafRing X))
    [F.IsFinitePresentation] :
    ∀ x : X.carrier, ∃ U : Opens X.carrier, x ∈ U ∧
      ∃ m n : ℕ,
        ∃ f : (∐ (fun _ : Fin m => G.over U)) ⟶ (∐ (fun _ : Fin n => G.over U)),
          Nonempty ((_root_.Stacks.SheafOfModules.sheafHom X.presheaf
              (structureSheafRing X).property F G).over
                U ≅
            (kernel f :
              _root_.SheafOfModules.{u}
                ((structureSheafRing X).over U)))

Stacks.AlgebraicGeometry.InternalHomLocalKernel.sheafHom_isCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InternalHomLocalKernel/Basic.lean, line 395. The attribute's comment: “coherence of internal Hom”.

Stacks 01CQ, second assertion, for a ringed space. Internal Hom from a finitely presented module into a coherent module is coherent.

theorem sheafHom_isCoherent
    (F G : _root_.SheafOfModules.{u}
      (structureSheafRing X))
    [F.IsFinitePresentation] [G.IsCoherent] :
    (_root_.Stacks.SheafOfModules.sheafHom X.presheaf
      (structureSheafRing X).property F G).IsCoherent

Tag 0GMV, a lemma

Tag 0GMV in the Stacks Project.

Stacks.SheafOfModules.isColimit_sheafHomCocone, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SheafHomFilteredColimit.lean, line 170.

Stacks Project, Tag 0GMV. Let F be an O_X-module of finite presentation on a ringed space and let G = colim_λ G_λ be a filtered colimit of O_X-modules. Then the canonical cocone of internal homs over SheafHom_{O_X}(F, G), whose legs are the postcomposition maps induced by the colimit inclusions, is a colimit cocone; that is, the canonical map colim_λ SheafHom_{O_X}(F, G_λ) ⟶ SheafHom_{O_X}(F, G) is an isomorphism.

noncomputable def isColimit_sheafHomCocone [F.IsFinitePresentation] [IsFiltered K]
    (c : Cocone D) (hc : IsColimit c)
    (H : ∀ j, SheafHom Rc F (D.obj j)) (Hc : SheafHom Rc F c.pt) :
    IsColimit (sheafHomCocone F D c H Hc)

Stacks.SheafOfModules.isIso_desc_sheafHomCocone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SheafHomFilteredColimit.lean, line 196.

Stacks Project, Tag 0GMV, in comparison-map form: for F of finite presentation and a filtered diagram, the canonical map from any colimit of the internal homs SheafHom_{O_X}(F, G_λ) to SheafHom_{O_X}(F, colim_λ G_λ) is an isomorphism.

theorem isIso_desc_sheafHomCocone [F.IsFinitePresentation] [IsFiltered K]
    (c : Cocone D) (hc : IsColimit c)
    (H : ∀ j, SheafHom Rc F (D.obj j)) (Hc : SheafHom Rc F c.pt)
    (t : Cocone (sheafHomDiagram F D H)) (ht : IsColimit t) :
    IsIso (ht.desc (sheafHomCocone F D c H Hc))

Tag 01BS, a lemma

Tag 01BS in the Stacks Project.

Stacks.SheafOfModules.preservesColimitsOfShape_coyoneda_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SheafHomFilteredColimitSections.lean, line 120.

Stacks Project, Tag 01BS. Let X be a ringed space with a cofinal system of open coverings X = ⋃_{j ∈ J} U_j with J finite and all U_j ∩ U_j' quasi-compact, let F be an O_X-module of finite presentation and let λ ↦ G_λ be a filtered system of O_X-modules. Then

colim_λ Hom_X(F, G_λ) = Hom_X(F, colim_λ G_λ);

here in the form that Hom_X(F, -) preserves colimits of the given filtered shape, which says exactly that the canonical comparison map out of any colimit of the Hom_X(F, G_λ) is an isomorphism.

theorem preservesColimitsOfShape_coyoneda_of_isFinitePresentation
    (F : _root_.SheafOfModules.{u} (structureSheaf Rc)) [F.IsFinitePresentation]
    (K : Type u) [Category.{u} K] [IsFiltered K]
    (hX : DirectedColimitOfSheaves.HasFiniteCompactCofinalCovers (X := X) ⊤) :
    PreservesColimitsOfShape K (coyoneda.obj (op F))

Stacks.SheafOfModules.isIso_colimitPost_coyoneda_of_hasFiniteCompactCofinalCovers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SheafHomFilteredColimitSections.lean, line 146.

Stacks Project, Tag 01BS as the source displays it. The canonical comparison map

colim_λ Hom_X(F, G_λ) ⟶ Hom_X(F, colim_λ G_λ)

is an isomorphism of types, for F an O_X-module of finite presentation and G a filtered system of O_X-modules on a ringed space with a cofinal system of finite open coverings having quasi-compact pairwise intersections.

theorem isIso_colimitPost_coyoneda_of_hasFiniteCompactCofinalCovers
    (F : _root_.SheafOfModules.{u} (structureSheaf Rc)) [F.IsFinitePresentation]
    {K : Type u} [Category.{u} K] [IsFiltered K]
    (G : K ⥤ _root_.SheafOfModules.{u} (structureSheaf Rc))
    (hX : DirectedColimitOfSheaves.HasFiniteCompactCofinalCovers (X := X) ⊤) :
    IsIso (colimit.post G (coyoneda.obj (op F)))

Sources

• Section 17.22, Tag 01CM
• AxiomMath/Stacks at 5ed82d14

LeanStacks.SheafOfModules.internalHomTensorIso · Stacks.SheafOfModules.internalHomTensorIso_hom_app_tmul · Stacks.SheafOfModules.tensorHomEquiv · Stacks.SheafOfModules.tensorHomEquiv_isTensorCurry · Stacks.SheafOfModules.internalHomTensorIso_natural_left · Stacks.SheafOfModules.internalHomTensorIso_natural_middle · Stacks.SheafOfModules.internalHomTensorIso_natural_right · sheafHom_leftExact_fst

Section17.23 The annihilator of a sheaf of modules#

Section 17.23 of the Stacks Project, Tag 0H2G. 5 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0H2H, a definition

Tag 0H2H in the Stacks Project.

Stacks.SheafOfModules.annihilatorSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/InvertibleAndOperators/Annihilator.lean, line 125. References: EGA 0 (5.3.7), “annihilator def”.

Stacks Project, Tag 0H2H. The annihilator of an 𝒪_X-module F is the subsheaf of 𝒪_X consisting of the local functions that act as zero on F. Equivalently, it is the kernel of the canonical map from 𝒪_X to the internal endomorphism sheaf of F.

noncomputable def annihilatorSheaf :
    (SheafOfModules.unit (structureSheafRing X)).Submodule

Tag 0H2I, an equation

Tag 0H2I in the Stacks Project.

Stacks.SheafOfModules.stalk_annihilatorSheaf_le_annihilator_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/InvertibleAndOperators/Annihilator.lean, line 257.

Stacks Project, Tag 0H2I. The germs of local sections of the annihilator sheaf at x annihilate the stalk Fₓ.

theorem stalk_annihilatorSheaf_le_annihilator_stalk (x : X) :
    { a : (show X.carrier.Presheaf RingCat from (structureSheafRing X).obj).stalk x |
      ∃ (U : Opens X.carrier) (hx : x ∈ U) (r : (structureSheafRing X).obj.obj (op U)),
        r ∈ (annihilatorSheaf X F).toSubmodule.obj (op U) ∧
          (show X.carrier.Presheaf RingCat from (structureSheafRing X).obj).germ U x hx r = a } ⊆
      Module.annihilator
        ((show X.carrier.Presheaf RingCat from (structureSheafRing X).obj).stalk x)
        ((show X.carrier.Presheaf Ab.{u} from F.val.presheaf).stalk x)

Tag 0H2J, a lemma

Tag 0H2J in the Stacks Project.

Stacks.SheafOfModules.annihilatorSheaf_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/InvertibleAndOperators/AnnihilatorStalk.lean, line 189.

Stacks Project, Tag 0H2J. For F of finite type, the germs at x of the local sections of the annihilator sheaf of F are exactly the elements of the local ring O_{X,x} that annihilate the stalk F_x.

theorem annihilatorSheaf_stalk [F.IsFiniteType] (x : X) :
    {r : TopCat.Presheaf.stalk (C := CommRingCat.{u}) X.sheaf.obj x |
      ∃ (U : Opens X) (hx : x ∈ U) (s : (structureSheafRing X).obj.obj (op U)),
        s ∈ (annihilatorSheaf X F).toSubmodule.obj (op U) ∧
          TopCat.Presheaf.germ (C := CommRingCat.{u}) X.sheaf.obj U x hx s = r} =
      (Module.annihilator
        (TopCat.Presheaf.stalk (C := CommRingCat.{u}) X.sheaf.obj x)
        (TopCat.Presheaf.stalk (C := Ab.{u})
          (show PresheafOfModules.{u}
              (X.sheaf.obj ⋙ forget₂ CommRingCat RingCat) from F.val).presheaf x) :
          Set (TopCat.Presheaf.stalk (C := CommRingCat.{u}) X.sheaf.obj x))

Tag 0H2K, a lemma

Tag 0H2K in the Stacks Project.

Stacks.SheafOfModules.quotientRingSheafModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/InvertibleAndOperators/AnnihilatorQuotient.lean, line 184. The attribute's comment: “the descended module structure”.

Stacks Project, Tag 0H2K. The canonical 𝒪_X/I-module structure on a sheaf of modules annihilated by the ideal subsheaf I: its underlying presheaf of abelian groups is that of F, and a local section of 𝒪_X/I acts through any local lift of it to 𝒪_X.

noncomputable def quotientRingSheafModule (hI : I ≤ annihilatorSheaf X F) :
    SheafOfModules.{v} (quotientRingSheaf X I).sheaf

Stacks.SheafOfModules.quotientRingSheafModule_restrictScalars, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/InvertibleAndOperators/AnnihilatorQuotient.lean, line 236. The attribute's comment: “compatibility with the given action”.

Stacks Project, Tag 0H2K. The descended action is compatible with the given one: restricting scalars along the quotient map returns F.

theorem quotientRingSheafModule_restrictScalars (hI : I ≤ annihilatorSheaf X F) :
    (SheafOfModules.restrictScalars (quotientRingSheaf X I).quotientMap).obj
      (quotientRingSheafModule X I F hI) = F

Stacks.SheafOfModules.quotientRingSheafModule_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/InvertibleAndOperators/AnnihilatorQuotient.lean, line 251. The attribute's comment: “uniqueness of the descended action”.

Stacks Project, Tag 0H2K. The descended action is the only 𝒪_X/I-action whose restriction of scalars along the quotient map is the given 𝒪_X-action.

theorem quotientRingSheafModule_unique (hI : I ≤ annihilatorSheaf X F)
    (G : SheafOfModules.{v} (quotientRingSheaf X I).sheaf)
    (hG : (SheafOfModules.restrictScalars (quotientRingSheaf X I).quotientMap).obj G = F) :
    G = quotientRingSheafModule X I F hI

Stacks.SheafOfModules.quotientRingSheafModule_stalk_smul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/InvertibleAndOperators/AnnihilatorQuotient.lean, line 393. The attribute's comment: “the action on stalks”.

Stacks Project, Tag 0H2K. On stalks the descended action is the ordinary action of the quotient ring 𝒪_{X,x}/I_x on the stalk F_x, which the stalk of I annihilates: the class of a germ r acts on F_x exactly as r itself.

theorem quotientRingSheafModule_stalk_smul (F : SheafOfModules.{u} (structureSheafRing X))
    (hI : I ≤ annihilatorSheaf X F) (x : X.carrier)
    (r : TopCat.Presheaf.stalk (C := RingCat) (structureSheafRing X).obj x)
    (m : TopCat.Presheaf.stalk (C := Ab.{u}) F.val.presheaf x) :
    quotientStalkSMul X I F hI x
        (quotientRingSheafStalkIdealEquiv X I x
          (Ideal.Quotient.mk (idealSheafStalk X I x) r)) m = r • m

Tag 0H2L, a lemma

Tag 0H2L in the Stacks Project.

Stacks.SheafOfModules.isCoherent_annihilatorSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/InvertibleAndOperators/AnnihilatorCoherent.lean, line 75.

Stacks Project, Tag 0H2L. If the structure sheaf of a ringed space and an 𝒪_X-module F are coherent, then the annihilator of F is coherent.

theorem isCoherent_annihilatorSheaf (F : SheafOfModules.{u} (structureSheafRing X))
    [IsCoherent (SheafOfModules.unit (structureSheafRing X))] [IsCoherent F] :
    IsCoherent (annihilatorSheaf X F).toSheafOfModules

Sources

• Section 17.23, Tag 0H2G
• AxiomMath/Stacks at 5ed82d14

LeanStacks.SheafOfModules.annihilatorSheaf · Stacks.SheafOfModules.stalk_annihilatorSheaf_le_annihilator_stalk · Stacks.SheafOfModules.annihilatorSheaf_stalk · Stacks.SheafOfModules.quotientRingSheafModule · Stacks.SheafOfModules.quotientRingSheafModule_restrictScalars · Stacks.SheafOfModules.quotientRingSheafModule_unique · Stacks.SheafOfModules.quotientRingSheafModule_stalk_smul · Stacks.SheafOfModules.isCoherent_annihilatorSheaf

Section17.24 Koszul complexes#

Section 17.24 of the Stacks Project, Tag 062J. 2 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 062K, a definition

Tag 062K in the Stacks Project.

SheafOfModules.koszulDifferentialGradedAlgebra, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Koszul/Sheaf/DifferentialGradedAlgebra.lean, line 193. References: SGA 3 III (4.6.1), “Koszul complex”.

The Koszul complex K_•(φ) of an O-module map φ : F → O, as a sheaf of differential graded algebras. This is Stacks tag 062K. Its underlying graded algebra is the exterior algebra ⋀(F) of Section 17.21, read with the grading negated because the complex of a sheaf of differential graded algebras is a cochain complex while the Koszul differential lowers the exterior degree; that is SheafOfModules.koszulDifferentialGradedAlgebra_toGradedAlgebra, and ⋀(F) has the universal property of the exterior algebra on F by SheafOfModules.isExteriorAlgebra_sheafifiedExteriorAlgebra, which is item (1) of the tag. Its differential is the Koszul differential of φ, which is the unique graded derivation of ⋀(F) taking a degree-one local section e to φ(e) (SheafOfModules.existsUnique_koszulDerivation), which is item (2). The tag calls the result a commutative differential graded algebra; SheafOfModules.DifferentialGradedAlgebra is Stacks tag 0FRF's notion and carries no commutativity axiom, and graded commutativity of ⋀(F) is SheafOfModules.sheafifiedExteriorMul_comm.

SheafOfModules.ringedSpaceKoszulDifferentialGradedAlgebra is the specialization to a ringed space, which is the generality the tag is stated in.

noncomputable def koszulDifferentialGradedAlgebra :
    DifferentialGradedAlgebra.{w, w} (toRingCat J Osharp)

Tag 062L, a definition

Tag 062L in the Stacks Project.

PresheafOfModules.seqExteriorFunctional, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Koszul/Sheaf/Sequence.lean, line 167. The attribute's comment: “the morphism (f₁, …, f_r) : O^{⊕ r} → O the Koszul complex is attached to, not the complex itself”.

The functional (f₁, …, f_r) : O^{⊕ r} → O. Over each object it is the ring-level Koszul.seqDual of the family of sections restricted there.

noncomputable def seqExteriorFunctional {r : ℕ} (f : Sequence O r) :
    ExteriorFunctional.{v, u, w, w} (finFree O r)

Stacks.AlgebraicGeometry.SeqKoszul.sheafComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Koszul/Sheaf/SheafCondition.lean, line 192. The attribute's comment: “the complex K_•(O_X, f₁, …, f_r) itself, on a ringed space and as a chain complex of sheaves of modules”. References: EGA III (1.1.1), “more general”; SGA 3 III (4.6.1), “more general”; SGA 6 VII (1.1), “special case”.

K_•(O_X, f₁, …, f_r) as a chain complex of sheaves of modules. In degree n it is the sheaf of exterior powers U ↦ ⋀^n_{O_X(U)}(O_X(U)^r) and the differential is contraction by (f₁, …, f_r). This is the complex whose acyclicity in positive degrees is Koszul-regularity of the family, in the sense of Stacks tag 063D.

noncomputable def sheafComplex : ChainComplex (SheafOfModules.{u} (ringSheaf X)) ℕ

Sources

• Section 17.24, Tag 062J
• AxiomMath/Stacks at 5ed82d14

LeanSheafOfModules.koszulDifferentialGradedAlgebra · PresheafOfModules.seqExteriorFunctional · Stacks.AlgebraicGeometry.SeqKoszul.sheafComplex

Section17.25 Invertible modules#

Section 17.25 of the Stacks Project, Tag 01CR. 11 tags here are carried by 78 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01CS, a definition

Tag 01CS in the Stacks Project.

Stacks.SheafOfModules.IsInvertible, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorInvertible.lean, line 130. The attribute's comment: “invertible”.

Stacks Project, Tag 01CS, equivalently Tag 0409 (2). A sheaf of O-modules is invertible when its tensor functor is an equivalence. The universal property specifies that tensor functor independently of any chosen construction of sheafification, hence on every site; so the ringed-space form of the definition and the ringed-site form coincide here.

class IsInvertible
    (L : SheafOfModules.{w} (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO)) : Prop

AlgebraicGeometry.SheafOfModules.IsTrivial, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/Invertible.lean, line 137. The attribute's comment: “trivial”.

An O-module sheaf is trivial when it is isomorphic, as an O-module, to O itself.

noncomputable abbrev IsTrivial
    (L : _root_.SheafOfModules.{w} (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO))
      : Prop

Tag 0B8K, a lemma

Tag 0B8K in the Stacks Project.

Stacks.SheafOfModules.Invertible.tensorInverseIsoDualSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InvertibleDualEvaluation.lean, line 307. The attribute's comment: “the tensor inverse is the dual”. References: SGA 6 VIII (3.5), “partial”.

Stacks Project, Tag 0B8N (c). A sheaf of 𝒪-modules N whose tensor product with L is isomorphic to the structure sheaf is isomorphic to SheafHom(L, 𝒪).

The hypothesis is clause (2) of the tag, so L is invertible and the evaluation pairing SheafHom(L, 𝒪) ⊗_𝒪 L ⟶ 𝒪 is an isomorphism by isIso_evaluation. That exhibits SheafHom(L, 𝒪) as a two-sided tensor inverse of L, the braiding supplying the other order, while the given isomorphism exhibits N as one; a two-sided tensor inverse in a monoidal category is unique up to isomorphism (CategoryTheory.MonoidalCategory.HasInverse.inv_iso).

noncomputable def tensorInverseIsoDualSheaf
    (N : SheafOfModules.{max u v} (TensorSheafification.structureSheaf 𝒪 h𝒪))
    (e : ((Tensor.sheafTensor
      ⟨𝒪, Presheaf.isSheaf_of_isSheaf_comp _ 𝒪 (forget₂ CommRingCat RingCat) h𝒪⟩).obj L).obj N ≅
      SheafOfModules.unit (TensorSheafification.structureSheaf 𝒪 h𝒪)) :
    N ≅ dualSheaf 𝒪 h𝒪 L

Stacks.SheafOfModules.isInvertible_iff_exists_tensor_iso_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InvertibleRankOne.lean, line 298. The attribute's comment: “(1) ⟺ (2)”.

Stacks Project, Tag 0B8K and Tag 0B8N, (1) ⟺ (2). A sheaf of O-modules L is invertible if and only if there is a sheaf of O-modules N whose tensor product with L is isomorphic to O.

For the forward implication the tensor functor of L is an equivalence, so O has a preimage N under it, and the universal property identifies the image of that preimage with L ⊗_O N. For the converse the isomorphism L ⊗_O N ≅ O is turned into a pairing of presheaves of modules by composing with the sheafification unit, and isInvertible_of_pairing applies.

Tag 0B8K states this for a ringed space and Tag 0B8N for an arbitrary ringed site; the statement here is the one on a ringed site, so it carries both.

theorem isInvertible_iff_exists_tensor_iso_unit
    (L : SheafOfModules.{w} (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO)) :
    IsInvertible O hO L ↔ ∃ N : SheafOfModules.{w}
      (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO),
      Nonempty (((Tensor.sheafTensor.{u, v, w, w, w}
        ⟨O, Presheaf.isSheaf_of_isSheaf_comp _ O (forget₂ CommRingCat RingCat) hO⟩).obj L).obj N ≅
        SheafOfModules.unit (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO))

Stacks.SheafOfModules.Invertible.isInvertible_iff_exists_tensor_iso_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Ample/DescentStep.lean, line 200. The attribute's comment: “tensor_inverse_characterization”.

Stacks Project, Tag 0B8K. A sheaf of modules is invertible if and only if it has a tensor inverse, that is, if and only if some N satisfies L ⊗ N ≅ 𝒪.

theorem isInvertible_iff_exists_tensor_iso_unit
    (L : _root_.SheafOfModules.{w} (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO))
      :
    IsInvertible O hO L ↔
      ∃ N : _root_.SheafOfModules.{w} (Stacks.SheafOfModules.TensorSheafification.structureSheaf O
        hO),
        Nonempty (((Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, w, w}
          ⟨O, Presheaf.isSheaf_of_isSheaf_comp _ O (forget₂ CommRingCat RingCat) hO⟩).obj L).obj N ≅
          _root_.SheafOfModules.unit (Stacks.SheafOfModules.TensorSheafification.structureSheaf O
            hO))

Stacks.SheafOfModules.LocallyFiniteFree.isLocallyFiniteFreeSummand_of_isInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Ample/LocallyFiniteFreeSummand.lean, line 1191. The attribute's comment: “locally_finite_free_summand”.

Stacks Project, Tag 0B8K. An invertible sheaf of modules is locally a direct summand of a finite free sheaf.

theorem isLocallyFiniteFreeSummand_of_isInvertible
    (X : RingedSpace.{u, w}) (L : _root_.SheafOfModules.{u} (ringSheaf X))
    [HasWeakSheafify (Opens.grothendieckTopology X.carrier) AddCommGrpCat.{u}]
    [(Opens.grothendieckTopology X.carrier).WEqualsLocallyBijective AddCommGrpCat.{u}]
    [∀ U : Opens X,
      HasWeakSheafify (Opens.grothendieckTopology (X.restrict U.isOpenEmbedding).carrier)
        AddCommGrpCat.{u}]
    [∀ U : Opens X,
      (Opens.grothendieckTopology
        (X.restrict U.isOpenEmbedding).carrier).WEqualsLocallyBijective
        AddCommGrpCat.{u}]
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf
      (Presheaf.isSheaf_comp_of_isSheaf _ X.presheaf
        (forget₂ CommRingCat.{u} RingCat.{u}) X.IsSheaf) L) :
    ∀ x : X, ∃ (U : Opens X) (_ : x ∈ U) (n : ℕ),
      Nonempty (Retract ((modulePullback (X.ofRestrict U.isOpenEmbedding)).obj L)
        (_root_.SheafOfModules.free (ULift.{u} (Fin n))))

Tag 0B8L, a lemma

Tag 0B8L in the Stacks Project.

Stacks.RingedSpace.modulePullback_isInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PullbackInvertible/Basic.lean, line 56.

Stacks Project, Tag 0B8L. The pullback of an invertible module along a morphism of ringed spaces is invertible.

theorem modulePullback_isInvertible {X Y : RingedSpace.{u, u}} (f : X ⟶ Y)
    (L : SheafOfModules.{u} (structureSheafRing Y))
    [Stacks.SheafOfModules.IsInvertible Y.presheaf
      (Presheaf.isSheaf_comp_of_isSheaf _ _ (forget₂ CommRingCat RingCat) Y.IsSheaf) L] :
    Stacks.SheafOfModules.IsInvertible X.presheaf
      (Presheaf.isSheaf_comp_of_isSheaf _ _ (forget₂ CommRingCat RingCat) X.IsSheaf)
      ((modulePullback f).obj L)

AlgebraicGeometry.Scheme.isInvertibleModule_pushforward_of_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelKernel.lean, line 143. The attribute's comment: “the direct image of an invertible module along an isomorphism”.

The direct image of an invertible module along an isomorphism of schemes is invertible. The direct image along the inverse of an isomorphism is its inverse image (AlgebraicGeometry.Scheme.Modules.pushforwardInvIsoPullback), and the inverse image of an invertible module is invertible (Stacks.Modules.isInvertible_pullback).

public theorem isInvertibleModule_pushforward_of_isIso {X Y : Scheme.{u}} (e : X ≅ Y)
    (L : Y.Modules) (hL : Stacks.Ample.IsInvertibleModule Y L) :
    Stacks.Ample.IsInvertibleModule X ((Scheme.Modules.pushforward e.inv).obj L)

Stacks.InvertiblePullback.isInvertible_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InvertiblePullback/Basic.lean, line 126.

Stacks Tag 0B8L. The pullback of an invertible sheaf of modules along a morphism of ringed spaces is invertible.

A tensor inverse N of L, which Tag 0B8K produces from invertibility, is carried by f^* to a tensor inverse of f^*L: Tag 01CD turns f^*(L ⊗ N) into f^*L ⊗ f^*N, and RingedSpaceModuleAdjunction.modulePullbackObjUnitIso turns f^* 𝒪_Y into 𝒪_X.

theorem isInvertible_pullback (L : SheafOfModules.{u} (structureRingSheaf Y))
    [Stacks.SheafOfModules.IsInvertible Y.sheaf.obj (structureRingSheaf Y).property L] :
    Stacks.SheafOfModules.IsInvertible X.sheaf.obj (structureRingSheaf X).property
      ((pullbackFunctor f).obj L)

Stacks.RingedSpace.isInvertible_modulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PullbackInvertible/RingedSpace.lean, line 88.

Stacks Project, Tag 0B8L. The pullback f^*L of an invertible 𝒪_Y-module along a morphism of ringed spaces f : X ⟶ Y is an invertible 𝒪_X-module.

The proof is the one the Stacks Project gives. Tag 0B8K produces an 𝒪_Y-module N with L ⊗_{𝒪_Y} N ≅ 𝒪_Y; Stacks.RingedSpace.tensorIsoUnitPullback pulls that pairing back, which is where Tag 01CD enters; and Tag 0B8K read in the other direction concludes.

theorem isInvertible_modulePullback (f : X ⟶ Y)
    (L : SheafOfModules.{u} (structureSheafRing Y))
    [Stacks.SheafOfModules.IsInvertible Y.sheaf.obj (structureSheafRing Y).property L] :
    Stacks.SheafOfModules.IsInvertible X.sheaf.obj (structureSheafRing X).property
      ((modulePullback f).obj L)

RingedSpaceModuleAdjunction.modulePullback_isInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/RingedSpace/ModulePullbackInvertible.lean, line 43.

The pullback of an invertible module is invertible: if tensoring by L is an autoequivalence of Mod(𝒪_Y), then tensoring by f^* L is an autoequivalence of Mod(𝒪_X).

theorem modulePullback_isInvertible {X Y : RingedSpace.{u, u}} (f : X ⟶ Y)
    (L : SheafOfModules.{u}
      (Stacks.SheafOfModules.TensorSheafification.structureSheaf Y.presheaf (structureSheafRing
        Y).property))
    [IsInvertible Y.presheaf (structureSheafRing Y).property L] :
    IsInvertible X.presheaf (structureSheafRing X).property
      ((RingedSpaceModuleAdjunction.modulePullback f).obj L)

Tag 0B8M, a lemma

Tag 0B8M in the Stacks Project.

Stacks.SheafOfModules.Invertible.isInvertible_of_isFiniteLocallyFreeOfRank_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InvertibleRankOneLocal.lean, line 285. The attribute's comment: “locally free of rank one implies invertible”.

Stacks Project, Tag 0B8M. A finite locally free sheaf of modules of rank one is invertible.

This is the statement for Stacks.SheafOfModules.Invertible.IsFiniteLocallyFreeOfRank, and it lives in that predicate's namespace; Stacks.SheafOfModules.isInvertible_of_isFiniteLocallyFreeOfRank_one of StacksFrontier.Algebra.Category.ModuleCat.Sheaf.LocallyTrivialInvertible.Basic is the statement for AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank, the other rank predicate of [Stacks, Tag 01CS].

The local generators of rank one give a covering family of the final object on which L becomes isomorphic to the structure sheaf; each such trivialization is a rank-one dual basis, and isInvertible_of_dualBasisOne turns a family of those on a covering family into invertibility by way of the evaluation pairing L^∨ ⊗ L ⟶ 𝒪 and Tag 0B8K.

theorem isInvertible_of_isFiniteLocallyFreeOfRank_one
    (L : SheafOfModules.{max u v} (Stacks.SheafOfModules.TensorSheafification.structureSheaf 𝒪 h𝒪))
    [Invertible.IsFiniteLocallyFreeOfRank L 1] : IsInvertible 𝒪 h𝒪 L

Stacks.RingedSpace.isInvertible_of_isFiniteLocallyFreeOfRank_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocallyTrivialInvertible/Basic.lean, line 229. The attribute's comment: “locally free of rank one implies invertible”.

A sheaf of modules on a ringed space that is finite locally free of rank one is invertible.

theorem isInvertible_of_isFiniteLocallyFreeOfRank_one (X : RingedSpace.{u, u})
    (L : SheafOfModules.{u} (structureSheaf X.sheaf))
    [h : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank
      (C := Opens X) (J := Opens.grothendieckTopology X) L 1] :
    Stacks.SheafOfModules.IsInvertible X.sheaf.obj (structureSheaf X.sheaf).property L

Stacks.RingedSpace.exists_isInvertible_not_isFiniteLocallyFreeOfRank_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InvertibleCounterexample/Clause3.lean, line 49. The attribute's comment: “the converse fails for general ringed spaces”.

Clause 3 of Stacks Tag 0B8M. On a general ringed space an invertible sheaf of modules need not be finite locally free of rank one: there is a ringed space X and a sheaf of 𝒪_X-modules L with L invertible and L not finite locally free of rank one.

The witness is the one-point ringed space whose ring of global sections is ℤ[√-5], carrying the sheaf of modules attached to the non-principal invertible ideal (2, 1 + √-5). Its single stalk is ℤ[√-5], which is not a local ring; this is exactly what the local-stalk hypothesis of Stacks.RingedSpace.isInvertible_iff_isFiniteLocallyFreeOfRank_one rules out.

theorem exists_isInvertible_not_isFiniteLocallyFreeOfRank_one :
    ∃ (X : AlgebraicGeometry.RingedSpace.{u})
      (L : SheafOfModules.{u} (structureSheaf X.sheaf)),
      Stacks.SheafOfModules.IsInvertible X.sheaf.obj (structureSheaf X.sheaf).property L ∧
        ¬AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank
          (C := Opens X) (J := Opens.grothendieckTopology X) L 1

Stacks.InvertibleLocallyFree.isInvertible_of_isFiniteLocallyFreeOfRank_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InvertibleLocallyFree/DualBasis.lean, line 284. The attribute's comment: “(1)”.

Clause 1 of Stacks Tag 0B8M. A sheaf of modules that is finite locally free of rank one is invertible, with invertibility read as AlgebraicGeometry.SheafOfModules.IsInvertible — the predicate every consumer in this repository uses.

This is unconditional. It does not use Stacks.InvertibleLocallyFree.InvertibleIsLocal (which is itself proved, as Stacks.SheafOfModules.invertibleIsLocal): clause 1 does not need descent of the inverse object, because the inverse is the dual sheaf L^∨ = SheafHom(L, 𝒪) and the only local-to-global step is that a locally bijective pairing is inverted by sheafification. See the module documentation for the forced universe constraint w = max u v, inherited from the internal hom of Tag 03EM.

theorem isInvertible_of_isFiniteLocallyFreeOfRank_one
    (L : SheafOfModules.{max u v} (Stacks.SheafOfModules.TensorSheafification.structureSheaf 𝒪 h𝒪))
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank L 1] :
    AlgebraicGeometry.SheafOfModules.IsInvertible 𝒪 h𝒪 L

Stacks.InvertibleRankOneIff.isInvertible_of_isFiniteLocallyFreeOfRank_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InvertibleRankOneIff/Basic.lean, line 137. The attribute's comment: “locally free of rank one implies invertible”.

Clause 1 of Stacks Tag 0B8M. A finite locally free module of rank one on a ringed space is invertible. There is no hypothesis on the stalks of the structure sheaf, and none on the site.

The content is Stacks.SheafDescent.isInvertible_of_isFiniteLocallyFreeOfRank_one; what is done here is to restate it over structureSheaf X.sheaf, which forces the carrier universe of the ringed space to agree with the universe of its rings and so makes the sheafification instances available.

theorem isInvertible_of_isFiniteLocallyFreeOfRank_one
    (X : RingedSpace.{u})
    (L : SheafOfModules.{u} (structureSheaf X.sheaf))
    [SheafOfModules.IsFiniteLocallyFreeOfRank (C := Opens X)
      (J := Opens.grothendieckTopology X) L 1] :
    SheafOfModules.IsInvertible X.sheaf.obj (structureSheaf X.sheaf).property L

Stacks.InvertibleRankOneIff.isInvertible_iff_isFiniteLocallyFreeOfRank_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InvertibleRankOneIff/Basic.lean, line 157. The attribute's comment: “characterization for local stalks”.

Clause 2 of Stacks Tag 0B8M. On a ringed space all of whose stalks 𝒪_{X, x} are local rings, a sheaf of modules is invertible exactly when it is finite locally free of rank one.

The forward implication is Stacks.SheafRankOne.isFiniteLocallyFreeOfRank_one_of_isInvertible and is where the local-stalk hypothesis is spent; the reverse implication is clause 1, which holds on every ringed space.

theorem isInvertible_iff_isFiniteLocallyFreeOfRank_one
    (X : RingedSpace.{u})
    (L : SheafOfModules.{u} (structureSheaf X.sheaf))
    [∀ x : X, IsLocalRing (X.presheaf.stalk x)] :
    SheafOfModules.IsInvertible X.sheaf.obj (structureSheaf X.sheaf).property L ↔
      SheafOfModules.IsFiniteLocallyFreeOfRank (C := Opens X)
        (J := Opens.grothendieckTopology X) L 1

Stacks.RingedSpace.isInvertible_iff_isFiniteLocallyFreeOfRank_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InvertibleTrivialization/Sheaf.lean, line 114. The attribute's comment: “characterization for local stalks”.

On a ringed space all of whose structure-sheaf stalks are local rings, a sheaf of modules is invertible if and only if it is finite locally free of rank one.

theorem isInvertible_iff_isFiniteLocallyFreeOfRank_one (X : RingedSpace.{u, u})
    (L : SheafOfModules.{u} (structureSheaf X.sheaf))
    [∀ x : X, IsLocalRing (X.presheaf.stalk x)] :
    Stacks.SheafOfModules.IsInvertible X.sheaf.obj (structureSheaf X.sheaf).property L ↔
      AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank
        (C := Opens X) (J := Opens.grothendieckTopology X) L 1

AlgebraicGeometry.RingedSite.isInvertible_of_isFiniteLocallyFreeOfRank_one_of_essentiallySmall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InvertibleRankOneEssentiallySmall.lean, line 319. The attribute's comment: “locally free of rank one implies invertible, on an essentially small site”.

Stacks Project, Tag 0B8M, clause 1, on an essentially small ringed site. A sheaf of modules which is locally free of rank one is invertible, with the universe of the sections of the structure sheaf independent of the universes of the site.

theorem isInvertible_of_isFiniteLocallyFreeOfRank_one_of_essentiallySmall
    (X : AlgebraicGeometry.RingedSite.{u₁, v₁, w}) [EssentiallySmall.{w} X.C]
    [HasWeakSheafify X.J AddCommGrpCat.{w}] [X.J.WEqualsLocallyBijective AddCommGrpCat.{w}]
    (L : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
    (hL : AlgebraicGeometry.RingedSite.IsFiniteLocallyFreeOfRank X L 1) :
    Stacks.SheafOfModules.IsInvertible X.O.obj
      (Stacks.SheafOfModules.Tensor.ringSheaf X.O).property L

Tag 01CT, a lemma

Tag 01CT in the Stacks Project.

Stacks.SheafOfModules.Invertible.isIso_evaluation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InvertibleDualEvaluation.lean, line 261. The attribute's comment: “evaluation”. References: EGA 0 (5.4.3), “more general”.

Stacks Project, Tag 040A (2), the evaluation clause. For an invertible sheaf of 𝒪-modules L on a ringed site the evaluation pairing SheafHom(L, 𝒪) ⊗_𝒪 L ⟶ 𝒪 is an isomorphism.

The dual is a left dual of L by exactPairingDualSheafOfIsInvertible, and the evaluation of an exact pairing is an isomorphism whenever tensoring on the right by the first object is an equivalence, which for an invertible sheaf of modules it is.

A ringed space is a ringed site, so this is also the evaluation clause of Tag 01CT (2); see Stacks.SheafOfModules.isIso_evaluation_of_isInvertible for that reading.

theorem isIso_evaluation [IsInvertible 𝒪 h𝒪 L] : IsIso (evaluation 𝒪 h𝒪 L)

Stacks.SheafOfModules.Invertible.isIso_tensorSheafBraiding_hom_comp_evaluation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InvertibleDualEvaluation.lean, line 277. The attribute's comment: “evaluation”. References: EGA 0 (5.4.3), “more general”.

Stacks Project, Tag 040A (2) and Tag 01CT (2), the evaluation clause in the order the tags write it. The evaluation map L ⊗_𝒪 SheafHom(L, 𝒪) ⟶ 𝒪 is an isomorphism. It is the canonical pairing of Stacks.SheafOfModules.evaluation, whose factors come in the order Tag 0FNV writes them, preceded by the braiding of the tensor product sheaf, which is what exchanges the two factors; in this order it is the trivializing pairing identifying L^∨ as a tensor inverse of L.

theorem isIso_tensorSheafBraiding_hom_comp_evaluation [IsInvertible 𝒪 h𝒪 L] :
    IsIso ((tensorSheafBraiding 𝒪 h𝒪 L (dualSheaf 𝒪 h𝒪 L)).hom ≫ evaluation 𝒪 h𝒪 L)

Stacks.SheafOfModules.Invertible.isInvertible_dualSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InvertibleDualEvaluation.lean, line 287. The attribute's comment: “dual_invertible”.

Stacks Project, Tag 040A (2) and Tag 01CT (2), the invertibility clause. The dual L^∨ = SheafHom(L, 𝒪) of an invertible sheaf of 𝒪-modules is again invertible: the evaluation pairing is an isomorphism L^∨ ⊗_𝒪 L ≅ 𝒪, which is Tag 0B8K (2) for L^∨.

theorem isInvertible_dualSheaf [IsInvertible 𝒪 h𝒪 L] :
    IsInvertible 𝒪 h𝒪 (dualSheaf 𝒪 h𝒪 L)

Stacks.SheafOfModules.tensorProduct_isInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorInvertible.lean, line 474. The attribute's comment: “tensor_invertible”.

Stacks Project, Tag 01CT (1), Tag 040A (1). The tensor product of two invertible sheaves of modules is invertible.

theorem tensorProduct_isInvertible
    (L N : SheafOfModules.{w} (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO))
    [IsInvertible O hO L] [IsInvertible O hO N] :
    IsInvertible O hO ((((Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, w, w}
      ⟨O, Presheaf.isSheaf_of_isSheaf_comp _ O (forget₂ CommRingCat RingCat) hO⟩).obj L)).obj N)

Stacks.SheafOfModules.Invertible.tensorProduct_isInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Ample/AmpleCriteria.lean, line 70. The attribute's comment: “tensor_invertible”.

Stacks Project, Tag 01CT, part (1). The tensor product of two invertible sheaves of modules is invertible: tensoring by it is the composite of the two tensor functors.

theorem tensorProduct_isInvertible
    (L N : _root_.SheafOfModules.{w} (Stacks.SheafOfModules.TensorSheafification.structureSheaf O
      hO))
    [IsInvertible O hO L] [IsInvertible O hO N] :
    IsInvertible O hO (((Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, w, w}
      ⟨O, Presheaf.isSheaf_of_isSheaf_comp _ O (forget₂ CommRingCat RingCat) hO⟩).obj L).obj N)

Tag 01CU, a definition

Tag 01CU in the Stacks Project.

Stacks.SheafOfModules.TensorPower.tensorPower, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorPower.lean, line 213.

The nth tensor power of an invertible sheaf of modules L, for n : ℤ: the image of the structure sheaf under the nth power of the autoequivalence given by tensoring by L.

noncomputable def tensorPower
    (L : SheafOfModules.{w} (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO))
    [(((Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, w, w}
      ⟨O, Presheaf.isSheaf_of_isSheaf_comp _ O (forget₂ CommRingCat RingCat)
        hO⟩).flip.obj L)).IsEquivalence] (n : ℤ) :
    SheafOfModules.{w} (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO)

Stacks.SheafOfModules.TensorPower.isInvertible_tensorPower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorPowerCoherence.lean, line 200. The attribute's comment: “tensor powers are invertible”.

Every integer tensor power of an invertible sheaf of modules is invertible. For non-negative exponents this is Tag 01CT (1) and the successor comparison; for negative exponents it is the same two inputs read backwards, cancelling the invertible factor L.

theorem isInvertible_tensorPower [IsInvertible O hO L] (n : ℤ) :
    IsInvertible O hO (tensorPower O hO L n)

Stacks.SheafOfModules.TensorPower.mulIso_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorPowerCommutativity.lean, line 461. The attribute's comment: “commutativity of the canonical multiplication”.

The commutativity normalisation of Tag 01CU: the canonical multiplication on the integer tensor powers of an invertible sheaf of modules agrees with itself after the symmetry constraint of the tensor product sheaf. This was the last of the four normalisations of Tag 01CU still outstanding.

theorem mulIso_comm (n m p : ℤ) (h : n + m = p) (h' : m + n = p) :
    mulIso O hO L n m p h =
      Stacks.SheafOfModules.tensorSheafBraiding O hO (pow L n) (pow L m) ≪≫
        mulIso O hO L m n p h'

Stacks.SheafOfModules.TensorPower.tensorPowerCoherence_exists, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorPowerCommutativity.lean, line 595. The attribute's comment: “canonical multiplication and coherence”. References: EGA 0 (5.4.4), “partial”.

The canonical multiplication on the integer tensor powers of an invertible sheaf of modules exists and satisfies every normalisation asserted by Tag 01CU: the two unit constraints, the degree-(n, 1) normalisation by the defining iteration, naturality of that comparison, associativity against the associativity constraint of the tensor product sheaf, and commutativity against its symmetry constraint.

The multiplication is transported from Stacks.MonoidalCategory.mul by Stacks.MonoidalCategory.nonempty_powCoherence, which is what absorbs the fact that the tensor powers of Tag 01CU are built from (Stacks.SheafOfModules.Tensor.sheafTensor _).flip.obj L while the multiplication is built from tensorRight: the two functors are equal but their chosen quasi-inverses, used by the negative exponents, have no common normal form.

theorem tensorPowerCoherence_exists : Nonempty (TensorPowerCoherence O hO L)

Stacks.SheafOfModules.TensorPower.braidingScalar_eq_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorPowerConstraints.lean, line 344. The attribute's comment: “commutativity constraint”.

The braiding scalar of the tensor powers of an invertible sheaf of modules is the identity, in every degree.

theorem braidingScalar_eq_id (n : ℤ) : braidingScalar O hO L n = 𝟙 _

Stacks.SheafOfModules.TensorPower.mulIso_zero_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorPowerInteger.lean, line 738. The attribute's comment: “left unit normalisation of the canonical multiplication”.

Multiplication by the zeroth tensor power on the left is the left unit constraint of the tensor product sheaf.

theorem mulIso_zero_left (n : ℤ) (h : 0 + n = n) :
    mulIso O hO L 0 n n h = Stacks.SheafOfModules.tensorSheafLeftUnitor O hO (pow L n)

Stacks.SheafOfModules.TensorPower.mulIso_assoc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorPowerInteger.lean, line 767. The attribute's comment: “associativity of the canonical multiplication”.

Associativity of the canonical multiplication, against the associativity constraint of the tensor product sheaf.

theorem mulIso_assoc (n m k p t s : ℤ) (h₁ : n + m = p) (h₂ : m + k = t) (h₃ : p + k = s) :
    tensorSheafMapIso O hO (mulIso O hO L n m p h₁) (Iso.refl (pow L k)) ≪≫
        mulIso O hO L p k s h₃ =
      Stacks.SheafOfModules.tensorSheafAssociator O hO (pow L n) (pow L m) (pow L k) ≪≫
        tensorSheafMapIso O hO (Iso.refl (pow L n)) (mulIso O hO L m k t h₂) ≪≫
          mulIso O hO L n t s (by omega)

Stacks.SheafOfModules.TensorPower.tensorPowerMulIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorPowerMultiplication.lean, line 339. The attribute's comment: “canonical multiplication”.

The canonical multiplication isomorphism L^{⊗ n} ⊗_O L^{⊗ m} ≅ L^{⊗ (n + m)}, the addition law CategoryTheory.Equivalence.powAdd for the powers of - ⊗ L applied to the structure sheaf, read through powFunctorIsoTensorRight.

noncomputable def tensorPowerMulIso (n m : ℤ) :
    (((Stacks.SheafOfModules.Tensor.sheafTensor ⟨O, Presheaf.isSheaf_of_isSheaf_comp _ (O) (forget₂
      CommRingCat RingCat) (hO)⟩).obj ((tensorPower O hO L n))).obj ((tensorPower
      O hO L m))) ≅
      tensorPower O hO L (n + m)

Stacks.SheafOfModules.Invertible.tensorPower, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/TensorPower.lean, line 156.

Stacks Project, Tag 01CU. The nth tensor power L^{⊗ n} of an invertible sheaf L, for n an arbitrary integer: the image of the structure sheaf under the nth power of the right-tensor autoequivalence.

noncomputable def tensorPower
    (L : SheafOfModules.{w} (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO))
    [IsInvertible O hO L] (n : ℤ) :
    SheafOfModules.{w} (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO)

Stacks.SelfBraidingInvertible.braidingScalar_eq_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SelfBraidingInvertible/TensorPowerScalar.lean, line 87. The attribute's comment: “canonical multiplication and coherence”.

The braiding scalar of a tensor power of an invertible sheaf of modules is the identity, in every degree. By Stacks.SheafOfModules.TensorPower.tensorSheafBraiding_self_eq_refl_iff this is the commutativity constraint of Stacks Tag 01CU in degrees (n, n).

theorem braidingScalar_eq_id (n : ℤ) :
    Stacks.SheafOfModules.TensorPower.braidingScalar 𝒪 h𝒪 L n = 𝟙 _

AlgebraicGeometry.SheafOfModules.tensorPowAddIso_zero_right_natCast, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TensorPowerAssoc/SheafOfModules.lean, line 107. The attribute's comment: “canonical multiplication and coherence”.

The right unit constraint: multiplication by L ^⊗ 0 on the right is the right unitor.

theorem tensorPowAddIso_zero_right_natCast (a : ℕ) :
    tensorPowAddIso 𝒪 h𝒪 L (a : ℤ) ((0 : ℕ) : ℤ) = ρ_ (tensorPow 𝒪 h𝒪 L (a : ℤ))

AlgebraicGeometry.SheafOfModules.tensorPowAddIso_zero_left_natCast, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TensorPowerAssoc/SheafOfModules.lean, line 113. The attribute's comment: “canonical multiplication and coherence”.

The left unit constraint: multiplication by L ^⊗ 0 on the left is the left unitor.

theorem tensorPowAddIso_zero_left_natCast (b : ℕ) :
    tensorPowAddIso 𝒪 h𝒪 L ((0 : ℕ) : ℤ) (b : ℤ) ≪≫
        tensorPowNatCongrIso 𝒪 h𝒪 L (Nat.zero_add b) =
      λ_ (tensorPow 𝒪 h𝒪 L (b : ℤ))

AlgebraicGeometry.SheafOfModules.tensorPowAddIso_one_right_natCast, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TensorPowerAssoc/SheafOfModules.lean, line 126. The attribute's comment: “canonical multiplication and coherence”.

The normalisation in degree one. Multiplication by the first tensor power is AlgebraicGeometry.SheafOfModules.tensorPowOneIso whiskered into L ^⊗ a, followed by the successor step L ^⊗ a ⊗ L = L ^⊗ (a + 1) of the iteration which defines the powers; in nonnegative degree that step is the identity. This is what pins the canonical multiplication down: an associative family of multiplication isomorphisms is determined by its degree-(a, 1) value.

theorem tensorPowAddIso_one_right_natCast (a : ℕ) :
    tensorPowAddIso 𝒪 h𝒪 L (a : ℤ) ((1 : ℕ) : ℤ) =
      whiskerLeftIso (tensorPow 𝒪 h𝒪 L (a : ℤ)) (tensorPowOneIso 𝒪 h𝒪 L)

AlgebraicGeometry.SheafOfModules.tensorPowAddIso_assoc_natCast, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TensorPowerAssoc/SheafOfModules.lean, line 135. The attribute's comment: “canonical multiplication and coherence”.

The associativity constraint on the multiplication of tensor powers, which Stacks Tag 01CU asserts with the formulation omitted, in nonnegative degree and against the associator of the monoidal structure on sheaves of modules itself.

theorem tensorPowAddIso_assoc_natCast (a b c : ℕ) :
    whiskerRightIso (tensorPowAddIso 𝒪 h𝒪 L (a : ℤ) (b : ℤ)) (tensorPow 𝒪 h𝒪 L (c : ℤ)) ≪≫
        tensorPowAddIso 𝒪 h𝒪 L ((a + b : ℕ) : ℤ) (c : ℤ) =
      α_ (tensorPow 𝒪 h𝒪 L (a : ℤ)) (tensorPow 𝒪 h𝒪 L (b : ℤ)) (tensorPow 𝒪 h𝒪 L (c : ℤ)) ≪≫
        whiskerLeftIso (tensorPow 𝒪 h𝒪 L (a : ℤ)) (tensorPowAddIso 𝒪 h𝒪 L (b : ℤ) (c : ℤ)) ≪≫
          tensorPowAddIso 𝒪 h𝒪 L (a : ℤ) ((b + c : ℕ) : ℤ) ≪≫
            tensorPowNatCongrIso 𝒪 h𝒪 L (Nat.add_assoc a b c).symm

AlgebraicGeometry.SheafOfModules.tensorPowAddIso_comm_natCast, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TensorPowerAssoc/SheafOfModules.lean, line 150. The attribute's comment: “canonical multiplication and coherence”.

The commutativity constraint on the multiplication of tensor powers, in nonnegative degree.

At degrees (1, 1) the constraint is the triviality of the self-braiding of L, which holds for every invertible L by the instance Stacks.SelfBraidingInvertible.hasTrivialSelfBraiding.

theorem tensorPowAddIso_comm_natCast (a b : ℕ) :
    β_ (tensorPow 𝒪 h𝒪 L (a : ℤ)) (tensorPow 𝒪 h𝒪 L (b : ℤ)) ≪≫
        tensorPowAddIso 𝒪 h𝒪 L (b : ℤ) (a : ℤ) =
      tensorPowAddIso 𝒪 h𝒪 L (a : ℤ) (b : ℤ) ≪≫
        tensorPowNatCongrIso 𝒪 h𝒪 L (Nat.add_comm a b)

Stacks.SheafOfModules.Invertible.tensorPowerCoherence_exists, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TensorPowerCoherence/Basic.lean, line 225. The attribute's comment: “canonical multiplication and coherence”.

Existence of a coherent multiplication on the tensor powers. The integer tensor powers of an invertible sheaf of modules L carry coherent multiplication data Stacks.SheafOfModules.Invertible.TensorPowerCoherence O hO L.

theorem tensorPowerCoherence_exists
    (L : SheafOfModules.{w} (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO))
    [_root_.AlgebraicGeometry.SheafOfModules.IsInvertible O hO L] :
    Nonempty (TensorPowerCoherence O hO L)

Tag 01CV, a definition

Tag 01CV in the Stacks Project.

Stacks.SheafOfModules.sectionRingStructure_exists, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TwistSectionRing.lean, line 742. The attribute's comment: “graded ring multiplication”.

There is a graded ring structure on the section ring whose homogeneous product is tensor multiplication.

theorem sectionRingStructure_exists
    (L : SheafOfModules.{w} (TensorSheafification.structureSheaf O hO))
    [IsInvertible O hO L] :
    Nonempty (SectionRingStructure O hO L)

Stacks.SheafOfModules.sectionModuleStructure_exists, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TwistSectionRing.lean, line 1158. The attribute's comment: “graded module action”.

There is a module structure of the section module over the section ring whose action on homogeneous terms is tensor multiplication.

theorem sectionModuleStructure_exists
    (L F : SheafOfModules.{w} (TensorSheafification.structureSheaf O hO))
    [IsInvertible O hO L] :
    Nonempty (SectionModuleStructure O hO L F)

Stacks.SheafOfModules.Invertible.sectionRing, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/InvertibleSections/TwistedSections.lean, line 168. The attribute's comment: “underlying graded ring”. References: EGA II (4.5.1), “S = ⊕Γ(X,L^⊗n)”; EGA III (2.1.1), “(2.1.1.1)”; EGA II (2.6.1), “Γ_•(O_X) definition”; EGA 0 (5.4.6), “Γ•(L) carrier”.

Stacks Project, Tag 01CV. The associated graded ring Γ_*(X, L) of an invertible sheaf of modules: the direct sum of the global sections of its non-negative tensor powers. Its graded ring structure is Stacks.SheafOfModules.Invertible.homGradedRing.

abbrev sectionRing

Stacks.SheafOfModules.Invertible.twistedSections, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/InvertibleSections/TwistedSections.lean, line 181. The attribute's comment: “underlying graded module”. References: EGA 0 (5.4.6), “partial”; EGA II (2.6.1); EGA III (2.1.2), “partial”.

Stacks Project, Tag 01CV. The graded module Γ_*(X, L, F) of a sheaf of modules F: the direct sum, over all integers n, of the global sections of the twists F ⊗ L^{⊗ n}. Its module structure over Γ_*(X, L) is Stacks.SheafOfModules.Invertible.twistedSectionsModule.

abbrev twistedSections
    (F : _root_.SheafOfModules.{w}
      (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO))

Stacks.SheafOfModules.Invertible.twistedSectionsGmodule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/InvertibleSections/TwistedSections.lean, line 208. The attribute's comment: “graded module action”.

Stacks Project, Tag 01CV. Γ_*(X, L, F) is a ℤ-graded module over the ℕ-graded ring Γ_*(X, L), with the action twistedSectionsSMul on homogeneous sections. No commutativity of Γ_*(X, L) is used.

noncomputable def twistedSectionsGmodule
    (F : _root_.SheafOfModules.{w}
      (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO)) :
    letI : GradedMonoid.GMonoid (fun n : ℕ =>
        𝟙_ (_root_.SheafOfModules.{w}
          (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO))
            ⟶ tensorPower O hO L (n : ℤ)) := (tensorPowerSystem O hO L).gradedMonoid
    DirectSum.Gmodule
      (fun n : ℕ => 𝟙_ (_root_.SheafOfModules.{w}
        (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO))
          ⟶ tensorPower O hO L (n : ℤ))
      (fun n : ℤ => 𝟙_ (_root_.SheafOfModules.{w}
        (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO))
          ⟶ twist O hO L F n)

Stacks.SheafOfModules.Invertible.homGradedCommRingOfInvertible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GradedSectionRing/Commutativity.lean, line 313. The attribute's comment: “associated graded ring”. References: EGA II (4.5.1), “S = ⊕Γ(X,L^⊗n)”; EGA III (2.1.1), “(2.1.1.1)”; EGA II (2.6.1), “graded ring Γ_•(O_X)”; EGA 0 (5.4.6), “graded ring Γ•(L)”.

Stacks Project, Tag 01CV: the associated graded ring Γ_*(X, L) = ⨁_{n ≥ 0} Γ(X, L^{⊗ n}) of an invertible sheaf of modules. This is the commutative graded ring on the morphism groups 𝟙 ⟶ L^{⊗ n}, with the commutativity constraint of Tag 01CU discharged by tensorPowerMulIso_comm above, so it is unconditional.

The direct sum itself needs no declaration of ours: Mathlib's DirectSum.commRing turns a DirectSum.GCommRing on the family into a commutative ring on ⨁ n : ℕ, (𝟙 ⟶ L^{⊗ n}), the tensor unit is the structure sheaf on the nose (Stacks.SheafOfModules.tensorUnit_eq) so the summands are the global sections the tag names, and Stacks.SheafOfModules.Invertible.homToSection_sectionMul identifies the multiplication with the one already defined on PresheafOfModules.sections. This declaration alone is therefore the covering set of the tag's first displayed object; the tag's second one, the ℤ-graded module Γ_*(X, L, F), is not claimed — see the implementation notes.

noncomputable def homGradedCommRingOfInvertible :
    DirectSum.GCommRing (fun n : ℕ =>
      (𝟙_ (_root_.SheafOfModules.{w} (Stacks.SheafOfModules.TensorSheafification.structureSheaf O
        hO))
        ⟶ tensorPower O hO L (n : ℤ)))

Stacks.SectionRingProjTheta.sectionRingAddEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjTheta/SectionRingComparison.lean, line 147. The attribute's comment: “the repository's two realisations of the graded ring Γ_*(X, L) — the Stacks.GradedSections.sectionRing one on morphisms out of the monoidal unit and the Stacks.SheafOfModules.sectionRing one on honest global sections — have the same carrier, ADDITIVELY and degree by degree, and the grading corresponds (map_summand_eq_sectionRingGrading). The two MULTIPLICATIONS are not identified BY THIS DECLARATION, which is an AddEquiv and nothing more; they ARE identified, by Stacks.SectionRingProjTheta.sectionRingEquiv in StacksFrontier/AlgebraicGeometry/SectionRingProjTheta/SectionRingMultiplicative.lean, which is this map with its multiplicativity supplied”.

The two section rings of an invertible sheaf of modules have the same carrier.

Degree by degree this is powSectionsAddEquiv: a morphism out of the monoidal unit into the natTensorPow spelling of L^{⊗ n} against an honest section over ⊤_ C of the tensorPower spelling.

def sectionRingAddEquiv :
    Stacks.GradedSections.sectionRing L ≃+ Stacks.SheafOfModules.sectionRing 𝒪 h𝒪 L

Stacks.SectionRingProjTheta.sectionRingEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjTheta/SectionRingMultiplicative.lean, line 260. The attribute's comment: “the repository's two realisations of the graded ring Γ_*(X, L) — the Stacks.GradedSections.sectionRing one on morphisms out of the monoidal unit and the Stacks.SheafOfModules.sectionRing one on honest global sections — are isomorphic as RINGS, and the isomorphism is graded (sectionGradedRingHom)”.

The two section rings of an invertible sheaf of modules are isomorphic as rings. This is Stacks.SectionRingProjTheta.sectionRingAddEquiv with its multiplicativity supplied; the underlying function is unchanged, so every computation rule of that additive isomorphism applies verbatim.

def sectionRingEquiv :
    Stacks.GradedSections.sectionRing L ≃+* Stacks.SheafOfModules.sectionRing 𝒪 h𝒪 L

Stacks.SheafOfModules.sectionRing, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/InvertibleAndOperators/SectionRing.lean, line 113. The attribute's comment: “underlying graded ring”. References: EGA II (4.5.1), “partial”.

Stacks Project, Tag 01CV. The section ring of an invertible sheaf L: the direct sum of the global sections of the nonnegative tensor powers of L.

abbrev sectionRing (L : SheafOfModules.{w} (TensorSheafification.structureSheaf O hO))
    [IsInvertible O hO L] : Type _

Stacks.SheafOfModules.sectionModule, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/InvertibleAndOperators/SectionRing.lean, line 121. The attribute's comment: “underlying graded module”.

Stacks Project, Tag 01CV. The section module of a sheaf of modules F: the direct sum of the global sections of all the twists of F by integer tensor powers of an invertible sheaf L.

abbrev sectionModule (L F : SheafOfModules.{w} (TensorSheafification.structureSheaf O hO))
    [IsInvertible O hO L] : Type _

Declarations registered for the tag:

• Stacks.SheafOfModules.Invertible.homGradedRing, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Divisors/InvertibleSections/TwistedSections.lean, line 241 (StacksFrontier): “graded ring multiplication”.

Tag 01CW, a lemma

Tag 01CW in the Stacks Project.

AlgebraicGeometry.SheafOfModules.essentiallySmall_isInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InvertibleRingedSpaceEssentiallySmall.lean, line 107.

Stacks Project, Tag 01CW. The invertible sheaves of modules over the structure sheaf of a ringed space have only a set of isomorphism classes: there is a set of invertible modules, of size max u w, meeting every isomorphism class of invertible modules on the space.

theorem essentiallySmall_isInvertible (X : RingedSpace.{u, w}) :
    ObjectProperty.EssentiallySmall.{max u w}
      (AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf
        (Presheaf.isSheaf_comp_of_isSheaf _ X.presheaf
          (forget₂ CommRingCat.{u} RingCat.{u}) X.IsSheaf))

AlgebraicGeometry.SheafOfModules.exists_unique_representative_isInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InvertibleRingedSpaceEssentiallySmall.lean, line 180. The attribute's comment: “exactly one representative”.

Stacks Project, Tag 01CW. There is a family of invertible modules over the structure sheaf of a ringed space, indexed by a type of size max u w, whose members are pairwise non-isomorphic and such that every invertible module on the space is isomorphic to the member of exactly one index.

theorem exists_unique_representative_isInvertible (X : RingedSpace.{u, w}) :
    ∃ (I : Type (max u w)) (L : I → _root_.SheafOfModules.{u}
        (Stacks.SheafOfModules.TensorSheafification.structureSheaf X.presheaf
          (Presheaf.isSheaf_comp_of_isSheaf _ X.presheaf
            (forget₂ CommRingCat.{u} RingCat.{u}) X.IsSheaf))),
      (∀ i, AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf
          (Presheaf.isSheaf_comp_of_isSheaf _ X.presheaf
            (forget₂ CommRingCat.{u} RingCat.{u}) X.IsSheaf) (L i)) ∧
      (∀ i j, Nonempty (L i ≅ L j) → i = j) ∧
      ∀ M, AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf
          (Presheaf.isSheaf_comp_of_isSheaf _ X.presheaf
            (forget₂ CommRingCat.{u} RingCat.{u}) X.IsSheaf) M →
        ∃! i, Nonempty (M ≅ L i)

Tag 01CX, a definition

Tag 01CX in the Stacks Project.

Stacks.SheafOfModules.Picard.PicardGroup, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/Picard.lean, line 170. The attribute's comment: “the Picard group”. References: EGA IV (21.3.2), “Pic(X) definition”; SGA 6 X (5.1), “Pic(X) definition”.

The Picard group of O: the group of isomorphism classes of invertible sheaves of O-modules, as a small type.

noncomputable def PicardGroup : Type (max (max u v) w)

Stacks.SheafOfModules.Picard.instAddCommGroupPicardGroup, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/Picard.lean, line 176. The attribute's comment: “abelian group structure”.

The abelian group structure on the Picard group; its addition is the tensor product sheaf, by classOf_tensor.

noncomputable instance instAddCommGroupPicardGroup : AddCommGroup (PicardGroup O hO)

Stacks.SheafOfModules.Picard.classOf_tensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/Picard.lean, line 211. The attribute's comment: “addition is tensor product”.

Addition in the Picard group is the tensor product sheaf.

theorem classOf_tensor (L N : SheafOfModules.{w}
  (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO))
    (hL : IsInvertible O hO L) (hN : IsInvertible O hO N)
    (hLN : IsInvertible O hO ((((Stacks.SheafOfModules.Tensor.sheafTensor
      ⟨O, Presheaf.isSheaf_of_isSheaf_comp _ (O) (forget₂ CommRingCat RingCat) (hO)⟩).obj
        (L)).obj (N)))) :
    classOf O hO L hL + classOf O hO N hN =
      classOf O hO ((((Stacks.SheafOfModules.Tensor.sheafTensor
        ⟨O, Presheaf.isSheaf_of_isSheaf_comp _ (O) (forget₂ CommRingCat RingCat) (hO)⟩).obj
          (L)).obj (N))) hLN

Stacks.SheafOfModules.PicardGroup, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardGroup/Basic.lean, line 269. The attribute's comment: “the Picard group”. References: EGA IV (21.3.2), “Pic(X) definition”; SGA 6 X (5.1), “Pic(X) definition”.

The Picard group of a sheaf of rings O on a site: the abelian group whose elements are the isomorphism classes of invertible sheaves of O-modules and whose addition is the tensor product.

noncomputable def PicardGroup : Type _

Stacks.SheafOfModules.instAddCommGroupPicardGroup, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardGroup/Basic.lean, line 275. The attribute's comment: “abelian group structure”. References: EGA IV (21.3.2), “Pic(X) comm. group”.

The addition of the Picard group, induced by the tensor product of invertible sheaves of modules.

noncomputable instance instAddCommGroupPicardGroup : AddCommGroup (PicardGroup O hO)

Stacks.SheafOfModules.picardClass_tensorSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardGroup/Basic.lean, line 319. The attribute's comment: “addition is tensor product”. References: EGA IV (21.3.2), “cl(L)cl(L')=cl(L⊗L')”.

Addition in the Picard group is the tensor product.

theorem picardClass_tensorSheaf (L N : SheafOfModules.{w}
  (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO))
    (hL : IsInvertible O hO L) (hN : IsInvertible O hO N)
    (hLN : IsInvertible O hO ((((Stacks.SheafOfModules.Tensor.sheafTensor
      ⟨O, Presheaf.isSheaf_of_isSheaf_comp _ (O) (forget₂ CommRingCat RingCat) (hO)⟩).obj
        (L)).obj (N)))) :
    picardClass O hO L hL + picardClass O hO N hN =
      picardClass O hO ((((Stacks.SheafOfModules.Tensor.sheafTensor
        ⟨O, Presheaf.isSheaf_of_isSheaf_comp _ (O) (forget₂ CommRingCat RingCat) (hO)⟩).obj
          (L)).obj (N))) hLN

Stacks.SheafPicardGroup.PicardGroup, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SheafPicardGroup/Basic.lean, line 182. The attribute's comment: “the Picard group”.

The Picard group of 𝒪, Stacks Tag 01CX: the isomorphism classes of invertible sheaves of 𝒪-modules, with multiplication induced by tensor product. It is realised as the group of units of the monoid ClassMonoid 𝒪 h𝒪 of all isomorphism classes; that these units are exactly the invertible sheaves is isInvertible_iff_isUnit, and that every one of them is the class of such a sheaf is exists_classOf.

abbrev PicardGroup : Type _

Stacks.SheafPicardGroup.commGroup, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SheafPicardGroup/Basic.lean, line 190. The attribute's comment: “abelian group structure”.

The Picard group is an abelian group, Stacks Tag 01CX. The structure is Units.instCommGroup over instCommMonoid: no coherence law is proved by hand, because the skeleton of a braided monoidal category is already a commutative monoid. The additive reading the source sometimes uses is Additive (PicardGroup 𝒪 h𝒪), and instAddCommGroupAdditivePicardGroup records it.

noncomputable def commGroup : CommGroup (PicardGroup 𝒪 h𝒪)

Stacks.SheafPicardGroup.instAddCommGroupAdditivePicardGroup, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SheafPicardGroup/Basic.lean, line 195. The attribute's comment: “abelian group structure”.

The Picard group, written additively, as Stacks Tag 01CX sometimes does.

noncomputable instance instAddCommGroupAdditivePicardGroup :
    AddCommGroup (Additive (PicardGroup 𝒪 h𝒪))

Stacks.SheafPicardGroup.exists_classOf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SheafPicardGroup/Basic.lean, line 238. The attribute's comment: “the Picard group”.

Every element of the Picard group is the class of an invertible sheaf of modules, so classOf is onto.

theorem exists_classOf (x : PicardGroup 𝒪 h𝒪) :
    ∃ (M : _root_.SheafOfModules.{w} (structureSheaf 𝒪 h𝒪)) (_ : IsInvertible 𝒪 h𝒪 M),
      classOf 𝒪 h𝒪 M = x

Stacks.SheafPicardGroup.classOf_eq_classOf_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SheafPicardGroup/Basic.lean, line 250. The attribute's comment: “the Picard group”.

Two invertible sheaves have the same Picard class exactly when they are isomorphic.

theorem classOf_eq_classOf_iff [IsInvertible 𝒪 h𝒪 L] [IsInvertible 𝒪 h𝒪 N] :
    classOf 𝒪 h𝒪 L = classOf 𝒪 h𝒪 N ↔ Nonempty (L ≅ N)

Stacks.SheafPicardGroup.classOf_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SheafPicardGroup/Basic.lean, line 257. The attribute's comment: “addition is tensor product”.

Multiplication in the Picard group is tensor product, Stacks Tag 01CX.

theorem classOf_mul [IsInvertible 𝒪 h𝒪 L] [IsInvertible 𝒪 h𝒪 N] :
    classOf 𝒪 h𝒪 (L ⊗ N) = classOf 𝒪 h𝒪 L * classOf 𝒪 h𝒪 N

Stacks.SheafPicardGroup.classOf_tensorSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SheafPicardGroup/Basic.lean, line 264. The attribute's comment: “addition is tensor product”.

Multiplication in the Picard group is the tensor product sheaf, Stacks Tag 01CX in the spelling whose statement mentions no monoidal structure.

theorem classOf_tensorSheaf [IsInvertible 𝒪 h𝒪 L] [IsInvertible 𝒪 h𝒪 N]
    [IsInvertible 𝒪 h𝒪 ((((Stacks.SheafOfModules.Tensor.sheafTensor
      ⟨𝒪, Presheaf.isSheaf_of_isSheaf_comp _ (𝒪) (forget₂ CommRingCat RingCat) (h𝒪)⟩).obj (L)).obj
      (N)))] :
    classOf 𝒪 h𝒪 ((((Stacks.SheafOfModules.Tensor.sheafTensor
      ⟨𝒪, Presheaf.isSheaf_of_isSheaf_comp _ (𝒪) (forget₂ CommRingCat RingCat) (h𝒪)⟩).obj (L)).obj
      (N))) = classOf 𝒪 h𝒪 L * classOf 𝒪 h𝒪 N

Stacks.SheafPicardGroup.classOf_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SheafPicardGroup/Basic.lean, line 276. The attribute's comment: “abelian group structure”.

The neutral element of the Picard group is the class of the structure sheaf, Stacks Tag 01CX.

theorem classOf_unit :
    classOf 𝒪 h𝒪 (_root_.SheafOfModules.unit (structureSheaf 𝒪 h𝒪)) = 1

Stacks.SheafPicardGroup.classOf_tensorInv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SheafPicardGroup/Basic.lean, line 283. The attribute's comment: “abelian group structure”.

The inverse of a Picard class is the class of the inverse sheaf, Stacks Tag 01CT (2) read in the Picard group of Stacks Tag 01CX.

theorem classOf_tensorInv [IsInvertible 𝒪 h𝒪 L] :
    classOf 𝒪 h𝒪 (tensorInv 𝒪 h𝒪 L) = (classOf 𝒪 h𝒪 L)⁻¹

Stacks.SheafPicardGroup.classOf_tensorPow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SheafPicardGroup/Basic.lean, line 316. The attribute's comment: “addition is tensor product”.

The class of the n-th tensor power is the n-th power of the class, for every integer n. The powers are the integer tensor powers of Stacks Tag 01CU; this is the sense in which the Picard group records them.

theorem classOf_tensorPow [IsInvertible 𝒪 h𝒪 L] (n : ℤ) :
    classOf 𝒪 h𝒪 (tensorPow 𝒪 h𝒪 L n) = classOf 𝒪 h𝒪 L ^ n

Stacks.SheafPicardGroup.schemePicardGroup, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SheafPicardGroup/Scheme.lean, line 59. The attribute's comment: “the Picard group”. References: EGA 0 (5.4.7), “special case”; EGA IV (21.3.2); SGA 4 IX (3.3); SGA 4½ Arcata (2.2.3); SGA 6 X (5.1), “special case”.

The Picard group Pic X of a scheme: the isomorphism classes of invertible 𝒪_X-modules under tensor product.

noncomputable abbrev schemePicardGroup : Type (u + 1)

Stacks.SheafPicardGroup.schemeClassOf_eq_schemeClassOf_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SheafPicardGroup/Scheme.lean, line 71. The attribute's comment: “the Picard group”. References: EGA IV (21.3.2), “partial”.

Two invertible 𝒪_X-modules have the same Picard class exactly when they are isomorphic.

theorem schemeClassOf_eq_schemeClassOf_iff (L N : X.Modules)
    [Stacks.Ample.IsInvertibleModule X L] [Stacks.Ample.IsInvertibleModule X N] :
    schemeClassOf X L = schemeClassOf X N ↔ Nonempty (L ≅ N)

Stacks.SheafPicardGroup.schemeClassOf_tensorSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SheafPicardGroup/Scheme.lean, line 78. The attribute's comment: “addition is tensor product”.

Multiplication in Pic X is tensor product.

theorem schemeClassOf_tensorSheaf (L N : X.Modules)
    [Stacks.Ample.IsInvertibleModule X L] [Stacks.Ample.IsInvertibleModule X N]
    [Stacks.Ample.IsInvertibleModule X
      ((((Stacks.SheafOfModules.Tensor.sheafTensor ⟨X.presheaf,
        Presheaf.isSheaf_of_isSheaf_comp _ (X.presheaf) (forget₂ CommRingCat RingCat)
          ((Stacks.SheafInternalHom.isSheaf_structureRingPresheaf X))⟩).obj (L)).obj (N)))] :
    schemeClassOf X
        ((((Stacks.SheafOfModules.Tensor.sheafTensor ⟨X.presheaf,
          Presheaf.isSheaf_of_isSheaf_comp _ (X.presheaf) (forget₂ CommRingCat RingCat)
            ((Stacks.SheafInternalHom.isSheaf_structureRingPresheaf X))⟩).obj (L)).obj (N))) =
      schemeClassOf X L * schemeClassOf X N

Stacks.WeilCohomology.picardClassOf_tensorObjRingedSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/ChernClasses/InvertibleTensor.lean, line 68. The attribute's comment: “addition in Pic(X) is the tensor product, read at the spelling of the tensor product that the Grothendieck ring of Tag 0FDK multiplies with”.

Stacks Tag 01CX, addition in Pic(X) is the tensor product, at the spelling of the tensor product that K₀(Vect(X)) multiplies with.

theorem picardClassOf_tensorObjRingedSpace {X : Scheme.{u}} (L N : X.Modules)
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 L)
    (hN : AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2 N)
    (hLN : AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf X.ringCatSheaf.2
      (Scheme.Modules.tensorObjRingedSpace X L N)) :
    picardClassOf X (Scheme.Modules.tensorObjRingedSpace X L N) hLN =
      picardClassOf X L hL + picardClassOf X N hN

Tag 01CY, a lemma

Tag 01CY in the Stacks Project.

Stacks.SheafOfModules.isOpen_nonvanishingLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FinitePresentationStalk.lean, line 461. The attribute's comment: “openness”. References: EGA 0 (5.5.2).

Stacks Project, Tag 01CY (openness). For an invertible sheaf of modules on a ringed space all of whose stalks are local rings, the nonvanishing locus of a global section is open.

theorem isOpen_nonvanishingLocus
    (L : SheafOfModules.{u} (structureSheafRing X))
    [IsInvertible X.presheaf (structureSheafRing X).property L] (s : L.sections) :
    IsOpen (nonvanishingLocus L s)

Stacks.SheafOfModules.exists_tensorPairing_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InvertibleTrivialization.lean, line 298. The attribute's comment: “inverse section”.

Stacks Project, Tag 01CY (inverse section). Let L be an invertible sheaf of modules on a ringed space with local stalks, let N be a sheaf of modules with a trivialization ψ : L ⊗ N ≅ O_X, and let s be a global section of L. Then over the nonvanishing open X_s there is a section b of N with ψ (s ⊗ b) = 1.

Stacks states this for N = L^{⊗ -1}; see the implementation notes.

theorem exists_tensorPairing_eq_one
    [IsInvertible X.presheaf (structureSheafRing X).property L] (s : L.sections) :
    ∃ b : N.val.obj (op (nonvanishingOpen L s)),
      tensorPairing ψ (nonvanishingOpen L s) (s.eval (op (nonvanishingOpen L s))) b
        = unitSection X (nonvanishingOpen L s)

Stacks.InverseSection.exists_tensorInv_section_pairing_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InverseSection/Basic.lean, line 559. The attribute's comment: “inverse section”. References: EGA 0 (5.5.2), “(b) => (c)”.

Stacks Tag 01CY, the inverse-section clause, in the shape of the tagged statement: on the nonvanishing open of a global section s of an invertible module, there is a section t of the (-1)-st tensor power whose canonical tensor-power pairing with s evaluates to 1.

The pairing is the one the tagged statement names: form the elementary tensor of s, read in the first tensor power, with t; push it into the sheafified tensor product; apply the addition isomorphism of Stacks Tag 01CU in degrees 1 and -1; reindex along 1 + (-1) = 0. The tagged statement then compares the result with 1 directly, its zeroth tensor power being the unit of SheafOfModules on the nose; here the zeroth tensor power is the sheafified unit, so AlgebraicGeometry.SheafOfModules.tensorPowZeroIso is inserted, and only then is the comparison with 1 : 𝒪_X(X_s) a statement.

theorem exists_tensorInv_section_pairing_eq_one (s : L.sections) :
    ∃ t : (tensorPow X.sheaf.obj (structureSheaf X.sheaf).property L (-1)).val.obj
        (op (Stacks.NonvanishingTrivialize.nonvanishingOpen X L s)),
      (tensorPowZeroIso X.sheaf.obj (structureSheaf X.sheaf).property L).hom.val.app
        (op (Stacks.NonvanishingTrivialize.nonvanishingOpen X L s))
        ((tensorPowReindexIso X.sheaf.obj (structureSheaf X.sheaf).property L
            (show (1 : ℤ) + -1 = 0 by omega)).hom.val.app
          (op (Stacks.NonvanishingTrivialize.nonvanishingOpen X L s))
          ((tensorPowAddIsoSheaf X.sheaf.obj (structureSheaf X.sheaf).property L
              1 (-1)).hom.val.app
            (op (Stacks.NonvanishingTrivialize.nonvanishingOpen X L s))
            ((toSheafify X.sheaf.obj (structureSheaf X.sheaf).property
                ((PresheafOfModules.tensorObj (O := X.sheaf.obj) ((powPre L 1))
                  ((powPre L (-1)))))).app
              (op (Stacks.NonvanishingTrivialize.nonvanishingOpen X L s))
              ((tensorPowOneIso X.sheaf.obj (structureSheaf X.sheaf).property L).inv.val.app
                  (op (Stacks.NonvanishingTrivialize.nonvanishingOpen X L s))
                  (s.eval (op (Stacks.NonvanishingTrivialize.nonvanishingOpen X L s)))
                ⊗ₜ[X.presheaf.obj
                    (op (Stacks.NonvanishingTrivialize.nonvanishingOpen X L s))] t)))) =
      (1 : X.presheaf.obj
        (op (Stacks.NonvanishingTrivialize.nonvanishingOpen X L s)))

Stacks.SheafOfModules.isIso_over_nonvanishingOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NonvanishingTrivialization/Basic.lean, line 221. The attribute's comment: “trivialization”.

Stacks Project, Tag 01CY (trivialization). For an invertible sheaf of modules L on a ringed space all of whose stalks are local rings, and a global section s of L, the morphism 𝒪_X ⟶ L given by multiplication by s restricts to an isomorphism over the nonvanishing locus X_s.

theorem isIso_over_nonvanishingOpen (L : SheafOfModules.{u} (structureSheafRing X))
    [IsInvertible X.presheaf (structureSheafRing X).property L] (s : L.sections) :
    IsIso ((L.unitHomEquiv.symm s).over (nonvanishingOpen L s))

Tag 0H78, a remark

Tag 0H78 in the Stacks Project.

Stacks.NonvanishingPullback.preimage_nonvanishingLocus_lrs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NonvanishingPullback/LocallyRingedSpace.lean, line 97. References: EGA II (4.6.13.1), “more general”.

Stacks Tag 0H78. For a morphism of locally ringed spaces, the inverse image of the nonvanishing locus of a global section of a module is the nonvanishing locus of the pulled-back section.

theorem preimage_nonvanishingLocus_lrs (s : L.sections) :
    f.base ⁻¹' Stacks.NonvanishingTrivialize.nonvanishingLocus X.toRingedSpace L s =
      Stacks.NonvanishingTrivialize.nonvanishingLocus Y.toRingedSpace
        ((modulePullback f.toShHom).obj L) (pullbackSections f L s)

Stacks.SheafOfModules.preimage_nonvanishingLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PullbackSections/Nonvanishing.lean, line 165.

Stacks Project, Tag 0H78. For a morphism f : Y ⟶ X of locally ringed spaces and a global section s of a sheaf of 𝒪_X-modules L, the nonvanishing locus of the pullback of s is the preimage of the nonvanishing locus of s.

public theorem preimage_nonvanishingLocus (s : L.sections) :
    f.base ⁻¹' nonvanishingLocus (X := X.toRingedSpace) L s =
      nonvanishingLocus (X := Y.toRingedSpace)
        ((modulePullback f.toShHom).obj L) (modulePullbackSection f L s)

Sources

• Section 17.25, Tag 01CR
• AxiomMath/Stacks at 5ed82d14

LeanStacks.SheafOfModules.IsInvertible · AlgebraicGeometry.SheafOfModules.IsTrivial · Stacks.SheafOfModules.Invertible.tensorInverseIsoDualSheaf · Stacks.SheafOfModules.isInvertible_iff_exists_tensor_iso_unit · Stacks.SheafOfModules.Invertible.isInvertible_iff_exists_tensor_iso_unit · Stacks.SheafOfModules.LocallyFiniteFree.isLocallyFiniteFreeSummand_of_isInvertible · Stacks.RingedSpace.modulePullback_isInvertible · AlgebraicGeometry.Scheme.isInvertibleModule_pushforward_of_isIso

Section17.26 Rank and determinant#

Section 17.26 of the Stacks Project, Tag 0B37. 3 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0B37, the section

Tag 0B37 in the Stacks Project.

Stacks.SheafOfModules.rankDecomposition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RankDecomposition.lean, line 186. The attribute's comment: “the locally constant rank and the clopen rank decomposition X = X_0 ⊔ X_1 ⊔ … with E finite locally free of rank i on X_i; the exact category Vect(X) and its K-group, the rank homomorphism K_0(Vect(X)) → Map_cont(X, Z), the invertible sheaf det(E) and the homomorphism det : K_0(Vect(X)) → Pic(X) are not covered”. References: EGA 0 (5.4.1), “partial”.

Stacks Project, Tag 0B37: the rank decomposition. A finite locally free sheaf of modules E on a ringed space whose structure stalks are all nonzero has locally constant rank, so the loci X_i where the rank is i are open and closed, pairwise disjoint and cover X, and E is finite locally free of rank i on X_i.

theorem rankDecomposition :
    IsLocallyConstant (⇑(finiteLocallyFreeRank F hO)) ∧
      (∀ i : ℕ, IsClopen (rankStratum F hO i : Set X)) ∧
      Pairwise (Function.onFun Disjoint fun i : ℕ => (rankStratum F hO i : Set X)) ∧
      (⨆ i : ℕ, rankStratum F hO i) = ⊤ ∧
      ∀ (i : ℕ) (x : X), x ∈ rankStratum F hO i →
        ∃ (V : Opens X) (_ : x ∈ V) (_ : V ≤ rankStratum F hO i) (I : Type u),
          Nonempty (I ≃ Fin i) ∧ Nonempty (_root_.SheafOfModules.free.{u} I ≅ F.over V)

Tag 0B38, a lemma

Tag 0B38 in the Stacks Project.

Stacks.SheafOfModules.TopWedge.detSummandComparison_ι_unit_wedge, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExteriorAnnihilatorShortExactIso.lean, line 591. The attribute's comment: “the WEDGE-AND-LIFT FORMULA in the GENERAL case, with no constant-rank hypothesis”.

The wedge-and-lift formula for the comparison between determinant summands, in every pair of degrees, read inside ⋀ⁿ⁺ᵐ E through the inclusion of the degree-n+m summand of det(E).

This is the wedge-and-lift formula of [Stacks, Tag 0B38] in the general case: a short exact sequence of finite locally free sheaves with no constant-rank hypothesis. On the summand det(E')ₙ ⊗ det(E'')ₘ of det(E') ⊗ det(E'') the canonical map of Stacks.SheafOfModules.TopWedge.determinantTensorDeterminantHom carries the image of (s₁∧⋯∧sₙ) ⊗ (g(l₁)∧⋯∧g(lₘ)) to f(s₁)∧⋯∧f(sₙ)∧l₁∧⋯∧lₘ, for arbitrary local lifts lⱼ. This is the formula the source gives for its canonical map, and Stacks.SheafOfModules.TopWedge.eq_determinantTensorDeterminantHom and Stacks.SheafOfModules.TopWedge.eq_detTensorAnnComparison say it determines the map.

theorem detSummandComparison_ι_unit_wedge
    (hS : (ShortComplex.mk f g hfg).Exact) [Mono f] [Epi g]
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E']
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E''] (n m : ℕ)
    (V : (Opens ↥X)ᵒᵖ)
    (w : ToType ((A'.exteriorAnnihilator n).toSheafOfModules.val.obj V))
    (s : Fin n → E'.val.obj V)
    (hw : (A'.exteriorAnnihilator n).ι.val.app V w = wedgeSec A' V n s)
    (z : ToType ((A''.exteriorAnnihilator m).toSheafOfModules.val.obj V))
    (l : Fin m → E.val.obj V)
    (hz : (A''.exteriorAnnihilator m).ι.val.app V z =
      wedgeSec A'' V m fun i => g.val.app V (l i)) :
    (detSummandComparison A' A A'' f g hfg hS n m ≫
          (A.exteriorAnnihilator (n + m)).ι).val.app V
        ((PresheafOfModules.tensorSheafUnit (A'.exteriorAnnihilator n).toSheafOfModules
          (A''.exteriorAnnihilator m).toSheafOfModules).app V (w ⊗ₜ z)) =
      wedgeSec A V (n + m) (Fin.append (fun i => f.val.app V (s i)) l)

Stacks.SheafOfModules.TopWedge.isIso_determinantTensorDeterminantHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExteriorAnnihilatorShortExactIso.lean, line 990. The attribute's comment: “the ISOMORPHISM clause in the GENERAL case: the canonical map det(E')⊗det(E'')⟶det(E) of Stacks.SheafOfModules.TopWedge.determinantTensorDeterminantHom is an isomorphism, for a short exact sequence of finite locally free sheaves with NO constant-rank hypothesis. Here det is the det of 0FJN. The isomorphism itself is determinantTensorDeterminantIsoOfFiniteLocallyFree”.

Stacks 0B38: the canonical map det(E') ⊗ det(E'') ⟶ det(E) is an isomorphism, for a short exact sequence 0 → E' → E → E'' → 0 of sheaves of modules on a ringed space whose outer terms are finite locally free of no particular rank.

theorem isIso_determinantTensorDeterminantHom
    (hS : (ShortComplex.mk f g hfg).Exact) [Mono f] [Epi g]
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E']
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E''] :
    IsIso (determinantTensorDeterminantHom A' A A'' f g hfg hS)

Stacks.SheafOfModules.TopWedge.eq_determinantTensorDeterminantHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExteriorAnnihilatorShortExactIso.lean, line 1035. The attribute's comment: “uniqueness of the canonical map det(E')⊗det(E'')⟶det(E) in the GENERAL case — a short exact sequence of finite locally free sheaves of modules with no constant-rank hypothesis. Together with eq_detTensorAnnComparison and the wedge-and-lift formula detSummandComparison_ι_unit_wedge this says the map is determined by the formula the source gives for it”.

The canonical map is the only morphism restricting to Stacks.SheafOfModules.TopWedge.detTensorAnnComparison on every degree-m summand of det(E''). Together with Stacks.SheafOfModules.TopWedge.eq_detTensorAnnComparison and the wedge-and-lift formula Stacks.SheafOfModules.TopWedge.detSummandComparison_ι_unit_wedge this is the precise sense in which the map of [Stacks, Tag 0B38] is canonical.

theorem eq_determinantTensorDeterminantHom
    (hS : (ShortComplex.mk f g hfg).Exact) [Mono f] [Epi g]
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E']
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E'']
    (ψ : ((Stacks.SheafOfModules.Tensor.sheafTensor Osharp).obj A'.determinant).obj A''.determinant
        ⟶ A.determinant)
    (hψ : ∀ m : ℕ, (Stacks.SheafOfModules.TensorLocalProperties.tensorSheafRight
            (Opens.grothendieckTopology ↥X) Osharp A'.determinant).map
          (Limits.Sigma.ι (fun j : ℕ => (A''.exteriorAnnihilator j).toSheafOfModules) m) ≫ ψ =
        detTensorAnnComparison A' A A'' f g hfg hS m) :
    ψ = determinantTensorDeterminantHom A' A A'' f g hfg hS

Stacks.SheafOfModules.TopWedge.determinantTensorDeterminantIsoOfFiniteLocallyFree, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExteriorAnnihilatorShortExactIso.lean, line 1072. The attribute's comment: “the canonical isomorphism det(E')⊗det(E'')≅det(E) in the GENERAL case, with NO constant-rank hypothesis”. References: SGA 6 X (5.1), “special case”.

Stacks 0B38, the general case. For a short exact sequence 0 → E' → E → E'' → 0 of sheaves of O_X-modules on a ringed space with E' and E'' finite locally free of no particular rank, there is a canonical isomorphism

det(E') ⊗_{O_X} det(E'') ≅ det(E)

of the determinants of [Stacks, Tag 0FJN] — the annihilator of the degree-one part of the exterior algebra.

The underlying map is Stacks.SheafOfModules.TopWedge.determinantTensorDeterminantHom, which Stacks.SheafOfModules.TopWedge.detSummandComparison_ι_unit_wedge pins to the wedge-and-lift formula the source gives for it, which the uniqueness statements Stacks.SheafOfModules.TopWedge.eq_determinantTensorDeterminantHom and Stacks.SheafOfModules.TopWedge.eq_detTensorAnnComparison show that formula determines, and which Stacks.SheafOfModules.TopWedge.isIso_determinantTensorDeterminantHom shows is an isomorphism.

No hypothesis on E is needed: the freeness of its stalks is derived from the split stalk sequence, so the statement is a strengthening of the one in the source, which assumes all three terms finite locally free.

noncomputable def determinantTensorDeterminantIsoOfFiniteLocallyFree
    (hS : (ShortComplex.mk f g hfg).Exact) [Mono f] [Epi g]
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E']
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E''] :
    ((Stacks.SheafOfModules.Tensor.sheafTensor Osharp).obj A'.determinant).obj A''.determinant ≅
        A.determinant

Stacks.SheafOfModules.TopWedge.determinantTensorDeterminantHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExteriorAnnihilatorShortExactSummand.lean, line 713. The attribute's comment: “the canonical MAP det(E')⊗det(E'')⟶det(E) in the GENERAL case, with NO constant-rank hypothesis”.

The canonical map det(E') ⊗ det(E'') ⟶ det(E) of [Stacks, Tag 0B38], for a short exact sequence 0 → E' → E → E'' → 0 of sheaves of modules on a ringed space with E' and E'' finite locally free of NO PARTICULAR RANK.

The determinant of [Stacks, Tag 0FJN] is the coproduct over the degrees of the degreewise annihilators of the degree-one part of the exterior algebra, and the tensor product of sheaves of modules preserves coproducts in each variable, so a map out of det(E') ⊗ det(E'') is the same thing as a family of maps det(E')ₙ ⊗ det(E'')ₘ ⟶ det(E). This is the family obtained from Stacks.SheafOfModules.TopWedge.detSummandComparison followed by the inclusion of the degree-n+m summand of det(E).

That this map is an isomorphism is Stacks.SheafOfModules.TopWedge.isIso_determinantTensorDeterminantHom, the isomorphism itself is Stacks.SheafOfModules.TopWedge.determinantTensorDeterminantIsoOfFiniteLocallyFree, and the wedge-and-lift formula pinning it is Stacks.SheafOfModules.TopWedge.detSummandComparison_ι_unit_wedge — all three in StacksFrontier.Algebra.Category.ModuleCat.Sheaf.ExteriorAnnihilatorShortExactIso.

noncomputable def determinantTensorDeterminantHom [Mono f] [Epi g]
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E']
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E''] :
    ((Stacks.SheafOfModules.Tensor.sheafTensor Osharp).obj A'.determinant).obj A''.determinant ⟶
        A.determinant

Stacks.SheafOfModules.TopWedge.determinantTensorDeterminantIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExteriorDeterminantShortExactIso.lean, line 93. The attribute's comment: “the canonical isomorphism det(E')⊗det(E'')≅det(E) in DETERMINANT form, for a short exact sequence of finite locally free sheaves of CONSTANT rank”. References: SGA 6 X (5.1), “special case”; SGA 6 X (6.2.7), “special case”.

Stacks 0B38 in determinant form, at constant rank. For a short exact sequence 0 → E' → E → E'' → 0 of sheaves of modules on a ringed space, with E', E'' and E finite locally free of constant ranks r', k + 1 and r' + k + 1, there is a canonical isomorphism det(E') ⊗ det(E'') ≅ det(E) of the determinants of [Stacks, Tag 0FJN] — the annihilator of the degree-one part of the exterior algebra.

It is the comparison of top exterior powers of Stacks.SheafOfModules.TopWedge.detComparison, which Stacks.SheafOfModules.TopWedge.isIso_detComparison shows is an isomorphism, conjugated by the identifications ⋀ʳ F ≅ det(F) of [Stacks, Tag 0B37]. The map is pinned by Stacks.SheafOfModules.TopWedge.determinantTensorDeterminantIso_hom to that top-exterior-power comparison, which Stacks.SheafOfModules.TopWedge.detComparison_wedge in turn pins to the wedge-and-lift formula of the source.

This is the CONSTANT-RANK form of the tag. The general case, where the ranks are only locally constant, is carried by Stacks.SheafOfModules.TopWedge.determinantTensorDeterminantIsoOfFiniteLocallyFree in StacksFrontier.Algebra.Category.ModuleCat.Sheaf.ExteriorAnnihilatorShortExactIso.

noncomputable def determinantTensorDeterminantIso
    (A' : _root_.SheafOfModules.TensorExteriorSymmetricAlgebras
      (Opens.grothendieckTopology ↥X) E')
    (A : _root_.SheafOfModules.TensorExteriorSymmetricAlgebras
      (Opens.grothendieckTopology ↥X) E)
    (A'' : _root_.SheafOfModules.TensorExteriorSymmetricAlgebras
      (Opens.grothendieckTopology ↥X) E'')
    (f : E' ⟶ E) (g : E ⟶ E'') (hfg : f ≫ g = 0)
    (hS : (ShortComplex.mk f g hfg).Exact) [Mono f] [Epi g] (r' k : ℕ)
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E' r']
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E'' (k + 1)]
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E (r' + (k + 1))] :
    ((Stacks.SheafOfModules.Tensor.sheafTensor Osharp).obj A'.determinant).obj A''.determinant ≅
        A.determinant

Stacks.SheafOfModules.TopWedge.detComparison_wedge, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExteriorPowerShortExact.lean, line 780. The attribute's comment: “the CONSTANT-RANK form of the canonical map det(E')⊗det(E'')⟶det(E) and of its wedge-and-lift formula”.

Stacks 0B38, the wedge-and-lift formula. The canonical comparison carries the image of (s₁ ∧ ⋯ ∧ s_{r'}) ⊗ (g(l₁) ∧ ⋯ ∧ g(l_{k+1})) to f(s₁) ∧ ⋯ ∧ f(s_{r'}) ∧ l₁ ∧ ⋯ ∧ l_{k+1}: the wedge of the images of the sections of E' with arbitrary local lifts lⱼ of the sections of E''. This equation is the one the source gives for its canonical map, and it determines the comparison, since the wedges of local sections generate the exterior powers locally.

Here det is the top exterior power, which SheafOfModules.TensorExteriorSymmetricAlgebras.determinantIsoExteriorPower identifies with the det of [Stacks, Tag 0FJN] at constant rank; what is carried here is E' of constant rank r' and E'' of constant rank r'' = k + 1. The ISOMORPHISM clause of the tag is carried separately by Stacks.SheafOfModules.TopWedge.isIso_detComparison.

This is the CONSTANT-RANK form of the tag. The general case — a short exact sequence of finite locally free sheaves with no constant-rank hypothesis — is carried by Stacks.SheafOfModules.TopWedge.detSummandComparison_ι_unit_wedge and Stacks.SheafOfModules.TopWedge.determinantTensorDeterminantIsoOfFiniteLocallyFree in StacksFrontier.Algebra.Category.ModuleCat.Sheaf.ExteriorAnnihilatorShortExactIso.

theorem detComparison_wedge [Epi g]
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E' r']
    (V : (Opens ↥X)ᵒᵖ) (s : Fin r' → E'.val.obj V) (l : Fin (k + 1) → E.val.obj V) :
    (detComparison A' A A'' f g hfg hS r' k).val.app V
        ((PresheafOfModules.tensorSheafUnit (A'.exteriorPower r')
            (A''.exteriorPower (k + 1))).app V
          (wedgeSec A' V r' s ⊗ₜ wedgeSec A'' V (k + 1) fun i => g.val.app V (l i))) =
      wedgeSec A V (r' + (k + 1)) (Fin.append (fun i => f.val.app V (s i)) l)

Stacks.SheafOfModules.TopWedge.eq_detComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExteriorPowerShortExact.lean, line 807. The attribute's comment: “uniqueness of the map satisfying the wedge-and-lift formula, which is the precise sense of CANONICAL here — again in the constant-rank form, with the same carried hypotheses as detComparison_wedge; the isomorphism clause is carried by Stacks.SheafOfModules.TopWedge.isIso_detComparison, and the general case by Stacks.SheafOfModules.TopWedge.eq_determinantTensorDeterminantHom”.

The canonical comparison is the only morphism satisfying its defining equation. The morphism ⋀ʳ' E' ⊗ ⋀ᵏ⁺¹(g) is an epimorphism, so a morphism out of ⋀ʳ' E' ⊗ ⋀ᵏ⁺¹ E'' is determined by its composite with it.

theorem eq_detComparison [Epi g]
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E' r']
    (ψ : ((Stacks.SheafOfModules.Tensor.sheafTensor.{_, _, _, u, u} Osharp).obj (A'.exteriorPower
        r')).obj
        (A''.exteriorPower (k + 1)) ⟶
      A.exteriorPower (r' + (k + 1)))
    (hψ : ((Stacks.SheafOfModules.Tensor.sheafTensor.{_, _, _, u, u} Osharp).obj
      (A'.exteriorPower r')).map ((extHom A A'' g).app ((k + 1 : ℕ) : ℤ)) ≫ ψ =
      wedgeHom A' A f r' (k + 1)) :
    ψ = detComparison A' A A'' f g hfg hS r' k

Stacks.SheafOfModules.TopWedge.isIso_detComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExteriorPowerShortExactIso.lean, line 432. The attribute's comment: “the ISOMORPHISM clause, in the constant-rank form”. References: SGA 6 X (5.1), “special case”; SGA 6 X (6.2.7), “(6.2.9), special case”.

Stacks 0B38, the isomorphism clause in the constant-rank form. For a short exact sequence 0 → E' → E → E'' → 0 of sheaves of modules on a ringed space with E' finite locally free of constant rank r' and E'' finite locally free of constant rank k + 1, the canonical comparison ⋀^{r'} E' ⊗ ⋀^{k+1} E'' ⟶ ⋀^{r'+k+1} E is an isomorphism.

The canonical map det(E') ⊗ det(E'') ⟶ det(E) shown invertible here is Stacks.SheafOfModules.TopWedge.detComparison. Here det is the top exterior power, identified with the det of [Stacks, Tag 0FJN] at constant rank by SheafOfModules.TensorExteriorSymmetricAlgebras.determinantIsoExteriorPower; what is carried here is E' of constant rank r' and E'' of constant rank r'' = k + 1.

This is the CONSTANT-RANK form of the tag. The general case — a short exact sequence of finite locally free sheaves with no constant-rank hypothesis — is carried by Stacks.SheafOfModules.TopWedge.isIso_determinantTensorDeterminantHom and Stacks.SheafOfModules.TopWedge.determinantTensorDeterminantIsoOfFiniteLocallyFree in StacksFrontier.Algebra.Category.ModuleCat.Sheaf.ExteriorAnnihilatorShortExactIso.

theorem isIso_detComparison
    (A' : _root_.SheafOfModules.TensorExteriorSymmetricAlgebras
      (Opens.grothendieckTopology ↥X) E')
    (A : _root_.SheafOfModules.TensorExteriorSymmetricAlgebras
      (Opens.grothendieckTopology ↥X) E)
    (A'' : _root_.SheafOfModules.TensorExteriorSymmetricAlgebras
      (Opens.grothendieckTopology ↥X) E'')
    (f : E' ⟶ E) (g : E ⟶ E'') (hfg : f ≫ g = 0)
    (hS : (ShortComplex.mk f g hfg).Exact) [Mono f] [Epi g] (r' k : ℕ)
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E' r']
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E'' (k + 1)] :
    IsIso (detComparison A' A A'' f g hfg hS r' k)

Tag 0FJN, a lemma

Tag 0FJN in the Stacks Project.

SheafOfModules.TensorExteriorSymmetricAlgebras.determinant_isInvertible_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DeterminantFinitePresentationFlat.lean, line 329. The attribute's comment: “flatness and finite presentation of F are its only hypotheses on F, which is what the source assumes, and it carries no hypothesis about det(F)”. References: SGA 3 XV (5.7), “partial”.

[Stacks, Tag 0FJN]. The determinant of a flat sheaf of modules of finite presentation on a ringed space is an invertible module.

Its hypotheses on F are exactly the source's: F is flat, in the sense AlgebraicGeometry.SheafOfModules.IsFlat that the source assumes, and of finite presentation. Nothing is assumed about det(F). Three statements stand behind it, each proved in this repository: every stalk of det(F) is an invertible module (SheafOfModules.TensorExteriorSymmetricAlgebras.determinant_stalk_invertible, with Tag 05NE turning flatness of the sheaf into flatness of the stalks); det(F) is of finite presentation (isFinitePresentation_determinant_of_isFlat above); and invertibility descends from the stalks for a sheaf of modules of finite presentation (Stacks.SheafOfModules.stalkwiseInvertibleDescent).

This is the whole covering set of Tag 0FJN. The two other statements of the tag's conclusion — determinant_isInvertible in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExteriorAlgebraDeterminant.lean and determinant_isInvertible_of_finitePresentationDescent in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExteriorAnnihilatorStalk.lean — assume more than this one and do not carry the attribute.

The statement lives here rather than beside determinant_stalk_invertible_of_isFlat, which is where it was while the finite presentation of det(F) was a hypothesis, because StacksFrontier.Algebra.Category.ModuleCat.Sheaf.ExteriorDeterminantInvertible cannot import the file that proves that finite presentation: the closure of StacksFrontier.Algebra.Category.ModuleCat.Sheaf.ExteriorPowerShortExact, which this file needs through the two retract conditions, makes HasCoproduct unsynthesizable in the coproduct section of that file, where a family of sheaves of modules on a space is summed. That is a pre-existing incompatibility between those two files and has nothing to do with the determinant; it is recorded here because it is the reason for the split.

theorem determinant_isInvertible_of_isFlat {Y : RingedSpace.{u, u}}
    (G : SheafOfModules.{u} (structureSheafRing Y)) [G.IsFinitePresentation]
    (A : TensorExteriorSymmetricAlgebras (Opens.grothendieckTopology Y.carrier) G)
    (hflat : AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u} (O := Y.sheaf) G) :
    AlgebraicGeometry.SheafOfModules.IsInvertible Y.presheaf
      (Presheaf.isSheaf_comp_of_isSheaf _ Y.presheaf
        (forget₂ CommRingCat.{u} RingCat.{u}) Y.IsSheaf) A.determinant

Sources

• Section 17.26, Tag 0B37
• AxiomMath/Stacks at 5ed82d14

LeanStacks.SheafOfModules.rankDecomposition · Stacks.SheafOfModules.TopWedge.detSummandComparison_ι_unit_wedge · Stacks.SheafOfModules.TopWedge.isIso_determinantTensorDeterminantHom · Stacks.SheafOfModules.TopWedge.eq_determinantTensorDeterminantHom · Stacks.SheafOfModules.TopWedge.determinantTensorDeterminantIsoOfFiniteLocallyFree · Stacks.SheafOfModules.TopWedge.determinantTensorDeterminantHom · Stacks.SheafOfModules.TopWedge.determinantTensorDeterminantIso · Stacks.SheafOfModules.TopWedge.detComparison_wedge

Section17.27 Localizing sheaves of rings#

Section 17.27 of the Stacks Project, Tag 01CZ. 2 tags here are carried by 7 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01D0, a lemma

Tag 01D0 in the Stacks Project.

Stacks.Presheaf.Localization.isLocalization_stalk_localizationSheaf, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Presheaf/LocalizationStalk.lean, line 177. The attribute's comment: “sheaf_localization_stalk”.

At every point, the stalk of the sheafification of the sectionwise localization is the localization of the original stalk at the germs of the prescribed denominators.

lemma isLocalization_stalk_localizationSheaf (D : PresheafLocalizationData.{u}) (x : D.X) :
    letI : Algebra (D.O.stalk x) ((localizationSheaf D).presheaf.stalk x) :=
      (toLocalizationSheafStalk D x).hom.toAlgebra
    IsLocalization (D.S.stalk x) ((localizationSheaf D).presheaf.stalk x)

Stacks.Presheaf.Localization.existsUnique_lift_localizationPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Presheaf/LocalizationUniversalProperty.lean, line 80. The attribute's comment: “presheaf_universal_property”. References: EGA 0 (1.2.4), “more general”.

Stacks 01D0. A morphism of presheaves of commutative rings which inverts every section of the multiplicative subpresheaf S factors uniquely through the sectionwise localization at S.

theorem existsUnique_lift_localizationPresheaf (S : O.SubmonoidPresheaf) (f : O ⟶ A)
    (hf : ∀ (U : (Opens X)ᵒᵖ) (s : S.obj U), IsUnit ((f.app U).hom (s : O.obj U))) :
    ∃! g : S.localizationPresheaf ⟶ A, S.toLocalizationPresheaf ≫ g = f

Stacks.Presheaf.Localization.toLocalizationSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Presheaf/LocalizationUniversalProperty.lean, line 112. The attribute's comment: “sheaf_universal_property”.

The canonical map from the sheafification of a presheaf of commutative rings to the sheafification of its sectionwise localization.

noncomputable def toLocalizationSheaf (S : O.SubmonoidPresheaf) :
    (presheafToSheaf (Opens.grothendieckTopology X) CommRingCat.{u}).obj O ⟶
      (presheafToSheaf (Opens.grothendieckTopology X) CommRingCat.{u}).obj
        S.localizationPresheaf

Stacks.Presheaf.Localization.isUnit_toLocalizationSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Presheaf/LocalizationUniversalProperty.lean, line 130. The attribute's comment: “sheaf_universal_property”.

Stacks 01D0. Every prescribed local denominator becomes invertible in the sheafified localization.

theorem isUnit_toLocalizationSheaf (S : O.SubmonoidPresheaf) (U : (Opens X)ᵒᵖ) (s : S.obj U) :
    IsUnit (((toLocalizationSheaf S).hom.app U).hom
      (((toSheafify (Opens.grothendieckTopology X) O).app U).hom (s : O.obj U)))

Stacks.Presheaf.Localization.existsUnique_lift_localizationSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Presheaf/LocalizationUniversalProperty.lean, line 140. The attribute's comment: “sheaf_universal_property”.

Stacks 01D0. A morphism out of the sheafification of O which inverts every prescribed section factors uniquely through the sheafified localization.

theorem existsUnique_lift_localizationSheaf (S : O.SubmonoidPresheaf) (A : X.Sheaf CommRingCat.{u})
    (f : (presheafToSheaf (Opens.grothendieckTopology X) CommRingCat.{u}).obj O ⟶ A)
    (hf : ∀ (U : (Opens X)ᵒᵖ) (s : S.obj U),
      IsUnit ((f.hom.app U).hom
        (((toSheafify (Opens.grothendieckTopology X) O).app U).hom (s : O.obj U)))) :
    ∃! g : (presheafToSheaf (Opens.grothendieckTopology X) CommRingCat.{u}).obj
        S.localizationPresheaf ⟶ A,
      toLocalizationSheaf S ≫ g = f

Declarations registered for the tag:

• Stacks.Presheaf.Localization.localizationPresheaf_stalk_isLocalization, declared in the repository, registered with add_to_stacks in StacksFrontier/Topology/Sheaves/Presheaf/LocalizationStalk.lean, line 202 (StacksFrontier): “presheaf_localization_stalk: the stalk of the localization presheaf”.
• TopCat.Presheaf.SubmonoidPresheaf.toLocalizationPresheaf registered with add_to_stacks in StacksFrontier/Topology/Sheaves/Presheaf/LocalizationUniversalProperty.lean, line 168 (StacksFrontier): “localization_map: the canonical morphism to the sectionwise localization”.
• IsLocalization.map_units registered with add_to_stacks in StacksFrontier/Topology/Sheaves/Presheaf/LocalizationUniversalProperty.lean, line 170 (StacksFrontier): “localization_map: every prescribed section becomes a unit”.

Tag 01D1, a lemma

Tag 01D1 in the Stacks Project.

Stacks.Presheaf.Localization.sectionwiseLocalizedModuleIsoTensor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Presheaf/LocalizationModule.lean, line 245. The attribute's comment: “presheaf assertion”.

Stacks Project, Tag 01D1, presheaf assertion.

Any sectionwise localization of a presheaf of modules is canonically isomorphic to extension of scalars from the original presheaf of rings to its sectionwise localization.

noncomputable def sectionwiseLocalizedModuleIsoTensor
    (O Oₛ : TopCat.Presheaf CommRingCat X) (α : O ⟶ Oₛ)
    (S : (U : (TopologicalSpace.Opens X)ᵒᵖ) → Submonoid (O.obj U))
    (F : PresheafOfModules.{0} (ringPresheaf O))
    (Fₛ : PresheafOfModules.{0} (ringPresheaf Oₛ))
    (ι : F ⟶ Stacks.Sheafify.ChangeOfRingsAdjunction.restrictPresheaf O Oₛ α Fₛ)
    (hO : IsSectionwiseLocalization O Oₛ α S)
    (hF : IsSectionwiseLocalizedModule O Oₛ α S F Fₛ ι) :
    Fₛ ≅ tensorPresheafOfModules O Oₛ α F

Stacks.Presheaf.Localization.sheafificationSectionwiseLocalizedModuleIsoTensor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Presheaf/LocalizationModule.lean, line 295. The attribute's comment: “sheaf assertion”.

Stacks Project, Tag 01D1, sheaf assertion.

If O and F are sheaves, sheafifying a sectionwise localization Fₛ along a sheafification Oₛ ⟶ Oₛ♯ gives the tensor product of F with Oₛ♯ over O.

noncomputable def sheafificationSectionwiseLocalizedModuleIsoTensor
    (O : TopCat.Sheaf CommRingCat X) (Oₛ : TopCat.Presheaf CommRingCat X)
    (Oₛ' : TopCat.Sheaf CommRingCat X) (α : O.presheaf ⟶ Oₛ) (σ : Oₛ ⟶ Oₛ'.presheaf)
    (S : (U : (TopologicalSpace.Opens X)ᵒᵖ) → Submonoid (O.presheaf.obj U))
    (F : SheafOfModules (ringSheaf O))
    (Fₛ : PresheafOfModules (ringPresheaf Oₛ))
    (ι : F.val ⟶ Stacks.Sheafify.ChangeOfRingsAdjunction.restrictPresheaf O.presheaf Oₛ α Fₛ)
    (hO : IsSectionwiseLocalization O.presheaf Oₛ α S)
    (hF : IsSectionwiseLocalizedModule O.presheaf Oₛ α S F.val Fₛ ι)
    (hσi : Presheaf.IsLocallyInjective (Opens.grothendieckTopology X)
      (Stacks.Sheafify.ChangeOfRingsAdjunction.ringPresheafMap Oₛ Oₛ'.presheaf σ))
    (hσs : Presheaf.IsLocallySurjective (Opens.grothendieckTopology X)
      (Stacks.Sheafify.ChangeOfRingsAdjunction.ringPresheafMap Oₛ Oₛ'.presheaf σ)) :
    (moduleSheafificationAlong (Stacks.Sheafify.ChangeOfRingsAdjunction.ringPresheafMap Oₛ
      Oₛ'.presheaf σ) hσi hσs).obj Fₛ ≅
      tensorSheaf O Oₛ'
        ((fullyFaithfulSheafToPresheaf (Opens.grothendieckTopology X) CommRingCat).homEquiv.symm
          (α ≫ σ)) F

Sources

• Section 17.27, Tag 01CZ
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Presheaf.Localization.isLocalization_stalk_localizationSheaf · Stacks.Presheaf.Localization.existsUnique_lift_localizationPresheaf · Stacks.Presheaf.Localization.toLocalizationSheaf · Stacks.Presheaf.Localization.isUnit_toLocalizationSheaf · Stacks.Presheaf.Localization.existsUnique_lift_localizationSheaf · Stacks.Presheaf.Localization.localizationPresheaf_stalk_isLocalization · TopCat.Presheaf.SubmonoidPresheaf.toLocalizationPresheaf · IsLocalization.map_units

Section17.28 Modules of differentials#

Section 17.28 of the Stacks Project, Tag 08RL. 14 tags here are carried by 37 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01UN, a definition

Tag 01UN in the Stacks Project.

Declarations registered for the tag:

• PresheafOfModulesOfCommRing.Derivation' registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch17.lean, line 61 (StacksFrontier): “for presheaves of modules over any category; Stacks' sheaf case is F.val.Derivation' φ.hom”. References: EGA IV (16.5.1), “more general”.
• PresheafOfModulesOfCommRing.Derivation registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch17.lean, line 64 (StacksFrontier): “the structure: additive on sections, compatible with restriction, Leibniz rule, kills the image of φ”.

Tag 08RM, a lemma

Tag 08RM in the Stacks Project.

AlgebraicGeometry.SheafOfModules.universalDerivation_isUniversal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/Differentials.lean, line 130. References: EGA IV (16.5.3), “(ii)”.

Stacks Project, Tag 08RM. Postcomposition with the universal derivation gives the unique morphism from the module of relative differentials to any coefficient sheaf.

theorem universalDerivation_isUniversal {X : TopCat.{u}}
    {O₁ O₂ : TopCat.Sheaf CommRingCat.{max u v} X} (φ : O₁ ⟶ O₂) :
    IsUniversal.{u, v, u_1} (universalDerivation.{u, v, u_1} φ)

Tag 08RP, a definition

Tag 08RP in the Stacks Project.

AlgebraicGeometry.SheafOfModules.moduleOfDifferentials, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/Differentials.lean, line 111. The attribute's comment: “the module of differentials”.

The sheaf of relative differentials representing derivations along φ.

noncomputable def moduleOfDifferentials {X : TopCat.{u}}
    {O₁ O₂ : TopCat.Sheaf CommRingCat.{max u v} X} (φ : O₁ ⟶ O₂) :
    _root_.SheafOfModules.{max u v w} (underlyingRingSheaf O₂)

AlgebraicGeometry.SheafOfModules.universalDerivation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/Differentials.lean, line 118. The attribute's comment: “the module of differentials”. References: EGA IV (16.3.6), “dt”; EGA IV (16.5.3), “(i)”.

The universal relative derivation into moduleOfDifferentials φ.

noncomputable def universalDerivation {X : TopCat.{u}}
    {O₁ O₂ : TopCat.Sheaf CommRingCat.{max u v} X} (φ : O₁ ⟶ O₂) :
    SheafDerivation.{u, v, u_1} φ (moduleOfDifferentials.{u, v, u_1} φ)

Tag 08TD, a lemma

Tag 08TD in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.SheafOfModules.moduleOfDifferentialsIsoSectionwise, declared in the repository, registered with add_to_stacks in StacksFrontier/Topology/Sheaves/Modules/Differentials/Stalk.lean, line 89 (StacksFrontier).

Tag 08RQ, a lemma

Tag 08RQ in the Stacks Project.

AlgebraicGeometry.SheafOfModules.pullbackDifferentialsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/Differentials/InverseImage.lean, line 559. The attribute's comment: “the open-inclusion case: the identification of the restriction of the”.

The canonical identification between the inverse image of the module of relative differentials and the module of relative differentials of the inverse-image morphism.

noncomputable def pullbackDifferentialsIso (phi : O₁ ⟶ O₂) :
    inverseImageModule f O₂ (moduleOfDifferentials phi) ≅
      moduleOfDifferentials ((TopCat.Sheaf.pullback CommRingCat.{u} f).map phi)

Tag 08RR, a lemma

Tag 08RR in the Stacks Project.

AlgebraicGeometry.SheafOfModules.inverseImageDerivation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/Differentials/InverseImage.lean, line 456. The attribute's comment: “inverse image of the derivation”.

The inverse image of a relative derivation, specified by its action on the images of local sections under the inverse-image units.

noncomputable def inverseImageDerivation
    {M : _root_.SheafOfModules.{u} (underlyingRingSheaf O₂)}
    (d : SheafDerivation phi M) :
    {δ : SheafDerivation ((TopCat.Sheaf.pullback CommRingCat.{u} f).map phi)
        (inverseImageModule f O₂ M) //
      ∀ (U : (Opens X)ᵒᵖ) (b : O₂.obj.obj U),
        δ.d (((inverseImageRingHom f O₂).hom.app U) b) =
          ((inverseImageModuleUnit f O₂ M).val.app U).hom (d.d b)}

AlgebraicGeometry.SheafOfModules.inverseImageDerivation_isUniversal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/Differentials/InverseImage.lean, line 483. The attribute's comment: “universality”.

The inverse image of the universal derivation remains universal.

theorem inverseImageDerivation_isUniversal (phi : O₁ ⟶ O₂) :
    IsUniversal (inverseImageDerivation f (universalDerivation phi)).val

AlgebraicGeometry.SheafOfModules.pullbackDifferentialsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/Differentials/InverseImage.lean, line 559. The attribute's comment: “canonical identification”.

The canonical identification between the inverse image of the module of relative differentials and the module of relative differentials of the inverse-image morphism.

noncomputable def pullbackDifferentialsIso (phi : O₁ ⟶ O₂) :
    inverseImageModule f O₂ (moduleOfDifferentials phi) ≅
      moduleOfDifferentials ((TopCat.Sheaf.pullback CommRingCat.{u} f).map phi)

AlgebraicGeometry.SheafOfModules.pullbackDifferentialsIso_compatible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/Differentials/InverseImage.lean, line 588. The attribute's comment: “compatibility with universal derivations”.

The canonical identification carries the inverse image of the universal derivation to the universal derivation.

theorem pullbackDifferentialsIso_compatible (phi : O₁ ⟶ O₂) :
    (inverseImageDerivation f (universalDerivation phi)).val.postcomp
        (pullbackDifferentialsIso f phi).hom.val =
      universalDerivation ((TopCat.Sheaf.pullback CommRingCat.{u} f).map phi)

AlgebraicGeometry.SheafOfModules.pullbackDifferentialsIso_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/Differentials/InverseImage.lean, line 597. The attribute's comment: “canonicity”.

Compatibility with universal derivations uniquely characterizes the canonical identification.

theorem pullbackDifferentialsIso_unique (phi : O₁ ⟶ O₂)
    (e : inverseImageModule f O₂ (moduleOfDifferentials phi) ≅
      moduleOfDifferentials ((TopCat.Sheaf.pullback CommRingCat.{u} f).map phi))
    (he : (inverseImageDerivation f (universalDerivation phi)).val.postcomp e.hom.val =
      universalDerivation ((TopCat.Sheaf.pullback CommRingCat.{u} f).map phi)) :
    e = pullbackDifferentialsIso f phi

Tag 08TE, a lemma

Tag 08TE in the Stacks Project.

Stacks.RelativeDifferentialStalk.stalkModuleOfDifferentialsKaehlerLinearEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeDifferentialStalk/Sheafify.lean, line 151. The attribute's comment: “the identification”.

Stacks Project, Tag 08TE. The stalk of the sheaf of relative differentials of a morphism of sheaves of commutative rings is the module of Kähler differentials of its stalk map: Ω_{O₂/O₁, x} = Ω_{O₂,x / O₁,x}.

It is also Stacks Tag 01V0 at a point: the sheaf of relative differentials commutes with taking stalks.

public noncomputable def stalkModuleOfDifferentialsKaehlerLinearEquiv (x : X)
    [DecidableEq (OrderDual (TopologicalSpace.OpenNhds x))] :
    letI := algebraStalk φ.hom x
    ToType (TopCat.Presheaf.stalk (C := AddCommGrpCat.{u})
        (moduleOfDifferentials.{u, u, u} φ).val.presheaf x)
      ≃ₗ[ToType (O₂.presheaf.stalk x)]
      KaehlerDifferential (ToType (O₁.presheaf.stalk x)) (ToType (O₂.presheaf.stalk x))

Stacks.RelativeDifferentialStalk.stalkModuleOfDifferentialsKaehlerLinearEquiv_germ_d, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RelativeDifferentialStalk/Sheafify.lean, line 224. The attribute's comment: “compatibility with the universal derivations”.

Stacks Project, Tag 08TE. The identification of the stalk of the sheaf of relative differentials with the Kähler differentials of the stalk map carries universal differentials to universal differentials.

The germ at x of the universal relative differential of a section of O₂ over a neighbourhood of x goes to the universal differential of the germ of that section. This is what makes the identification canonical.

public theorem stalkModuleOfDifferentialsKaehlerLinearEquiv_germ_d (x : X)
    [DecidableEq (OrderDual (TopologicalSpace.OpenNhds x))]
    (i : OrderDual (TopologicalSpace.OpenNhds x)) (a : nhdRing O₂.presheaf i) :
    letI := algebraStalk φ.hom x
    stalkModuleOfDifferentialsKaehlerLinearEquiv φ x
        (TopCat.Presheaf.germ (C := AddCommGrpCat.{u})
          (moduleOfDifferentials.{u, u, u} φ).val.presheaf (nhdOpen i) x (mem_nhdOpen i)
          ((universalDerivation.{u, u, u} φ).d a)) =
      KaehlerDifferential.D (ToType (O₁.presheaf.stalk x)) (ToType (O₂.presheaf.stalk x))
        (O₂.presheaf.germ (nhdOpen i) x (mem_nhdOpen i) a)

Tag 08RS, a lemma

Tag 08RS in the Stacks Project.

Stacks.Sheaves.DifferentialsFunctorial.compDeriv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialsFunctorial.lean, line 117. The attribute's comment: “the composite of O_2 -> O_2' with d is an O_1-derivation”.

Given a commutative square of sheaves of commutative rings

  O₂ --φ--> O₂'
  ↑ι        ↑ι'
  O₁ --ψ--> O₁'

and a relative ι'-derivation d' with values in a sheaf of O₂'-modules F, the composite d' ∘ φ is a relative ι-derivation with values in F regarded as a sheaf of O₂-modules by restriction of scalars along φ.

noncomputable def compDeriv {F : SheafOfModules.{u} (Differentials.underlyingRingSheaf O₂')}
    (d' : Differentials.SheafDerivation O₁' O₂' ι' F) (φ : O₂ ⟶ O₂') (ψ : O₁ ⟶ O₁')
    (hcomm : ι ≫ φ = ψ ≫ ι') :
    Differentials.SheafDerivation O₁ O₂ ι (restrictAlong φ F)

Stacks.Sheaves.DifferentialsFunctorial.differentialMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialsFunctorial.lean, line 182. The attribute's comment: “the canonical map of O_2-modules Omega_{O_2/O_1} -> Omega_{O_2'/O_1'}”. References: EGA 0 (20.5.2), “(20.5.2.3) map u''”.

The canonical morphism of sheaves of modules between the sheaves of relative differentials attached to a commutative square

  O₂ --φ--> O₂'
  ↑ι        ↑ι'
  O₁ --ψ--> O₁'

of sheaves of commutative rings. It goes from Ω_{O₂/O₁} to Ω_{O₂'/O₁'} regarded as a sheaf of O₂-modules by restriction of scalars along φ, and is characterized by differentialMap_comp_d.

noncomputable def differentialMap (ι : O₁ ⟶ O₂) (ι' : O₁' ⟶ O₂') (φ : O₂ ⟶ O₂')
    (ψ : O₁ ⟶ O₁') (hcomm : ι ≫ φ = ψ ≫ ι') :
    Differentials.moduleOfDifferentials O₁ O₂ ι ⟶
      restrictAlong φ (Differentials.moduleOfDifferentials O₁' O₂' ι')

Stacks.Sheaves.DifferentialsFunctorial.differentialMap_comp_d, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialsFunctorial.lean, line 201. The attribute's comment: “the characterizing property d(f) |-> d(phi f) on local sections”.

The characterizing property of differentialMap: on local sections it sends d a to d' (φ a), where d and d' are the universal derivations of Ω_{O₂/O₁} and Ω_{O₂'/O₁'}.

theorem differentialMap_comp_d (ι : O₁ ⟶ O₂) (ι' : O₁' ⟶ O₂') (φ : O₂ ⟶ O₂')
    (ψ : O₁ ⟶ O₁') (hcomm : ι ≫ φ = ψ ≫ ι') {U : Cᵒᵖ} (a : O₂.obj.obj U) :
    ((differentialMap ι ι' φ ψ hcomm).val.app U).hom
        ((Differentials.universalDerivation O₁ O₂ ι).d a)
      = (Differentials.universalDerivation O₁' O₂' ι').d ((φ.hom.app U).hom a)

Stacks.Sheaves.DifferentialsFunctorial.differentialMap_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialsFunctorial.lean, line 212. The attribute's comment: “the canonical map is uniquely characterized by that property”.

Uniqueness: a morphism of sheaves of modules satisfying the characterizing property of differentialMap is differentialMap.

theorem differentialMap_unique (ι : O₁ ⟶ O₂) (ι' : O₁' ⟶ O₂') (φ : O₂ ⟶ O₂')
    (ψ : O₁ ⟶ O₁') (hcomm : ι ≫ φ = ψ ≫ ι')
    (β : Differentials.moduleOfDifferentials O₁ O₂ ι ⟶
      restrictAlong φ (Differentials.moduleOfDifferentials O₁' O₂' ι'))
    (hβ : ∀ {U : Cᵒᵖ} (a : O₂.obj.obj U), (β.val.app U).hom
        ((Differentials.universalDerivation O₁ O₂ ι).d a)
      = (Differentials.universalDerivation O₁' O₂' ι').d ((φ.hom.app U).hom a)) :
    β = differentialMap ι ι' φ ψ hcomm

Stacks.Sheaves.DifferentialsFunctorial.differentialsArrowFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialsFunctorial.lean, line 326. The attribute's comment: “a functor on the category of arrows of sheaves of rings”.

Stacks Project, Tag 08RS. The relative differentials as a functor on the category of arrows of sheaves of commutative rings: an arrow ι : O₁ ⟶ O₂ is sent to Ω_{O₂/O₁} and a commutative square to the canonical map differentialMap, the identity and composition laws being differentialMap_id and differentialMap_comp.

The target is the total category ArrowModules rather than a fixed category of modules, because the sheaf of rings over which Ω_{O₂/O₁} is linear is O₂, which varies with the arrow.

noncomputable def differentialsArrowFunctor :
    CategoryTheory.Arrow (Sheaf J CommRingCat.{u}) ⥤ ArrowModules J

Tag 08TF, a lemma

Tag 08TF in the Stacks Project.

Stacks.Sites.Conormal.differentialSequence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/CorepresentingConormalSequence.lean, line 888. The attribute's comment: “canonical conormal sequence”.

The conormal sequence I/I² ⟶ B ⊗_A Ω_{A/R} ⟶ Ω_{B/R} ⟶ 0, with its middle and right terms expressed by the sheaves of relative differentials that corepresent derivations.

noncomputable def differentialSequence :
    ShortComplex
      (_root_.SheafOfModules.{max w u v z} (Stacks.SheafOfModules.Tensor.ringSheaf B))

Stacks.Sites.Conormal.differentialSequence_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/CorepresentingConormalSequence.lean, line 928. The attribute's comment: “exactness”. References: SGA 3 III (4.25), “exactness of (+)”.

The transported sequence is exact at the extension of scalars of Ω_{A/R}.

theorem differentialSequence_exact :
    (differentialSequence.{v, u, w, z} J R A B a φ).Exact

Stacks.Sites.Conormal.differentialSequence_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/CorepresentingConormalSequence.lean, line 936. The attribute's comment: “surjectivity”. References: SGA 3 III (4.25), “surjectivity in (+)”.

The transported sequence surjects onto Ω_{B/R}.

theorem differentialSequence_epi :
    Epi (differentialSequence.{v, u, w, z} J R A B a φ).g

Stacks.Sites.Conormal.differentialSequence_f_class, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/CorepresentingConormalSequence.lean, line 946. The attribute's comment: “formula on local kernel sections”.

The left-hand map carries the conormal class of a local section of the kernel to the source's d x ⊗ 1.

theorem differentialSequence_f_class (X : Cᵒᵖ) (x : kernelIdeal φ.hom X) :
    ((differentialSequence.{v, u, w, z} J R A B a φ).f.val.app X)
      (conormalClass.{v, u, w, z} J R A B a φ X x) =
      ((_root_.SheafOfModules.pullbackPushforwardAdjunction
        (underlyingRingHomForPullback J A B φ)).unit.app
          (moduleOfDifferentialsOfSite.{v, u, w, z} R A a)).val.app X
        ((universalDerivationOfSite.{v, u, w, z} R A a).d x.1)

Stacks.Sites.Conormal.differentialSequence_g_differential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/CorepresentingConormalSequence.lean, line 962. The attribute's comment: “right map on differentials”.

The right-hand map carries d x ⊗ 1 to the universal differential of the image of x.

theorem differentialSequence_g_differential (X : Cᵒᵖ) (x : A.obj.obj X) :
    ((differentialSequence.{v, u, w, z} J R A B a φ).g.val.app X)
      (((_root_.SheafOfModules.pullbackPushforwardAdjunction
        (underlyingRingHomForPullback J A B φ)).unit.app
          (moduleOfDifferentialsOfSite.{v, u, w, z} R A a)).val.app X
        ((universalDerivationOfSite.{v, u, w, z} R A a).d x)) =
      (universalDerivationOfSite.{v, u, w, z} R B (a ≫ φ)).d (φ.hom.app X x)

Stacks.Sites.Conormal.differentialSequence_g_eq_mapDifferentials, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/CorepresentingConormalSequence.lean, line 982. The attribute's comment: “canonical right-hand map”.

Under extension/restriction of scalars, the right-hand map is exactly the canonical map on relative differentials attached to the square R → A → B by Stacks 08TR.

theorem differentialSequence_g_eq_mapDifferentials :
    (_root_.SheafOfModules.pullbackPushforwardAdjunction
      (underlyingRingHomForPullback J A B φ)).homEquiv
      (moduleOfDifferentialsOfSite.{v, u, w, z} R A a)
        (moduleOfDifferentialsOfSite.{v, u, w, z} R B (a ≫ φ))
        (differentialSequence.{v, u, w, z} J R A B a φ).g =
      mapDifferentials.{v, u, w, z} a (a ≫ φ) (𝟙 R) φ (by simp)

Stacks.Sites.Conormal.differentialSequence_f_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/CorepresentingConormalSequence.lean, line 1010. The attribute's comment: “uniqueness of the conormal map”.

The formula on local conormal classes determines the left-hand map.

theorem differentialSequence_f_unique
    (g : (differentialSequence.{v, u, w, z} J R A B a φ).X₁ ⟶
      (differentialSequence.{v, u, w, z} J R A B a φ).X₂)
    (hg : ∀ (X : Cᵒᵖ) (x : kernelIdeal φ.hom X),
      g.val.app X (conormalClass.{v, u, w, z} J R A B a φ X x) =
        ((_root_.SheafOfModules.pullbackPushforwardAdjunction
          (underlyingRingHomForPullback J A B φ)).unit.app
            (moduleOfDifferentialsOfSite.{v, u, w, z} R A a)).val.app X
          ((universalDerivationOfSite.{v, u, w, z} R A a).d x.1)) :
    g = (differentialSequence.{v, u, w, z} J R A B a φ).f

Tag 08RT, a definition

Tag 08RT in the Stacks Project.

Stacks.Sheaves.RingedSpaceDifferentials.SDerivation, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RingedSpaceDifferentials.lean, line 182. The attribute's comment: “S-derivations into an O_X-module: the set Der_S(O_X, F)”. References: EGA IV (16.5.1); SGA 3 VIIA (1.2.0), “more general”.

Der_S(𝒪_X, F), the type of S-derivations of a morphism of ringed spaces h : X ⟶ S with values in a sheaf of 𝒪_X-modules F: a derivation of 𝒪_X relative to h⁻¹ 𝒪_S, that is, an inverseImageStructureMap h-derivation in the sense of Tag 01UN.

noncomputable abbrev SDerivation (h : X ⟶ S)
    (F : SheafOfModules.{u} (structureSheafRing X))

Stacks.Sheaves.RingedSpaceDifferentials.moduleOfDifferentials, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RingedSpaceDifferentials.lean, line 190. The attribute's comment: “the sheaf of differentials Omega_{X/S} of X over S”.

The sheaf of relative differentials Ω_{X/S} of a morphism of ringed spaces h : X ⟶ S: the sheaf of differentials of 𝒪_X relative to h⁻¹ 𝒪_S.

noncomputable def moduleOfDifferentials (h : X ⟶ S) :
    SheafOfModules.{u} (structureSheafRing X)

Stacks.Sheaves.RingedSpaceDifferentials.universalDerivation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RingedSpaceDifferentials.lean, line 196. The attribute's comment: “the universal S-derivation d_{X/S} with which Omega_{X/S} is endowed”.

The universal relative derivation d_{X/S} : 𝒪_X ⟶ Ω_{X/S}.

noncomputable def universalDerivation (h : X ⟶ S) :
    SDerivation h (moduleOfDifferentials h)

Tag 01UP, a lemma

Tag 01UP in the Stacks Project.

Stacks.Sheaves.SquareZeroExtension.sectionsEquivDerivations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SquareZeroExtensionSections.lean, line 259.

Stacks 01UP. Relative derivations into the square-zero kernel act simply transitively on the algebra sections of the extension. Under the resulting bijection, the derivation corresponding to t is the pointwise difference t - s.

theorem sectionsEquivDerivations {X : TopCat.{u}}
    {B O A : TopCat.Sheaf CommRingCat.{max u v} X}
    (α : B ⟶ O) (β : B ⟶ A) (π : A ⟶ O)
    (s : AlgebraSection α β π)
    (I : SheafOfModules.{max u v w} (underlyingRingSheaf O))
    (hI : SquareZeroKernel α β π s I) :
    ∃ e : AlgebraSection α β π ≃ SheafDerivation α I,
      ∀ (t : AlgebraSection α β π) (U : (Opens X)ᵒᵖ) (a : O.obj.obj U),
        hI.ι U ((e t).d a) = t.hom.hom.app U a - s.hom.hom.app U a

Tag 08RU, a lemma

Tag 08RU in the Stacks Project.

Stacks.Sheaves.RingedSpaceDifferentials.differentialMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RingedSpaceDifferentials.lean, line 334.

The canonical comparison map c : f^* Ω_{X/S} ⟶ Ω_{X'/S'} of sheaves of 𝒪_{X'}-modules attached to a commutative diagram of morphisms of ringed spaces

  X' --f--> X
  |         |
  h'        h
  v         v
  S' --g--> S

It is the morphism adjoint to pushforwardDifferentialMap, and differentialMap_isDifferentialMap together with differentialMap_unique say that it is the unique morphism carrying the pullback of d a to d (f^♯ a) on local sections.

noncomputable def differentialMap :
    (RingedSpaceModuleAdjunction.modulePullback f).obj (moduleOfDifferentials h) ⟶
      moduleOfDifferentials h'

AlgebraicGeometry.SheafOfModules.existsUnique_compositeDerivation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/Differentials/Functoriality.lean, line 221. The attribute's comment: “composite derivation”.

The composite of f^♯ with the pushforward of the universal derivation is an S-derivation, and it is the unique one whose value on every local section a is the universal derivation of f^♯ a.

theorem existsUnique_compositeDerivation {X' X S' S : RingedSpace.{u, u}}
    (f : X' ⟶ X) (h : X ⟶ S) (h' : X' ⟶ S') (g : S' ⟶ S)
    (hcomm : f ≫ h = h' ≫ g) :
    ∃! D : SheafDerivation (inverseImageStructureMap h)
      ((RingedSpaceModuleAdjunction.modulePushforward f).obj
        (moduleOfDifferentials (inverseImageStructureMap h'))),
      ∀ (U : Opens X.carrier) (a : X.presheaf.obj (.op U)),
        D.d a = (universalDerivation
          (inverseImageStructureMap h')).d ((f.hom.c.app (.op U)).hom a)

AlgebraicGeometry.SheafOfModules.pushforwardDifferentialMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/Differentials/Functoriality.lean, line 288. The attribute's comment: “map to pushforward differentials”.

The universal map Ω_{X/S} ⟶ f_* Ω_{X'/S'}.

noncomputable def pushforwardDifferentialMap {X' X S' S : RingedSpace.{u, u}}
    (f : X' ⟶ X) (h : X ⟶ S) (h' : X' ⟶ S') (g : S' ⟶ S) (hcomm : f ≫ h = h' ≫ g) :
    moduleOfDifferentials (inverseImageStructureMap h) ⟶
      (RingedSpaceModuleAdjunction.modulePushforward f).obj
        (moduleOfDifferentials (inverseImageStructureMap h'))

AlgebraicGeometry.SheafOfModules.existsUnique_differentialMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/Differentials/Functoriality.lean, line 314. The attribute's comment: “canonical map and uniqueness”. References: EGA IV (16.4.3), “(16.4.3.6),(16.4.3.7)”.

The canonical morphism of differentials for a commutative square of ringed spaces exists and is uniquely determined by its action on differentials of local sections.

theorem existsUnique_differentialMap {X' X S' S : RingedSpace.{u, u}}
    (f : X' ⟶ X) (h : X ⟶ S) (h' : X' ⟶ S') (g : S' ⟶ S)
    (hcomm : f ≫ h = h' ≫ g) :
    ∃! c : (RingedSpaceModuleAdjunction.modulePullback f).obj
        (moduleOfDifferentials (inverseImageStructureMap h)) ⟶
      moduleOfDifferentials (inverseImageStructureMap h'),
      IsDifferentialMap f h h' c

AlgebraicGeometry.SheafOfModules.differentialMap_adjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/Differentials/Functoriality.lean, line 360. The attribute's comment: “agreement under adjunction”.

The pullback map on differentials is adjoint to the canonical map into pushforward differentials.

theorem differentialMap_adjoint {X' X S' S : RingedSpace.{u, u}}
    (f : X' ⟶ X) (h : X ⟶ S) (h' : X' ⟶ S') (g : S' ⟶ S)
    (hcomm : f ≫ h = h' ≫ g) :
    (RingedSpaceModuleAdjunction.homEquiv f
      (moduleOfDifferentials (inverseImageStructureMap h'))
      (moduleOfDifferentials (inverseImageStructureMap h)))
        (differentialMap f h h' g hcomm) =
      pushforwardDifferentialMap f h h' g hcomm

AlgebraicGeometry.SheafOfModules.inverseImageDifferentialMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/Differentials/Functoriality.lean, line 562. The attribute's comment: “inverse-image map”.

The canonical map f⁻¹Ω_{X/S} ⟶ Ω_{X'/S'} of f⁻¹𝒪_X-modules. The target carries its restricted scalar action.

noncomputable def inverseImageDifferentialMap {X' X S' S : RingedSpace.{u, u}}
    (f : X' ⟶ X) (h : X ⟶ S) (h' : X' ⟶ S') (g : S' ⟶ S) (hcomm : f ≫ h = h' ≫ g) :
    inverseImageModule f.hom.base X.sheaf
      (moduleOfDifferentials (inverseImageStructureMap h)) ⟶
        inverseImageDifferentialTarget f h'

AlgebraicGeometry.SheafOfModules.inverseImageDifferentialMap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/Differentials/Functoriality.lean, line 574. The attribute's comment: “inverse-image and tensor comparison”.

The inverse-image differential map is the restriction of the scalar-extended map c_f, after the canonical tensor-unit map f⁻¹Ω ⟶ f*Ω.

theorem inverseImageDifferentialMap_eq {X' X S' S : RingedSpace.{u, u}}
    (f : X' ⟶ X) (h : X ⟶ S) (h' : X' ⟶ S') (g : S' ⟶ S) (hcomm : f ≫ h = h' ≫ g) :
    inverseImageDifferentialMap f h h' g hcomm =
      inverseImageToPullback f (moduleOfDifferentials (inverseImageStructureMap h)) ≫
      (_root_.SheafOfModules.restrictScalars (inverseImageStructureRingMap f)).map
        (differentialMap f h h' g hcomm)

Tag 01UW, a lemma

Tag 01UW in the Stacks Project.

Stacks.Sheaves.RingedSpaceDifferentials.differentialMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RingedSpaceDifferentials.lean, line 464.

Functoriality, composition: the comparison map of a vertical composite of two commutative diagrams of ringed spaces is the composite of the comparison maps, after the canonical identification (f' ≫ f)^* ⟶ f'^* (f^*). This is the relation c_{f ∘ f'} = c_{f'} ∘ (f')^* c_f of Tag 01UW.

theorem differentialMap_comp :
    differentialMap (f' ≫ f) h h'' (g' ≫ g) hcomm''
      = modulePullbackComparison f f' (moduleOfDifferentials h) ≫
        ((RingedSpaceModuleAdjunction.modulePullback f').map
            (differentialMap f h h' g hcomm) ≫ differentialMap f' h' h'' g' hcomm')

Tag 0H79, a lemma

Tag 0H79 in the Stacks Project.

Stacks.Sheaves.RingedSpaceDifferentials.triangleDifferentials_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RingedSpaceDifferentials.lean, line 845. The attribute's comment: “exactness at the right term”. References: EGA IV (16.4.19), “surjectivity on right”.

The canonical map to relative differentials over Y is an epimorphism.

theorem triangleDifferentials_epi (f : X ⟶ Y) (g : Y ⟶ S) :
    Epi (toRelativeDifferentials f g)

Stacks.Sheaves.RingedSpaceDifferentials.triangleDifferentials_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RingedSpaceDifferentials.lean, line 917. The attribute's comment: “exactness at the middle term”. References: EGA IV (16.4.19), “exactness at middle”.

For morphisms of ringed spaces f : X ⟶ Y and g : Y ⟶ S the canonical maps form a complex f^* Ω_{Y/S} ⟶ Ω_{X/S} ⟶ Ω_{X/Y} which is exact at Ω_{X/S}. Together with triangleDifferentials_epi this is the exactness of f^* Ω_{Y/S} ⟶ Ω_{X/S} ⟶ Ω_{X/Y} ⟶ 0.

theorem triangleDifferentials_exact (f : X ⟶ Y) (g : Y ⟶ S) :
    ∃ h : differentialMap f g (f ≫ g) (𝟙 S) (by simp) ≫ toRelativeDifferentials f g = 0,
      (ShortComplex.mk _ _ h).Exact

Sources

• Section 17.28, Tag 08RL
• AxiomMath/Stacks at 5ed82d14

LeanPresheafOfModulesOfCommRing.Derivation' · PresheafOfModulesOfCommRing.Derivation · AlgebraicGeometry.SheafOfModules.universalDerivation_isUniversal · AlgebraicGeometry.SheafOfModules.moduleOfDifferentials · AlgebraicGeometry.SheafOfModules.universalDerivation · AlgebraicGeometry.SheafOfModules.moduleOfDifferentialsIsoSectionwise · AlgebraicGeometry.SheafOfModules.pullbackDifferentialsIso · AlgebraicGeometry.SheafOfModules.inverseImageDerivation

Section17.29 Finite order differential operators#

Section 17.29 of the Stacks Project, Tag 0G3P. 7 tags here are carried by 2 declarations of the repository (all in StacksFrontier) and 5 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0G3Q, a definition

Tag 0G3Q in the Stacks Project.

Declarations registered for the tag:

• DiffOp.IsGlobalDiffOpOfOrder, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Modules/DifferentialOperators.lean, line 72 (StacksFrontier).

Tag 0G3R, a lemma

Tag 0G3R in the Stacks Project.

Declarations registered for the tag:

• DiffOp.isGlobalDiffOpOfOrder_comp, declared in the repository, registered with add_to_stacks in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialOperatorsRingedSpace.lean, line 40 (StacksFrontier): “the ringed-space case of 09CS”.

Tag 0G3S, a lemma

Tag 0G3S in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.SheafOfModules.differentialOperatorsFunctor_isCorepresentable, declared in the repository, registered with add_to_stacks in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialOperatorsRingedSpace.lean, line 42 (StacksFrontier): “the ringed-space case of 09CT”.

Tag 0G3T, a definition

Tag 0G3T in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.SheafOfModules.moduleOfPrincipalParts, declared in the repository, registered with add_to_stacks in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PrincipalPartsRingedSpace.lean, line 33 (StacksFrontier): “the ringed-space case of 09CU”.

Tag 0G3U, a lemma

Tag 0G3U in the Stacks Project.

Stacks.Sheaves.PrincipalParts.principalPartsSheafification, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/PrincipalPartsSheafification.lean, line 697. References: EGA IV (16.4.24), “(ii)”.

Stacks Project, Tag 0G3U, which read as a statement about the sheaf of principal parts is Tag 09CV. Let φ : O₁ ⟶ O₂ be a morphism of presheaves of commutative rings on a site and let F be a presheaf of O₂-modules. Then the sheaf of principal parts of order k of F^# relative to O₂^# / O₁^# is the sheaf associated to the presheaf X ↦ Pᵏ_{O₂(X)/O₁(X)}(F X) of sectionwise modules of principal parts, and the sectionwise universal operators are compatible with restriction.

noncomputable def principalPartsSheafification [HasWeakSheafify J CommRingCat.{u}]
    [J.WEqualsLocallyBijective CommRingCat.{u}]
    [J.HasSheafCompose (forget₂ CommRingCat.{u} RingCat.{u})]
    [J.WEqualsLocallyBijective AddCommGrpCat.{max u u₁ v₁ v}]
    [HasWeakSheafify J AddCommGrpCat.{max u u₁ v₁ v}] {O₁ O₂ : Cᵒᵖ ⥤ CommRingCat.{u}}
    (φ : O₁ ⟶ O₂)
    (F : PresheafOfModules.{max u u₁ v₁ v} (O₂ ⋙ forget₂ CommRingCat.{u} RingCat.{u}))
    (k : ℕ) :
    Σ' P : PresheafOfModules.{max u u₁ v₁ v}
        (O₂ ⋙ forget₂ CommRingCat.{u} RingCat.{u}),
      Σ' D : F.presheaf ⟶ P.presheaf,
        Σ' _e : (AlgebraicGeometry.SheafOfModules.differentialOperatorsFunctor.{v₁, u₁, u,
            max u u₁ v₁ v}
            ((sheafCompose J (forget₂ CommRingCat.{u} RingCat.{u})).map
              (associatedCommRingSheafMap J φ))
            ((PresheafOfModules.sheafification (toAssociatedRingSheaf J O₂)).obj F)
            k).coreprX (hF :=
              AlgebraicGeometry.SheafOfModules.differentialOperatorsFunctor_isCorepresentable
                ((sheafCompose J (forget₂ CommRingCat.{u} RingCat.{u})).map
                  (associatedCommRingSheafMap J φ))
                ((PresheafOfModules.sheafification (toAssociatedRingSheaf J O₂)).obj F) k) ≅
          (PresheafOfModules.sheafification (toAssociatedRingSheaf J O₂)).obj P,
        ∀ X : Cᵒᵖ,
          letI : Algebra (O₁.obj X) (O₂.obj X) := (φ.app X).hom.toAlgebra
          letI : Module (O₁.obj X) (F.obj X) :=
            Module.compHom (F.obj X) (φ.app X).hom
          letI : Module (O₁.obj X) (P.obj X) :=
            Module.compHom (P.obj X) (φ.app X).hom
          letI : IsScalarTower (O₁.obj X) (O₂.obj X) (F.obj X) :=
            IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl
          letI : IsScalarTower (O₁.obj X) (O₂.obj X) (P.obj X) :=
            IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl
          ∃ d : F.obj X →ₗ[O₁.obj X] P.obj X,
            (∀ x, d x = (D.app X).hom x) ∧
              d.IsUniversalDifferentialOperatorOfOrderLE (O₂.obj X) k

Tag 0G3V, a lemma

Tag 0G3V in the Stacks Project.

AlgebraicGeometry.SheafOfModules.nonempty_principalPartsSequence_opens, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/Differentials/PrincipalParts.lean, line 77. References: SGA 6 II (AppII.1.2.4), “n = 1, top. space”.

Stacks Project, Tag 0G3V. For a homomorphism φ : O₁ ⟶ O₂ of sheaves of commutative rings on a topological space, the sheaves of first principal parts of the sheaves of O₂-modules assemble into a functor sitting in a short exact sequence

0 ⟶ Ω_{O₂/O₁} ⊗_{O₂} F ⟶ P¹_{O₂/O₁}(F) ⟶ F ⟶ 0

natural in F, with its two arrows determined by their values on universal differential operators.

theorem nonempty_principalPartsSequence_opens {X : TopCat.{u}}
    (O₁ O₂ : TopCat.Sheaf CommRingCat.{u} X) (φ : O₁ ⟶ O₂) :
    Nonempty (PrincipalPartsSequence.{u, u, u, m} (J := Opens.grothendieckTopology X) O₁ O₂ φ)

Tag 0G3X, a definition

Tag 0G3X in the Stacks Project.

Declarations registered for the tag:

• DiffOp.IsGlobalDiffOpOfOrder, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Modules/DifferentialOperators.lean, line 73 (StacksFrontier): “differential operators on X/S, for the map f♯ : f⁻¹𝒪_S ⟶ 𝒪_X”.

Sources

• Section 17.29, Tag 0G3P
• AxiomMath/Stacks at 5ed82d14

LeanDiffOp.IsGlobalDiffOpOfOrder · DiffOp.isGlobalDiffOpOfOrder_comp · AlgebraicGeometry.SheafOfModules.differentialOperatorsFunctor_isCorepresentable · AlgebraicGeometry.SheafOfModules.moduleOfPrincipalParts · Stacks.Sheaves.PrincipalParts.principalPartsSheafification · AlgebraicGeometry.SheafOfModules.nonempty_principalPartsSequence_opens

Section17.30 The de Rham complex#

Section 17.30 of the Stacks Project, Tag 0FKL. 5 tags here are carried by 12 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0FKM, a definition

Tag 0FKM in the Stacks Project.

AlgebraicGeometry.SheafOfModules.deRhamDifferential, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/DeRhamExistence.lean, line 363. The attribute's comment: “existence: the de Rham differential exists. The tag defines the complex by a uniqueness property, so the covering set is this construction, relativeDeRhamComplex and deRhamDifferential_unique.”. References: EGA IV (16.6.2), “existence”.

The relative de Rham differential of φ exists. The differential in each degree is the sheafification of the ring-level de Rham differential, read on ⋀ᵖ Ω through the exact-wedge comparison; it squares to zero and obeys the de Rham rule because the sectionwise differential does.

noncomputable def deRhamDifferential : DeRhamDifferential B

AlgebraicGeometry.SheafOfModules.relativeDeRhamComplex, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/DeRhamExistence.lean, line 372. The attribute's comment: “the canonical complex: the de Rham complex of B over A, assembled from the differential of deRhamDifferential. Its terms and arrows are deRhamComplex_X and deRhamComplex_d.”.

The relative de Rham complex ⋀⁰ Ω → ⋀¹ Ω → ⋀² Ω → ⋯ of sheaves of A-modules.

noncomputable abbrev relativeDeRhamComplex :
    CochainComplex
      (_root_.SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf.{u, u, u} A)) ℕ

AlgebraicGeometry.SheafOfModules.deRhamDifferential_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/DeRhamExistence.lean, line 382. The attribute's comment: “uniqueness: a de Rham differential is the one constructed here, so the complex of Tag 0FKM is well defined. The general two-differential form is DeRhamDifferential.eq of StacksFrontier.Topology.Sheaves.Modules.DeRhamUniqueness.”. References: EGA IV (16.6.2), “uniqueness”.

The relative de Rham differential is unique. This is AlgebraicGeometry.SheafOfModules.DeRhamDifferential.eq read at the constructed differential.

theorem deRhamDifferential_unique (D : DeRhamDifferential B) : D = deRhamDifferential B

Tag 0FKP, a lemma

Tag 0FKP in the Stacks Project.

AlgebraicGeometry.SheafOfModules.inverseImageExteriorAlgebraIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/DeRhamInverseImage.lean, line 209. The attribute's comment: “canonicality of the identification of the terms, as sheaves of f⁻¹ℬ-modules: the comparison is the one compatible with the exterior products, the units and the exact differentials, and that determines it. The complex-level statement of the tag is inverseImageDeRhamComplexIso below.”.

Stacks Project, Tag 0FKP, canonicality. The canonical comparison between the inverse image of the exterior algebra of Ω_{ℬ/𝒜} and the exterior algebra of Ω_{f⁻¹ℬ/f⁻¹𝒜}, in every degree and on the underlying direct-sum sheaf, together with its compatibility with the exterior products, the degree-zero units and the degree-one generators. Those compatibilities determine the comparison, by Stacks.PullbackExteriorAlgebra.exteriorAlgebraPullbackIso_unique.

def inverseImageExteriorAlgebraIso :
    ExteriorAlgebraPullbackIso (RingedSpace.inverseImageProjection X f)
      (differentialAlgebras.{u} φ).exterior (differentialAlgebras.{u} φ).exteriorGenerator
      (differentialAlgebras.{u} (inverseImageRingMap φ f)).exterior
      (inverseImageExteriorGenerator φ f)

AlgebraicGeometry.SheafOfModules.inverseImageDifferentialForms, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/DeRhamInverseImage.lean, line 224. The attribute's comment: “the identification of the terms: in each degree p the inverse image of Ωᵖ_{ℬ/𝒜} is Ωᵖ_{f⁻¹ℬ/f⁻¹𝒜}, as sheaves of f⁻¹ℬ-modules. The identification of the complexes of f⁻¹𝒜-modules is inverseImageDeRhamComplexIso below, which is built from this one by inverseImageRestrictScalarsIso.”.

Stacks Project, Tag 0FKP, on the terms. The canonical identification f⁻¹ Ωᵖ_{ℬ/𝒜} = Ωᵖ_{f⁻¹ℬ/f⁻¹𝒜} of the inverse image of the sheaf of relative differential p-forms with the sheaf of relative differential p-forms of the inverse-image rings.

def inverseImageDifferentialForms (p : ℕ) :
    (pullbackFunctor (RingedSpace.inverseImageProjection X f)).obj (differentialForms.{u} φ p) ≅
      differentialForms.{u} (inverseImageRingMap φ f) p

AlgebraicGeometry.SheafOfModules.inverseImageDeRhamComplexIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/DeRhamInverseImage.lean, line 716. The attribute's comment: “the identification of the de Rham COMPLEXES: f⁻¹Ω•_{ℬ/𝒜} = Ω•_{f⁻¹ℬ/f⁻¹𝒜} as complexes of sheaves of f⁻¹𝒜-modules”.

Stacks Project, Tag 0FKP. The canonical identification f⁻¹Ω•_{ℬ/𝒜} = Ω•_{f⁻¹ℬ/f⁻¹𝒜} of de Rham complexes: the degreewise identification of the differential forms, moved into sheaves of f⁻¹𝒜-modules and assembled into an isomorphism of complexes.

noncomputable def inverseImageDeRhamComplexIso :
    inverseImageDeRhamComplex φ f ≅
      relativeDeRhamComplex (differentialAlgebras.{u} (inverseImageRingMap φ f))

AlgebraicGeometry.SheafOfModules.inverseImageDeRhamComplexIso_canonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/DeRhamInverseImage.lean, line 730. The attribute's comment: “canonicality of the identification of the complexes: it is the map determined by b · d b₁ ∧ ⋯ ∧ d bₚ ↦ f⁻¹b · d(f⁻¹b₁) ∧ ⋯ ∧ d(f⁻¹bₚ) on the inverse-image sections”.

Stacks Project, Tag 0FKP, canonicality. The identification of the complexes is the one that carries each local multiple of an ordered product of exact differentials to the same expression in the inverse-image rings.

theorem inverseImageDeRhamComplexIso_canonical :
    IsCanonicalInverseImageDeRhamIso φ f (inverseImageDeRhamComplexIso φ f)

AlgebraicGeometry.SheafOfModules.inverseImageDeRhamComplexIso_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/DeRhamInverseImage.lean, line 739. The attribute's comment: “uniqueness: a canonical identification of the de Rham complexes is the one constructed here”.

Stacks Project, Tag 0FKP, uniqueness. Canonicality determines the identification of the complexes: the local multiples of the ordered products of exact differentials generate the terms locally, so an isomorphism of complexes prescribed on them is prescribed.

theorem inverseImageDeRhamComplexIso_unique
    (e : inverseImageDeRhamComplex φ f ≅
      relativeDeRhamComplex (differentialAlgebras.{u} (inverseImageRingMap φ f)))
    (he : IsCanonicalInverseImageDeRhamIso φ f e) :
    e = inverseImageDeRhamComplexIso φ f

Tag 0G3Y, a lemma

Tag 0G3Y in the Stacks Project.

AlgebraicGeometry.SheafOfModules.deRhamDifferentialHom_isGlobalDiffOpOfOrder_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/DeRhamDifferentialOperator.lean, line 256.

Stacks Project, Tag 0G3Y. For a morphism φ : A ⟶ B of sheaves of commutative rings on a topological space, every differential d : ⋀ᵖ Ω ⟶ ⋀ᵖ⁺¹ Ω of the relative de Rham complex is a differential operator of order at most one relative to φ.

theorem deRhamDifferentialHom_isGlobalDiffOpOfOrder_one (p : ℕ) :
    DiffOp.IsGlobalDiffOpOfOrder (underlyingRingHom (φ := φ)) 1 (deRhamGlobalOp B p)

Tag 0FKQ, a definition

Tag 0FKQ in the Stacks Project.

AlgebraicGeometry.Scheme.Hom.deRhamComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DeRham/SchemeComplex.lean, line 106. The attribute's comment: “the morphism-of-schemes case”.

The relative de Rham complex Ω^•_{X/S} of a morphism of schemes f : X ⟶ S: the de Rham complex of 𝒪_X over f^{-1}𝒪_S, a cochain complex of sheaves of f^{-1}𝒪_S-modules on X.

noncomputable def deRhamComplex :
    CochainComplex (_root_.SheafOfModules.{u}
      (AlgebraicGeometry.SheafOfModules.underlyingRingSheaf
        ((TopCat.Sheaf.pullback CommRingCat.{u} f.base).obj S.sheaf))) ℕ

AlgebraicGeometry.SheafOfModules.relativeDeRhamComplex, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/DeRhamExistence.lean, line 372. The attribute's comment: “the morphism-of-ringed-spaces case, at A := f⁻¹𝒪_Y”.

The relative de Rham complex ⋀⁰ Ω → ⋀¹ Ω → ⋀² Ω → ⋯ of sheaves of A-modules.

noncomputable abbrev relativeDeRhamComplex :
    CochainComplex
      (_root_.SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf.{u, u, u} A)) ℕ

Tag 0G3Z, a lemma

Tag 0G3Z in the Stacks Project.

AlgebraicGeometry.SheafOfModules.deRhamDifferentialHom_isGlobalDiffOpOfOrder_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/DeRhamDifferentialOperator.lean, line 256. The attribute's comment: “the case of a morphism of ringed spaces f : X -> Y, at phi : f^{-1} O_Y -> O_X”.

Stacks Project, Tag 0G3Y. For a morphism φ : A ⟶ B of sheaves of commutative rings on a topological space, every differential d : ⋀ᵖ Ω ⟶ ⋀ᵖ⁺¹ Ω of the relative de Rham complex is a differential operator of order at most one relative to φ.

theorem deRhamDifferentialHom_isGlobalDiffOpOfOrder_one (p : ℕ) :
    DiffOp.IsGlobalDiffOpOfOrder (underlyingRingHom (φ := φ)) 1 (deRhamGlobalOp B p)

Sources

• Section 17.30, Tag 0FKL
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.SheafOfModules.deRhamDifferential · AlgebraicGeometry.SheafOfModules.relativeDeRhamComplex · AlgebraicGeometry.SheafOfModules.deRhamDifferential_unique · AlgebraicGeometry.SheafOfModules.inverseImageExteriorAlgebraIso · AlgebraicGeometry.SheafOfModules.inverseImageDifferentialForms · AlgebraicGeometry.SheafOfModules.inverseImageDeRhamComplexIso · AlgebraicGeometry.SheafOfModules.inverseImageDeRhamComplexIso_canonical · AlgebraicGeometry.SheafOfModules.inverseImageDeRhamComplexIso_unique

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.