71.2 Associated and weakly… to 71.10 Meromorphic functions and…

Section71.2 Associated and weakly associated points#

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

Tag 0CTW, a lemma

Tag 0CTW in the Stacks Project.

AlgebraicGeometry.Space.isWeaklyAssociatedPoint_restrictToChart_iff_isWeaklyAssociatedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/SpaceFibreChartScheme.lean, line 94. The attribute's comment: “conditions (1) and (2) at a point of a chart scheme, with no geometric point in the statement”.

Zariski and étale weak association agree at a point of a chart scheme. Let F be a quasi-coherent 𝒪_Z-module and let w be a point of the scheme of an étale chart W of Z. Then w is weakly associated to the restriction F|_W, in the Zariski sense of Stacks 056L, exactly when the point of Z it lies over is weakly associated to F in the sense of Stacks 0CTX.

theorem isWeaklyAssociatedPoint_restrictToChart_iff_isWeaklyAssociatedPoint
    (Z : AlgebraicSpaces B S hS) (F : Modules.{u, u} B S hS Z.1 Z.2)
    [F.IsQuasicoherentOnSite] (W : SmallEtale B S hS Z.1) (w : chartScheme W) :
    Stacks.Divisors.IsWeaklyAssociatedPoint (restrictToChart B S hS Z.2 F W) w ↔
      IsWeaklyAssociatedPoint B S hS Z F (chartSchemeToPoints B S hS Z.1 W w)

AlgebraicGeometry.Space.isAssociatedPoint_restrictToChart_iff_isWeaklyAssociatedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AssociatedPointsChartTFAE.lean, line 99. The attribute's comment: “conditions (4) and (5) at a point of a chart scheme”.

Stacks 0CTW, conditions (4) and (5) at a point of a chart scheme. Let X be a locally Noetherian algebraic space, F a quasi-coherent 𝒪_X-module and w a point of the scheme of an étale chart W of X. Then w is associated to the restriction F|_W, in the Zariski sense of Stacks 02OJ, exactly when the point of X it lies over is weakly associated to F in the sense of Stacks 0CTX.

The chart's scheme is locally Noetherian by Stacks 03E8, so the maximal ideal of 𝒪_{W, w} is finitely generated and association at w is weak association at w by Stacks 05AR; that is conditions (1) and (2).

theorem isAssociatedPoint_restrictToChart_iff_isWeaklyAssociatedPoint
    (hLN : HasEtaleLocalProperty B S hS X.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite]
    (W : SmallEtale B S hS X.1) (w : chartScheme W) :
    Stacks.Divisors.IsAssociatedPoint (restrictToChart B S hS X.2 F W) w ↔
      IsWeaklyAssociatedPoint B S hS X F (chartSchemeToPoints B S hS X.1 W w)

AlgebraicGeometry.Space.isWeaklyAssociatedPoint_iff_exists_isAssociatedPoint_restrictToChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AssociatedPointsChartTFAE.lean, line 116. The attribute's comment: “condition (4)”.

Stacks 0CTW, condition (4). Let X be a locally Noetherian algebraic space and F a quasi-coherent 𝒪_X-module. A point x of X is weakly associated to F exactly when there is some étale scheme chart W of X and some point w of its scheme above x which is associated to the restriction F|_W.

theorem isWeaklyAssociatedPoint_iff_exists_isAssociatedPoint_restrictToChart
    (hLN : HasEtaleLocalProperty B S hS X.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite] (x : points B S hS X.1) :
    IsWeaklyAssociatedPoint B S hS X F x ↔
      ∃ (W : SmallEtale B S hS X.1) (w : chartScheme W),
        chartSchemeToPoints B S hS X.1 W w = x ∧
          Stacks.Divisors.IsAssociatedPoint (restrictToChart B S hS X.2 F W) w

AlgebraicGeometry.Space.isWeaklyAssociatedPoint_iff_forall_isAssociatedPoint_restrictToChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AssociatedPointsChartTFAE.lean, line 136. The attribute's comment: “condition (5)”.

Stacks 0CTW, condition (5). Let X be a locally Noetherian algebraic space and F a quasi-coherent 𝒪_X-module. A point x of X is weakly associated to F exactly when every point of the scheme of every étale chart of X lying above x is associated to the restriction of F to that chart.

theorem isWeaklyAssociatedPoint_iff_forall_isAssociatedPoint_restrictToChart
    (hLN : HasEtaleLocalProperty B S hS X.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite] (x : points B S hS X.1) :
    IsWeaklyAssociatedPoint B S hS X F x ↔
      ∀ (W : SmallEtale B S hS X.1) (w : chartScheme W),
        chartSchemeToPoints B S hS X.1 W w = x →
          Stacks.Divisors.IsAssociatedPoint (restrictToChart B S hS X.2 F W) w

AlgebraicGeometry.Space.exists_isAssociatedPoint_restrictToChart_iff_forall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AssociatedPointsChartTFAE.lean, line 156. The attribute's comment: “conditions (4) and (5)”.

Stacks 0CTW, conditions (4) and (5). On a locally Noetherian algebraic space ordinary association of some point of some étale scheme chart above x is ordinary association of every point of every such chart.

theorem exists_isAssociatedPoint_restrictToChart_iff_forall
    (hLN : HasEtaleLocalProperty B S hS X.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite] (x : points B S hS X.1) :
    (∃ (W : SmallEtale B S hS X.1) (w : chartScheme W),
        chartSchemeToPoints B S hS X.1 W w = x ∧
          Stacks.Divisors.IsAssociatedPoint (restrictToChart B S hS X.2 F W) w) ↔
      ∀ (W : SmallEtale B S hS X.1) (w : chartScheme W),
        chartSchemeToPoints B S hS X.1 W w = x →
          Stacks.Divisors.IsAssociatedPoint (restrictToChart B S hS X.2 F W) w

AlgebraicGeometry.Space.isAssociatedPoint_restrictToChart_iff_isWeaklyAssociatedPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AssociatedPointsChartTFAE.lean, line 177. The attribute's comment: “conditions (4) and (5) against condition (3)”.

Stacks 0CTW, conditions (4) and (5) against condition (3). Let X be a locally Noetherian algebraic space, F a quasi-coherent 𝒪_X-module and φ : (U, ū) → (X, x̄) an étale neighbourhood of a geometric point whose chart U is a scheme. Then u is associated to φ^*F exactly when the maximal ideal of 𝒪_{X, x̄} is a weakly associated prime of the geometric stalk F_{x̄}.

theorem isAssociatedPoint_restrictToChart_iff_isWeaklyAssociatedPrime
    (hLN : HasEtaleLocalProperty B S hS X.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    {xbar : GeometricPoint B S hS X.1} (V : SmallEtaleNeighborhood xbar)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite] :
    Stacks.Divisors.IsAssociatedPoint (restrictToChart B S hS X.2 F V.chart)
        (chartPoint B S hS X.1 V) ↔
      letI : IsLocalRing (etaleLocalRing B S hS X.1 xbar) :=
        isLocalRing_etaleLocalRing B S hS X.1 X.2 xbar
      letI : Module (etaleLocalRing B S hS X.1 xbar) (geometricModuleStalk B S hS X xbar F) :=
        (geometricModuleStalk B S hS X xbar F).isModule
      IsWeaklyAssociatedPrime (etaleLocalRing B S hS X.1 xbar)
        (geometricModuleStalk B S hS X xbar F)
        (IsLocalRing.maximalIdeal (etaleLocalRing B S hS X.1 xbar))

AlgebraicGeometry.Space.isAssociatedPoint_restrictToChart_iff_isAssociatedPrimeStacks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AssociatedPointsChartTFAE.lean, line 200. The attribute's comment: “conditions (4) and (5) against condition (6)”.

Stacks 0CTW, conditions (4) and (5) against condition (6). In the situation of AlgebraicGeometry.Space.isAssociatedPoint_restrictToChart_iff_isWeaklyAssociatedPrime, u is associated to φ^*F exactly when the maximal ideal of the étale local ring 𝒪_{X, x̄} is an associated prime of the geometric stalk F_{x̄}.

theorem isAssociatedPoint_restrictToChart_iff_isAssociatedPrimeStacks
    (hLN : HasEtaleLocalProperty B S hS X.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    {xbar : GeometricPoint B S hS X.1} (V : SmallEtaleNeighborhood xbar)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite] :
    letI : IsLocalRing (etaleLocalRing B S hS X.1 xbar) :=
      isLocalRing_etaleLocalRing B S hS X.1 X.2 xbar
    letI : Module (etaleLocalRing B S hS X.1 xbar) (geometricModuleStalk B S hS X xbar F) :=
      (geometricModuleStalk B S hS X xbar F).isModule
    (Stacks.Divisors.IsAssociatedPoint (restrictToChart B S hS X.2 F V.chart)
        (chartPoint B S hS X.1 V) ↔
      IsAssociatedPrimeStacks (etaleLocalRing B S hS X.1 xbar)
        (geometricModuleStalk B S hS X xbar F)
        (IsLocalRing.maximalIdeal (etaleLocalRing B S hS X.1 xbar)))

AlgebraicGeometry.Space.isWeaklyAssociatedPrime_maximalIdeal_iff_isAssociatedPrimeStacks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedTFAE.lean, line 236. The attribute's comment: “conditions (3) and (6) at a geometric point”.

Stacks 0CTW, (3) ⟺ (6). Let F be an 𝒪_X-module on an algebraic space and x̄ a geometric point of X at which the maximal ideal of 𝒪_{X, x̄} is finitely generated. That maximal ideal is a weakly associated prime of the geometric stalk F_{x̄} if and only if it is an associated prime of F_{x̄}.

theorem isWeaklyAssociatedPrime_maximalIdeal_iff_isAssociatedPrimeStacks
    (F : Modules.{u, m} B S hS X.1 X.2) (xbar : GeometricPoint B S hS X.1) :
    letI : IsLocalRing (etaleLocalRing B S hS X.1 xbar) :=
      isLocalRing_etaleLocalRing B S hS X.1 X.2 xbar
    letI : Module (etaleLocalRing B S hS X.1 xbar) (geometricModuleStalk B S hS X xbar F) :=
      (geometricModuleStalk B S hS X xbar F).isModule
    (IsLocalRing.maximalIdeal (etaleLocalRing B S hS X.1 xbar)).FG →
      (IsWeaklyAssociatedPrime (etaleLocalRing B S hS X.1 xbar)
          (geometricModuleStalk B S hS X xbar F)
          (IsLocalRing.maximalIdeal (etaleLocalRing B S hS X.1 xbar)) ↔
        IsAssociatedPrimeStacks (etaleLocalRing B S hS X.1 xbar)
          (geometricModuleStalk B S hS X xbar F)
          (IsLocalRing.maximalIdeal (etaleLocalRing B S hS X.1 xbar)))

AlgebraicGeometry.Space.isWeaklyAssociatedPoint_iff_exists_isAssociatedPrimeStacks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedTFAE.lean, line 255. The attribute's comment: “conditions (3) and (6) on a Noetherian algebraic space”.

Stacks 0CTW, (3) ⟺ (6) on a Noetherian algebraic space: a point is weakly associated to an 𝒪_X-module exactly when, at some geometric point above it, the maximal ideal of the étale local ring is an associated prime of the geometric stalk.

theorem isWeaklyAssociatedPoint_iff_exists_isAssociatedPrimeStacks
    (hZ : B.Contains (⊤_ Scheme.{u})) (hNoetherian : IsNoetherian B S hS hZ X.1)
    (F : Modules.{u, m} B S hS X.1 X.2) (x : points B S hS X.1) :
    IsWeaklyAssociatedPoint B S hS X F x ↔
      ∃ xbar : GeometricPoint B S hS X.1, xbar.LiesOver x ∧
        letI : IsLocalRing (etaleLocalRing B S hS X.1 xbar) :=
          isLocalRing_etaleLocalRing B S hS X.1 X.2 xbar
        letI : Module (etaleLocalRing B S hS X.1 xbar) (geometricModuleStalk B S hS X xbar F) :=
          (geometricModuleStalk B S hS X xbar F).isModule
        IsAssociatedPrimeStacks (etaleLocalRing B S hS X.1 xbar)
          (geometricModuleStalk B S hS X xbar F)
          (IsLocalRing.maximalIdeal (etaleLocalRing B S hS X.1 xbar))

AlgebraicGeometry.Space.weaklyAssociatedPoints_eq_setOf_exists_isAssociatedPrimeStacks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedTFAE.lean, line 279. The attribute's comment: “conditions (3) and (6) as a set of points”.

Stacks 0CTW, (3) ⟺ (6) on a Noetherian algebraic space, as an equality of sets of points: WeakAss(F) is the set of points carrying a geometric point at whose stalk the maximal ideal of the étale local ring is an associated prime.

theorem weaklyAssociatedPoints_eq_setOf_exists_isAssociatedPrimeStacks
    (hZ : B.Contains (⊤_ Scheme.{u})) (hNoetherian : IsNoetherian B S hS hZ X.1)
    (F : Modules.{u, m} B S hS X.1 X.2) :
    weaklyAssociatedPoints B S hS X F =
      {x : points B S hS X.1 | ∃ xbar : GeometricPoint B S hS X.1, xbar.LiesOver x ∧
        letI : IsLocalRing (etaleLocalRing B S hS X.1 xbar) :=
          isLocalRing_etaleLocalRing B S hS X.1 X.2 xbar
        letI : Module (etaleLocalRing B S hS X.1 xbar) (geometricModuleStalk B S hS X xbar F) :=
          (geometricModuleStalk B S hS X xbar F).isModule
        IsAssociatedPrimeStacks (etaleLocalRing B S hS X.1 xbar)
          (geometricModuleStalk B S hS X xbar F)
          (IsLocalRing.maximalIdeal (etaleLocalRing B S hS X.1 xbar))}

AlgebraicGeometry.Space.isWeaklyAssociatedPrime_maximalIdeal_geometricModuleStalk_of_chart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedTFAE.lean, line 325. The attribute's comment: “condition (1) implies condition (3) at a geometric point”.

Stacks 0CTW, (1) ⟹ (3). Let F be a quasi-coherent 𝒪_X-module and let φ : (U, ū) → (X, x̄) be an étale neighbourhood of a geometric point x̄ whose chart U is a scheme. If u is weakly associated to φ^*F, then the maximal ideal of 𝒪_{X, x̄} is a weakly associated prime of the geometric stalk F_{x̄}.

By Stacks 05VP the geometric stalk is (φ^*F)_u ⊗_{𝒪_{U, u}} 𝒪_{X, x̄} and the comparison map is flat and carries the maximal ideal of 𝒪_{U, u} onto that of 𝒪_{X, x̄}.

theorem isWeaklyAssociatedPrime_maximalIdeal_geometricModuleStalk_of_chart
    {xbar : GeometricPoint B S hS X.1} (V : SmallEtaleNeighborhood xbar)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite]
    (h : Stacks.Divisors.IsWeaklyAssociatedPoint (restrictToChart B S hS X.2 F V.chart)
      (chartPoint B S hS X.1 V)) :
    letI : IsLocalRing (etaleLocalRing B S hS X.1 xbar) :=
      isLocalRing_etaleLocalRing B S hS X.1 X.2 xbar
    letI : Module (etaleLocalRing B S hS X.1 xbar) (geometricModuleStalk B S hS X xbar F) :=
      (geometricModuleStalk B S hS X xbar F).isModule
    IsWeaklyAssociatedPrime (etaleLocalRing B S hS X.1 xbar)
      (geometricModuleStalk B S hS X xbar F)
      (IsLocalRing.maximalIdeal (etaleLocalRing B S hS X.1 xbar))

AlgebraicGeometry.Space.isWeaklyAssociatedPoint_restrictToChart_of_isWeaklyAssociatedPrime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedTFAE.lean, line 365. The attribute's comment: “condition (3) implies condition (1) at an étale neighbourhood”.

Stacks 0CTW, (3) ⟹ (1). Let F be a quasi-coherent 𝒪_X-module and let φ : (U, ū) → (X, x̄) be an étale neighbourhood of a geometric point x̄ whose chart U is a scheme. If the maximal ideal of 𝒪_{X, x̄} is a weakly associated prime of F_{x̄} then u is weakly associated to φ^*F.

This is the descent of weak association from a strict henselization, Stacks 0CTU: the étale local ring at x̄ is the strict henselization of 𝒪_{U, u} chosen in AlgebraicGeometry.Space.chartHenselizationTower by Stacks 04KF, and the geometric stalk is the base change of the Zariski stalk (φ^*F)_u along it by Stacks 05VP.

theorem isWeaklyAssociatedPoint_restrictToChart_of_isWeaklyAssociatedPrime
    {xbar : GeometricPoint B S hS X.1} (V : SmallEtaleNeighborhood xbar)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite]
    (h : letI : IsLocalRing (etaleLocalRing B S hS X.1 xbar) :=
          isLocalRing_etaleLocalRing B S hS X.1 X.2 xbar
        letI : Module (etaleLocalRing B S hS X.1 xbar)
            (geometricModuleStalk B S hS X xbar F) :=
          (geometricModuleStalk B S hS X xbar F).isModule
        IsWeaklyAssociatedPrime (etaleLocalRing B S hS X.1 xbar)
          (geometricModuleStalk B S hS X xbar F)
          (IsLocalRing.maximalIdeal (etaleLocalRing B S hS X.1 xbar))) :
    Stacks.Divisors.IsWeaklyAssociatedPoint (restrictToChart B S hS X.2 F V.chart)
      (chartPoint B S hS X.1 V)

AlgebraicGeometry.Space.isWeaklyAssociatedPoint_restrictToChart_of_isWeaklyAssociatedPrime_of_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedTFAE.lean, line 432. The attribute's comment: “condition (3) implies condition (1) at a chart whose Zariski module stalk has finitely many weakly associated primes”.

Stacks 0CTW, (3) ⟹ (1), by flat descent over finitely many weakly associated primes. The conclusion of AlgebraicGeometry.Space.isWeaklyAssociatedPoint_restrictToChart_of_isWeaklyAssociatedPrime, reached instead by flat descent of weak association along the comparison map of Stacks 05VP, under finiteness of the set of weakly associated primes of the Zariski module stalk of the chart.

Stacks.WeaklyAssociatedPrimes.isWeaklyAssociatedPrime_comap_tensorProduct, used here, turns the covering of the maximal ideal by the weakly associated primes of the localization into an equality by prime avoidance over finitely many primes. That is not the source's own route: Stacks 0CTW proves (1), (2) and (3) equivalent with nothing beyond quasi-coherence, by More on Flatness, Lemma 38.2.9, which is Tag 0CTU, and which AlgebraicGeometry.Space.isWeaklyAssociatedPoint_restrictToChart_of_isWeaklyAssociatedPrime above now takes. This form is retained as the one a local finiteness statement about the weakly associated points of the chart discharges directly, since the primes of the local ring at a point all lie in every neighbourhood of it.

theorem isWeaklyAssociatedPoint_restrictToChart_of_isWeaklyAssociatedPrime_of_finite
    {xbar : GeometricPoint B S hS X.1} (V : SmallEtaleNeighborhood xbar)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite]
    (hfin : (weaklyAssociatedPrimes (chartLocalRing B S hS X.1 V)
      (chartZariskiModuleStalk B S hS X.1 X.2 V F)).Finite)
    (h : letI : IsLocalRing (etaleLocalRing B S hS X.1 xbar) :=
          isLocalRing_etaleLocalRing B S hS X.1 X.2 xbar
        letI : Module (etaleLocalRing B S hS X.1 xbar)
            (geometricModuleStalk B S hS X xbar F) :=
          (geometricModuleStalk B S hS X xbar F).isModule
        IsWeaklyAssociatedPrime (etaleLocalRing B S hS X.1 xbar)
          (geometricModuleStalk B S hS X xbar F)
          (IsLocalRing.maximalIdeal (etaleLocalRing B S hS X.1 xbar))) :
    Stacks.Divisors.IsWeaklyAssociatedPoint (restrictToChart B S hS X.2 F V.chart)
      (chartPoint B S hS X.1 V)

AlgebraicGeometry.Space.isWeaklyAssociatedPoint_restrictToChart_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedTFAE.lean, line 474. The attribute's comment: “conditions (1) and (3) at an étale neighbourhood”.

Stacks 0CTW, (1) ⟺ (3) at an étale neighbourhood: the point u of the chart is weakly associated to φ^*F exactly when the maximal ideal of 𝒪_{X, x̄} is a weakly associated prime of F_{x̄}.

theorem isWeaklyAssociatedPoint_restrictToChart_iff
    {xbar : GeometricPoint B S hS X.1} (V : SmallEtaleNeighborhood xbar)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite] :
    Stacks.Divisors.IsWeaklyAssociatedPoint (restrictToChart B S hS X.2 F V.chart)
        (chartPoint B S hS X.1 V) ↔
      letI : IsLocalRing (etaleLocalRing B S hS X.1 xbar) :=
        isLocalRing_etaleLocalRing B S hS X.1 X.2 xbar
      letI : Module (etaleLocalRing B S hS X.1 xbar) (geometricModuleStalk B S hS X xbar F) :=
        (geometricModuleStalk B S hS X xbar F).isModule
      IsWeaklyAssociatedPrime (etaleLocalRing B S hS X.1 xbar)
        (geometricModuleStalk B S hS X xbar F)
        (IsLocalRing.maximalIdeal (etaleLocalRing B S hS X.1 xbar))

AlgebraicGeometry.Space.isWeaklyAssociatedPoint_of_isWeaklyAssociatedPoint_restrictToChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedTFAE.lean, line 493. The attribute's comment: “condition (1) implies the weak association of Stacks 0CTX”.

Stacks 0CTW, (1) ⟹ (3) in the form of Stacks 0CTX. If the point u of an étale scheme chart is weakly associated to φ^*F then the point of X it lies over is weakly associated to F.

theorem isWeaklyAssociatedPoint_of_isWeaklyAssociatedPoint_restrictToChart
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite] (x : points B S hS X.1)
    {xbar : GeometricPoint B S hS X.1} (hxbar : xbar.LiesOver x)
    (V : SmallEtaleNeighborhood xbar)
    (h : Stacks.Divisors.IsWeaklyAssociatedPoint (restrictToChart B S hS X.2 F V.chart)
      (chartPoint B S hS X.1 V)) :
    IsWeaklyAssociatedPoint B S hS X F x

AlgebraicGeometry.Space.isWeaklyAssociatedPoint_restrictToChart_of_restrictToChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedTFAE.lean, line 507. The attribute's comment: “conditions (1) and (2) for the étale neighbourhoods of a geometric point”.

Stacks 0CTW, conditions (1) and (2). Weak association at a chart point does not depend on the chart: if the point of one étale scheme chart of x̄ is weakly associated to the restriction of F there, so is the point of any other.

theorem isWeaklyAssociatedPoint_restrictToChart_of_restrictToChart
    {xbar : GeometricPoint B S hS X.1} (V V' : SmallEtaleNeighborhood xbar)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite]
    (h : Stacks.Divisors.IsWeaklyAssociatedPoint (restrictToChart B S hS X.2 F V.chart)
      (chartPoint B S hS X.1 V)) :
    Stacks.Divisors.IsWeaklyAssociatedPoint (restrictToChart B S hS X.2 F V'.chart)
      (chartPoint B S hS X.1 V')

AlgebraicGeometry.Space.isWeaklyAssociatedPoint_iff_exists_restrictToChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedTFAE.lean, line 522. The attribute's comment: “conditions (1) and (2) as the weak association of Stacks 0CTX”.

Stacks 0CTW, conditions (1) and (2) in the form of Stacks 0CTX. A point of X is weakly associated to a quasi-coherent F exactly when, at some geometric point above it, the corresponding point of some étale scheme chart is weakly associated to the restriction of F there.

theorem isWeaklyAssociatedPoint_iff_exists_restrictToChart
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite] (x : points B S hS X.1) :
    IsWeaklyAssociatedPoint B S hS X F x ↔
      ∃ (xbar : GeometricPoint B S hS X.1), xbar.LiesOver x ∧
        ∃ V : SmallEtaleNeighborhood xbar,
          Stacks.Divisors.IsWeaklyAssociatedPoint (restrictToChart B S hS X.2 F V.chart)
            (chartPoint B S hS X.1 V)

Tag 0CTX, a definition

Tag 0CTX in the Stacks Project.

AlgebraicGeometry.Space.isWeaklyAssociatedPoint_iff_moduleStalkLarge, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedChart.lean, line 129. The attribute's comment: “weak association on the stalk at the point of the small étale site”.

Stacks 0CTX, weak association read before the extension of scalars: a point of an algebraic space is weakly associated to an 𝒪_X-module exactly when, at some geometric point above it, the maximal ideal of the stalk of the structure sheaf at the corresponding point of the small étale site is weakly associated to the stalk of the module there.

theorem isWeaklyAssociatedPoint_iff_moduleStalkLarge (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (X : AlgebraicSpaces B S hS) (F : Modules.{u, m} B S hS X.1 X.2)
    (x : points B S hS X.1) :
    IsWeaklyAssociatedPoint B S hS X F x ↔
      ∃ xbar : GeometricPoint B S hS X.1, xbar.LiesOver x ∧
        letI : IsLocalRing (etaleLocalRing B S hS X.1 xbar) :=
          isLocalRing_etaleLocalRing B S hS X.1 X.2 xbar
        letI : IsLocalRing
            (((etaleSitePoint B S hS X.1 xbar X.2).presheafFiber (A := CommRingCat.{u})).obj
              (smallEtaleRingedTopos B S hS X).O.obj) :=
          (pointStalkRingEquiv B S hS X xbar).symm.isLocalRing
        IsWeaklyAssociatedPrime
          (((etaleSitePoint B S hS X.1 xbar X.2).presheafFiber (A := CommRingCat.{u})).obj
            (smallEtaleRingedTopos B S hS X).O.obj)
          (Stacks.moduleStalkLarge (etaleSitePoint B S hS X.1 xbar X.2)
            (smallEtaleRingedTopos B S hS X).O F)
          (IsLocalRing.maximalIdeal _)

AlgebraicGeometry.Space.isWeaklyAssociatedPoint_of_forall_exists_pow_smul_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedMinimalSupport.lean, line 217. The attribute's comment: “weak association from a stalk element killed by powers of the non-units”.

Stacks 0CTX, the algebraic criterion for weak association. A point of an algebraic space is weakly associated to an 𝒪_X-module as soon as, at some geometric point above it, the geometric stalk has a nonzero element some power of each non-unit of the étale local ring annihilates: the annihilator of that element lies in the maximal ideal because the ring is local, and a prime below the maximal ideal containing the annihilator then contains every non-unit.

theorem isWeaklyAssociatedPoint_of_forall_exists_pow_smul_eq_zero
    (F : Modules.{u, m} B S hS X.1 X.2) (x : points B S hS X.1)
    (xbar : GeometricPoint B S hS X.1) (hxbar : xbar.LiesOver x)
    (t : geometricModuleStalk B S hS X xbar F) (ht : t ≠ 0)
    (hpow : ∀ a : etaleLocalRing B S hS X.1 xbar, ¬ IsUnit a → ∃ n : ℕ, a ^ n • t = 0) :
    IsWeaklyAssociatedPoint B S hS X F x

AlgebraicGeometry.Space.IsWeaklyAssociatedPoint, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedPoints.lean, line 73. The attribute's comment: “weakly associated point”.

Stacks 0CTX, part (1). A point x of an algebraic space X is weakly associated to an 𝒪_X-module F when, at some geometric point above x, the maximal ideal of the étale local ring is a weakly associated prime of the geometric stalk of F, that is, when it is minimal among the primes containing the annihilator of some element of that stalk.

noncomputable def IsWeaklyAssociatedPoint (F : Modules.{u, m} B S hS X.1 X.2)
    (x : points B S hS X.1) : Prop

AlgebraicGeometry.Space.weaklyAssociatedPoints, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedPoints.lean, line 86. The attribute's comment: “set of weakly associated points”.

Stacks 0CTX, part (2). The set WeakAss(F) of points of an algebraic space weakly associated to an 𝒪_X-module F.

noncomputable abbrev weaklyAssociatedPoints (F : Modules.{u, m} B S hS X.1 X.2) :
    Set (points B S hS X.1)

AlgebraicGeometry.Space.weaklyAssociatedPointsOfSpace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedPoints.lean, line 101. The attribute's comment: “weakly associated points of the space”.

Stacks 0CTX, part (3). The weakly associated points WeakAss(X) of an algebraic space X are the weakly associated points of its structure sheaf.

noncomputable abbrev weaklyAssociatedPointsOfSpace : Set (points B S hS X.1)

Tag 0CTY, a lemma

Tag 0CTY in the Stacks Project.

AlgebraicGeometry.Space.weaklyAssociatedPoints_subset_supportOfSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedSupport.lean, line 153.

Stacks 0CTY. The weakly associated points of an 𝒪_X-module on an algebraic space lie in the support of its underlying abelian sheaf.

theorem weaklyAssociatedPoints_subset_supportOfSheaf
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (X : AlgebraicSpaces B S hS) (F : Modules.{u, m} B S hS X.1 X.2) :
    weaklyAssociatedPoints B S hS X F ⊆
      supportOfSheaf B S hS X.1 ((SheafOfModules.toSheaf _).obj F)

Tag 0CTZ, a lemma

Tag 0CTZ in the Stacks Project.

AlgebraicGeometry.Space.weaklyAssociatedPoints_subset_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedShortExact.lean, line 313. The attribute's comment: “subsheaf”.

Stacks 0CTZ, first inclusion. In a short exact sequence of 𝒪_X-modules on an algebraic space, every weakly associated point of the first module is weakly associated to the middle module.

theorem weaklyAssociatedPoints_subset_of_shortExact
    (σ : ShortComplex (Modules.{u, m} B S hS X.1 X.2)) (hσ : σ.ShortExact) :
    weaklyAssociatedPoints B S hS X σ.X₁ ⊆ weaklyAssociatedPoints B S hS X σ.X₂

AlgebraicGeometry.Space.weaklyAssociatedPoints_subset_union_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedShortExact.lean, line 328. The attribute's comment: “middle_term”.

Stacks 0CTZ, second inclusion. In a short exact sequence of 𝒪_X-modules on an algebraic space, every weakly associated point of the middle module is weakly associated to one of the outer modules.

theorem weaklyAssociatedPoints_subset_union_of_shortExact
    [Balanced (Modules.{u, m} B S hS X.1 X.2)]
    (σ : ShortComplex (Modules.{u, m} B S hS X.1 X.2)) (hσ : σ.ShortExact) :
    weaklyAssociatedPoints B S hS X σ.X₂ ⊆
      weaklyAssociatedPoints B S hS X σ.X₁ ∪ weaklyAssociatedPoints B S hS X σ.X₃

AlgebraicGeometry.Space.weaklyAssociatedPoints_subset_union_of_shortExact_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedShortExactBalanced.lean, line 48. The attribute's comment: “middle_term, for sections in any universe containing the universe of the schemes and with no assumed inputs: the balancedness of the category of modules that the general form takes as an instance hypothesis is discharged here”.

Stacks 0CTZ, second inclusion. In a short exact sequence of 𝒪_X-modules on an algebraic space, every weakly associated point of the middle module is weakly associated to one of the outer modules.

This is AlgebraicGeometry.Space.weaklyAssociatedPoints_subset_union_of_shortExact with its balancedness instance supplied by AlgebraicGeometry.Space.balanced_modules_max: the 𝒪_X-modules with sections in a universe containing the universe of the schemes are abelian, the small étale site being essentially small there, and an abelian category is balanced.

theorem weaklyAssociatedPoints_subset_union_of_shortExact_unconditional
    (σ : ShortComplex (Modules.{u, max u m} B S hS X.1 X.2)) (hσ : σ.ShortExact) :
    weaklyAssociatedPoints B S hS X σ.X₂ ⊆
      weaklyAssociatedPoints B S hS X σ.X₁ ∪ weaklyAssociatedPoints B S hS X σ.X₃

Tag 0CU0, a lemma

Tag 0CU0 in the Stacks Project.

AlgebraicGeometry.Space.weaklyAssociatedPoints_eq_empty_of_isZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedVanishing.lean, line 74. The attribute's comment: “a zero module has no weakly associated points”.

Stacks 0CU0, the direction that a vanishing module has no weakly associated points: a zero 𝒪_X-module on an algebraic space has empty set of weakly associated points.

theorem weaklyAssociatedPoints_eq_empty_of_isZero
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (X : AlgebraicSpaces B S hS) (F : Modules.{u, m} B S hS X.1 X.2) (hF : IsZero F) :
    weaklyAssociatedPoints B S hS X F = ∅

AlgebraicGeometry.Space.isZero_iff_weaklyAssociatedPoints_eq_empty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedVanishingQuasicoherent.lean, line 100.

Stacks 0CU0. A quasi-coherent 𝒪_X-module on an algebraic space is zero if and only if it has no weakly associated point.

theorem isZero_iff_weaklyAssociatedPoints_eq_empty (F : Modules.{u, u} B S hS X.1 X.2)
    [F.IsQuasicoherentOnSite] : IsZero F ↔ weaklyAssociatedPoints B S hS X F = ∅

Tag 0CUL, a lemma

Tag 0CUL in the Stacks Project.

AlgebraicGeometry.Space.isWeaklyAssociatedPoint_of_mem_supportOfSheaf_of_localRingDimension_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedCodimensionZero.lean, line 90. The attribute's comment: “the first assertion, that a codimension-zero point of the support is weakly associated, stated for every module in place of a quasi-coherent one”.

Stacks 0CUL, the first assertion. A point of an algebraic space which lies in the support of an 𝒪_X-module and has codimension zero, in the sense that the local ring of the space there has Krull dimension zero, is weakly associated to that module.

theorem isWeaklyAssociatedPoint_of_mem_supportOfSheaf_of_localRingDimension_eq_zero
    (F : Modules.{u, m} B S hS X.1 X.2) (x : points B S hS X.1)
    (hsupp : x ∈ supportOfSheaf B S hS X.1 ((SheafOfModules.toSheaf _).obj F))
    (codim : localRingDimension B S hS x = 0) :
    IsWeaklyAssociatedPoint B S hS X F x

AlgebraicGeometry.Space.isWeaklyAssociatedPoint_of_localRingDimension_schemeTheoreticSupport_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedCodimensionZero.lean, line 152. The attribute's comment: “the second assertion, for a codimension-zero point of the scheme theoretic support of a quasi-coherent module of finite type”.

Stacks 0CUL, the second assertion. Let F be a quasi-coherent 𝒪_X-module of finite type with scheme theoretic support Z. A point of Z of codimension zero in Z, in the sense that the local ring of Z there has Krull dimension zero, has an image in X weakly associated to F.

The scheme theoretic support is a closed subspace and F is the direct image of a quasi-coherent module G on it, by Stacks 07U0; the direct image of Stacks 03LU along the closed immersion is the direct image along base change of étale charts. The image of the point lies in the support of F, which is the set of points of Z, so the stalk of G at a geometric point above it is nonzero, and the first assertion's argument applies on Z.

theorem isWeaklyAssociatedPoint_of_localRingDimension_schemeTheoreticSupport_eq_zero
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite]
    [SheafOfModules.IsFiniteTypeOnSite F]
    (x : points B S hS (schemeTheoreticSupport B S hS X F).toFunctor)
    (codim : localRingDimension B S hS x = 0) :
    IsWeaklyAssociatedPoint B S hS X F
      (pointsMap B S hS (schemeTheoreticSupport B S hS X F).toFunctor
        (schemeTheoreticSupport B S hS X F).ι x)

Tag 0CUM, a lemma

Tag 0CUM in the Stacks Project.

AlgebraicGeometry.Space.isWeaklyAssociatedPoint_of_mem_supportOfSheaf_of_specializes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedMinimalSupportDecent.lean, line 206. The attribute's comment: “with decency read as condition (α) of Stacks 03JX, which is all Stacks 03K5 needs, and with no assumed inputs”.

Stacks 0CUM. Let X be an algebraic space over S all of whose chart fibres are finite — in particular a decent one — and let F be a quasi-coherent 𝒪_X-module. A point of |X| which lies in the support of F and is not a specialization of another point of that support is weakly associated to F.

theorem isWeaklyAssociatedPoint_of_mem_supportOfSheaf_of_specializes
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite]
    (hdecent : HasFiniteChartFibersAtEveryPoint B S hS X.1)
    (x : points B S hS X.1)
    (hx : x ∈ supportOfSheaf B S hS X.1 ((SheafOfModules.toSheaf _).obj F))
    (hmin : ∀ y, y ∈ supportOfSheaf B S hS X.1 ((SheafOfModules.toSheaf _).obj F) →
      y ⤳ x → y = x) :
    IsWeaklyAssociatedPoint B S hS X F x

Tag 0CUN, a lemma

Tag 0CUN in the Stacks Project.

AlgebraicGeometry.Space.weaklyAssociatedPoints_inter_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedFinite.lean, line 92.

Stacks 0CUN. Let X be a locally Noetherian algebraic space over a scheme S and let F be a coherent 𝒪_X-module. Then the weakly associated points of F — the associated points, in the terminology of the source — meet every quasi-compact open subset of |X| in a finite set.

theorem weaklyAssociatedPoints_inter_finite
    (hX : HasEtaleLocalProperty B S hS X.1 (fun Y : Scheme.{u} => IsLocallyNoetherian Y))
    (F : Modules.{u, u} B S hS X.1 X.2) [hF : IsCoherent B S hS X.1 X.2 F]
    (W : Set (points B S hS X.1)) (_hWopen : IsOpen W) (hWcompact : IsCompact W) :
    (weaklyAssociatedPoints B S hS X F ∩ W).Finite

Tag 0CUP, a lemma

Tag 0CUP in the Stacks Project.

AlgebraicGeometry.Space.injective_sections_eval_of_weaklyAssociatedPoints_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedSectionsInjective.lean, line 106.

Stacks Project, Tag 0CUP. Let F be a quasi-coherent 𝒪_X-module on an algebraic space X and let U be an étale chart of X such that every weakly associated point of F lies in the image of |U| → |X|. Then the restriction Γ(X, F) → Γ(U, F) of global sections to the chart is injective.

theorem injective_sections_eval_of_weaklyAssociatedPoints_subset
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite] (U : SmallEtale B S hS X.1)
    (weakAss_subset :
      weaklyAssociatedPoints B S hS X F ⊆ Set.range (chartSchemeToPoints B S hS X.1 U)) :
    Function.Injective fun s : F.sections => s.eval (op U)

Tag 0CUQ, a lemma

Tag 0CUQ in the Stacks Project.

AlgebraicGeometry.Space.not_isWeaklyAssociatedPoint_modulePushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/SpacePushforwardWeaklyAssociatedRange.lean, line 53.

Stacks 0CUQ. Let f : X ⟶ Y be a quasi-compact morphism of algebraic spaces over S, let F be a quasi-coherent 𝒪_X-module and let y be a point of Y outside the image of |f|. Then y is not weakly associated to f_*F.

This is AlgebraicGeometry.Space.not_isWeaklyAssociatedPoint_modulePushforward_of_notMem_range with its Stacks 0CU2 hypothesis discharged by AlgebraicGeometry.Space.weaklyAssociatedPoints_modulePushforward_subset_image_of_isAffineHom. Quasi-separatedness of f, which the source assumes, is not needed; see the implementation notes of StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedPushforward.lean.

theorem not_isWeaklyAssociatedPoint_modulePushforward
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hfqc : IsQuasiCompact B S hS f.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite)
    (y : points B S hS Y.1) (hy : y ∉ Set.range (pointsMap B S hS X.1 f.hom)) :
    ¬ IsWeaklyAssociatedPoint B S hS Y ((modulePushforward B S hS f).obj F) y

AlgebraicGeometry.Space.weaklyAssociatedPoints_modulePushforward_subset_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/SpacePushforwardWeaklyAssociatedRange.lean, line 70. The attribute's comment: “as an inclusion of sets of points”.

Stacks 0CUQ, as an inclusion of sets of points. Let f : X ⟶ Y be a quasi-compact morphism of algebraic spaces over S and let F be a quasi-coherent 𝒪_X-module. Then every weakly associated point of f_*F lies in the image of |f|.

This is the pointwise statement AlgebraicGeometry.Space.not_isWeaklyAssociatedPoint_modulePushforward contraposed.

theorem weaklyAssociatedPoints_modulePushforward_subset_range
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hfqc : IsQuasiCompact B S hS f.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite) :
    weaklyAssociatedPoints B S hS Y ((modulePushforward B S hS f).obj F) ⊆
      Set.range (pointsMap B S hS X.1 f.hom)

AlgebraicGeometry.Space.not_isWeaklyAssociatedPoint_modulePushforward_of_notMem_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedPushforward.lean, line 390. The attribute's comment: “granting Stacks 0CU2”.

Stacks 0CUQ, granting Stacks 0CU2.

Let f : X ⟶ Y be a quasi-compact morphism of algebraic spaces over S, let F be a quasi-coherent 𝒪_X-module and let y be a point of Y outside the image of |f|. Then y is not weakly associated to f_*F.

The hypothesis h0CU2 is Stacks 0CU2, the inclusion WeakAss(g_*H) ⊆ |g|(WeakAss(H)) for an affine morphism g; it is the one step of the source's argument that this development does not have. Quasi-separatedness of f, which the source assumes, is not needed: it enters the source only through Stacks 03M9, and the argument below does not use quasi-coherence of the direct image, so Stacks 03M9 is not needed either.

theorem not_isWeaklyAssociatedPoint_modulePushforward_of_notMem_range
    (h0CU2 : AffinePushforwardWeaklyAssociatedImage B S hS)
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hfqc : IsQuasiCompact B S hS f.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite)
    (y : points B S hS Y.1) (hy : y ∉ Set.range (pointsMap B S hS X.1 f.hom)) :
    ¬ IsWeaklyAssociatedPoint B S hS Y ((modulePushforward B S hS f).obj F) y

Tag 0CUR, a lemma

Tag 0CUR in the Stacks Project.

AlgebraicGeometry.Space.mono_of_stalk_injective_or_notMem_weaklyAssociatedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedInjective.lean, line 250.

Stacks Project, Tag 0CUR.

Let φ : F ⟶ G be a map of quasi-coherent 𝒪_X-modules on an algebraic space X such that every point x of X satisfies at least one of: the induced map F_x̄ → G_x̄ is injective for a geometric point x̄ above x, or x is not a weakly associated point of F. Then φ is injective.

The proof follows the source: Ker(φ) is quasi-coherent by the kernel clause of Stacks 03M1(3), WeakAss(Ker(φ)) = ∅, and Ker(φ) vanishes by Stacks 0CU0.

theorem mono_of_stalk_injective_or_notMem_weaklyAssociatedPoints
    (F G : Modules.{u, u} B S hS X.1 X.2)
    [F.IsQuasicoherentOnSite] [G.IsQuasicoherentOnSite] (φ : F ⟶ G)
    (hφ : ∀ y : points B S hS X.1,
      (∃ ybar : GeometricPoint B S hS X.1, ybar.LiesOver y ∧
          Function.Injective (geometricModuleStalkMap B S hS X ybar φ)) ∨
        y ∉ weaklyAssociatedPoints B S hS X F) :
    Mono φ

Tag 0EN1, a lemma

Tag 0EN1 in the Stacks Project.

AlgebraicGeometry.Space.weaklyAssociatedPointsOfSpace_eq_setOf_localRingDimension_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedReduced.lean, line 198.

Stacks 0EN1. The weakly associated points of a reduced algebraic space are exactly its points of codimension zero, that is the points whose local ring has Krull dimension zero.

theorem weaklyAssociatedPointsOfSpace_eq_setOf_localRingDimension_eq_zero
    (hred : HasEtaleLocalProperty B S hS X.1 (fun Y : Scheme.{u} => IsReduced Y)) :
    weaklyAssociatedPointsOfSpace B S hS X =
      {x : points B S hS X.1 | localRingDimension B S hS x = 0}

Sources

• Section 71.2, Tag 0CTV
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.isWeaklyAssociatedPoint_restrictToChart_iff_isWeaklyAssociatedPoint · AlgebraicGeometry.Space.isAssociatedPoint_restrictToChart_iff_isWeaklyAssociatedPoint · AlgebraicGeometry.Space.isWeaklyAssociatedPoint_iff_exists_isAssociatedPoint_restrictToChart · AlgebraicGeometry.Space.isWeaklyAssociatedPoint_iff_forall_isAssociatedPoint_restrictToChart · AlgebraicGeometry.Space.exists_isAssociatedPoint_restrictToChart_iff_forall · AlgebraicGeometry.Space.isAssociatedPoint_restrictToChart_iff_isWeaklyAssociatedPrime · AlgebraicGeometry.Space.isAssociatedPoint_restrictToChart_iff_isAssociatedPrimeStacks · AlgebraicGeometry.Space.isWeaklyAssociatedPrime_maximalIdeal_iff_isAssociatedPrimeStacks

Section71.3 Morphisms and weakly associated points#

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

Tag 0CU2, a lemma

Tag 0CU2 in the Stacks Project.

AlgebraicGeometry.Space.weaklyAssociatedPoints_modulePushforward_subset_image_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/SpaceAffineDirectImage.lean, line 148.

Let f : X ⟶ Y be an affine morphism of algebraic spaces over S and let F be a quasi-coherent 𝒪_X-module. Then every weakly associated point of f_*F is the image of a weakly associated point of F.

theorem weaklyAssociatedPoints_modulePushforward_subset_image_of_isAffineHom
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hf : IsAffineHom B S hS f.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite) :
    weaklyAssociatedPoints B S hS Y ((modulePushforward B S hS f).obj F) ⊆
      pointsMap B S hS X.1 f.hom '' weaklyAssociatedPoints B S hS X F

AlgebraicGeometry.Space.affinePushforwardWeaklyAssociatedImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/SpaceAffinePushforward.lean, line 62. The attribute's comment: “the reduction to a target represented by an affine scheme of the site, which is the hypothesis h; that case needs the comparison of the Zariski and small-étale modules of a represented algebraic space, absent here”.

Let f : X ⟶ Y be an affine morphism of algebraic spaces over S and let F be a quasi-coherent 𝒪_X-module. Granted the hypothesis h, the same inclusion for a target represented by an affine scheme of the site, every weakly associated point of f_*F is the image of a weakly associated point of F.

theorem affinePushforwardWeaklyAssociatedImage
    (h : SchemeTargetAffinePushforwardWeaklyAssociatedImage B S hS) :
    AffinePushforwardWeaklyAssociatedImage B S hS

Tag 0CU8, a lemma

Tag 0CU8 in the Stacks Project.

AlgebraicGeometry.Space.weaklyAssociatedPoints_modulePushforward_eq_image_of_isAffineHom_locallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/SpaceAffineDirectImageLocallyNoetherian.lean, line 58.

Let f : X ⟶ Y be an affine morphism of algebraic spaces over S and let F be a quasi-coherent 𝒪_X-module. If X is locally Noetherian, then the weakly associated points of f_*F are exactly the images of the weakly associated points of F.

theorem weaklyAssociatedPoints_modulePushforward_eq_image_of_isAffineHom_locallyNoetherian
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hf : IsAffineHom B S hS f.hom)
    (hX : HasEtaleLocalProperty B S hS X.1
      (fun T : Scheme.{u} => _root_.AlgebraicGeometry.IsLocallyNoetherian T))
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite) :
    weaklyAssociatedPoints B S hS Y ((modulePushforward B S hS f).obj F) =
      pointsMap B S hS X.1 f.hom '' weaklyAssociatedPoints B S hS X F

AlgebraicGeometry.Space.weaklyAssociatedPoints_modulePushforward_eq_image_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/WeaklyAssociatedAffinePushforward.lean, line 342.

Stacks 0CU8. Let f : X → Y be an affine morphism of algebraic spaces with X locally Noetherian and let F be a quasi-coherent 𝒪_X-module. Then the weakly associated points of the direct image f_*F are exactly the images of the weakly associated points of F.

The inclusion h0CU2 is Stacks 0CU2, and h05VP is the affine chart presentation of the two geometric stalks of Stacks 05VP, which also carries the quasi-coherence of the direct image of Stacks 03M9; both are assumed here in the affine, locally Noetherian, quasi-coherent situation in which they are asserted.

theorem weaklyAssociatedPoints_modulePushforward_eq_image_of_isAffineHom
    (hf : IsAffineHom B S hS f.hom)
    (hX : HasEtaleLocalProperty B S hS X.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite)
    (h0CU2 : IsAffineHom B S hS f.hom →
      HasEtaleLocalProperty B S hS X.1 (fun T : Scheme.{u} => IsLocallyNoetherian T) →
      F.IsQuasicoherentOnSite →
      weaklyAssociatedPoints B S hS Y ((modulePushforward B S hS f).obj F) ⊆
        pointsMap B S hS X.1 f.hom '' weaklyAssociatedPoints B S hS X F)
    (h05VP : IsAffineHom B S hS f.hom →
      HasEtaleLocalProperty B S hS X.1 (fun T : Scheme.{u} => IsLocallyNoetherian T) →
      F.IsQuasicoherentOnSite →
      ∀ xbar : GeometricPoint B S hS X.1,
        HasAffineStalkSquare B S hS f F ((modulePushforward B S hS f).obj F) xbar) :
    weaklyAssociatedPoints B S hS Y ((modulePushforward B S hS f).obj F) =
      pointsMap B S hS X.1 f.hom '' weaklyAssociatedPoints B S hS X F

Tag 0CU9, a lemma

Tag 0CU9 in the Stacks Project.

AlgebraicGeometry.Space.weaklyAssociatedPoints_modulePushforward_eq_image_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/SpaceFiniteDirectImage.lean, line 164.

Weakly associated points of a finite direct image. Let f : X ⟶ Y be a finite morphism of algebraic spaces over a scheme S and let F be a quasi-coherent 𝒪_X-module. Then WeakAss(f_*F) = f(WeakAss(F)).

theorem weaklyAssociatedPoints_modulePushforward_eq_image_of_isFinite
    {X Y : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hf : IsFinite B S hS f.hom) (F : Modules.{u, u} B S hS X.1 X.2)
    (hF : F.IsQuasicoherentOnSite) :
    weaklyAssociatedPoints B S hS Y ((modulePushforward B S hS f).obj F) =
      pointsMap B S hS X.1 f.hom '' weaklyAssociatedPoints B S hS X F

Tag 0CUA, a lemma

Tag 0CUA in the Stacks Project.

AlgebraicGeometry.Space.isWeaklyAssociatedPoint_modulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/SpacePullback.lean, line 368. The attribute's comment: “the zero-dimensional local ring of the fibre read as the equality of the maximal ideal of the étale local ring with the radical of the ideal extended from the maximal ideal of the target, at a geometric point above the given point”.

Stacks 0CUA. Let f : X ⟶ Y be a morphism of algebraic spaces over a scheme S, let G be an 𝒪_Y-module, let x be a point of X with image y, and let x̄ be a geometric point above x. Suppose that y is weakly associated to G, that f is flat at x, and that the local ring of the fibre of f at x̄ has dimension zero — that is, the maximal ideal of 𝒪_{X, x̄} is the radical of the ideal generated by the maximal ideal of 𝒪_{Y, ȳ}. Then x is weakly associated to f^*G.

The stalk of f^*G at x̄ is the base change 𝒪_{X, x̄} ⊗_{𝒪_{Y, ȳ}} G_{ȳ} by the base-change clause of Stacks 05VQ, and weak association at ȳ follows from weak association of y because the condition does not depend on the geometric point chosen above a point.

theorem isWeaklyAssociatedPoint_modulePullback (f : X ⟶ Y) (x : points B S hS X.1)
    (xbar : GeometricPoint B S hS X.1) (hxbar : xbar.LiesOver x)
    (hflat : IsFlatAt B S hS f.hom x) (G : Modules.{u, u} B S hS Y.1 Y.2) :
    letI : IsLocalRing (etaleLocalRing B S hS Y.1 (geometricPointMap f.hom xbar)) :=
      isLocalRing_etaleLocalRing B S hS Y.1 Y.2 (geometricPointMap f.hom xbar)
    letI : IsLocalRing (etaleLocalRing B S hS X.1 xbar) :=
      isLocalRing_etaleLocalRing B S hS X.1 X.2 xbar
    letI : Algebra (etaleLocalRing B S hS Y.1 (geometricPointMap f.hom xbar))
        (etaleLocalRing B S hS X.1 xbar) := (etaleLocalRingMap X.2 f.hom xbar).toAlgebra
    (Ideal.map (algebraMap (etaleLocalRing B S hS Y.1 (geometricPointMap f.hom xbar))
            (etaleLocalRing B S hS X.1 xbar))
          (maximalIdeal (etaleLocalRing B S hS Y.1 (geometricPointMap f.hom xbar)))).radical =
        maximalIdeal (etaleLocalRing B S hS X.1 xbar) →
      IsWeaklyAssociatedPoint B S hS Y G (pointsMap B S hS X.1 f.hom x) →
        IsWeaklyAssociatedPoint B S hS X ((modulePullback B S hS f).obj G) x

Tag 0CUS, a lemma

Tag 0CUS in the Stacks Project.

AlgebraicGeometry.Space.isWeaklyAssociatedPoint_fibre_of_refines, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/SpaceFibreEtaleRefinement.lean, line 163. The attribute's comment: “at a refinement of field-valued points of the target, read on the comparison of the two fibres”.

Weak association descends along a refinement of field-valued points. Let f : X ⟶ Y be a morphism of algebraic spaces over S, let F be a quasi-coherent 𝒪_X-module, let q refine p as a field-valued point of Y through κ : q.siteObject ⟶ p.siteObject, and let π be the comparison morphism of the fibre of f over q with the fibre of f over p, compatible with the projections to X and presenting the one fibre as the base change of the other along κ. If a point of the fibre over q is weakly associated to the restriction of F there, then its image in the fibre over p is weakly associated to the restriction of F there.

theorem isWeaklyAssociatedPoint_fibre_of_refines (f : X ⟶ Y)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite)
    {p q : FieldValuedPoint B S hS Y.1} (κ : q.siteObject ⟶ p.siteObject)
    {π : fibreAtFieldValuedPoint B S hS f q ⟶ fibreAtFieldValuedPoint B S hS f p}
    (hπ : π ≫ fibreAtFieldValuedPointProjection B S hS f p =
      fibreAtFieldValuedPointProjection B S hS f q)
    (sq : IsPullback π.hom (pullback.snd f.hom (fieldMorphism B S hS Y.1 q))
      (pullback.snd f.hom (fieldMorphism B S hS Y.1 p)) (yoneda.map κ))
    {ζ : points B S hS (fibreAtFieldValuedPoint B S hS f q).1}
    (h : IsWeaklyAssociatedPoint B S hS (fibreAtFieldValuedPoint B S hS f q)
      ((modulePullback B S hS (fibreAtFieldValuedPointProjection B S hS f q)).obj F) ζ) :
    IsWeaklyAssociatedPoint B S hS (fibreAtFieldValuedPoint B S hS f p)
      ((modulePullback B S hS (fibreAtFieldValuedPointProjection B S hS f p)).obj F)
      (pointsMap B S hS (fibreAtFieldValuedPoint B S hS f q).1 π.hom ζ)

AlgebraicGeometry.Space.isWeaklyAssociatedPoint_of_fieldBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/SpaceFieldBaseChange.lean, line 61.

Weak association descends along a field extension. Let K/k be a field extension, presented by objects Tk and Tk' of the site with underlying schemes Spec k and Spec K and a morphism gk : Tk' ⟶ Tk inducing Spec K → Spec k. Let X be an algebraic space over Y = h_{Tk}, let X' = X ×_Y Y' be its base change along g : Y' ⟶ Y for Y' = h_{Tk'}, and let F be a quasi-coherent 𝒪_X-module. If a point y of X' is weakly associated to the pullback of F, then its image in X is weakly associated to F.

theorem isWeaklyAssociatedPoint_of_fieldBaseChange (k K : Type u) [Field k] [Field K]
    [Algebra k K] (Tk Tk' : BigFppfOver B S hS) (gk : Tk' ⟶ Tk)
    (f : X ⟶ Y) (f' : X' ⟶ Y') (g : Y' ⟶ Y) (π : X' ⟶ X) (sq : IsPullback π f' f g)
    (ek : (BigFppfOver.toScheme B S hS).obj Tk ≅ Spec (CommRingCat.of k))
    (eK : (BigFppfOver.toScheme B S hS).obj Tk' ≅ Spec (CommRingCat.of K))
    (hgk : (BigFppfOver.toScheme B S hS).map gk =
      eK.hom ≫ Spec.map (CommRingCat.ofHom (algebraMap k K)) ≫ ek.inv)
    (eY : Y.1 ≅ yoneda.obj Tk) (eY' : Y'.1 ≅ yoneda.obj Tk')
    (hg : g.hom ≫ eY.hom = eY'.hom ≫ yoneda.map gk)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite]
    (y : points B S hS X'.1)
    (hy : IsWeaklyAssociatedPoint B S hS X' ((modulePullback B S hS π).obj F) y) :
    IsWeaklyAssociatedPoint B S hS X F (pointsMap B S hS X'.1 π.hom y)

Tag 0CUT, a lemma

Tag 0CUT in the Stacks Project.

AlgebraicGeometry.Space.isWeaklyAssociatedPoint_modulePullback_iff_of_isFinite_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/SpaceFiniteFlatPullback.lean, line 60.

Stacks 0CUT. Let f : X ⟶ Y be a finite flat morphism of algebraic spaces over a scheme S, let G be an 𝒪_Y-module and let x ∈ |X| be a point with image y ∈ |Y|. Then x ∈ WeakAss(f^*G) if and only if y ∈ WeakAss(G).

The source takes G quasi-coherent; that hypothesis is not needed.

theorem isWeaklyAssociatedPoint_modulePullback_iff_of_isFinite_of_isFlat (f : X ⟶ Y)
    (hfinite : IsFinite B S hS f.hom) (hflat : IsFlat B S hS f.hom)
    (G : Modules.{u, u} B S hS Y.1 Y.2) (x : points B S hS X.1) :
    IsWeaklyAssociatedPoint B S hS X ((modulePullback B S hS f).obj G) x ↔
      IsWeaklyAssociatedPoint B S hS Y G (pointsMap B S hS X.1 f.hom x)

AlgebraicGeometry.Space.isWeaklyAssociatedPrime_geometricModuleStalk_modulePullback_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/SpacePullback.lean, line 271. The attribute's comment: “at the étale local ring, for the geometric stalk of the pullback module”.

Stacks 0CUT at the étale local ring, for the geometric stalk of the pullback module. Let f : X ⟶ Y be a finite flat morphism of algebraic spaces and let x̄ be a geometric point of X with image ȳ. Then the maximal ideal of 𝒪_{Y, ȳ} is weakly associated to the geometric stalk G_{ȳ} exactly when the maximal ideal of 𝒪_{X, x̄} is weakly associated to the geometric stalk (f^*G)_{x̄} of the pullback module.

theorem isWeaklyAssociatedPrime_geometricModuleStalk_modulePullback_iff (f : X ⟶ Y)
    (hfinite : IsFinite B S hS f.hom) (hflat : IsFlat B S hS f.hom)
    (xbar : GeometricPoint B S hS X.1)
    (G : Modules.{u, u} B S hS Y.1 Y.2) :
    letI : IsLocalRing (etaleLocalRing B S hS Y.1 (geometricPointMap f.hom xbar)) :=
      isLocalRing_etaleLocalRing B S hS Y.1 Y.2 (geometricPointMap f.hom xbar)
    letI : IsLocalRing (etaleLocalRing B S hS X.1 xbar) :=
      isLocalRing_etaleLocalRing B S hS X.1 X.2 xbar
    letI : Module (etaleLocalRing B S hS Y.1 (geometricPointMap f.hom xbar))
        (geometricModuleStalk B S hS Y (geometricPointMap f.hom xbar) G) :=
      (geometricModuleStalk B S hS Y (geometricPointMap f.hom xbar) G).isModule
    letI : Module (etaleLocalRing B S hS X.1 xbar)
        (geometricModuleStalk B S hS X xbar ((modulePullback B S hS f).obj G)) :=
      (geometricModuleStalk B S hS X xbar ((modulePullback B S hS f).obj G)).isModule
    (IsWeaklyAssociatedPrime (etaleLocalRing B S hS Y.1 (geometricPointMap f.hom xbar))
          (geometricModuleStalk B S hS Y (geometricPointMap f.hom xbar) G)
          (maximalIdeal (etaleLocalRing B S hS Y.1 (geometricPointMap f.hom xbar))) ↔
      IsWeaklyAssociatedPrime (etaleLocalRing B S hS X.1 xbar)
        (geometricModuleStalk B S hS X xbar ((modulePullback B S hS f).obj G))
        (maximalIdeal (etaleLocalRing B S hS X.1 xbar)))

Tag 0CUU, a lemma

Tag 0CUU in the Stacks Project.

AlgebraicGeometry.Space.isWeaklyAssociatedPoint_modulePullback_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/SpaceEtalePullback.lean, line 551.

Weak association along an étale pullback. Let f : X ⟶ Y be an étale morphism of algebraic spaces over a scheme S, let G be an 𝒪_Y-module and let x be a point of X with image y. Then x is weakly associated to f^*G if and only if y is weakly associated to G.

theorem isWeaklyAssociatedPoint_modulePullback_iff (f : X ⟶ Y) (hf : IsEtale B S hS f.hom)
    (G : Modules.{u, u} B S hS Y.1 Y.2) (x : points B S hS X.1) :
    IsWeaklyAssociatedPoint B S hS X ((modulePullback B S hS f).obj G) x ↔
      IsWeaklyAssociatedPoint B S hS Y G (pointsMap B S hS X.1 f.hom x)

AlgebraicGeometry.Space.isWeaklyAssociatedPoint_fibre_refines_iff_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/SpaceFibreEtaleRefinement.lean, line 206. The attribute's comment: “at an etale refinement of field-valued points of the target, read on the comparison of the two fibres”.

Weak association transfers along an étale refinement of field-valued points. In the situation of AlgebraicGeometry.Space.isWeaklyAssociatedPoint_fibre_of_refines, with F an arbitrary 𝒪_X-module, if the morphism of field spectra the refinement presents is étale, then a point of the fibre over q is weakly associated to the restriction of F exactly when its image in the fibre over p is.

theorem isWeaklyAssociatedPoint_fibre_refines_iff_of_isEtale (f : X ⟶ Y)
    (F : Modules.{u, u} B S hS X.1 X.2)
    {p q : FieldValuedPoint B S hS Y.1} (κ : q.siteObject ⟶ p.siteObject)
    (hκ : IsEtale B S hS (yoneda.map κ))
    {π : fibreAtFieldValuedPoint B S hS f q ⟶ fibreAtFieldValuedPoint B S hS f p}
    (hπ : π ≫ fibreAtFieldValuedPointProjection B S hS f p =
      fibreAtFieldValuedPointProjection B S hS f q)
    (sq : IsPullback π.hom (pullback.snd f.hom (fieldMorphism B S hS Y.1 q))
      (pullback.snd f.hom (fieldMorphism B S hS Y.1 p)) (yoneda.map κ))
    (ζ : points B S hS (fibreAtFieldValuedPoint B S hS f q).1) :
    IsWeaklyAssociatedPoint B S hS (fibreAtFieldValuedPoint B S hS f q)
        ((modulePullback B S hS (fibreAtFieldValuedPointProjection B S hS f q)).obj F) ζ ↔
      IsWeaklyAssociatedPoint B S hS (fibreAtFieldValuedPoint B S hS f p)
        ((modulePullback B S hS (fibreAtFieldValuedPointProjection B S hS f p)).obj F)
        (pointsMap B S hS (fibreAtFieldValuedPoint B S hS f q).1 π.hom ζ)

Sources

• Section 71.3, Tag 0CU1
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.weaklyAssociatedPoints_modulePushforward_subset_image_of_isAffineHom · AlgebraicGeometry.Space.affinePushforwardWeaklyAssociatedImage · AlgebraicGeometry.Space.weaklyAssociatedPoints_modulePushforward_eq_image_of_isAffineHom_locallyNoetherian · AlgebraicGeometry.Space.weaklyAssociatedPoints_modulePushforward_eq_image_of_isAffineHom · AlgebraicGeometry.Space.weaklyAssociatedPoints_modulePushforward_eq_image_of_isFinite · AlgebraicGeometry.Space.isWeaklyAssociatedPoint_modulePullback · AlgebraicGeometry.Space.isWeaklyAssociatedPoint_fibre_of_refines · AlgebraicGeometry.Space.isWeaklyAssociatedPoint_of_fieldBaseChange

Section71.4 Relative weak assassin#

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

Tag 0CUW, a lemma

Tag 0CUW in the Stacks Project.

AlgebraicGeometry.Space.isLocallyNoetherianFiber_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Fibres/LocallyNoetherian.lean, line 400. The attribute's comment: “conditions (1), (2) and (3)”.

For a morphism f : X ⟶ Y of algebraic spaces over S and a point y of Y, local Noetherianity of the fibre of f over the residue field of a point of an étale scheme chart of Y above y holds for some such chart exactly when it holds for every such chart, and exactly when the base change of f along some field-valued representative of y is locally Noetherian.

theorem isLocallyNoetherianFiber_tfae
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (y : points B S hS Y) :
    List.TFAE [
      (∃ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y)
          (v : (BigFppfOver.toScheme B S hS).obj V),
        IsEtale B S hS g ∧
          pointsMap B S hS (yoneda.obj V) g
            ((schemePointRepresentative B S hS V v).class B S hS (yoneda.obj V)) = y ∧
          IsLocallyNoetherianFiberAt B S hS f
            (FieldValuedPoint.map B S hS (yoneda.obj V) g
              (schemePointRepresentative B S hS V v))),
      (∀ (V : BigFppfOver B S hS) (g : yoneda.obj V ⟶ Y)
          (v : (BigFppfOver.toScheme B S hS).obj V),
        IsEtale B S hS g →
          pointsMap B S hS (yoneda.obj V) g
            ((schemePointRepresentative B S hS V v).class B S hS (yoneda.obj V)) = y →
          IsLocallyNoetherianFiberAt B S hS f
            (FieldValuedPoint.map B S hS (yoneda.obj V) g
              (schemePointRepresentative B S hS V v))),
      (∃ p : FieldValuedPoint B S hS Y,
        p.class B S hS Y = y ∧ IsLocallyNoetherianFiberAt B S hS f p)
    ]

AlgebraicGeometry.Space.isLocallyNoetherianFiberAt_iff_exists, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Fibres/LocallyNoetherian.lean, line 479. The attribute's comment: “condition (4): a monomorphic representative”.

If a point y of Y has a field-valued representative presenting it by a monomorphism, then the fibre of f over that representative is locally Noetherian exactly when the fibre over some field-valued representative of y is.

theorem isLocallyNoetherianFiberAt_iff_exists
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (y : points B S hS Y) (p₀ : FieldValuedPoint B S hS Y)
    [Mono (fieldMorphism B S hS Y p₀)] (hp₀ : p₀.class B S hS Y = y) :
    IsLocallyNoetherianFiberAt B S hS f p₀ ↔
      ∃ p : FieldValuedPoint B S hS Y,
        p.class B S hS Y = y ∧ IsLocallyNoetherianFiberAt B S hS f p

Tag 0CUX, a definition

Tag 0CUX in the Stacks Project.

AlgebraicGeometry.Space.IsLocallyNoetherianFiber, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Fibres/LocallyNoetherian.lean, line 506. The attribute's comment: “the fibre over a point”.

The fibre of a morphism f : X ⟶ Y of algebraic spaces over S above a point y of Y is locally Noetherian when the base change of f along some field-valued representative of y is locally Noetherian.

By AlgebraicGeometry.Space.isLocallyNoetherianFiber_tfae this is equivalent to the fibre over the residue field of a point above y of some, equivalently of every, étale scheme chart of Y being locally Noetherian.

abbrev IsLocallyNoetherianFiber {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (y : points B S hS Y) : Prop

AlgebraicGeometry.Space.HasLocallyNoetherianFibersAtPoints, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Fibres/LocallyNoetherian.lean, line 518. The attribute's comment: “all fibres”.

A morphism of algebraic spaces over S has locally Noetherian fibres when its fibre above every point of its target is locally Noetherian.

AlgebraicGeometry.Space.HasLocallyNoetherianFibers is the every-chart reading of the same condition, quantifying instead over the points of the étale scheme charts of the target; by AlgebraicGeometry.Space.isLocallyNoetherianFiber_tfae the two agree pointwise.

abbrev HasLocallyNoetherianFibersAtPoints {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : X ⟶ Y) : Prop

Tag 0CUY, a lemma

Tag 0CUY in the Stacks Project.

AlgebraicGeometry.Space.hasLocallyNoetherianFibersAtPoints_of_isLocallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/Fibres/LocallyNoetherian.lean, line 551.

A morphism of algebraic spaces over S which is locally of finite type has locally Noetherian fibres: the spectrum of a field is Noetherian, so Stacks 04ZK applies to the base change of f along any field-valued representative of a point of the target.

theorem hasLocallyNoetherianFibersAtPoints_of_isLocallyOfFiniteType
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (hf : IsLocallyOfFiniteType B S hS f) :
    HasLocallyNoetherianFibersAtPoints B S hS f

Tag 0CUZ, a lemma

Tag 0CUZ in the Stacks Project.

AlgebraicGeometry.Space.relativeWeakAssassin_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/SpaceRelativeWeakAssassinTFAE.lean, line 316. The attribute's comment: “conditions (1) to (5)”.

Let f : X ⟶ Y be a morphism of algebraic spaces over S, let 𝓕 be a quasi-coherent 𝒪_X-module and let x ∈ |X|. The following are equivalent:

1. for some étale V ⟶ Y with V a scheme, some v ∈ V above f(x) and some x' ∈ |X_v| above x, the point x' is weakly associated to 𝓕|_{X_v};
2. for every such V, v and x', the point x' is weakly associated to 𝓕|_{X_v};
3. for some étale V ⟶ Y, some étale U ⟶ X ×_Y V with U, V schemes and some u ∈ U above x, with image v ∈ V, the point u is weakly associated to 𝓕|_{U_v};
4. for every such U, V and u, the point u is weakly associated to 𝓕|_{U_v};
5. for some field k, some Spec(k) ⟶ Y representing f(x) and some t ∈ |X_k| above x, the point t is weakly associated to 𝓕|_{X_k}.

theorem relativeWeakAssassin_tfae (f : X ⟶ Y) (F : Modules.{u, u} B S hS X.1 X.2)
    [F.IsQuasicoherentOnSite] (x : points B S hS X.1) :
    List.TFAE [IsWeaklyAssociatedOnSomeSchemeChartFibre B S hS f F x,
      IsWeaklyAssociatedOnEverySchemeChartFibre B S hS f F x,
      IsWeaklyAssociatedOnSomeEtaleChartSquare B S hS f F x,
      IsWeaklyAssociatedOnEveryEtaleChartSquare B S hS f F x,
      IsRelativeWeaklyAssociatedPoint B S hS f F x]

AlgebraicGeometry.Space.isRelativeWeaklyAssociatedPoint_iff_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/SpaceRelativeWeakAssassinTFAE.lean, line 348. The attribute's comment: “condition (6), at a monomorphism from the spectrum of a field representing the image point”.

Let f : X ⟶ Y be a morphism of algebraic spaces over S, let 𝓕 be a quasi-coherent 𝒪_X-module, let x ∈ |X| and let Spec(k₀) ⟶ Y be a monomorphism representing f(x). Then there is a unique point x₀ ∈ |X_{k₀}| mapping to x, and the equivalent conditions of AlgebraicGeometry.Space.relativeWeakAssassin_tfae hold exactly when x₀ is a weakly associated point of 𝓕|_{X_{k₀}}.

theorem isRelativeWeaklyAssociatedPoint_iff_of_mono (f : X ⟶ Y)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite]
    (p₀ : FieldValuedPoint B S hS Y.1) [Mono (fieldMorphism B S hS Y.1 p₀)]
    {x : points B S hS X.1} (rep : p₀.class B S hS Y.1 = pointsMap B S hS X.1 f.hom x) :
    (∃! x₀ : points B S hS (fibreAtFieldValuedPoint B S hS f p₀).1,
      pointsMap B S hS (fibreAtFieldValuedPoint B S hS f p₀).1
        (fibreAtFieldValuedPointProjection B S hS f p₀).hom x₀ = x) ∧
    ∀ x₀ : points B S hS (fibreAtFieldValuedPoint B S hS f p₀).1,
      pointsMap B S hS (fibreAtFieldValuedPoint B S hS f p₀).1
          (fibreAtFieldValuedPointProjection B S hS f p₀).hom x₀ = x →
        (IsRelativeWeaklyAssociatedPoint B S hS f F x ↔
          IsWeaklyAssociatedPoint B S hS (fibreAtFieldValuedPoint B S hS f p₀)
            ((modulePullback B S hS (fibreAtFieldValuedPointProjection B S hS f p₀)).obj F)
            x₀)

AlgebraicGeometry.Space.isRelativeWeaklyAssociatedPoint_iff_associated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/SpaceRelativeWeakAssassinTFAE.lean, line 530. The attribute's comment: “the locally Noetherian case: weakly associated replaced by associated in conditions (1), (2), (3), (4) and (6)”.

Let f : X ⟶ Y be a morphism of algebraic spaces over S, let 𝓕 be a quasi-coherent 𝒪_X-module and let x ∈ |X| be such that the fibre of f over f(x) is locally Noetherian. Then in conditions (1), (2), (3), (4) and (6) of AlgebraicGeometry.Space.relativeWeakAssassin_tfae and AlgebraicGeometry.Space.isRelativeWeaklyAssociatedPoint_iff_of_mono "weakly associated" may be replaced by "associated": each of the resulting conditions is equivalent to x lying in the relative weak assassin WeakAss_{X/Y}(𝓕).

theorem isRelativeWeaklyAssociatedPoint_iff_associated (f : X ⟶ Y)
    (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite] (x : points B S hS X.1)
    (noeth : IsLocallyNoetherianFiber B S hS f.hom (pointsMap B S hS X.1 f.hom x)) :
    (IsRelativeWeaklyAssociatedPoint B S hS f F x ↔
        IsAssociatedOnSomeSchemeChartFibre B S hS f F x) ∧
      (IsRelativeWeaklyAssociatedPoint B S hS f F x ↔
        IsAssociatedOnEverySchemeChartFibre B S hS f F x) ∧
      (IsRelativeWeaklyAssociatedPoint B S hS f F x ↔
        IsAssociatedOnSomeEtaleChartSquare B S hS f F x) ∧
      (IsRelativeWeaklyAssociatedPoint B S hS f F x ↔
        IsAssociatedOnEveryEtaleChartSquare B S hS f F x) ∧
      ∀ (p₀ : FieldValuedPoint B S hS Y.1) [Mono (fieldMorphism B S hS Y.1 p₀)],
        p₀.class B S hS Y.1 = pointsMap B S hS X.1 f.hom x →
        ∀ x₀ : points B S hS (fibreAtFieldValuedPoint B S hS f p₀).1,
          pointsMap B S hS (fibreAtFieldValuedPoint B S hS f p₀).1
              (fibreAtFieldValuedPointProjection B S hS f p₀).hom x₀ = x →
            (IsRelativeWeaklyAssociatedPoint B S hS f F x ↔
              IsAssociatedPoint B S hS (fibreAtFieldValuedPoint B S hS f p₀)
                ((modulePullback B S hS (fibreAtFieldValuedPointProjection B S hS f p₀)).obj F)
                x₀)

Tag 0CV0, a definition

Tag 0CV0 in the Stacks Project.

AlgebraicGeometry.Space.IsRelativeWeaklyAssociatedPoint, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PurityCriterion.lean, line 124. The attribute's comment: “the membership predicate, via condition (5) of 0CUZ; stated for every module, not only a quasi-coherent one”.

A point x of X lies in the relative weak assassin WeakAss_{X/Y}(F) of an 𝒪_X-module F along a morphism f : X ⟶ Y of algebraic spaces: for some field-valued representative of the image of x in Y, the fibre of f over that representative carries a point above x which is weakly associated to the restriction of F to the fibre.

This is condition (5) of Stacks 0CUZ, the field-valued one. When the fibres of f are locally Noetherian — for instance when f is locally of finite type, by Stacks 0CUY — this set is also written Ass_{X/Y}(F).

noncomputable def IsRelativeWeaklyAssociatedPoint {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (F : Modules.{u, u} B S hS X.1 X.2) (x : points B S hS X.1) : Prop

AlgebraicGeometry.Space.relativeWeaklyAssociatedPoints, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Flat/PurityCriterion.lean, line 138. The attribute's comment: “the set WeakAss_{X/Y}(F), which under locally Noetherian fibres is Ass_{X/Y}(F)”.

The relative weak assassin WeakAss_{X/Y}(F) ⊆ |X| of an 𝒪_X-module along a morphism of algebraic spaces. When the fibres of f are locally Noetherian this is the set written Ass_{X/Y}(F).

noncomputable abbrev relativeWeaklyAssociatedPoints {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (F : Modules.{u, u} B S hS X.1 X.2) : Set (points B S hS X.1)

Tag 0CV1, a lemma

Tag 0CV1 in the Stacks Project.

AlgebraicGeometry.Space.weaklyAssociatedPoints_tensor_modulePullback_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/SpaceTensorPullbackLocallyNoetherian.lean, line 204.

Let f : X ⟶ Y be a morphism of algebraic spaces over a scheme S, let 𝓕 be a quasi-coherent 𝒪_X-module and 𝓖 a quasi-coherent 𝒪_Y-module. Assume 𝓕 is flat over Y, that X and Y are locally Noetherian and that the fibres of f are locally Noetherian. Then

Ass_X(𝓕 ⊗_{𝒪_X} f^*𝓖) = {x ∈ Ass_{X/Y}(𝓕) such that f(x) ∈ Ass_Y(𝓖)},

where Ass and Ass_{X/Y} are AlgebraicGeometry.Space.weaklyAssociatedPoints and AlgebraicGeometry.Space.relativeWeaklyAssociatedPoints.

theorem weaklyAssociatedPoints_tensor_modulePullback_eq (f : X ⟶ Y)
    (F : Modules.{u, u} B S hS X.1 X.2) (G : Modules.{u, u} B S hS Y.1 Y.2)
    [hFqc : F.IsQuasicoherentOnSite] [G.IsQuasicoherentOnSite]
    (hF : IsFlatOver B S hS X.2 f.hom F)
    (hLNX : HasEtaleLocalProperty B S hS X.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (hLNY : HasEtaleLocalProperty B S hS Y.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (hfib : HasLocallyNoetherianFibersAtPoints B S hS f.hom) :
    weaklyAssociatedPoints B S hS X (F ⊗ (modulePullback B S hS f).obj G) =
      {x | x ∈ relativeWeaklyAssociatedPoints B S hS f F ∧
        pointsMap B S hS X.1 f.hom x ∈ weaklyAssociatedPoints B S hS Y G}

Tag 0CV2, a lemma

Tag 0CV2 in the Stacks Project.

AlgebraicGeometry.Space.isRelativeWeaklyAssociatedPoint_of_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/SpaceBaseChange.lean, line 199. The attribute's comment: “part (1), for the relative weak assassin of Stacks 0CV0 and with no finiteness hypothesis on f, which part (1) does not use: the two fibres are identified outright by pasting the cartesian squares”.

In a cartesian square of algebraic spaces over S with vertical morphisms f : X ⟶ Y and f' : X' ⟶ Y' and horizontal morphisms g : Y' ⟶ Y and g' : X' ⟶ X, and for an 𝒪_X-module F with F' = (g')^*F, the image under g' of a point of WeakAss_{X'/Y'}(F') lies in WeakAss_{X/Y}(F).

theorem isRelativeWeaklyAssociatedPoint_of_baseChange
    (sq : IsPullback g'.hom f'.hom f.hom g.hom) (F : Modules.{u, u} B S hS X.1 X.2)
    {x' : points B S hS X'.1}
    (hx' : IsRelativeWeaklyAssociatedPoint B S hS f' ((modulePullback B S hS g').obj F) x') :
    IsRelativeWeaklyAssociatedPoint B S hS f F (pointsMap B S hS X'.1 g'.hom x')

AlgebraicGeometry.Space.exists_isRelativeWeaklyAssociatedPoint_baseChange_of_pointsMap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/SpaceBaseChange.lean, line 252. The attribute's comment: “part (2), for the relative weak assassin of Stacks 0CV0 and with no finiteness hypothesis on f, which the proof does not use: in place of the source's appeal to Stacks 05DC the witness is carried to a representative coming from y' by the ascent of weak association along the flat surjective base change identifying the two fibres”.

In a cartesian square of algebraic spaces over S with vertical morphisms f : X ⟶ Y and f' : X' ⟶ Y' and horizontal morphisms g : Y' ⟶ Y and g' : X' ⟶ X, and for a quasi-coherent 𝒪_X-module F with F' = (g')^*F: for every point x of WeakAss_{X/Y}(F) and every point y' of Y' whose image in Y is the image of x, there is a point of WeakAss_{X'/Y'}(F') whose image under g' is x and whose image under f' is y'.

theorem exists_isRelativeWeaklyAssociatedPoint_baseChange_of_pointsMap_eq
    (sq : IsPullback g'.hom f'.hom f.hom g.hom) (F : Modules.{u, u} B S hS X.1 X.2)
    (hF : F.IsQuasicoherentOnSite) {x : points B S hS X.1} {y' : points B S hS Y'.1}
    (hx : IsRelativeWeaklyAssociatedPoint B S hS f F x)
    (hy' : pointsMap B S hS Y'.1 g.hom y' = pointsMap B S hS X.1 f.hom x) :
    ∃ x' : points B S hS X'.1,
      IsRelativeWeaklyAssociatedPoint B S hS f' ((modulePullback B S hS g').obj F) x' ∧
        pointsMap B S hS X'.1 g'.hom x' = x ∧
          pointsMap B S hS X'.1 f'.hom x' = y'

Tag 0CV3, a lemma

Tag 0CV3 in the Stacks Project.

AlgebraicGeometry.Space.relativeWeaklyAssociatedPoints_modulePullback_eq_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/SpaceBaseChangePreimage.lean, line 351.

Let

X' --g'--> X
|f'        |f
Y' --g---> Y

be a cartesian square of algebraic spaces over S, let F be a quasi-coherent 𝒪_X-module and put F' = (g')^*F. Assume that f is locally of finite type and that for every y' ∈ |Y'| the transcendence degree of y'/g(y') is 0 (Stacks 04NM). Then the relative weak assassin WeakAss_{X'/Y'}(F') of Stacks 0CV0 is the inverse image of WeakAss_{X/Y}(F) under |g'|.

theorem relativeWeaklyAssociatedPoints_modulePullback_eq_preimage
    (sq : IsPullback g'.hom f'.hom f.hom g.hom) (F : Modules.{u, u} B S hS X.1 X.2)
    [F.IsQuasicoherentOnSite] (f_lft : IsLocallyOfFiniteType B S hS f.hom)
    (g_trdeg : ∀ y' : points B S hS Y'.1, HasTranscendenceDegreeAt B S hS g.hom y' 0) :
    relativeWeaklyAssociatedPoints B S hS f' ((modulePullback B S hS g').obj F) =
      pointsMap B S hS X'.1 g'.hom ⁻¹' relativeWeaklyAssociatedPoints B S hS f F

Tag 0CV4, a lemma

Tag 0CV4 in the Stacks Project.

AlgebraicGeometry.Space.relativeWeaklyAssociatedPoints_modulePushforward_eq_image_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/SpaceFiniteDirectImage.lean, line 225.

The relative weak assassin of a finite direct image. Let f : X ⟶ Y be a morphism of algebraic spaces over a scheme S, let i : Z ⟶ X be a finite morphism and let G be a quasi-coherent 𝒪_Z-module. Then the relative weak assassin WeakAss_{X/Y}(i_*G) is the image under i of WeakAss_{Z/Y}(G).

theorem relativeWeaklyAssociatedPoints_modulePushforward_eq_image_of_isFinite
    (f : X ⟶ Y) (i : Z ⟶ X)
    (hi : IsFinite B S hS i.hom) (G : Modules.{u, u} B S hS Z.1 Z.2)
    (hG : G.IsQuasicoherentOnSite) :
    relativeWeaklyAssociatedPoints B S hS f ((modulePushforward B S hS i).obj G) =
      pointsMap B S hS Z.1 i.hom '' relativeWeaklyAssociatedPoints B S hS (i ≫ f) G

Tag 0CVV, a lemma

Tag 0CVV in the Stacks Project.

AlgebraicGeometry.Space.isLocallyConstructible_relativeAssassinContainmentLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/RepresentedFibreComparison.lean, line 625. The attribute's comment: “the surjective etale scheme chart of X is a hypothesis rather than a construction, and so are the transfers along it of quasi-compactness and quasi-separatedness of alpha, of finite presentation of the chart restriction of F, and of quasi-compactness of U over V”.

Let V be a scheme of the site, let f : X ⟶ schemeSpace V be a morphism of algebraic spaces which is locally of finite presentation, let F be a quasi-coherent 𝒪_X-module and let U be an open subset of |X|. Let φ : schemeSpace W ⟶ X be a surjective étale scheme chart and α : W ⟶ V a quasi-compact and quasi-separated morphism of the site with φ ≫ f = schemeSpaceMap α, such that the chart restriction of F is of finite presentation and φ⁻¹(U) is quasi-compact over V. Then the set of points y of V over which every point of the relative assassin of F above y lies in U is locally constructible in V.

theorem isLocallyConstructible_relativeAssassinContainmentLocus
    {X : AlgebraicSpaces B S hS} (V W : BigFppfOver B S hS)
    (f : X ⟶ schemeSpace V) (F : Modules.{u, u} B S hS X.1 X.2)
    (U : Set (points B S hS X.1)) (hUopen : @IsOpen _ (pointTopology B S hS X.1) U)
    (φ : schemeSpace W ⟶ X)
    (hφ : IsEtale B S hS φ.hom)
    (hsurj : Function.Surjective (pointsMap B S hS (schemeSpace W).1 φ.hom))
    (α : W ⟶ V) (hα : φ ≫ f = schemeSpaceMap α)
    (hfX : IsLocallyOfFinitePresentation B S hS f.hom)
    (hαqc : QuasiCompact ((BigFppfOver.toScheme B S hS).map α))
    (hαqs : QuasiSeparated ((BigFppfOver.toScheme B S hS).map α))
    (hF : F.IsQuasicoherentOnSite)
    (hGfp : (baseChangeModule B S hS F W φ.hom).IsFinitePresentation)
    (hUqc : QuasiCompact ((chartOpenOfOpenPoints B S hS W φ U hUopen).ι ≫
      (BigFppfOver.toScheme B S hS).map α)) :
    IsLocallyConstructible (relativeAssassinContainmentLocus B S hS V f F U)

AlgebraicGeometry.Space.isLocallyConstructible_relativeAssassinContainmentLocus_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/SpaceContainmentGeneralBase.lean, line 166. The attribute's comment: “with U → V quasi-compact read on the point sets”.

Let V be a scheme of the site, let X be an algebraic space of finite presentation over V, let F be a quasi-coherent 𝒪_X-module of finite presentation and let U be an open subset of |X| whose map to |V| is quasi-compact. Then the set of points of V over which every point of the relative assassin of F above that point lies in U is locally constructible.

Here hUqc is the point-level reading of "U → V is quasi-compact": the part of U lying over a quasi-compact open of |V| is quasi-compact.

theorem isLocallyConstructible_relativeAssassinContainmentLocus_of_isFinitePresentation
    {X : AlgebraicSpaces B S hS} (V : BigFppfOver B S hS)
    (f : X ⟶ schemeSpace V) (hf : IsFinitePresentation B S hS f.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite)
    (hFfp : SheafOfModules.IsFinitePresentationOnSite F)
    (U : Set (points B S hS X.1)) (hUopen : IsOpen U)
    (hUqc : ∀ A : ((BigFppfOver.toScheme B S hS).obj V).Opens,
      IsCompact (A : Set ((BigFppfOver.toScheme B S hS).obj V)) →
      IsCompact (U ∩ (fun x =>
          schemeSpacePointToScheme B S hS V (pointsMap B S hS X.1 f.hom x)) ⁻¹'
        (A : Set ((BigFppfOver.toScheme B S hS).obj V)))) :
    IsLocallyConstructible (relativeAssassinContainmentLocus B S hS V f F U)

AlgebraicGeometry.Space.isLocallyConstructible_relativeAssassinContainmentLocus_of_isQuasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/SpaceContainmentGeneralBase.lean, line 246.

Let V be a scheme of the site, let X be an algebraic space of finite presentation over V, let F be a quasi-coherent 𝒪_X-module of finite presentation and let U ⊆ X be an open subspace whose morphism to V is quasi-compact. Then the set of points of V over which every point of the relative assassin of F above that point lies in U is locally constructible.

theorem isLocallyConstructible_relativeAssassinContainmentLocus_of_isQuasiCompact
    {X : AlgebraicSpaces B S hS} (V : BigFppfOver B S hS)
    (f : X ⟶ schemeSpace V) (hf : IsFinitePresentation B S hS f.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : F.IsQuasicoherentOnSite)
    (hFfp : SheafOfModules.IsFinitePresentationOnSite F)
    (U : Subfunctor X.1) (hU : IsOpenSubspace B S hS U)
    (hUqc : IsQuasiCompact B S hS (U.ι ≫ f.hom)) :
    IsLocallyConstructible (relativeAssassinContainmentLocus B S hS V f F
      (Set.range (pointsMap B S hS U.toFunctor U.ι)))

Sources

• Section 71.4, Tag 0CUV
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.isLocallyNoetherianFiber_tfae · AlgebraicGeometry.Space.isLocallyNoetherianFiberAt_iff_exists · AlgebraicGeometry.Space.IsLocallyNoetherianFiber · AlgebraicGeometry.Space.HasLocallyNoetherianFibersAtPoints · AlgebraicGeometry.Space.hasLocallyNoetherianFibersAtPoints_of_isLocallyOfFiniteType · AlgebraicGeometry.Space.relativeWeakAssassin_tfae · AlgebraicGeometry.Space.isRelativeWeaklyAssociatedPoint_iff_of_mono · AlgebraicGeometry.Space.isRelativeWeaklyAssociatedPoint_iff_associated

Section71.5 Fitting ideals#

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

Tag 0CZ3, the section

Tag 0CZ3 in the Stacks Project.

AlgebraicGeometry.Space.fittingIdealInt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FittingIdealChain.lean, line 275. The attribute's comment: “the chain Fit_k, k : ℤ”.

The k-th Fitting ideal sheaf of an 𝒪_F-module, for k : ℤ: the smallest sheaf of ideals of 𝒪_F whose sections over every affine étale chart contain the module-theoretic k-th Fitting ideal of the sections of the module there.

For k < 0 the chartwise ideal is zero, so Fit₋₁(G) = 0.

noncomputable def fittingIdealInt (G : Modules.{u, m} B S hS F hF) (k : ℤ) :
    (SheafOfModules.unit
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (smallEtaleRingedSite B S hS F hF).O))).Submodule

AlgebraicGeometry.Space.fittingIdealInt_obj_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FittingIdealChain.lean, line 350. The attribute's comment: “the chartwise characterisation of the sections”.

Stacks 0CZ3: over an affine étale chart the sections of Fit_k(G) are exactly the module-theoretic k-th Fitting ideal of the sections of G over the chart ring.

One inclusion is the defining property of AlgebraicGeometry.Space.fittingIdealInt; the other holds because the sections restricting into the chartwise Fitting ideals already form a sheaf of ideals containing them, so the infimum is below it.

theorem fittingIdealInt_obj_eq (G : Modules.{u, m} B S hS F hF)
    (hG : IsCartesianOnAffineCharts G)
    (hfin : ∀ W : SmallEtale B S hS F,
      IsAffine ((SmallEtale.toOver B S hS F ⋙ BigFppfOver.toScheme B S hS).obj W) →
        Module.Finite (chartRing B S hS F hF W) (G.val.obj (op W)))
    (k : ℤ) {U : SmallEtale B S hS F}
    (hU : IsAffine ((SmallEtale.toOver B S hS F ⋙ BigFppfOver.toScheme B S hS).obj U)) :
    (fittingIdealInt B S hS F hF G k).toSubmodule.obj (op U) =
      @_root_.fittingIdeal (chartRing B S hS F hF U) _ (G.val.obj (op U)) _ _ (hfin U hU) k

AlgebraicGeometry.Space.fittingIdeal_obj_eq_fittingIdealOnChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FittingIdealChain.lean, line 371. The attribute's comment: “the chartwise characterisation, in nonnegative degree”.

Stacks 0CZ3 for the ℕ-indexed Fitting ideal sheaf: over an affine étale chart the sections of AlgebraicGeometry.Space.fittingIdeal are exactly the chartwise Fitting ideal of AlgebraicGeometry.Space.fittingIdealOnChart.

theorem fittingIdeal_obj_eq_fittingIdealOnChart (G : Modules.{u, m} B S hS F hF)
    (hG : IsCartesianOnAffineCharts G)
    (hfin : ∀ W : SmallEtale B S hS F,
      IsAffine ((SmallEtale.toOver B S hS F ⋙ BigFppfOver.toScheme B S hS).obj W) →
        Module.Finite (chartRing B S hS F hF W) (G.val.obj (op W)))
    (r : ℕ) {U : SmallEtale B S hS F}
    (hU : IsAffine ((SmallEtale.toOver B S hS F ⋙ BigFppfOver.toScheme B S hS).obj U)) :
    (fittingIdeal B S hS F hF G r).toSubmodule.obj (op U) =
      @fittingIdealOnChart B S hS F hF G r U (hfin U hU)

AlgebraicGeometry.Space.fittingIdealInt_eq_bot_of_lt_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FittingIdealChain.lean, line 404. The attribute's comment: “Fit_{-1} = 0”.

Fit₋₁(G) = 0, and more generally the Fitting ideal sheaves vanish in negative degree: in negative degree the chartwise Fitting ideal is zero, so every sheaf of ideals belongs to the family whose infimum defines Fit_k(G).

theorem fittingIdealInt_eq_bot_of_lt_zero (G : Modules.{u, m} B S hS F hF) {k : ℤ} (hk : k < 0) :
    fittingIdealInt B S hS F hF G k = ⊥

AlgebraicGeometry.Space.monotone_fittingIdealInt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FittingIdealChain.lean, line 440. The attribute's comment: “the chain increases”.

The chain of Fitting ideal sheaves increases. A sheaf of ideals whose sections over every affine étale chart contain the chartwise Fit_l contains the chartwise Fit_k there too, for k ≤ l, so the family whose infimum is Fit_l(G) is contained in the family for Fit_k(G).

theorem monotone_fittingIdealInt (G : Modules.{u, m} B S hS F hF) :
    Monotone fun k : ℤ => fittingIdealInt B S hS F hF G k

AlgebraicGeometry.Space.fittingIdealInt_chain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FittingIdealChain.lean, line 459.

Stacks 0CZ3. For a finite type quasi-coherent 𝒪_X-module G on an algebraic space X the Fitting ideals form an increasing chain 0 = Fit₋₁(G) ⊆ Fit₀(G) ⊆ … ⊆ 𝒪_X of sheaves of ideals, characterised by: over every affine étale chart U the sections of Fit_k(G) are the module-theoretic k-th Fitting ideal of the sections G(U) over the chart ring 𝒪_X(U).

The finiteness of the sections over every affine chart is the étale-local reading of finite type used by the conventions of Stacks 0CZ3, under which the Fitting ideals are defined chartwise.

theorem fittingIdealInt_chain (X : AlgebraicSpaces B S hS) (G : Modules.{u, u} B S hS X.1 X.2)
    (hG : G.IsQuasicoherentOnSite)
    (hfin : ∀ W : SmallEtale B S hS X.1,
      IsAffine ((SmallEtale.toOver B S hS X.1 ⋙ BigFppfOver.toScheme B S hS).obj W) →
        Module.Finite (chartRing B S hS X.1 X.2 W) (G.val.obj (op W))) :
    fittingIdealInt B S hS X.1 X.2 G (-1) = ⊥ ∧
      Monotone (fun k : ℤ => fittingIdealInt B S hS X.1 X.2 G k) ∧
      (∀ k : ℤ, fittingIdealInt B S hS X.1 X.2 G k ≤ ⊤) ∧
      ∀ (k : ℤ) (U : SmallEtale B S hS X.1)
        (hU : IsAffine ((SmallEtale.toOver B S hS X.1 ⋙ BigFppfOver.toScheme B S hS).obj U)),
        (fittingIdealInt B S hS X.1 X.2 G k).toSubmodule.obj (op U) =
          @_root_.fittingIdeal (chartRing B S hS X.1 X.2 U) _ (G.val.obj (op U)) _ _
            (hfin U hU) k

Tag 0CZ4, a lemma

Tag 0CZ4 in the Stacks Project.

AlgebraicGeometry.Space.fittingIdealPullback_eq_fittingIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FittingIdealPullbackFiniteType.lean, line 65.

Let f : X ⟶ Y be a morphism of algebraic spaces and let G be a finite type quasi-coherent 𝒪_Y-module. Then the ideal sheaf on X generated by the inverse image of the r-th Fitting ideal sheaf of G is the r-th Fitting ideal sheaf of f^*G: f^{-1}Fit_r(G) · 𝒪_X = Fit_r(f^*G).

theorem fittingIdealPullback_eq_fittingIdeal {f : X ⟶ Y} {G : Modules.{u, u} B S hS Y.1 Y.2}
    (hqc : G.IsQuasicoherentOnSite)
    (hft : PresheafOfModules.IsFiniteType (smallEtaleRingedSite B S hS Y.1 Y.2).J G.val)
    (r : ℕ) :
    fittingIdealPullback B S hS f G r =
      fittingIdeal B S hS X.1 X.2 ((modulePullback B S hS f).obj G) r

Tag 0CZ5, a lemma

Tag 0CZ5 in the Stacks Project.

AlgebraicGeometry.Space.isFiniteTypeQuasicoherentIdeal_fittingIdeal_of_isFinitePresentationOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FittingIdealFiniteType.lean, line 286.

For a finitely presented quasi-coherent 𝒪_X-module ℱ on an algebraic space X, the r-th Fitting ideal Fit_r(ℱ) is a quasi-coherent ideal of finite type.

theorem isFiniteTypeQuasicoherentIdeal_fittingIdeal_of_isFinitePresentationOnSite
    (X : AlgebraicSpaces B S hS) (G : Modules.{u, u} B S hS X.1 X.2)
    (hG : G.IsQuasicoherentOnSite) (hfp : SheafOfModules.IsFinitePresentationOnSite G) (r : ℕ) :
    IsFiniteTypeQuasicoherentIdeal B S hS X (fittingIdeal B S hS X.1 X.2 G r)

Tag 0CZ6, a lemma

Tag 0CZ6 in the Stacks Project.

AlgebraicGeometry.Space.schemeTheoreticSupport_le_fittingClosedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FittingIdealZerothSchemeTheoreticSupport.lean, line 108. The attribute's comment: “part (1)”.

Stacks 0CZ6, part (1). Let G be a finite type, quasi-coherent 𝒪_X-module, let Z₀ be the closed subspace of X cut out by Fit_0(G) and let Z be the scheme-theoretic support of G. Then Z ⊆ Z₀ ⊆ X as closed subspaces.

The scheme-theoretic support of Stacks 07U1 is a closed subspace by AlgebraicGeometry.Space.exists_isClosedSubspace_schemeTheoreticSupport. It is the infimum of the closed subspaces whose defining ideal sheaf annihilates G, and Z₀ is one of them because Fit_0(G) annihilates G.

theorem schemeTheoreticSupport_le_fittingClosedSubspace
    (G : Modules.{u, u} B S hS X.1 X.2) [G.IsQuasicoherentOnSite]
    [SheafOfModules.IsFiniteTypeOnSite G] (Z₀ : ClosedSubspaces B S hS X.1)
    (cutOut : definingIdealSheaf B S hS X Z₀ = fittingIdeal B S hS X.1 X.2 G 0) :
    IsClosedSubspace B S hS (schemeTheoreticSupport B S hS X G) ∧
      schemeTheoreticSupport B S hS X G ≤ Z₀.1

AlgebraicGeometry.Space.range_pointsMap_schemeTheoreticSupport_eq_supportOfSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FittingIdealZerothSchemeTheoreticSupport.lean, line 133. The attribute's comment: “part (2)”. References: SGA 7 VI (5.1), “more general”.

Stacks 0CZ6, part (2). Let G be a finite type, quasi-coherent 𝒪_X-module, let Z₀ be the closed subspace of X cut out by Fit_0(G) and let Z be the scheme-theoretic support of G. Then |Z| = |Z₀| = Supp(G) as closed subsets of |X|.

The point set of a closed subspace is the zero locus of its defining ideal sheaf (AlgebraicGeometry.Space.range_pointsMap_ι_eq_idealZeroLocus); the defining ideal sheaves of Z and Z₀ are the annihilator and Fit_0(G). The support lies in the zero locus of the annihilator, which lies in the zero locus of Fit_0(G) because Fit_0(G) ⊆ Ann(G), and the latter is the support by AlgebraicGeometry.Space.idealZeroLocus_fittingIdeal_zero_eq_supportOfSheaf. The support is closed by Stacks 07TZ.

theorem range_pointsMap_schemeTheoreticSupport_eq_supportOfSheaf
    (G : Modules.{u, u} B S hS X.1 X.2) [G.IsQuasicoherentOnSite]
    [SheafOfModules.IsFiniteTypeOnSite G] (Z₀ : ClosedSubspaces B S hS X.1)
    (cutOut : definingIdealSheaf B S hS X Z₀ = fittingIdeal B S hS X.1 X.2 G 0) :
    Set.range (pointsMap B S hS (schemeTheoreticSupport B S hS X G).toFunctor
        (schemeTheoreticSupport B S hS X G).ι) =
        Set.range (pointsMap B S hS Z₀.1.toFunctor Z₀.1.ι) ∧
      Set.range (pointsMap B S hS Z₀.1.toFunctor Z₀.1.ι) =
        supportOfSheaf B S hS X.1 ((SheafOfModules.toSheaf _).obj G) ∧
      IsClosed (supportOfSheaf B S hS X.1 ((SheafOfModules.toSheaf _).obj G))

AlgebraicGeometry.Space.exists_module_on_fittingClosedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FittingIdealZerothSchemeTheoreticSupport.lean, line 174. The attribute's comment: “part (3)”.

Stacks 0CZ6, part (3). Let G be a finite type, quasi-coherent 𝒪_X-module and let Z₀ be the closed subspace of X cut out by Fit_0(G). Then there is a finite type, quasi-coherent 𝒪_{Z₀}-module G₀ with (Z₀ → X)_* G₀ ≅ G.

The ideal cutting out Z₀ is Fit_0(G), which annihilates G, so the essential-image assertion of Stacks 04CJ part (3) for the closed immersion Z₀ → X, AlgebraicGeometry.Space.isQuasicoherentEssImagePushforward_of_isClosedImmersion, produces the quasi-coherent module; it is of finite type by Stacks 07U0 part (3).

theorem exists_module_on_fittingClosedSubspace
    (G : Modules.{u, u} B S hS X.1 X.2) [G.IsQuasicoherentOnSite]
    [SheafOfModules.IsFiniteTypeOnSite G] (Z₀ : ClosedSubspaces B S hS X.1)
    (cutOut : definingIdealSheaf B S hS X Z₀ = fittingIdeal B S hS X.1 X.2 G 0) :
    ∃ G₀ : Modules.{u, u} B S hS (closedSubspaceToSpace B S hS X Z₀).1
        (closedSubspaceToSpace B S hS X Z₀).2,
      G₀.IsQuasicoherentOnSite ∧ SheafOfModules.IsFiniteTypeOnSite G₀ ∧
        Nonempty ((modulePushforward B S hS (closedSubspaceInclusion B S hS X Z₀)).obj G₀ ≅
          G)

Tag 0CZ7, a lemma

Tag 0CZ7 in the Stacks Project.

AlgebraicGeometry.Space.exists_fin_span_iff_fittingIdealGeometricStalk_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FittingIdealGeometricStalk.lean, line 384.

Stacks 0CZ7. Let G be a finite type quasi-coherent 𝒪_X-module on an algebraic space X and let x̄ be a geometric point of X. Then G can be generated by r elements on an affine étale neighbourhood of x̄ if and only if the stalk Fit_r(G)_{x̄} of its r-th Fitting ideal is the whole étale local ring 𝒪_{X, x̄}.

The finiteness of the sections over every affine étale chart is the étale-local reading of finite type used by the conventions of Stacks 0CZ3, under which the Fitting ideals are defined chartwise; hG is the cartesian property of Stacks 03DX, which a quasi-coherent module has by AlgebraicGeometry.Space.isCartesianOnAffineCharts_of_isQuasicoherentOnSite.

theorem exists_fin_span_iff_fittingIdealGeometricStalk_eq_top
    (G : Modules.{u, u} B S hS F hF) (hG : IsCartesianOnAffineCharts G)
    (hfin : ∀ W : SmallEtale B S hS F,
      IsAffine ((SmallEtale.toOver B S hS F ⋙ BigFppfOver.toScheme B S hS).obj W) →
        Module.Finite (chartRing B S hS F hF W) (G.val.obj (op W)))
    (r : ℕ) (x : GeometricPoint B S hS F) :
    (∃ U : SmallEtaleNeighborhood x,
        IsAffine ((SmallEtale.toOver B S hS F ⋙ BigFppfOver.toScheme B S hS).obj U.chart) ∧
          ∃ s : Fin r → G.val.obj (op U.chart),
            Submodule.span (chartRing B S hS F hF U.chart) (Set.range s) = ⊤) ↔
      fittingIdealGeometricStalk G r x = ⊤

Tag 0CZ8, a lemma

Tag 0CZ8 in the Stacks Project.

AlgebraicGeometry.Space.isFiniteLocallyFreeOfRank_tfae_fittingIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FittingLocallyFreeRank.lean, line 446.

Stacks Project, Tag 0CZ8. Let F be an algebraic space and let G be a quasi-coherent 𝒪_F-module on its small étale site. For every r, the following are equivalent: G is finite locally free of rank r; its (r-1)-st Fitting ideal sheaf vanishes and its r-th is the unit ideal sheaf; its Fitting ideal sheaves vanish below r and are the unit ideal sheaf from r onward.

The condition at index r - 1 is read with truncated subtraction and is therefore guarded by the disjunct r = 0, under which it is vacuous. No finite type hypothesis is needed; see the implementation notes.

theorem isFiniteLocallyFreeOfRank_tfae_fittingIdeal
    (G : Modules.{u, u} B S hS F hF) (hG : G.IsQuasicoherentOnSite) (r : ℕ) :
    List.TFAE [
      RingedSite.IsFiniteLocallyFreeOfRank (smallEtaleRingedSite B S hS F hF) G r,
      (r = 0 ∨ fittingIdeal B S hS F hF G (r - 1) = ⊥) ∧
        fittingIdeal B S hS F hF G r = ⊤,
      (∀ k < r, fittingIdeal B S hS F hF G k = ⊥) ∧
        (∀ k, r ≤ k → fittingIdeal B S hS F hF G k = ⊤)]

Tag 0CZ9, a lemma

Tag 0CZ9 in the Stacks Project.

AlgebraicGeometry.Space.exists_fittingClosedSubspaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FittingClosedSubspaces.lean, line 226. The attribute's comment: “the decreasing chain of closed subspaces cut out by the Fitting ideals”.

The closed subspaces cut out by the Fitting ideals of an 𝒪_X-module. If every Fitting ideal sheaf of G is quasi-coherent, there is a decreasing chain of closed subspaces of X whose defining ideal sheaves are the Fitting ideals of G. This is the chain X ⊇ Z_0 ⊇ Z_1 ⊇ … of Stacks 0CZ9.

Each subspace comes from the surjectivity half of Stacks 03MB, AlgebraicGeometry.Space.exists_definingIdealSheaf_eq_of_isQuasicoherentOnSite, and the chain decreases because the Fitting ideals increase and the correspondence of Stacks 03MB reverses inclusions.

theorem exists_fittingClosedSubspaces (G : Modules.{u, u} B S hS X.1 X.2)
    (hqc : ∀ r : ℕ,
      (fittingIdeal B S hS X.1 X.2 G r).toSheafOfModules.IsQuasicoherentOnSite) :
    ∃ Z : ℕ → ClosedSubspaces B S hS X.1,
      (∀ r, definingIdealSheaf B S hS X (Z r) = fittingIdeal B S hS X.1 X.2 G r) ∧
        Antitone fun r ↦ (Z r).1

AlgebraicGeometry.Space.iInf_fittingClosedSubspace_eq_sheafify_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FittingClosedSubspaces.lean, line 286. The attribute's comment: “(1) the intersection is empty; (2), (3) and finite presentation not covered”.

Clause (1) of Stacks 0CZ9: the intersection of the Fitting closed subspaces is the empty algebraic space. For a chain of closed subspaces of X whose defining ideal sheaves are the Fitting ideals of G, the intersection of the chain is the sheafification of the bottom subfunctor, as soon as the sections of G over every affine étale chart form a finite module.

The intersection has no points, by AlgebraicGeometry.Space.iInter_range_pointsMap_ι_fittingClosedSubspace_eq_empty, and an inclusion into the empty open subspace is detected on points by Stacks 03BZ; the reverse inclusion holds for any family of subsheaves.

theorem iInf_fittingClosedSubspace_eq_sheafify_bot
    (G : Modules.{u, u} B S hS X.1 X.2) (Z : ℕ → ClosedSubspaces B S hS X.1)
    (hZ : ∀ r, definingIdealSheaf B S hS X (Z r) = fittingIdeal B S hS X.1 X.2 G r)
    (hfin : ∀ W : SmallEtale B S hS X.1,
      IsAffine ((SmallEtale.toOver B S hS X.1 ⋙ BigFppfOver.toScheme B S hS).obj W) →
        Module.Finite (chartRing B S hS X.1 X.2 W) (G.val.obj (op W))) :
    (⨅ r : ℕ, (Z r).1) = (⊥ : Subfunctor X.1).sheafify (BigFppfOver.topology B S hS)

AlgebraicGeometry.Space.exists_fittingClosedSubspaces_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FittingStratumFinitePresentation.lean, line 194. References: EGA IV (1.4.5), “the closed subspaces”.

Stacks 0CZ9. Let X be an algebraic space over a scheme S contained in a big fppf site B and let G be a quasi-coherent 𝒪_X-module of finite type. The Fitting ideal sheaves of G cut out a decreasing chain of closed subspaces X = Z_{-1} ⊇ Z_0 ⊇ Z_1 ⊇ … such that

1. the intersection of the Z_r is empty;
2. for every algebraic space T ⟶ X the module G_T is locally generated by at most r sections exactly when T ⟶ X factors, necessarily uniquely, through X ∖ Z_r;
3. for every algebraic space T ⟶ X the module G_T is finite locally free of rank r exactly when T ⟶ X factors, necessarily uniquely, through Z_{r-1} ∖ Z_r;

and, if G is moreover of finite presentation, the three morphisms Z_r ⟶ X, X ∖ Z_r ⟶ X and Z_{r-1} ∖ Z_r ⟶ X are of finite presentation.

The chain is the one cut out by AlgebraicGeometry.Space.fittingIdeal, the test objects of clauses (2) and (3) are arbitrary algebraic spaces rather than only schemes over X, and Z_{r-1} ∖ Z_r is AlgebraicGeometry.Space.fittingRankStratum, which for r = 0 is X ∖ Z_0.

theorem exists_fittingClosedSubspaces_spec (hGqc : G.IsQuasicoherentOnSite)
    (hGft : SheafOfModules.IsFiniteTypeOnSite G) :
    ∃ Z : ℕ → ClosedSubspaces B S hS X.1,
      (∀ r, definingIdealSheaf B S hS X (Z r) = fittingIdeal B S hS X.1 X.2 G r) ∧
      (Antitone fun r ↦ (Z r).1) ∧
      (⨅ r : ℕ, (Z r).1) = (⊥ : Subfunctor X.1).sheafify (BigFppfOver.topology B S hS) ∧
      (∀ (T : AlgebraicSpaces B S hS) (r : ℕ) (f : T ⟶ X),
        (∀ x : points B S hS T.1, ∃ (U : SmallEtale B S hS T.1)
            (s : Fin r → ((modulePullback B S hS f).obj G).val.obj (op U)),
            IsAffine ((SmallEtale.toOver B S hS T.1 ⋙ BigFppfOver.toScheme B S hS).obj U) ∧
              Submodule.span (chartRing B S hS T.1 T.2 U) (Set.range s) = ⊤ ∧
                x ∈ Set.range (pointsMap B S hS
                  (yoneda.obj ((SmallEtale.toOver B S hS T.1).obj U)) U.1.hom)) ↔
          ∃! g : T.1 ⟶ (openComplement B S hS (Z r).1).toFunctor,
            g ≫ (openComplement B S hS (Z r).1).ι = f.hom) ∧
      (∀ (T : AlgebraicSpaces B S hS) (r : ℕ) (f : T ⟶ X),
        RingedSite.IsFiniteLocallyFreeOfRank (smallEtaleRingedSite B S hS T.1 T.2)
            ((modulePullback B S hS f).obj G) r ↔
          ∃! g : T.1 ⟶ (fittingRankStratum B S hS X Z r).toFunctor,
            g ≫ (fittingRankStratum B S hS X Z r).ι = f.hom) ∧
      (SheafOfModules.IsFinitePresentationOnSite G → ∀ r : ℕ,
        IsFinitePresentation B S hS (subspaceInclusion B S hS X (Z r)).hom ∧
          IsFinitePresentation B S hS (openComplement B S hS (Z r).1).ι ∧
            IsFinitePresentation B S hS (fittingRankStratum B S hS X Z r).ι)

Tag 0CZA, a lemma

Tag 0CZA in the Stacks Project.

AlgebraicGeometry.Space.isLocallyClosedSubspace_and_disjoint_fittingRankStratum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FittingRankStrata.lean, line 338. The attribute's comment: “the strata X_r = Z_{r-1} \ Z_r are disjoint locally closed subspaces”.

Stacks 0CZA, the Fitting rank strata. Let G be an 𝒪_X-module and let X ⊇ Z_0 ⊇ Z_1 ⊇ … be closed subspaces of X whose defining ideal sheaves are the Fitting ideals of G, as in Stacks 0CZ9. Then the strata X_r = Z_{r-1} \ Z_r, with the convention Z_{-1} = X, are locally closed subspaces of X, and distinct strata are disjoint.

theorem isLocallyClosedSubspace_and_disjoint_fittingRankStratum
    (G : Modules.{u, u} B S hS X.1 X.2) (Z : ℕ → ClosedSubspaces B S hS X.1)
    (hZ : ∀ r, definingIdealSheaf B S hS X (Z r) = fittingIdeal B S hS X.1 X.2 G r) :
    (∀ r : ℕ, IsLocallyClosedSubspace B S hS (fittingRankStratum B S hS X Z r)) ∧
      ∀ r s : ℕ, r ≠ s →
        fittingRankStratum B S hS X Z r ⊓ fittingRankStratum B S hS X Z s ≤
          (⊥ : Subfunctor X.1).sheafify (BigFppfOver.topology B S hS)

AlgebraicGeometry.Space.existsUnique_fittingRankStratum_index, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FittingRankStrata.lean, line 358. The attribute's comment: “every point of X lies in exactly one stratum X_r = Z_{r-1} \ Z_r”.

Stacks 0CZA, the Fitting rank strata cover X. Every point of X lies in exactly one Fitting rank stratum X_r = Z_{r-1} \ Z_r: there is a unique r with the point outside Z_r and inside every earlier member of the chain.

The input is clause (1) of Stacks 0CZ9, AlgebraicGeometry.Space.iInter_range_pointsMap_ι_fittingClosedSubspace_eq_empty: the point sets of the Fitting closed subspaces have empty intersection, so every point leaves the chain, and it does so at a unique index because the chain decreases.

theorem existsUnique_fittingRankStratum_index (G : Modules.{u, u} B S hS X.1 X.2)
    (Z : ℕ → ClosedSubspaces B S hS X.1)
    (hZ : ∀ r, definingIdealSheaf B S hS X (Z r) = fittingIdeal B S hS X.1 X.2 G r)
    (hfin : ∀ W : SmallEtale B S hS X.1,
      IsAffine ((SmallEtale.toOver B S hS X.1 ⋙ BigFppfOver.toScheme B S hS).obj W) →
        Module.Finite (chartRing B S hS X.1 X.2 W) (G.val.obj (op W)))
    (x : points B S hS X.1) :
    ∃! r : ℕ, x ∉ Set.range (pointsMap B S hS (Z r).1.toFunctor (Z r).1.ι) ∧
      ∀ k < r, x ∈ Set.range (pointsMap B S hS (Z k).1.toFunctor (Z k).1.ι)

AlgebraicGeometry.Space.isAlgebraicSpace_fittingRankStratification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FittingRankStrata.lean, line 399. The attribute's comment: “X' = ∐_{r ≥ 0} X_r is an algebraic space, with its morphism to X”.

Stacks 0CZA, the disjoint union of the Fitting rank strata. The disjoint union X' = ∐_{r ≥ 0} X_r of the strata X_r = Z_{r-1} \ Z_r of a chain X ⊇ Z_0 ⊇ Z_1 ⊇ … of closed subspaces of X is an algebraic space over S, and its structural morphism restricts on the r-th summand to the inclusion of X_r in X.

theorem isAlgebraicSpace_fittingRankStratification (Z : ℕ → ClosedSubspaces B S hS X.1) :
    IsAlgebraicSpace B S hS (fittingRankStratification B S hS X Z).obj ∧
      ∀ r : ℕ, Sigma.ι (fun k : ℕ ↦ fittingRankStratumSpace B S hS X Z k) r ≫
          fittingRankStratificationHom B S hS X Z = fittingRankStratumHom B S hS X Z r

AlgebraicGeometry.Space.exists_fittingRankStratification_flat_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FittingStratumAssembly.lean, line 443.

Stacks 0CZA. Let X be an algebraic space over a scheme S contained in a big fppf site B and let G be a quasi-coherent 𝒪_X-module of finite presentation. Then the Fitting ideal sheaves of G cut out a decreasing chain of closed subspaces X = Z_{-1} ⊇ Z_0 ⊇ Z_1 ⊇ … with empty intersection, the strata X_r = Z_{r-1} ∖ Z_r are pairwise disjoint locally closed subspaces of X and every point of X lies in exactly one of them, the disjoint union X' = ∐_{r ≥ 0} X_r is an algebraic space over S whose structural morphism restricts on the r-th summand to the inclusion of X_r, and

1. X' represents the functor sending a test object f : h_T ⟶ X of the site to a one-point set when G_T is flat over T in the sense of Stacks 05VV and to the empty set otherwise;
2. the pullback of G to X_r is finite locally free of rank r;
3. both X_r ⟶ X and X' ⟶ X are of finite presentation.

The hypotheses are exactly the ones Stacks 0CZA makes.

theorem exists_fittingRankStratification_flat_spec (hGqc : G.IsQuasicoherentOnSite)
    (hGfp : SheafOfModules.IsFinitePresentationOnSite G) :
    ∃ Z : ℕ → ClosedSubspaces B S hS X.1,
      (∀ r, definingIdealSheaf B S hS X (Z r) = fittingIdeal B S hS X.1 X.2 G r) ∧
      (Antitone fun r ↦ (Z r).1) ∧
      (⨅ r : ℕ, (Z r).1) = (⊥ : Subfunctor X.1).sheafify (BigFppfOver.topology B S hS) ∧
      (∀ r : ℕ, IsLocallyClosedSubspace B S hS (fittingRankStratum B S hS X Z r)) ∧
      (∀ r s : ℕ, r ≠ s →
        fittingRankStratum B S hS X Z r ⊓ fittingRankStratum B S hS X Z s ≤
          (⊥ : Subfunctor X.1).sheafify (BigFppfOver.topology B S hS)) ∧
      (∀ x : points B S hS X.1, ∃! r : ℕ,
        x ∉ Set.range (pointsMap B S hS (Z r).1.toFunctor (Z r).1.ι) ∧
          ∀ k < r, x ∈ Set.range (pointsMap B S hS (Z k).1.toFunctor (Z k).1.ι)) ∧
      IsAlgebraicSpace B S hS (fittingRankStratification B S hS X Z).obj ∧
      (∀ r : ℕ, Sigma.ι (fun k : ℕ ↦ fittingRankStratumSpace B S hS X Z k) r ≫
          fittingRankStratificationHom B S hS X Z = fittingRankStratumHom B S hS X Z r) ∧
      (∀ (T : BigFppfOver B S hS) (f : schemeSpace T ⟶ X),
        IsFlatOver B S hS (schemeSpace T).2
            (𝟙 (schemeSpace T) : schemeSpace T ⟶ schemeSpace T).hom
            ((modulePullback B S hS f).obj G) ↔
          ∃! h : yoneda.obj T ⟶ (fittingRankStratification B S hS X Z).1,
            h ≫ (fittingRankStratificationHom B S hS X Z).hom = f.hom) ∧
      (∀ r : ℕ, RingedSite.IsFiniteLocallyFreeOfRank
        (smallEtaleRingedSite B S hS (fittingRankStratumSpace B S hS X Z r).1
          (fittingRankStratumSpace B S hS X Z r).2)
        ((modulePullback B S hS (fittingRankStratumHom B S hS X Z r)).obj G) r) ∧
      (∀ r : ℕ, IsFinitePresentation B S hS (fittingRankStratum B S hS X Z r).ι) ∧
      IsFinitePresentation B S hS (fittingRankStratificationHom B S hS X Z).hom

Sources

• Section 71.5, Tag 0CZ3
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.fittingIdealInt · AlgebraicGeometry.Space.fittingIdealInt_obj_eq · AlgebraicGeometry.Space.fittingIdeal_obj_eq_fittingIdealOnChart · AlgebraicGeometry.Space.fittingIdealInt_eq_bot_of_lt_zero · AlgebraicGeometry.Space.monotone_fittingIdealInt · AlgebraicGeometry.Space.fittingIdealInt_chain · AlgebraicGeometry.Space.fittingIdealPullback_eq_fittingIdeal · AlgebraicGeometry.Space.isFiniteTypeQuasicoherentIdeal_fittingIdeal_of_isFinitePresentationOnSite

Section71.6 Effective Cartier divisors#

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

Tag 083B, a definition

Tag 083B in the Stacks Project.

AlgebraicGeometry.Space.IsLocallyPrincipal, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisor.lean, line 118. The attribute's comment: “locally_principal_closed_subspace”.

A closed subspace Z of an algebraic space X is locally principal when its defining ideal sheaf 𝓘_Z ⊆ 𝒪_X is locally generated by one section on the small étale site of X.

noncomputable abbrev IsLocallyPrincipal (X : AlgebraicSpaces B S hS)
    (Z : ClosedSubspaces B S hS X.1) : Prop

AlgebraicGeometry.Space.IsEffectiveCartierDivisor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisor.lean, line 126. The attribute's comment: “effective_cartier_divisor”.

A closed subspace D of an algebraic space X is an effective Cartier divisor when its defining ideal sheaf 𝓘_D ⊆ 𝒪_X is an invertible 𝒪_X-module on the small étale site of X.

noncomputable abbrev IsEffectiveCartierDivisor (X : AlgebraicSpaces B S hS)
    (D : ClosedSubspaces B S hS X.1) : Prop

Tag 083C, a lemma

Tag 083C in the Stacks Project.

AlgebraicGeometry.Space.hasAffinePrincipalEtaleNeighborhoods_of_hasEffectiveCartierEtaleCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierEtaleEquiv.lean, line 174. The attribute's comment: “part (2) implies part (4)”.

Stacks 083C, (2) ⟹ (4). If the inverse image of D is an effective Cartier divisor on one surjective étale scheme chart, then every point of |D| has an affine étale neighbourhood on which D is cut out by a nonzerodivisor.

The point of |D| lifts to a field-valued point of D ×_X U on the surjective chart, whose image in U lies in the support of the chart ideal sheaf. By the affine-local form of Stacks 01WS that ideal sheaf is generated by a nonzerodivisor on an affine open V of U around that image; V is again an étale chart of X, the inverse image of D on it is the base change of D ×_X U, and its ideal sheaf is therefore the principal ideal sheaf of the restricted generator.

theorem hasAffinePrincipalEtaleNeighborhoods_of_hasEffectiveCartierEtaleCover
    (X : AlgebraicSpaces B S hS) (D : ClosedSubspaces B S hS X.1)
    (h : HasEffectiveCartierEtaleCover B S hS X D) :
    HasAffinePrincipalEtaleNeighborhoods B S hS X D

AlgebraicGeometry.Space.hasEffectiveCartierEtalePullbacks_of_hasAffinePrincipal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierEtaleEquiv.lean, line 288. The attribute's comment: “part (4) implies part (3)”.

Stacks 083C, (4) ⟹ (3). If every point of |D| has an affine étale neighbourhood on which D is cut out by a nonzerodivisor, then the inverse image of D is an effective Cartier divisor on every étale scheme chart.

theorem hasEffectiveCartierEtalePullbacks_of_hasAffinePrincipal (X : AlgebraicSpaces B S hS)
    (D : ClosedSubspaces B S hS X.1)
    (h : HasAffinePrincipalEtaleNeighborhoods B S hS X D) :
    HasEffectiveCartierEtalePullbacks B S hS X D

AlgebraicGeometry.Space.hasEffectiveCartierEtalePullbacks_iff_hasAffinePrincipal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierEtaleEquiv.lean, line 299. The attribute's comment: “parts (3) and (4)”.

Stacks 083C, (3) ⟺ (4). The inverse image of a closed subspace is an effective Cartier divisor on every étale scheme chart if and only if every point of |D| has an affine étale neighbourhood on which the subspace is cut out by a nonzerodivisor.

theorem hasEffectiveCartierEtalePullbacks_iff_hasAffinePrincipal (X : AlgebraicSpaces B S hS)
    (D : ClosedSubspaces B S hS X.1) :
    HasEffectiveCartierEtalePullbacks B S hS X D ↔
      HasAffinePrincipalEtaleNeighborhoods B S hS X D

AlgebraicGeometry.Space.hasEffectiveCartierEtaleCover_iff_etalePullbacks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierEtaleEquiv.lean, line 314. The attribute's comment: “parts (2) and (3)”.

Stacks 083C, (2) ⟺ (3). The inverse image of a closed subspace is an effective Cartier divisor on one surjective étale scheme chart if and only if it is so on every étale scheme chart.

The nontrivial direction passes through condition (4): a surjective chart gives affine charts cut out by nonzerodivisors at every point of |D|, and those descend to an arbitrary chart.

theorem hasEffectiveCartierEtaleCover_iff_etalePullbacks (X : AlgebraicSpaces B S hS)
    (D : ClosedSubspaces B S hS X.1) :
    HasEffectiveCartierEtaleCover B S hS X D ↔
      HasEffectiveCartierEtalePullbacks B S hS X D

AlgebraicGeometry.Space.hasEffectiveCartierEtalePullbacks_of_isEffectiveCartier, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierEtaleEquiv.lean, line 329. The attribute's comment: “part (1) implies part (3)”.

Stacks 083C, (1) ⟹ (3). If a closed subspace is an effective Cartier divisor, then its inverse image is an effective Cartier divisor on every étale scheme chart.

theorem hasEffectiveCartierEtalePullbacks_of_isEffectiveCartier (X : AlgebraicSpaces B S hS)
    (D : ClosedSubspaces B S hS X.1) (h : IsEffectiveCartierDivisor B S hS X D) :
    HasEffectiveCartierEtalePullbacks B S hS X D

AlgebraicGeometry.Space.hasEffectiveCartierEtaleCover_of_isEffectiveCartier, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierEtaleEquiv.lean, line 339. The attribute's comment: “part (1) implies part (2)”.

Stacks 083C, (1) ⟹ (2). If a closed subspace is an effective Cartier divisor, then its inverse image is an effective Cartier divisor on some surjective étale scheme chart.

theorem hasEffectiveCartierEtaleCover_of_isEffectiveCartier (X : AlgebraicSpaces B S hS)
    (D : ClosedSubspaces B S hS X.1) (h : IsEffectiveCartierDivisor B S hS X D) :
    HasEffectiveCartierEtaleCover B S hS X D

AlgebraicGeometry.Space.hasAffinePrincipalEtaleNeighborhoods_of_isEffectiveCartier, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierEtaleEquiv.lean, line 349. The attribute's comment: “part (1) implies part (4)”.

Stacks 083C, (1) ⟹ (4). If a closed subspace is an effective Cartier divisor, then every point of |D| has an affine étale neighbourhood on which the subspace is cut out by a nonzerodivisor.

theorem hasAffinePrincipalEtaleNeighborhoods_of_isEffectiveCartier (X : AlgebraicSpaces B S hS)
    (D : ClosedSubspaces B S hS X.1) (h : IsEffectiveCartierDivisor B S hS X D) :
    HasAffinePrincipalEtaleNeighborhoods B S hS X D

AlgebraicGeometry.Space.isFiniteLocallyFreeOfRank_one_definingIdealSheaf_of_etalePullbacks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierEtaleEquiv.lean, line 375. The attribute's comment: “part (3) implies the rank clause of part (1)”.

Stacks 083C, condition (3) implies rank one. If the inverse image of a closed subspace D is an effective Cartier divisor on every étale scheme chart, then the defining ideal sheaf of D is finite locally free of rank one on the small étale site of X.

Over an arbitrary chart the affine opens on which the chart ideal sheaf is generated by a nonzerodivisor are again charts and they cover it; over such a chart the defining ideal is generated by the pullback of that nonzerodivisor at every chart above it, so multiplication by it is an isomorphism from the structure sheaf onto 𝓘_D, which is a one-legged colimit cofan of the structure sheaf.

theorem isFiniteLocallyFreeOfRank_one_definingIdealSheaf_of_etalePullbacks
    (X : AlgebraicSpaces B S hS) (D : ClosedSubspaces B S hS X.1)
    (h : HasEffectiveCartierEtalePullbacks B S hS X D) :
    RingedSite.IsFiniteLocallyFreeOfRank (smallEtaleRingedSite B S hS X.1 X.2)
      (definingIdealSheaf B S hS X D).toSheafOfModules 1

AlgebraicGeometry.Space.isEffectiveCartierDivisor_of_hasEffectiveCartierEtalePullbacks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierEtaleEquiv.lean, line 399. The attribute's comment: “part (3) implies part (1)”.

Stacks 083C, (3) ⟹ (1). If the inverse image of a closed subspace is an effective Cartier divisor on every étale scheme chart, then the subspace is an effective Cartier divisor.

The defining ideal sheaf is then finite locally free of rank one on the small étale site, and the small étale site is essentially small at the universe of the sections of its structure sheaf, so Stacks 0B8M applies to it.

theorem isEffectiveCartierDivisor_of_hasEffectiveCartierEtalePullbacks
    (X : AlgebraicSpaces B S hS) (D : ClosedSubspaces B S hS X.1)
    (h : HasEffectiveCartierEtalePullbacks B S hS X D) :
    IsEffectiveCartierDivisor B S hS X D

AlgebraicGeometry.Space.isEffectiveCartierDivisor_of_hasEffectiveCartierEtaleCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierEtaleEquiv.lean, line 419. The attribute's comment: “part (2) implies part (1)”.

Stacks 083C, (2) ⟹ (1). If the inverse image of a closed subspace is an effective Cartier divisor on one surjective étale scheme chart, then the subspace is an effective Cartier divisor.

theorem isEffectiveCartierDivisor_of_hasEffectiveCartierEtaleCover
    (X : AlgebraicSpaces B S hS) (D : ClosedSubspaces B S hS X.1)
    (h : HasEffectiveCartierEtaleCover B S hS X D) :
    IsEffectiveCartierDivisor B S hS X D

AlgebraicGeometry.Space.isEffectiveCartierDivisor_of_hasAffinePrincipalEtaleNeighborhoods, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierEtaleEquiv.lean, line 429. The attribute's comment: “part (4) implies part (1)”.

Stacks 083C, (4) ⟹ (1). If every point of |D| has an affine étale neighbourhood of X on which D is cut out by a nonzerodivisor, then D is an effective Cartier divisor.

theorem isEffectiveCartierDivisor_of_hasAffinePrincipalEtaleNeighborhoods
    (X : AlgebraicSpaces B S hS) (D : ClosedSubspaces B S hS X.1)
    (h : HasAffinePrincipalEtaleNeighborhoods B S hS X D) :
    IsEffectiveCartierDivisor B S hS X D

AlgebraicGeometry.Space.isEffectiveCartierDivisor_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierEtaleEquiv.lean, line 442. The attribute's comment: “the equivalence of parts (1), (2), (3) and (4)”.

Stacks 083C. For a closed subspace D of an algebraic space X over a scheme S the following are equivalent: D is an effective Cartier divisor on X; the inverse image of D is an effective Cartier divisor on some surjective étale scheme chart of X; it is so on every étale scheme chart of X; and every point of |D| has an affine étale neighbourhood of X on which D is cut out by a nonzerodivisor.

theorem isEffectiveCartierDivisor_tfae (X : AlgebraicSpaces B S hS)
    (D : ClosedSubspaces B S hS X.1) :
    List.TFAE
      [IsEffectiveCartierDivisor B S hS X D,
        HasEffectiveCartierEtaleCover B S hS X D,
        HasEffectiveCartierEtalePullbacks B S hS X D,
        HasAffinePrincipalEtaleNeighborhoods B S hS X D]

AlgebraicGeometry.Space.isLocallyPrincipal_of_hasEffectiveCartierEtalePullbacks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/StrictTransformLocalGenerators.lean, line 817. The attribute's comment: “part (3) implies the local principality of part (1) of 083B”.

A closed subspace whose inverse image is an effective Cartier divisor on every étale scheme chart is locally principal.

theorem isLocallyPrincipal_of_hasEffectiveCartierEtalePullbacks (X : AlgebraicSpaces B S hS)
    (D : ClosedSubspaces B S hS X.1) (hD : HasEffectiveCartierEtalePullbacks B S hS X D) :
    IsLocallyPrincipal B S hS X D

Tag 083D, a lemma

Tag 083D in the Stacks Project.

AlgebraicGeometry.Space.isAffineHom_ι_openComplement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/OpenComplementAffineHom.lean, line 163.

Let X be an algebraic space over a scheme S and let Z ⊆ X be a locally principal closed subspace. Then the inclusion of the open complement X \ Z into X is an affine morphism.

theorem isAffineHom_ι_openComplement (hZ : IsLocallyPrincipal B S hS X Z) :
    IsAffineHom B S hS (openComplement B S hS Z.1).ι

Tag 083S, a lemma

Tag 083S in the Stacks Project.

AlgebraicGeometry.Space.isAffineHom_ι_openComplement_of_isEffectiveCartierDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierComplement.lean, line 117. The attribute's comment: “the complement is affine over the ambient algebraic space”.

Let D ⊆ X be an effective Cartier divisor on an algebraic space X over a scheme S. Then the inclusion of the open complement X ∖ D into X is an affine morphism.

theorem isAffineHom_ι_openComplement_of_isEffectiveCartierDivisor (X : AlgebraicSpaces B S hS)
    (D : ClosedSubspaces B S hS X.1) (hD : IsEffectiveCartierDivisor B S hS X D) :
    IsAffineHom B S hS (openComplement B S hS D.1).ι

AlgebraicGeometry.Space.isSchemeTheoreticallyDense_openComplement_of_isEffectiveCartierDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierComplement.lean, line 143. The attribute's comment: “the complement is scheme theoretically dense in the ambient algebraic space”.

Let D ⊆ X be an effective Cartier divisor on an algebraic space X over a scheme S. Then the open complement X ∖ D is scheme-theoretically dense in X.

theorem isSchemeTheoreticallyDense_openComplement_of_isEffectiveCartierDivisor
    (X : AlgebraicSpaces B S hS) (D : ClosedSubspaces B S hS X.1)
    (hD : IsEffectiveCartierDivisor B S hS X D) :
    IsSchemeTheoreticallyDense B S hS (openComplement B S hS D.1)

Tag 083T, a lemma

Tag 083T in the Stacks Project.

AlgebraicGeometry.Space.dimensionAtPoint_lt_of_isEffectiveCartierDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisorDimension.lean, line 142.

Let D ⊆ X be an effective Cartier divisor on an algebraic space X over a scheme S, and let x be a point of |D| at which the dimension of X is finite. Then the dimension of D at x is strictly smaller than the dimension of X at the image of x.

theorem dimensionAtPoint_lt_of_isEffectiveCartierDivisor (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (X : AlgebraicSpaces B S hS) (D : ClosedSubspaces B S hS X.1)
    (hD : IsEffectiveCartierDivisor B S hS X D)
    (x : points B S hS D.1.toFunctor)
    (hfin : dimensionAtPoint B S hS X.1 X.2
      (pointsMap B S hS D.1.toFunctor D.1.ι x) < ⊤) :
    dimensionAtPoint B S hS D.1.toFunctor D.2.1 x <
      dimensionAtPoint B S hS X.1 X.2 (pointsMap B S hS D.1.toFunctor D.1.ι x)

Tag 083U, a definition

Tag 083U in the Stacks Project.

AlgebraicGeometry.Space.sumClosedSubspaces, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisorSum.lean, line 272. The attribute's comment: “the sum of two effective Cartier divisors, for arbitrary closed subspaces”.

The sum D₁ + D₂ of two closed subspaces of an algebraic space X: the closed subspace cut out by the product 𝓘_{D₁} 𝓘_{D₂} of their defining ideals, formed on a surjective étale scheme chart of X and descended.

noncomputable def sumClosedSubspaces (D₁ D₂ : ClosedSubspaces B S hS X.1) :
    ClosedSubspaces B S hS X.1

AlgebraicGeometry.Space.definingIdealAt_sumClosedSubspaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisorSum.lean, line 281. The attribute's comment: “the sum of two effective Cartier divisors, for arbitrary closed subspaces”.

The sum is cut out by the product of the ideal sheaves of the summands: over an étale chart of X lying over the chart on which it is formed, the defining ideal of D₁ + D₂ is the ideal of regular functions killed by the closed subscheme that the product of the chart ideal sheaves of D₁ and D₂ cuts out there.

theorem definingIdealAt_sumClosedSubspaces (D₁ D₂ : ClosedSubspaces B S hS X.1)
    (A : SmallEtale B S hS X.1)
    (m : A ⟶ (⟨CostructuredArrow.mk (atlasHom B S hS X), atlasHom_etale B S hS X⟩ :
      SmallEtale B S hS X.1)) :
    definingIdealAt B S hS X (sumClosedSubspaces B S hS X D₁ D₂) (op A) =
      RingHom.ker ((chartKer B S hS X D₁ A.1.hom *
        chartKer B S hS X D₂ A.1.hom).subschemeι.appTop).hom

AlgebraicGeometry.Space.definingIdealAt_sumClosedSubspaces_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisorSum.lean, line 294. The attribute's comment: “the sum of two effective Cartier divisors, for arbitrary closed subspaces”.

On an affine étale chart the defining ideal of the sum is the product of the defining ideals of the summands.

theorem definingIdealAt_sumClosedSubspaces_of_isAffine (D₁ D₂ : ClosedSubspaces B S hS X.1)
    (A : SmallEtale B S hS X.1)
    [IsAffine ((BigFppfOver.toScheme B S hS).obj A.1.left)]
    (m : A ⟶ (⟨CostructuredArrow.mk (atlasHom B S hS X), atlasHom_etale B S hS X⟩ :
      SmallEtale B S hS X.1)) :
    definingIdealAt B S hS X (sumClosedSubspaces B S hS X D₁ D₂) (op A) =
      definingIdealAt B S hS X D₁ (op A) * definingIdealAt B S hS X D₂ (op A)

Tag 083V, a lemma

Tag 083V in the Stacks Project.

AlgebraicGeometry.Space.isEffectiveCartierDivisor_sumClosedSubspaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisorSumEffective.lean, line 699.

Stacks 083V. The sum of two effective Cartier divisors on an algebraic space is again an effective Cartier divisor: its defining ideal sheaf is the tensor product of the defining ideal sheaves of the summands, and a tensor product of invertible sheaves is invertible.

theorem isEffectiveCartierDivisor_sumClosedSubspaces
    (hD₁ : IsEffectiveCartierDivisor B S hS X D₁)
    (hD₂ : IsEffectiveCartierDivisor B S hS X D₂) :
    IsEffectiveCartierDivisor B S hS X (sumClosedSubspaces B S hS X D₁ D₂)

Tag 083W, a lemma

Tag 083W in the Stacks Project.

AlgebraicGeometry.Space.isEffectiveCartierDivisor_left_of_sumClosedSubspaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisorSummands.lean, line 105. The attribute's comment: “effectivity of the first closed subspace”.

Stacks 083W. If the sum Z + Y of two closed subspaces of an algebraic space is an effective Cartier divisor, then so is the first summand Z.

theorem isEffectiveCartierDivisor_left_of_sumClosedSubspaces
    (h : IsEffectiveCartierDivisor B S hS X (sumClosedSubspaces B S hS X Z Y)) :
    IsEffectiveCartierDivisor B S hS X Z

AlgebraicGeometry.Space.isEffectiveCartierDivisor_right_of_sumClosedSubspaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisorSummands.lean, line 115. The attribute's comment: “effectivity of the second closed subspace”.

Stacks 083W. If the sum Z + Y of two closed subspaces of an algebraic space is an effective Cartier divisor, then so is the second summand Y.

theorem isEffectiveCartierDivisor_right_of_sumClosedSubspaces
    (h : IsEffectiveCartierDivisor B S hS X (sumClosedSubspaces B S hS X Z Y)) :
    IsEffectiveCartierDivisor B S hS X Y

AlgebraicGeometry.Space.eq_sumClosedSubspaces_of_definingIdealAt_eq_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisorSummands.lean, line 128. The attribute's comment: “identification with the sum”.

Stacks 083W. A closed subspace D of an algebraic space whose defining ideal is, on every affine étale chart lying over the chart carrying the sum, the product of the defining ideals of Z and Y is the sum Z + Y of Stacks 083U: that chartwise formula is what AlgebraicGeometry.Space.definingIdealAt_sumClosedSubspaces_of_isAffine asserts of the sum, and it determines a closed subspace.

theorem eq_sumClosedSubspaces_of_definingIdealAt_eq_mul
    (hD : ∀ A : SmallEtale B S hS X.1,
      IsAffine ((BigFppfOver.toScheme B S hS).obj ((SmallEtale.toOver B S hS X.1).obj A)) →
      (A ⟶ sumAtlasChart B S hS X) →
        definingIdealAt B S hS X D (op A) =
          definingIdealAt B S hS X Z (op A) * definingIdealAt B S hS X Y (op A)) :
    D = sumClosedSubspaces B S hS X Z Y

AlgebraicGeometry.Space.isEffectiveCartierDivisor_of_definingIdealAt_eq_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisorSummands.lean, line 146.

Stacks 083W. Let Z, Y be two closed subspaces of an algebraic space X with defining ideal sheaves ℐ and 𝒥. If ℐ𝒥 defines an effective Cartier divisor D ⊆ X, then Z and Y are effective Cartier divisors and D = Z + Y.

theorem isEffectiveCartierDivisor_of_definingIdealAt_eq_mul
    (hD : ∀ A : SmallEtale B S hS X.1,
      IsAffine ((BigFppfOver.toScheme B S hS).obj ((SmallEtale.toOver B S hS X.1).obj A)) →
      (A ⟶ sumAtlasChart B S hS X) →
        definingIdealAt B S hS X D (op A) =
          definingIdealAt B S hS X Z (op A) * definingIdealAt B S hS X Y (op A))
    (h : IsEffectiveCartierDivisor B S hS X D) :
    IsEffectiveCartierDivisor B S hS X Z ∧ IsEffectiveCartierDivisor B S hS X Y ∧
      D = sumClosedSubspaces B S hS X Z Y

Tag 083X, a lemma

Tag 083X in the Stacks Project.

AlgebraicGeometry.Space.isLocallyPrincipal_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LocallyPrincipalPullback.lean, line 981.

Stacks 083X. The inverse image of a locally principal closed subspace along a morphism of algebraic spaces is a locally principal closed subspace of the source.

The defining ideal of f⁻¹(Z) on an affine chart T of Y lying over an affine chart U of X is the ideal generated by the image of the defining ideal of Z on U (AlgebraicGeometry.Space.definingIdealAt_preimage_eq_map), because the closed subscheme Z ×_X T of T is the base change of the closed subscheme Z ×_X U of U. Local principality is then inherited chart by chart: every point of a chart of Y has such a pair (T, U) above it with the defining ideal of Z on U generated by a single section, and the pullback of that section generates the defining ideal of f⁻¹(Z) on T.

theorem isLocallyPrincipal_preimage (f : Y ⟶ X) (Z : ClosedSubspaces B S hS X.1)
    (hZ : IsLocallyPrincipal B S hS X Z) :
    IsLocallyPrincipal B S hS Y ⟨Z.1.preimage f.hom,
      isClosedSubspace_preimage B S hS f.hom Z.1 X.2 Y.2 Z.2⟩

Tag 083Y, a definition

Tag 083Y in the Stacks Project.

AlgebraicGeometry.Space.IsPullbackDefined, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisor.lean, line 137.

The pullback of a closed subspace D ⊆ X along a morphism f : Y ⟶ X of algebraic spaces is defined when the inverse image f⁻¹(D) ⊆ Y is an effective Cartier divisor; in that case f^*D = f⁻¹(D) is the pullback of the effective Cartier divisor.

noncomputable abbrev IsPullbackDefined {X Y : AlgebraicSpaces B S hS} (f : Y ⟶ X)
    (D : ClosedSubspaces B S hS X.1) : Prop

Tag 083Z, a lemma

Tag 083Z in the Stacks Project.

AlgebraicGeometry.Space.isPullbackDefined_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierPullbackCriteria.lean, line 161. The attribute's comment: “part (2): a flat morphism”.

Stacks 083Z (2). The pullback of an effective Cartier divisor D ⊆ Y along a flat morphism f : X ⟶ Y of algebraic spaces is defined.

A surjective étale scheme chart q : V ⟶ Y lifts to a surjective étale scheme chart p : U ⟶ X sitting over it by a morphism α : U ⟶ V of the site, and α is flat because f is. By Stacks 083C the inverse image of D is an effective Cartier divisor on V, hence by the scheme case Stacks 02OO also on U; and the inverse image of D on U through α is the inverse image of f⁻¹(D) through p, so Stacks 083C applies again, on X.

theorem isPullbackDefined_of_isFlat {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (D : ClosedSubspaces B S hS Y.1) (hD : IsEffectiveCartierDivisor B S hS Y D)
    (hf : IsFlat B S hS f.hom) :
    IsPullbackDefined B S hS f D

AlgebraicGeometry.Space.isPullbackDefined_of_notMem_weaklyAssociatedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierPullbackCriteria.lean, line 321. The attribute's comment: “part (1): no weakly associated point of the source is carried into the divisor”.

Stacks 083Z (1). The pullback of an effective Cartier divisor D ⊆ Y along a morphism f : X ⟶ Y of algebraic spaces is defined as soon as f carries no weakly associated point of X into |D|.

A surjective étale scheme chart q : V ⟶ Y lifts to a surjective étale scheme chart p : U ⟶ X over a morphism α : U ⟶ V of the site. By Stacks 083C the inverse image of D is an effective Cartier divisor on V, and the ideal sheaf of f⁻¹(D) ×_X U is its inverse image along α; the scheme case Stacks 02OO (1) therefore applies, because a weakly associated point of U lying over |D ×_Y V| would be a weakly associated point of X carried into |D|. Stacks 083C then returns the conclusion on X.

theorem isPullbackDefined_of_notMem_weaklyAssociatedPoints {X Y : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (D : ClosedSubspaces B S hS Y.1)
    (hD : IsEffectiveCartierDivisor B S hS Y D)
    (hf : ∀ x ∈ weaklyAssociatedPointsOfSpace B S hS X,
      pointsMap B S hS X.1 f.hom x ∉
        Set.range (pointsMap B S hS D.1.toFunctor D.1.ι)) :
    IsPullbackDefined B S hS f D

AlgebraicGeometry.Space.isEffectiveCartierDivisor_exceptionalPreimage_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/StrictTransformLocalGenerators.lean, line 847. The attribute's comment: “part (2), at the exceptional divisor of a blowup”.

The exceptional divisor of a blowup is an effective Cartier divisor on the fibre product in which the strict transform lives.

Let b : X' ⟶ X be the blowup of an algebraic space X in a closed subspace Z, and let E = b^{-1}Z ⊆ X' be its exceptional divisor. Then the preimage of E along the projection X ×_X X' ⟶ X' — the subspace the strict transform of an 𝒪_X-module divides out the sections supported on — is an effective Cartier divisor on X ×_X X'.

theorem isEffectiveCartierDivisor_exceptionalPreimage_id {X X' : AlgebraicSpaces B S hS}
    {Z : ClosedSubspaces B S hS X.1} {b : X' ⟶ X} (hb : IsBlowupAlong B S hS Z b) :
    IsEffectiveCartierDivisor B S hS (strictTransformPullback B S hS (𝟙 X) b)
      ⟨exceptionalPreimage B S hS (𝟙 X) b (preimageClosedSubspace b Z).1,
        exceptionalPreimage_isClosedSubspace B S hS (𝟙 X) b
          (preimageClosedSubspace b Z).1 (preimageClosedSubspace b Z).2⟩

Tag 0840, a lemma

Tag 0840 in the Stacks Project.

AlgebraicGeometry.Space.preimage_sumClosedSubspaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisorSumPullback.lean, line 206. The attribute's comment: “the inverse image commutes with the sum”.

Stacks 0840. The inverse image of a sum of closed subspaces is the sum of the inverse images: f^*(D₁ + D₂) = f^*D₁ + f^*D₂ for the sum of Stacks 083U.

theorem preimage_sumClosedSubspaces (f : Y ⟶ X) (D₁ D₂ : ClosedSubspaces B S hS X.1) :
    (⟨(sumClosedSubspaces B S hS X D₁ D₂).1.preimage f.hom,
        isClosedSubspace_preimage B S hS f.hom (sumClosedSubspaces B S hS X D₁ D₂).1 X.2 Y.2
          (sumClosedSubspaces B S hS X D₁ D₂).2⟩ : ClosedSubspaces B S hS Y.1) =
      sumClosedSubspaces B S hS Y
        ⟨D₁.1.preimage f.hom, isClosedSubspace_preimage B S hS f.hom D₁.1 X.2 Y.2 D₁.2⟩
        ⟨D₂.1.preimage f.hom, isClosedSubspace_preimage B S hS f.hom D₂.1 X.2 Y.2 D₂.2⟩

AlgebraicGeometry.Space.isPullbackDefined_sumClosedSubspaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisorSumPullback.lean, line 248. The attribute's comment: “the pullback of the sum is defined”.

Stacks 0840. If the pullbacks of two closed subspaces along f : Y ⟶ X are defined, then so is the pullback of their sum.

theorem isPullbackDefined_sumClosedSubspaces (f : Y ⟶ X) (D₁ D₂ : ClosedSubspaces B S hS X.1)
    (h₁ : IsPullbackDefined B S hS f D₁) (h₂ : IsPullbackDefined B S hS f D₂) :
    IsPullbackDefined B S hS f (sumClosedSubspaces B S hS X D₁ D₂)

Sources

• Section 71.6, Tag 083A
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.IsLocallyPrincipal · AlgebraicGeometry.Space.IsEffectiveCartierDivisor · AlgebraicGeometry.Space.hasAffinePrincipalEtaleNeighborhoods_of_hasEffectiveCartierEtaleCover · AlgebraicGeometry.Space.hasEffectiveCartierEtalePullbacks_of_hasAffinePrincipal · AlgebraicGeometry.Space.hasEffectiveCartierEtalePullbacks_iff_hasAffinePrincipal · AlgebraicGeometry.Space.hasEffectiveCartierEtaleCover_iff_etalePullbacks · AlgebraicGeometry.Space.hasEffectiveCartierEtalePullbacks_of_isEffectiveCartier · AlgebraicGeometry.Space.hasEffectiveCartierEtaleCover_of_isEffectiveCartier

Section71.7 Effective Cartier divisors and invertible sheaves#

Section 71.7 of the Stacks Project, Tag 0CPG. 8 tags here are carried by 35 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0841, a definition

Tag 0841 in the Stacks Project.

AlgebraicGeometry.Space.associatedInvertibleSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisor.lean, line 179. The attribute's comment: “part (1): the associated invertible sheaf”.

The invertible sheaf 𝒪_X(D) associated to an effective Cartier divisor D ⊆ X: the inverse tensor power 𝓘_D^{⊗ -1} of its defining ideal sheaf.

noncomputable def associatedInvertibleSheaf (D : ClosedSubspaces B S hS X.1)
    (hD : IsEffectiveCartierDivisor B S hS X D) :
    SheafOfModules.{u} (structureRingSheaf B S hS X)

AlgebraicGeometry.Space.associatedInvertibleSheaf_isInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisor.lean, line 195. The attribute's comment: “part (1): the associated invertible sheaf”.

The sheaf 𝒪_X(D) associated to an effective Cartier divisor is invertible.

theorem associatedInvertibleSheaf_isInvertible (D : ClosedSubspaces B S hS X.1)
    (hD : IsEffectiveCartierDivisor B S hS X D) :
    AlgebraicGeometry.SheafOfModules.IsInvertible (structureCommRings B S hS X)
      (structureRingSheaf B S hS X).property
      (associatedInvertibleSheaf B S hS X D hD)

AlgebraicGeometry.Space.idealSheafHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisor.lean, line 208. The attribute's comment: “part (1): the associated invertible sheaf”.

The sheaf-hom SheafHom_{𝒪_X}(𝓘_D, 𝒪_X), the second description of 𝒪_X(D). Its sections over an étale chart U are the morphisms 𝓘_D|_U ⟶ 𝒪_X|_U of 𝒪_X|_U-modules on the slice site over U, hence live one universe above the sections of the structure sheaf.

noncomputable def idealSheafHom (Z : ClosedSubspaces B S hS X.1) :
    SheafOfModules.{u + 1} (structureRingSheaf B S hS X)

AlgebraicGeometry.Space.associatedInvertibleSheafHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisor.lean, line 236. The attribute's comment: “part (1): the associated invertible sheaf”.

The two descriptions of 𝒪_X(D) agree: a section of 𝓘_D^{⊗ -1} over an étale chart U is the same thing as a morphism 𝓘_D|_U ⟶ 𝒪_X|_U, by a linear equivalence of sections.

noncomputable def associatedInvertibleSheafHomEquiv (D : ClosedSubspaces B S hS X.1)
    (hD : IsEffectiveCartierDivisor B S hS X D) (U : SmallEtale B S hS X.1) :
    (modulePresheaf B S hS X (associatedInvertibleSheaf B S hS X D hD)).obj (Opposite.op U)
        ≃ₗ[(structureCommRings B S hS X).obj (Opposite.op U)]
      internalHomObj (structureCommRings B S hS X)
        (modulePresheaf B S hS X (idealSheafOfModules B S hS X D))
        (modulePresheaf B S hS X (SheafOfModules.unit (structureRingSheaf B S hS X))) U

AlgebraicGeometry.Space.associatedInvertibleSheafHomEquiv_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisor.lean, line 273. The attribute's comment: “part (1): the associated invertible sheaf”.

The identification of the two descriptions of 𝒪_X(D) is given by the evaluation pairing: the morphism 𝓘_D|_U ⟶ 𝒪_X|_U attached to a section s of 𝓘_D^{⊗ -1} over U sends a section t of 𝓘_D over an étale chart V over U to the value of the evaluation pairing on the restriction of s tensored with t.

theorem associatedInvertibleSheafHomEquiv_apply (D : ClosedSubspaces B S hS X.1)
    (hD : IsEffectiveCartierDivisor B S hS X D) (U : SmallEtale B S hS X.1)
    (s : (modulePresheaf B S hS X
      (associatedInvertibleSheaf B S hS X D hD)).obj (Opposite.op U))
    (V : (SmallEtale B S hS X.1)ᵒᵖ) (f : V.unop ⟶ U)
    (t : (modulePresheaf B S hS X (idealSheafOfModules B S hS X D)).obj V) :
    homSectionCoeff (structureCommRings B S hS X)
        (modulePresheaf B S hS X (idealSheafOfModules B S hS X D))
        (modulePresheaf B S hS X (SheafOfModules.unit (structureRingSheaf B S hS X))) U
        (associatedInvertibleSheafHomEquiv B S hS X D hD U s) V f t =
      tensorHomAt (structureCommRings B S hS X)
        (modulePresheaf B S hS X (associatedInvertibleSheaf B S hS X D hD))
        (modulePresheaf B S hS X (idealSheafOfModules B S hS X D))
        (modulePresheaf B S hS X (SheafOfModules.unit (structureRingSheaf B S hS X)))
        (tensorPairing (structureCommRings B S hS X) (structureRingSheaf B S hS X).property
          (idealSheafOfModules B S hS X D) (associatedInvertibleSheaf B S hS X D hD)
          (SheafOfModules.unit (structureRingSheaf B S hS X))
          (associatedInvertibleSheafEvaluation B S hS X D hD)) V
        ((modulePresheaf B S hS X
          (associatedInvertibleSheaf B S hS X D hD)).restrictₛₗ f.op s ⊗ₜ t)

AlgebraicGeometry.Space.canonicalSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisor.lean, line 332. The attribute's comment: “part (2): the canonical section”.

The canonical section 1_D of 𝒪_X(D): the global section corresponding, under the identification of 𝒪_X(D) with SheafHom_{𝒪_X}(𝓘_D, 𝒪_X), to the inclusion 𝓘_D ⟶ 𝒪_X.

noncomputable def canonicalSection (D : ClosedSubspaces B S hS X.1)
    (hD : IsEffectiveCartierDivisor B S hS X D) :
    (associatedInvertibleSheaf B S hS X D hD).sections

AlgebraicGeometry.Space.canonicalSection_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisor.lean, line 348. The attribute's comment: “part (2): the canonical section”.

The canonical section of 𝒪_X(D) is, on every étale chart, the inclusion 𝓘_D ⟶ 𝒪_X read through the identification of 𝒪_X(D) with SheafHom_{𝒪_X}(𝓘_D, 𝒪_X).

theorem canonicalSection_apply (D : ClosedSubspaces B S hS X.1)
    (hD : IsEffectiveCartierDivisor B S hS X D) (U : (SmallEtale B S hS X.1)ᵒᵖ) :
    associatedInvertibleSheafHomEquiv B S hS X D hD U.unop
        ((canonicalSection B S hS X D hD).val U) =
      idealInclusionSection B S hS X D U

AlgebraicGeometry.Space.negativeDivisorSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisor.lean, line 359. The attribute's comment: “part (3): the negative of a divisor”.

The sheaf 𝒪_X(-D) = 𝒪_X(D)^{⊗ -1}.

noncomputable def negativeDivisorSheaf (D : ClosedSubspaces B S hS X.1)
    (hD : IsEffectiveCartierDivisor B S hS X D) :
    SheafOfModules.{u} (structureRingSheaf B S hS X)

AlgebraicGeometry.Space.negativeDivisorSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisor.lean, line 370. The attribute's comment: “part (3): the negative of a divisor”.

The identification 𝒪_X(-D) ≅ 𝓘_D.

noncomputable def negativeDivisorSheafIso (D : ClosedSubspaces B S hS X.1)
    (hD : IsEffectiveCartierDivisor B S hS X D) :
    negativeDivisorSheaf B S hS X D hD ≅ idealSheafOfModules B S hS X D

AlgebraicGeometry.Space.differenceDivisorSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisor.lean, line 400. The attribute's comment: “part (4): the difference of two divisors”.

The sheaf 𝒪_X(D - D') = 𝒪_X(D) ⊗_{𝒪_X} 𝒪_X(-D') attached to a pair of effective Cartier divisors.

noncomputable def differenceDivisorSheaf (D D' : ClosedSubspaces B S hS X.1)
    (hD : IsEffectiveCartierDivisor B S hS X D)
    (hD' : IsEffectiveCartierDivisor B S hS X D') :
    SheafOfModules.{u} (structureRingSheaf B S hS X)

Tag 0B4F, a lemma

Tag 0B4F in the Stacks Project.

AlgebraicGeometry.Space.conormalModuleIsoPullbackIdealSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleOfEffectiveCartierDivisor.lean, line 77. The attribute's comment: “the conormal sheaf is the restriction of the ideal sheaf”.

The first identification of Stacks 0B4F, 𝒞_{Z/X} = 𝓘_Z|_Z: the conormal module of a closed subspace Z of an algebraic space X is the restriction to Z of the defining ideal sheaf 𝓘_Z ⊆ 𝒪_X, where restriction is the inverse image along the inclusion i : Z ⟶ X. Z need not be an effective Cartier divisor.

noncomputable def conormalModuleIsoPullbackIdealSheaf (X : AlgebraicSpaces B S hS)
    (Z : ClosedSubspaces B S hS X.1) :
    conormalModule B S hS X Z ≅
      (modulePullback B S hS (subspaceInclusion B S hS X Z)).obj
        (idealSheafOfModules B S hS X Z)

AlgebraicGeometry.Space.pullbackIdealSheafIsoPullbackNegativeDivisorSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleOfEffectiveCartierDivisor.lean, line 99. The attribute's comment: “the restriction of the ideal sheaf is the restriction of the inverse of O_X(D)”.

The second identification of Stacks 0B4F, 𝓘_D|_D = 𝒪_X(D)^{⊗ -1}|_D: for an effective Cartier divisor D ⊆ X, the restriction to D of the defining ideal sheaf 𝓘_D agrees with the restriction to D of 𝒪_X(-D) = 𝒪_X(D)^{⊗ -1}.

It is the inverse image along the inclusion i : D ⟶ X of the canonical identification 𝒪_X(-D) ≅ 𝓘_D of Stacks 0841, part 3 (AlgebraicGeometry.Space.negativeDivisorSheafIso).

noncomputable def pullbackIdealSheafIsoPullbackNegativeDivisorSheaf
    (X : AlgebraicSpaces B S hS) (D : ClosedSubspaces B S hS X.1)
    (hD : IsEffectiveCartierDivisor B S hS X D) :
    (modulePullback B S hS (subspaceInclusion B S hS X D)).obj
        (idealSheafOfModules B S hS X D) ≅
      (modulePullback B S hS (subspaceInclusion B S hS X D)).obj
        (negativeDivisorSheaf B S hS X D hD)

Tag 0842, a lemma

Tag 0842 in the Stacks Project.

AlgebraicGeometry.Space.existsUnique_tensorInvertibleSheafIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisorTensorIso.lean, line 1310.

Stacks 0842. For two effective Cartier divisors D₁, D₂ on an algebraic space X with sum D = D₁ + D₂ there is a unique isomorphism 𝒪_X(D₁) ⊗_{𝒪_X} 𝒪_X(D₂) ⟶ 𝒪_X(D) carrying 1_{D₁} ⊗ 1_{D₂} to 1_D.

theorem existsUnique_tensorInvertibleSheafIso :
    ∃! e : (((Stacks.SheafOfModules.Tensor.sheafTensor.{u + 1, u, u, u, u}
        ⟨(structureCommRings B S hS X), Presheaf.isSheaf_of_isSheaf_comp _
        ((structureCommRings B S hS X)) (forget₂ CommRingCat RingCat)
        ((structureRingSheaf B S hS X).property)⟩).obj
        ((associatedInvertibleSheaf B S hS X D₁ hD₁))).obj
        ((associatedInvertibleSheaf B S hS X D₂ hD₂))) ≅
        associatedInvertibleSheaf B S hS X (sumClosedSubspaces B S hS X D₁ D₂)
          (isEffectiveCartierDivisor_sumClosedSubspaces B S hS X D₁ D₂ hD₁ hD₂),
      ∀ U : (SmallEtale B S hS X.1)ᵒᵖ,
        (e.hom.val.app U).hom
            ((tensorCanonicalSection B S hS X D₁ D₂ hD₁ hD₂).val U) =
          (canonicalSection B S hS X (sumClosedSubspaces B S hS X D₁ D₂)
            (isEffectiveCartierDivisor_sumClosedSubspaces B S hS X D₁ D₂ hD₁ hD₂)).val U

Tag 0843, a definition

Tag 0843 in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.IsRegularSection, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Decent/RegularSectionsAndRepresentability.lean, line 27 (StacksFrontier).

Tag 0844, a lemma

Tag 0844 in the Stacks Project.

AlgebraicGeometry.Space.isRegularSection_iff_etaleLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularSections.lean, line 289. The attribute's comment: “conditions (1) and (2)”.

Stacks 0844, conditions (1) and (2). A global regular function on an algebraic space is a regular section of the structure sheaf if and only if its image in the étale local ring at every geometric point is a nonzerodivisor.

theorem isRegularSection_iff_etaleLocalRing (f : GlobalFunctions B S hS X hX) :
    IsRegularSection (structurePresheaf B S hS X)
        (structureRingPresheaf_isSheaf B S hS X hX) f ↔
      ∀ (x : GeometricPoint B S hS X) (V : SmallEtaleNeighborhood x),
        IsSMulRegular (etaleLocalRing B S hS X x)
          (etaleLocalRingGerm B S hS X x (op V)
            (chartValue B S hS X hX f V.chart))

AlgebraicGeometry.Space.isRegularSection_iff_affineEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularSections.lean, line 320. The attribute's comment: “conditions (1) and (3)”.

Stacks 0844, conditions (1) and (3). A global regular function on an algebraic space is a regular section of the structure sheaf if and only if its restriction to every affine étale chart is a nonzerodivisor there.

theorem isRegularSection_iff_affineEtale (f : GlobalFunctions B S hS X hX) :
    IsRegularSection (structurePresheaf B S hS X)
        (structureRingPresheaf_isSheaf B S hS X hX) f ↔
      ∀ U : SmallEtale B S hS X, IsAffine (etaleChartScheme B S hS U) →
        IsSMulRegular (Γ(etaleChartScheme B S hS U, ⊤))
          (chartValue B S hS X hX f U)

AlgebraicGeometry.Space.isRegularSection_iff_exists_surjectiveChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularSections.lean, line 336. The attribute's comment: “conditions (1) and (4)”.

Stacks 0844, conditions (1) and (4). A global regular function on an algebraic space is a regular section of the structure sheaf if and only if there is a surjective étale scheme chart on which its restriction is a regular section.

theorem isRegularSection_iff_exists_surjectiveChart (f : GlobalFunctions B S hS X hX) :
    IsRegularSection (structurePresheaf B S hS X)
        (structureRingPresheaf_isSheaf B S hS X hX) f ↔
      ∃ C : SmallEtale B S hS X, IsSurjective B S hS C.obj.hom ∧
        IsRegularSection (etaleChartScheme B S hS C).presheaf
          ((Presheaf.isSheaf_iff_isSheaf_comp _ (etaleChartScheme B S hS C).presheaf
            (forget₂ CommRingCat.{u} RingCat.{u})).mp
              (etaleChartScheme B S hS C).IsSheaf)
          (chartFunctionSections B S hS X hX f C)

Tag 0845, a definition

Tag 0845 in the Stacks Project.

AlgebraicGeometry.Space.zeroSchemeSubfunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZeroScheme.lean, line 305. The attribute's comment: “underlying subfunctor construction”.

Stacks 0845. Intersect the closed subspaces whose defining ideals are contained in the ideals generated by local evaluations of the section.

noncomputable def zeroSchemeSubfunctor (X : AlgebraicSpaces B S hS)
    (L : Modules.{u, u} B S hS X.1 X.2) (s : L.sections) : Subfunctor X.1

AlgebraicGeometry.Space.zeroSchemeSubfunctor_isClosedSubspace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZeroScheme.lean, line 319. The attribute's comment: “closedness”.

Stacks 0845. The subfunctor cut out by evaluation at a section of a module sheaf is a closed subspace.

theorem zeroSchemeSubfunctor_isClosedSubspace (X : AlgebraicSpaces B S hS)
    (L : Modules.{u, u} B S hS X.1 X.2) (s : L.sections) :
    IsClosedSubspace B S hS (zeroSchemeSubfunctor B S hS X L s)

Tag 0846, a lemma

Tag 0846 in the Stacks Project.

AlgebraicGeometry.Space.isGreatest_zeroScheme_of_exists_definingIdealAt_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZeroSchemeAssertions.lean, line 179. The attribute's comment: “part (1): maximality, with vanishing on a closed subspace read chartwise and with the realization of the evaluation ideal by a closed subspace assumed”.

Stacks 0846 (1). Among the closed subspaces of X on which the section vanishes — read chartwise: those whose defining ideal contains the evaluation ideal of the section on every affine étale chart — the zero scheme of the section is the greatest.

The hypothesis is the surjectivity half of Stacks 03MB for the evaluation ideal: some closed subspace of X has that ideal as its defining ideal on the affine étale charts. It is used only to see that the zero scheme is itself a member of the ordered set; the upper-bound half AlgebraicGeometry.Space.le_zeroSchemeSubfunctor is unconditional.

theorem isGreatest_zeroScheme_of_exists_definingIdealAt_eq (X : AlgebraicSpaces B S hS)
    (L : Modules.{u, u} B S hS X.1 X.2) (s : L.sections)
    (hZ : ∃ Z : ClosedSubspaces B S hS X.1, ∀ U : SmallEtale B S hS X.1,
      IsAffine ((SmallEtale.toSchemes B S hS X.1).obj U).1 →
      definingIdealAt B S hS X Z (op U) = sectionEvaluationIdealAt B S hS X L s U) :
    IsGreatest {W : ClosedSubspaces B S hS X.1 |
      ∀ U : SmallEtale B S hS X.1,
        IsAffine ((SmallEtale.toSchemes B S hS X.1).obj U).1 →
        sectionEvaluationIdealAt B S hS X L s U ≤ definingIdealAt B S hS X W (op U)}
      (zeroScheme B S hS X L s)

AlgebraicGeometry.Space.exists_comp_eq_zeroScheme_iff_of_exists_definingIdealAt_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZeroSchemeAssertions.lean, line 205. The attribute's comment: “part (2): factorization, with vanishing of the pulled-back section read chartwise and with the realization of the evaluation ideal by a closed subspace assumed”.

Stacks 0846 (2). A morphism f : Y ⟶ X of algebraic spaces factors through the zero scheme of the section exactly when the section vanishes after pullback along f — read chartwise: on every affine étale chart U of X the evaluation ideal of the section is killed by pullback of regular functions along every point of Y lying over U.

The hypothesis is the same one as in part (1), and is used only for the direction from factoring to vanishing; the converse AlgebraicGeometry.Space.exists_comp_eq_zeroScheme_of_sectionEvaluationIdealAt_le is unconditional.

theorem exists_comp_eq_zeroScheme_iff_of_exists_definingIdealAt_eq
    (X Y : AlgebraicSpaces B S hS)
    (L : Modules.{u, u} B S hS X.1 X.2) (s : L.sections)
    (hZ : ∃ Z : ClosedSubspaces B S hS X.1, ∀ U : SmallEtale B S hS X.1,
      IsAffine ((SmallEtale.toSchemes B S hS X.1).obj U).1 →
      definingIdealAt B S hS X Z (op U) = sectionEvaluationIdealAt B S hS X L s U)
    (f : Y ⟶ X) :
    (∃ g : Y ⟶ (⟨(zeroScheme B S hS X L s).1.toFunctor,
        (zeroScheme B S hS X L s).2.1⟩ : AlgebraicSpaces B S hS),
      g ≫ ObjectProperty.homMk (zeroScheme B S hS X L s).1.ι = f) ↔
      ∀ U : SmallEtale B S hS X.1,
        IsAffine ((BigFppfOver.toScheme B S hS).obj U.1.left) →
        ∀ (a : BigFppfOver B S hS) (k : a ⟶ U.1.left) (y : yoneda.obj a ⟶ Y.1),
          yoneda.map k ≫ U.1.hom = y ≫ f.hom →
            sectionEvaluationIdealAt B S hS X L s U ≤
              RingHom.ker (Scheme.Γ.map ((BigFppfOver.toScheme B S hS).map k).op).hom

AlgebraicGeometry.Space.isLocallyPrincipal_zeroScheme_of_epi_inverseTensorPower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZeroSchemeAssertions.lean, line 239. The attribute's comment: “part (3): locally principal, assuming an epimorphism onto the ideal sheaf from the inverse tensor power of the invertible module and local generation of that power by one section”.

Stacks 0846 (3). The zero scheme of a section of an invertible 𝒪_X-module is a locally principal closed subspace of X.

Two hypotheses are carried, and both are used. The first is an epimorphism p onto the defining ideal sheaf of the zero scheme from the inverse tensor power L^{⊗ -1} of Stacks 01CU, which in the source is the image factorization of the evaluation map L^{⊗ -1} ⟶ 𝒪_X cutting out Z(s); its source is pinned to L^{⊗ -1} rather than left arbitrary, since for an arbitrary source the identity of the ideal sheaf would witness the hypothesis. The second is local generation of L^{⊗ -1} by one section, which for an invertible module is the descent clause of Stacks 0B8M.

theorem isLocallyPrincipal_zeroScheme_of_epi_inverseTensorPower (X : AlgebraicSpaces B S hS)
    (L : Modules.{u, u} B S hS X.1 X.2)
    [AlgebraicGeometry.SheafOfModules.IsInvertible (structureCommRings B S hS X)
      (structureRingSheaf B S hS X).property L]
    (s : L.sections)
    (hfree : _root_.SheafOfModules.IsLocallyGeneratedByOnSite
      (Stacks.SheafOfModules.Invertible.tensorPower (structureCommRings B S hS X)
        (structureRingSheaf B S hS X).property L (-1)) 1)
    (p : Stacks.SheafOfModules.Invertible.tensorPower (structureCommRings B S hS X)
        (structureRingSheaf B S hS X).property L (-1) ⟶
      idealSheafOfModules B S hS X (zeroScheme B S hS X L s))
    (hp : Epi p) :
    IsLocallyPrincipal B S hS X (zeroScheme B S hS X L s)

AlgebraicGeometry.Space.definingIdealAt_zeroScheme_eq_span_generator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZeroSchemeAssertions.lean, line 264. The attribute's comment: “part (4) read chartwise: the zero scheme is cut out on an affine chart by one regular function, with the realization of the evaluation ideal by a closed subspace assumed”.

Stacks 0846 (4), first half, read chartwise. On an affine étale chart U of X where L is free of rank one, with generator t and coordinate functional l₀, the zero scheme of the section is cut out by the single regular function l₀(s|_U).

The hypothesis is the one of parts (1) and (2): some closed subspace of X has the evaluation ideal of the section as its defining ideal on the affine étale charts.

theorem definingIdealAt_zeroScheme_eq_span_generator (X : AlgebraicSpaces B S hS)
    (L : Modules.{u, u} B S hS X.1 X.2) (s : L.sections)
    (hZ : ∃ Z : ClosedSubspaces B S hS X.1, ∀ U : SmallEtale B S hS X.1,
      IsAffine ((SmallEtale.toSchemes B S hS X.1).obj U).1 →
      definingIdealAt B S hS X Z (op U) = sectionEvaluationIdealAt B S hS X L s U)
    (U : SmallEtale B S hS X.1)
    (hU : IsAffine ((SmallEtale.toSchemes B S hS X.1).obj U).1)
    (t : ToType (L.val.obj (op U)))
    (l₀ : Module.Dual
      ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS X.1 X.2).O).obj.obj
        (op U))
      (L.val.obj (op U)))
    (hb : ∀ x, l₀ x • t = x) :
    definingIdealAt B S hS X (zeroScheme B S hS X L s) (op U) =
      Ideal.span {l₀ (s.eval (op U))}

AlgebraicGeometry.Space.isGreatest_zeroScheme_of_isInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZeroSchemeAssertionsInvertible.lean, line 59. The attribute's comment: “part (1): maximality of the zero scheme among the closed subspaces on which the section vanishes, read chartwise, with no assumed inputs”.

Stacks 0846 (1). Let L be an invertible 𝒪_X-module and s a global section of L. Among the closed subspaces of X on which s vanishes — read chartwise: those whose defining ideal contains the evaluation ideal of s on every affine étale chart — the zero scheme of s is the greatest.

The hypotheses are the source's own and nothing else: invertibility of L discharges the realization of the evaluation ideal by a closed subspace, through AlgebraicGeometry.Space.exists_definingIdealAt_eq_sectionEvaluationIdealAt_of_isInvertible.

theorem isGreatest_zeroScheme_of_isInvertible (X : AlgebraicSpaces B S hS)
    (L : Modules.{u, u} B S hS X.1 X.2)
    (hinv : AlgebraicGeometry.SheafOfModules.IsInvertible (structureCommRings B S hS X)
      (structureRingSheaf B S hS X).property L)
    (s : L.sections) :
    IsGreatest {W : ClosedSubspaces B S hS X.1 |
      ∀ U : SmallEtale B S hS X.1,
        IsAffine ((SmallEtale.toSchemes B S hS X.1).obj U).1 →
        sectionEvaluationIdealAt B S hS X L s U ≤ definingIdealAt B S hS X W (op U)}
      (zeroScheme B S hS X L s)

AlgebraicGeometry.Space.exists_comp_eq_zeroScheme_iff_of_isInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZeroSchemeAssertionsInvertible.lean, line 83. The attribute's comment: “part (2): a morphism factors through the zero scheme exactly when the pulled-back section vanishes, read chartwise, with no assumed inputs”.

Stacks 0846 (2). Let L be an invertible 𝒪_X-module and s a global section of L. A morphism f : Y ⟶ X of algebraic spaces factors through the zero scheme of s exactly when s vanishes after pullback along f — read chartwise: on every affine étale chart U of X the evaluation ideal of s is killed by pullback of regular functions along every point of Y lying over U.

The hypotheses are the source's own and nothing else: invertibility of L discharges the realization of the evaluation ideal by a closed subspace, through AlgebraicGeometry.Space.exists_definingIdealAt_eq_sectionEvaluationIdealAt_of_isInvertible.

theorem exists_comp_eq_zeroScheme_iff_of_isInvertible (X Y : AlgebraicSpaces B S hS)
    (L : Modules.{u, u} B S hS X.1 X.2)
    (hinv : AlgebraicGeometry.SheafOfModules.IsInvertible (structureCommRings B S hS X)
      (structureRingSheaf B S hS X).property L)
    (s : L.sections) (f : Y ⟶ X) :
    (∃ g : Y ⟶ (⟨(zeroScheme B S hS X L s).1.toFunctor,
        (zeroScheme B S hS X L s).2.1⟩ : AlgebraicSpaces B S hS),
      g ≫ ObjectProperty.homMk (zeroScheme B S hS X L s).1.ι = f) ↔
      ∀ U : SmallEtale B S hS X.1,
        IsAffine ((BigFppfOver.toScheme B S hS).obj U.1.left) →
        ∀ (a : BigFppfOver B S hS) (k : a ⟶ U.1.left) (y : yoneda.obj a ⟶ Y.1),
          yoneda.map k ≫ U.1.hom = y ≫ f.hom →
            sectionEvaluationIdealAt B S hS X L s U ≤
              RingHom.ker (Scheme.Γ.map ((BigFppfOver.toScheme B S hS).map k).op).hom

AlgebraicGeometry.Space.definingIdealAt_zeroScheme_eq_span_generator_of_isInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZeroSchemeAssertionsInvertible.lean, line 117. The attribute's comment: “part (4) read chartwise: the zero scheme is cut out on an affine chart by one regular function, with L carried as free of rank one on that chart by a generator t and a coordinate functional l₀; the chart U and the functional l₀ occur in the conclusion, which names the function as l₀ of the section over U”.

Stacks 0846 (4), first half, read chartwise. Let L be an invertible 𝒪_X-module and s a global section of L. On an affine étale chart U of X where L is free of rank one, with generator t and coordinate functional l₀, the zero scheme of s is cut out by the single regular function l₀(s|_U).

Invertibility of L discharges the realization of the evaluation ideal by a closed subspace, through AlgebraicGeometry.Space.exists_definingIdealAt_eq_sectionEvaluationIdealAt_of_isInvertible. The chart data t, l₀, hb is local freeness of rank one on U, which for an invertible L holds on a cover of X by Stacks 0B8Q; it is what makes the chartwise reading of the part a statement about one regular function, and it is what the global form AlgebraicGeometry.Space.isEffectiveCartierDivisor_zeroScheme_iff_isRegularSection supplies for itself instead of assuming.

theorem definingIdealAt_zeroScheme_eq_span_generator_of_isInvertible (X : AlgebraicSpaces B S hS)
    (L : Modules.{u, u} B S hS X.1 X.2)
    (hinv : AlgebraicGeometry.SheafOfModules.IsInvertible (structureCommRings B S hS X)
      (structureRingSheaf B S hS X).property L)
    (s : L.sections)
    (U : SmallEtale B S hS X.1)
    (hU : IsAffine ((SmallEtale.toSchemes B S hS X.1).obj U).1)
    (t : ToType (L.val.obj (op U)))
    (l₀ : Module.Dual
      ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS X.1 X.2).O).obj.obj
        (op U))
      (L.val.obj (op U)))
    (hb : ∀ x, l₀ x • t = x) :
    definingIdealAt B S hS X (zeroScheme B S hS X L s) (op U) =
      Ideal.span {l₀ (s.eval (op U))}

AlgebraicGeometry.Space.isEffectiveCartierDivisor_zeroScheme_iff_isRegularSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZeroSchemeEffectiveCartier.lean, line 382. The attribute's comment: “part (4): the zero scheme is an effective Cartier divisor exactly when the section is regular, with no assumed inputs”.

Stacks 0846 (4). Let X be an algebraic space over a scheme S, let L be an invertible 𝒪_X-module and let s be a global section of L. The zero scheme Z(s) of Stacks 0845 is an effective Cartier divisor on X if and only if s is a regular section of L in the sense of Stacks 0843.

The hypotheses are the source's own and nothing else: no local freeness of L of rank one on a chart, and no chart data, is assumed. Invertibility of L supplies that data chart by chart, by Stacks 0B8Q, and both sides of the equivalence are local on the small étale site of X, so the chartwise content of the part can be assembled into the global statement.

theorem isEffectiveCartierDivisor_zeroScheme_iff_isRegularSection
    (hinv : AlgebraicGeometry.SheafOfModules.IsInvertible (structureCommRings B S hS X)
      (structureRingSheaf B S hS X).property L) :
    IsEffectiveCartierDivisor B S hS X (zeroScheme B S hS X L s) ↔
      AlgebraicGeometry.IsRegularSection (structurePresheaf B S hS X.1)
        (Stacks.SheafOfModules.Tensor.ringSheaf
          (smallEtaleRingedSite B S hS X.1 X.2).O).property s

AlgebraicGeometry.Space.isLocallyPrincipal_zeroScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZeroSchemeLocallyPrincipal.lean, line 270. The attribute's comment: “part (3): the zero scheme of a section of an invertible module is a locally principal closed subspace”.

The zero scheme of a global section s of an invertible 𝒪_X-module L is a locally principal closed subspace of X.

theorem isLocallyPrincipal_zeroScheme
    (hinv : AlgebraicGeometry.SheafOfModules.IsInvertible (structureCommRings B S hS X)
      (structureRingSheaf B S hS X).property L) :
    IsLocallyPrincipal B S hS X (zeroScheme B S hS X L s)

AlgebraicGeometry.Space.isRegularSection_iff_forall_injective_mul_generator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZeroSchemeProperties.lean, line 224. The attribute's comment: “part (4) read chartwise: the section is regular exactly when the functions cutting out the zero scheme are nonzerodivisors, with L carried as free of rank one on every chart”.

A global section of a module free of rank one on every étale chart is regular exactly when the generators of its evaluation ideals are nonzerodivisors. This is the chartwise content of Stacks 0846 (4): the zero scheme is cut out on each chart by the single element l₀(s|_U), and regularity of s is injectivity of multiplication by each of them.

theorem isRegularSection_iff_forall_injective_mul_generator (X : AlgebraicSpaces B S hS)
    (L : Modules.{u, u} B S hS X.1 X.2) (s : L.sections)
    (t : ∀ U : SmallEtale B S hS X.1, ToType (L.val.obj (op U)))
    (l₀ : ∀ U : SmallEtale B S hS X.1,
      Module.Dual ((Stacks.SheafOfModules.Tensor.ringSheaf
          (smallEtaleRingedSite B S hS X.1 X.2).O).obj.obj (op U))
        (L.val.obj (op U)))
    (hb : ∀ (U : SmallEtale B S hS X.1) (x), l₀ U x • t U = x) :
    AlgebraicGeometry.IsRegularSection (structurePresheaf B S hS X.1)
        (Stacks.SheafOfModules.Tensor.ringSheaf
            (smallEtaleRingedSite B S hS X.1 X.2).O).property s ↔
      ∀ U : SmallEtale B S hS X.1,
        Function.Injective
          (fun r : ToType ((Stacks.SheafOfModules.Tensor.ringSheaf
              (smallEtaleRingedSite B S hS X.1 X.2).O).obj.obj (op U)) =>
            r * l₀ U (s.eval (op U)))

Tag 0847, a lemma

Tag 0847 in the Stacks Project.

AlgebraicGeometry.Space.iso_eq_of_canonicalSectionHom_comp_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CanonicalSectionIsoUnique.lean, line 169. The attribute's comment: “part (2): uniqueness of the isomorphism — two isomorphisms from the sheaf of an effective Cartier divisor to an invertible module, both carrying the canonical section to the given section, are equal; with no assumed inputs”.

Stacks 0847, part (2): the isomorphism is unique. Let D ⊆ X be an effective Cartier divisor on an algebraic space X and let s be a global section of an 𝒪_X-module L. Two isomorphisms 𝒪_X(D) ≅ L which both carry the canonical section 1_D of 𝒪_X(D) to s are equal.

Composing one with the inverse of the other gives an endomorphism of 𝒪_X(D) fixing 1_D, and AlgebraicGeometry.Space.eq_id_of_comp_eq_of_isInvertible makes it the identity: 𝒪_X(D) is invertible and 1_D is regular by part (1) of the same tag.

theorem iso_eq_of_canonicalSectionHom_comp_eq
    (L : SheafOfModules.{u} (structureRingSheaf B S hS X)) (s : L.sections)
    (i j : associatedInvertibleSheaf B S hS X D hD ≅ L)
    (hi : canonicalSectionHom B S hS X D hD ≫ i.hom = L.unitHomEquiv.symm s)
    (hj : canonicalSectionHom B S hS X D hD ≫ j.hom = L.unitHomEquiv.symm s) :
    i = j

AlgebraicGeometry.Space.canonicalSection_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CanonicalSectionRegular.lean, line 307. The attribute's comment: “part (1)”.

Stacks 0847, part (1). The canonical section 1_D of the invertible sheaf 𝒪_X(D) attached to an effective Cartier divisor D ⊆ X is a regular section: multiplication by it is a monomorphism 𝒪_X ⟶ 𝒪_X(D). Tensoring by the invertible sheaf 𝓘_D reflects monomorphisms, and it turns multiplication by 1_D into the inclusion 𝓘_D ⟶ 𝒪_X.

theorem canonicalSection_isRegular :
    IsRegularSection (structureCommRings B S hS X) (structureRingSheaf B S hS X).property
      (canonicalSection B S hS X D hD)

AlgebraicGeometry.Space.exists_isEffectiveCartierDivisor_associatedInvertibleSheaf_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularSectionEffectiveCartier.lean, line 81. The attribute's comment: “part (2), existence: a regular global section of an invertible module cuts out an effective Cartier divisor whose associated invertible sheaf it is”.

Stacks 0847, part (2), existence. Let X be an algebraic space over a scheme S and let L be an invertible 𝒪_X-module with a regular global section s. Then there is an effective Cartier divisor D ⊆ X and an isomorphism 𝒪_X(D) ≅ L.

Contraction with s is a monomorphism L^{⊗ -1} ⟶ 𝒪_X whose image is a quasi-coherent sheaf of ideals isomorphic to L^{⊗ -1}; by Stacks 03MB that sheaf of ideals is the defining ideal sheaf 𝓘_D of a closed subspace D, which is therefore an effective Cartier divisor, and 𝒪_X(D) ≅ L because both are inverse to 𝓘_D.

theorem exists_isEffectiveCartierDivisor_associatedInvertibleSheaf_iso
    (L : SheafOfModules.{u} (structureRingSheaf B S hS X))
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible (structureCommRings B S hS X)
      (structureRingSheaf B S hS X).property L)
    (s : L.sections)
    (hs : AlgebraicGeometry.IsRegularSection (structureCommRings B S hS X)
      (structureRingSheaf B S hS X).property s) :
    ∃ (D : ClosedSubspaces B S hS X.1) (hD : IsEffectiveCartierDivisor B S hS X D),
      Nonempty (associatedInvertibleSheaf B S hS X D hD ≅ L)

AlgebraicGeometry.Space.exists_unique_isEffectiveCartierDivisor_iso_canonicalSectionHom_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularSectionEffectiveCartierUnique.lean, line 166. The attribute's comment: “part (2): a regular global section of an invertible module cuts out a unique effective Cartier divisor, the zero scheme of the section, carrying a unique isomorphism from its associated invertible sheaf to the module which takes the canonical section to the given section; with no assumed inputs”.

Stacks 0847, part (2). Let X be an algebraic space over a scheme S and let L be an invertible 𝒪_X-module with a regular global section s. Then there is a unique effective Cartier divisor D ⊆ X, namely the zero scheme Z(s) of Stacks 0845, carrying a unique isomorphism 𝒪_X(D) ≅ L which takes the canonical section 1_D of 𝒪_X(D) to s.

Contraction with s is a monomorphism L^{⊗ -1} ⟶ 𝒪_X whose image is a quasi-coherent sheaf of ideals isomorphic to L^{⊗ -1}; by Stacks 03MB that sheaf of ideals is the defining ideal sheaf 𝓘_D of a closed subspace D, which is therefore an effective Cartier divisor. The identification of 𝓘_D with L^{⊗ -1} carries the inclusion 𝓘_D ⟶ 𝒪_X to contraction with s, so the pairing L ⊗ 𝓘_D ≅ 𝒪_X it induces curries s to that inclusion, exactly as the evaluation pairing 𝒪_X(D) ⊗ 𝓘_D ≅ 𝒪_X curries 1_D; the isomorphism matching the two pairings therefore carries 1_D to s. Uniqueness of the divisor is AlgebraicGeometry.Space.eq_zeroScheme_of_canonicalSectionHom_comp, which also identifies it as Z(s), and uniqueness of the isomorphism is AlgebraicGeometry.Space.iso_eq_of_canonicalSectionHom_comp_eq.

theorem exists_unique_isEffectiveCartierDivisor_iso_canonicalSectionHom_comp
    (L : SheafOfModules.{u} (structureRingSheaf B S hS X))
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible (structureCommRings B S hS X)
      (structureRingSheaf B S hS X).property L)
    (s : L.sections)
    (hs : AlgebraicGeometry.IsRegularSection (structureCommRings B S hS X)
      (structureRingSheaf B S hS X).property s) :
    ∃ (D : ClosedSubspaces B S hS X.1) (hD : IsEffectiveCartierDivisor B S hS X D)
      (i : associatedInvertibleSheaf B S hS X D hD ≅ L),
      D = zeroScheme B S hS X L s ∧
      canonicalSectionHom B S hS X D hD ≫ i.hom = L.unitHomEquiv.symm s ∧
      (∀ (D' : ClosedSubspaces B S hS X.1) (hD' : IsEffectiveCartierDivisor B S hS X D')
          (i' : associatedInvertibleSheaf B S hS X D' hD' ≅ L),
        canonicalSectionHom B S hS X D' hD' ≫ i'.hom = L.unitHomEquiv.symm s → D' = D) ∧
      ∀ i' : associatedInvertibleSheaf B S hS X D hD ≅ L,
        canonicalSectionHom B S hS X D hD ≫ i'.hom = L.unitHomEquiv.symm s → i' = i

AlgebraicGeometry.Space.effectiveCartierDivisor_regularSectionPair_mutuallyInverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularSectionEffectiveCartierUnique.lean, line 221. The attribute's comment: “part (3): the constructions D ↦ (𝒪_X(D), 1_D) and (L, s) ↦ Z(s) are mutually inverse, hence a bijection between the effective Cartier divisors and the pairs of an invertible module with a regular global section taken up to isomorphism; with no assumed inputs”.

Stacks 0847, part (3). The constructions D ↦ (𝒪_X(D), 1_D) and (L, s) ↦ Z(s) are mutually inverse, so they are a bijection between the effective Cartier divisors on X and the pairs consisting of an invertible 𝒪_X-module and a regular global section of it, taken up to isomorphism of pairs.

The first conjunct is that D ↦ (𝒪_X(D), 1_D) lands in such pairs — 𝒪_X(D) is invertible by Stacks 0841 and 1_D is regular by part (1) — and that the round trip D ↦ (𝒪_X(D), 1_D) ↦ Z(1_D) is the identity, which is AlgebraicGeometry.Space.zeroScheme_canonicalSection_eq. The second is that (L, s) ↦ Z(s) lands in the effective Cartier divisors and that the round trip (L, s) ↦ Z(s) ↦ (𝒪_X(Z(s)), 1_{Z(s)}) returns (L, s) itself: there is an isomorphism 𝒪_X(Z(s)) ≅ L carrying the canonical section to s, which is part (2). The third is that (L, s) ↦ Z(s) is constant on isomorphism classes of pairs, AlgebraicGeometry.Space.zeroScheme_eq_of_iso, which is what makes it a map out of them.

theorem effectiveCartierDivisor_regularSectionPair_mutuallyInverse :
    (∀ (D : ClosedSubspaces B S hS X.1) (hD : IsEffectiveCartierDivisor B S hS X D),
        AlgebraicGeometry.SheafOfModules.IsInvertible (structureCommRings B S hS X)
            (structureRingSheaf B S hS X).property (associatedInvertibleSheaf B S hS X D hD) ∧
          AlgebraicGeometry.IsRegularSection (structureCommRings B S hS X)
            (structureRingSheaf B S hS X).property (canonicalSection B S hS X D hD) ∧
          zeroScheme B S hS X (associatedInvertibleSheaf B S hS X D hD)
            (canonicalSection B S hS X D hD) = D) ∧
      (∀ (L : SheafOfModules.{u} (structureRingSheaf B S hS X)),
        AlgebraicGeometry.SheafOfModules.IsInvertible (structureCommRings B S hS X)
          (structureRingSheaf B S hS X).property L → ∀ (s : L.sections),
        AlgebraicGeometry.IsRegularSection (structureCommRings B S hS X)
          (structureRingSheaf B S hS X).property s →
        ∃ (hZ : IsEffectiveCartierDivisor B S hS X (zeroScheme B S hS X L s))
          (i : associatedInvertibleSheaf B S hS X (zeroScheme B S hS X L s) hZ ≅ L),
          canonicalSectionHom B S hS X (zeroScheme B S hS X L s) hZ ≫ i.hom =
            L.unitHomEquiv.symm s) ∧
      ∀ (L L' : SheafOfModules.{u} (structureRingSheaf B S hS X)) (s : L.sections)
        (s' : L'.sections) (i : L ≅ L'), SheafOfModules.sectionsMap i.hom s = s' →
        zeroScheme B S hS X L s = zeroScheme B S hS X L' s'

AlgebraicGeometry.Space.zeroScheme_canonicalSection_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZeroSchemeOfCanonicalSection.lean, line 335. The attribute's comment: “part (2): the construction D ↦ (𝒪_X(D), 1_D) followed by (L, s) ↦ Z(s) is the identity on effective Cartier divisors, with no assumed inputs”.

Stacks 0847 (2): an effective Cartier divisor is the zero scheme of its canonical section. This is the assertion of the source that the construction D ↦ (𝒪_X(D), 1_D) followed by (L, s) ↦ Z(s) is the identity on effective Cartier divisors.

The evaluation ideal of (𝒪_X(D), 1_D) of Stacks 0845 is the defining ideal of D on every affine étale chart, and a closed subspace whose defining ideal is the evaluation ideal on every affine chart is the zero scheme, by AlgebraicGeometry.Space.zeroSchemeSubfunctor_eq.

theorem zeroScheme_canonicalSection_eq :
    zeroScheme B S hS X (associatedInvertibleSheaf B S hS X D hD)
        (canonicalSection B S hS X D hD) = D

AlgebraicGeometry.Space.eq_zeroScheme_of_canonicalSectionHom_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZeroSchemeOfCanonicalSection.lean, line 396. The attribute's comment: “part (2): uniqueness of the divisor — an effective Cartier divisor with an isomorphism from its associated invertible sheaf to L carrying the canonical section to s is the zero scheme of s, with no assumed inputs”.

Stacks 0847 (2): the effective Cartier divisor is unique. Let L be an 𝒪_X-module with a global section s. An effective Cartier divisor D ⊆ X carrying an isomorphism 𝒪_X(D) ≅ L which sends the canonical section 1_D to s is the zero scheme Z(s) of Stacks 0845 — so there is at most one such divisor.

The isomorphism matches the evaluation ideals of the two pairs, so the defining ideal of D is the evaluation ideal of (L, s) on every affine étale chart, which by AlgebraicGeometry.Space.zeroSchemeSubfunctor_eq makes D the zero scheme.

theorem eq_zeroScheme_of_canonicalSectionHom_comp
    (L : Modules.{u, u} B S hS X.1 X.2) (s : L.sections)
    (i : associatedInvertibleSheaf B S hS X D hD ≅ L)
    (hi : canonicalSectionHom B S hS X D hD ≫ i.hom = L.unitHomEquiv.symm s) :
    D = zeroScheme B S hS X L s

Sources

• Section 71.7, Tag 0CPG
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.associatedInvertibleSheaf · AlgebraicGeometry.Space.associatedInvertibleSheaf_isInvertible · AlgebraicGeometry.Space.idealSheafHom · AlgebraicGeometry.Space.associatedInvertibleSheafHomEquiv · AlgebraicGeometry.Space.associatedInvertibleSheafHomEquiv_apply · AlgebraicGeometry.Space.canonicalSection · AlgebraicGeometry.Space.canonicalSection_apply · AlgebraicGeometry.Space.negativeDivisorSheaf

Section71.8 Effective Cartier divisors on Noetherian spaces#

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

Tag 0B4G, a lemma

Tag 0B4G in the Stacks Project.

AlgebraicGeometry.Space.isEffectiveCartierDivisor_hasPropertySk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisorSerreCondition.lean, line 228.

Stacks 0B4G. Let X be a locally Noetherian algebraic space over a scheme S satisfying Serre's condition (S_k), and let D ⊆ X be an effective Cartier divisor. Then D satisfies (S_{k-1}).

Both hypothesis and conclusion are Stacks 03E6 taken at the property of schemes "locally Noetherian and (S_k)", which is item (3) of Remark 03E7. By Stacks 083C the divisor is cut out on a surjective étale chart U of X by an effective Cartier ideal sheaf; U inherits (S_k) from X by Stacks 03E8, and the closed subscheme it cuts out satisfies (S_{k-1}) by the scheme case AlgebraicGeometry.isEffectiveCartierDivisor_hasPropertySk (Stacks 0B3R). That closed subscheme is a surjective étale chart of D.

The index k - 1 is truncated subtraction of natural numbers; at k = 0 the conclusion is the vacuous condition (S_0) and is supplied by AlgebraicGeometry.hasPropertySk_zero, so no hypothesis 1 ≤ k is required.

theorem isEffectiveCartierDivisor_hasPropertySk
    (X : AlgebraicSpaces B S hS) (D : ClosedSubspaces B S hS X.1)
    (hD : IsEffectiveCartierDivisor B S hS X D) (k : ℕ)
    (hX : HasEtaleLocalProperty B S hS X.1
      (fun T : Scheme.{u} => ∃ h : IsLocallyNoetherian T, @HasPropertySk T h k)) :
    HasEtaleLocalProperty B S hS D.1.toFunctor
      (fun T : Scheme.{u} => ∃ h : IsLocallyNoetherian T, @HasPropertySk T h (k - 1))

Tag 0B4H, a lemma

Tag 0B4H in the Stacks Project.

AlgebraicGeometry.Space.isNormal_effectiveCartierDivisor_hasPropertySk_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisorSerreCondition.lean, line 260.

Stacks 0B4H. Let X be a locally Noetherian normal algebraic space over a scheme S and let D ⊆ X be an effective Cartier divisor. Then D satisfies Serre's condition (S_1).

Normality and local Noetherianity of X are each Stacks 03E6 taken at the corresponding property of schemes, items (7) and (1) of Remark 03E7. By Stacks 083C the divisor is cut out on a surjective étale chart U of X by an effective Cartier ideal sheaf; U is locally Noetherian and normal by Stacks 03E8, and the closed subscheme it cuts out satisfies (S_1) by the scheme case AlgebraicGeometry.isNormal_effectiveCartierDivisor_hasPropertySk_one (Stacks 0B3S), which is where Serre's criterion is used. That closed subscheme is a surjective étale chart of D.

theorem isNormal_effectiveCartierDivisor_hasPropertySk_one
    (X : AlgebraicSpaces B S hS)
    (hXnoeth : HasEtaleLocalProperty B S hS X.1 (fun T : Scheme.{u} => IsLocallyNoetherian T))
    (hXnormal : IsNormal B S hS X.1) (D : ClosedSubspaces B S hS X.1)
    (hD : IsEffectiveCartierDivisor B S hS X D) :
    HasEtaleLocalProperty B S hS D.1.toFunctor
      (fun T : Scheme.{u} => ∃ h : IsLocallyNoetherian T, @HasPropertySk T h 1)

Tag 0DML, a lemma

Tag 0DML in the Stacks Project.

AlgebraicGeometry.Space.exists_isEffectiveCartierDivisor_compl_denseAffineOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDenseAffineOpen.lean, line 364.

Stacks Project, Tag 0DML. Let S be a scheme and let X be a regular Noetherian separated algebraic space over S. Let U ⊆ X be a dense affine open subspace, presented by an open immersion u : h_W ⟶ X whose source has affine underlying scheme and whose set of points is dense. Then there is an effective Cartier divisor D ⊆ X with U = X ∖ D: namely the reduced induced closed subspace on the closed set |X| ∖ |U|.

The hypothesis hBCW is Stacks 0BCW in the form its own proof gives, for the reduced induced closed subscheme on the complement of a dense affine open of a scheme, and h083C is the implication (2) ⟹ (1) of Stacks 083C; both are inputs this library does not have, and the conclusion of the chart-level statement AlgebraicGeometry.Space.exists_hasEffectiveCartierEtaleCover_reducedClosedSubspace_compl needs only the first of them.

theorem exists_isEffectiveCartierDivisor_compl_denseAffineOpen
    (X : AlgebraicSpaces B S hS)
    (hsep : IsAbsolutelySeparated B S hS hZ X.1)
    (hnoeth : IsNoetherian B S hS hZ X.1)
    (hreg : HasEtaleLocalProperty B S hS X.1
      (fun T : Scheme.{u} => _root_.AlgebraicGeometry.IsRegular T))
    (W : BigFppfOver B S hS) (hWaff : IsAffine ((BigFppfOver.toScheme B S hS).obj W))
    (u : yoneda.obj W ⟶ X.1) (hu : IsOpenImmersion B S hS u)
    (hudense : Dense (Set.range (pointsMap B S hS (yoneda.obj W) u)))
    (hBCW : ∀ Y : Scheme.{u}, _root_.AlgebraicGeometry.IsNoetherian Y → Scheme.IsSeparated Y →
      ∀ O : Y.Opens, IsAffineOpen O → Dense (O : Set Y) →
        (∀ y : Y, y ∉ O → UniqueFactorizationMonoid (Y.presheaf.stalk y)) →
          Stacks.Divisors.IsEffectiveCartierDivisor
            (Scheme.IdealSheafData.vanishingIdeal ⟨(O : Set Y)ᶜ, O.2.isClosed_compl⟩))
    (h083C : ∀ D : ClosedSubspaces B S hS X.1,
      HasEffectiveCartierEtaleCover B S hS X D → IsEffectiveCartierDivisor B S hS X D) :
    ∃ D : ClosedSubspaces B S hS X.1,
      IsEffectiveCartierDivisor B S hS X D ∧
        Set.range (pointsMap B S hS D.1.toFunctor D.1.ι) =
          (Set.range (pointsMap B S hS (yoneda.obj W) u))ᶜ

AlgebraicGeometry.Space.exists_isEffectiveCartierDivisor_compl_denseAffineOpen', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDenseAffineOpen.lean, line 400.

Stacks Project, Tag 0DML. Let S be a scheme and let X be a regular Noetherian separated algebraic space over S. Let U ⊆ X be a dense affine open subspace, presented by an open immersion u : h_W ⟶ X whose source has affine underlying scheme and whose set of points is dense. Then there is an effective Cartier divisor D ⊆ X with U = X ∖ D.

This is AlgebraicGeometry.Space.exists_isEffectiveCartierDivisor_compl_denseAffineOpen with both of its inputs supplied: the reduced induced form of Stacks 0BCW on a scheme by AlgebraicGeometry.isEffectiveCartierDivisor_vanishingIdeal_compl_denseAffineOpen, and the implication (2) ⟹ (1) of Stacks 083C by AlgebraicGeometry.Space.isEffectiveCartierDivisor_of_hasEffectiveCartierEtaleCover.

theorem exists_isEffectiveCartierDivisor_compl_denseAffineOpen'
    (X : AlgebraicSpaces B S hS)
    (hsep : IsAbsolutelySeparated B S hS hZ X.1)
    (hnoeth : IsNoetherian B S hS hZ X.1)
    (hreg : HasEtaleLocalProperty B S hS X.1
      (fun T : Scheme.{u} => _root_.AlgebraicGeometry.IsRegular T))
    (W : BigFppfOver B S hS) (hWaff : IsAffine ((BigFppfOver.toScheme B S hS).obj W))
    (u : yoneda.obj W ⟶ X.1) (hu : IsOpenImmersion B S hS u)
    (hudense : Dense (Set.range (pointsMap B S hS (yoneda.obj W) u))) :
    ∃ D : ClosedSubspaces B S hS X.1,
      IsEffectiveCartierDivisor B S hS X D ∧
        Set.range (pointsMap B S hS D.1.toFunctor D.1.ι) =
          (Set.range (pointsMap B S hS (yoneda.obj W) u))ᶜ

Tag 0DMM, a lemma

Tag 0DMM in the Stacks Project.

AlgebraicGeometry.Space.exists_isEffectiveCartierDivisor_iso_differenceDivisorSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/InvertibleDivisorDifference.lean, line 408.

Stacks Project, Tag 0DMM. Let S be a scheme and let X be a regular Noetherian separated algebraic space over S. Then every invertible 𝒪_X-module L is isomorphic to 𝒪_X(D - D') = 𝒪_X(D) ⊗_{𝒪_X} 𝒪_X(D')^{⊗ -1} for effective Cartier divisors D, D' ⊆ X.

Following the source: choose a dense affine open subspace U ⊆ X on which L is trivial (AlgebraicGeometry.Space.exists_denseAffineOpenChart_bijective_smul); its complement is an effective Cartier divisor D₀ by Stacks 0DML; the trivialization 𝒪_U ≅ L|_U extends to a monomorphism 𝓘_{D₀}^{n} ⟶ L for some n > 0 by Stacks 07UM (AlgebraicGeometry.Space.exists_mono_idealPowModule_of_iso), and 𝓘_{D₀}^{n} is the ideal sheaf of the effective Cartier divisor n D₀ (Stacks 083U, 083V). Twisting by 𝒪_X(n D₀) gives a regular global section of L ⊗ 𝒪_X(n D₀), which is 𝒪_X(D) for an effective Cartier divisor D by Stacks 0847, part (2); so L ≅ 𝒪_X(D - n D₀).

theorem exists_isEffectiveCartierDivisor_iso_differenceDivisorSheaf
    (X : AlgebraicSpaces B S hS)
    (separated : IsAbsolutelySeparated B S hS hZ X.1)
    (noetherian : IsNoetherian B S hS hZ X.1)
    (regular : HasEtaleLocalProperty B S hS X.1
      (fun T : Scheme.{u} => _root_.AlgebraicGeometry.IsRegular T))
    (L : SheafOfModules.{u} (structureRingSheaf B S hS X))
    (invertible : AlgebraicGeometry.SheafOfModules.IsInvertible (structureCommRings B S hS X)
      (structureRingSheaf B S hS X).property L) :
    ∃ (D D' : ClosedSubspaces B S hS X.1) (cD : IsEffectiveCartierDivisor B S hS X D)
      (cD' : IsEffectiveCartierDivisor B S hS X D'),
      Nonempty (L ≅ differenceDivisorSheaf B S hS X D D' cD cD')

Tag 0DMC, a lemma

Tag 0DMC in the Stacks Project.

AlgebraicGeometry.Space.exists_isEffectiveCartierDivisor_genericFibre_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierGenericFibreExtension.lean, line 960.

Let R be a valuation ring with fraction field K, and let X be an algebraic space over R whose structure morphism X → Spec R is smooth. For every effective Cartier divisor D ⊆ X_K there is an effective Cartier divisor D' ⊆ X with D'_K = D.

Here X_K is the base change of X along Spec K → Spec R, that is the restriction of X along CategoryTheory.OverShriek.relocalizeRestrict, and D'_K is the base change of the closed subspace D', CategoryTheory.OverShriek.relocalizeRestrictSubfunctor, a closed subspace of X_K. The divisor D' is the scheme-theoretic image of D → X_K → X.

theorem _root_.AlgebraicGeometry.Space.exists_isEffectiveCartierDivisor_genericFibre_eq
    {R : Type u} [CommRing R] [IsDomain R] [ValuationRing R]
    {K : Type u} [Field K] [Algebra R K] [IsFractionRing R K]
    (B : BigFppfSite.{u}) (hR : B.Contains (Spec (.of R))) (hK : B.Contains (Spec (.of K)))
    (X : AlgebraicSpaces B (Spec (.of R)) hR)
    (hX : Space.IsSmooth B (Spec (.of R)) hR (Space.toBaseSiteMap B (Spec (.of R)) hR X.1))
    (D : Space.ClosedSubspaces B (Spec (.of K)) hK
      ((OverShriek.relocalizeRestrict (Space.specAlgebraMapHom B R K hR hK)).obj X.1))
    (hD : Space.IsEffectiveCartierDivisor B (Spec (.of K)) hK
      ⟨(OverShriek.relocalizeRestrict (Space.specAlgebraMapHom B R K hR hK)).obj X.1,
        isAlgebraicSpace_relocalizeRestrict B (Spec (.of K)) (Spec (.of R)) hK hR
          (Space.specAlgebraMapHom B R K hR hK) X.1 X.2⟩ D) :
    ∃ D' : Space.ClosedSubspaces B (Spec (.of R)) hR X.1,
      Space.IsEffectiveCartierDivisor B (Spec (.of R)) hR X D' ∧
        OverShriek.relocalizeRestrictSubfunctor (Space.specAlgebraMapHom B R K hR hK) D'.1 =
          D.1

Sources

• Section 71.8, Tag 0CPH
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.isEffectiveCartierDivisor_hasPropertySk · AlgebraicGeometry.Space.isNormal_effectiveCartierDivisor_hasPropertySk_one · AlgebraicGeometry.Space.exists_isEffectiveCartierDivisor_compl_denseAffineOpen · AlgebraicGeometry.Space.exists_isEffectiveCartierDivisor_compl_denseAffineOpen' · AlgebraicGeometry.Space.exists_isEffectiveCartierDivisor_iso_differenceDivisorSheaf · AlgebraicGeometry.Space.exists_isEffectiveCartierDivisor_genericFibre_eq

Section71.9 Relative effective Cartier divisors#

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

Tag 0EPN, a lemma

Tag 0EPN in the Stacks Project.

AlgebraicGeometry.Space.isPullbackDefined_of_isPullback_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierBaseChange.lean, line 177.

Let f : X ⟶ Y be a morphism of algebraic spaces and let D ⊆ X be an effective Cartier divisor whose structure morphism D ⟶ Y is flat. Then for every morphism g : Y' ⟶ Y and every fibre product square exhibiting X' as Y' ×_Y X, the pullback of D along the projection g' : X' ⟶ X is defined: the inverse image of D on X' is again an effective Cartier divisor.

Stacks 0EPN asks g to be a morphism of schemes and X' to be the chosen fibre product; it is stated here for an arbitrary morphism of algebraic spaces and an arbitrary cartesian square.

theorem isPullbackDefined_of_isPullback_of_isFlat {X Y Y' X' : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (g : Y' ⟶ Y) {f' : X' ⟶ Y'} {g' : X' ⟶ X} (hsq : IsPullback f' g' g f)
    (D : ClosedSubspaces B S hS X.1) (hD : IsEffectiveCartierDivisor B S hS X D)
    (hflat : IsFlat B S hS (D.1.ι ≫ f.hom)) :
    IsPullbackDefined B S hS g' D

Tag 0EPP, a definition

Tag 0EPP in the Stacks Project.

AlgebraicGeometry.Space.IsRelativeEffectiveCartierDivisor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierDivisor.lean, line 146.

A closed subspace D ⊆ X is a relative effective Cartier divisor on X over Y, for a morphism f : X ⟶ Y of algebraic spaces, when D is an effective Cartier divisor on X and the structure morphism D ⟶ Y is flat.

noncomputable abbrev IsRelativeEffectiveCartierDivisor {X Y : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (D : ClosedSubspaces B S hS X.1) : Prop

Sources

• Section 71.9, Tag 0EPM
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.isPullbackDefined_of_isPullback_of_isFlat · AlgebraicGeometry.Space.IsRelativeEffectiveCartierDivisor

Section71.10 Meromorphic functions and sections#

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

Tag 0EN3, a definition

Tag 0EN3 in the Stacks Project.

AlgebraicGeometry.Space.meromorphicFunctionSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicFunctions.lean, line 214. The attribute's comment: “the sheaf of meromorphic functions”.

Stacks 0EN3. The sheaf of meromorphic functions 𝒦_F on the algebraic space F: the sheaf on the small étale site of F associated to the presheaf of sectionwise localizations U ↦ 𝒮_F(U)⁻¹ 𝒪_F(U).

noncomputable def meromorphicFunctionSheaf (hF : IsAlgebraicSpace B S hS F) :
    Sheaf (SmallEtale.topology B S hS F) CommRingCat.{u}

AlgebraicGeometry.Space.MeromorphicFunction, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicFunctions.lean, line 227. The attribute's comment: “meromorphic functions”.

Stacks 0EN3. A meromorphic function on the algebraic space F is a global section of its sheaf of meromorphic functions 𝒦_F.

abbrev MeromorphicFunction (hF : IsAlgebraicSpace B S hS F)

Tag 0EN4, a lemma

Tag 0EN4 in the Stacks Project.

AlgebraicGeometry.Space.isRegularSection_iff_mem_nonZeroDivisors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicFunctions.lean, line 336.

Stacks 0EN4. Over an affine étale chart U of the algebraic space F the regular sections of 𝒪_F are exactly the nonzerodivisors of the ring of sections 𝒪_F(U).

theorem isRegularSection_iff_mem_nonZeroDivisors (U : SmallEtale B S hS F)
    (hU : IsAffine (smallEtaleScheme B S hS F U))
    (s : (structurePresheaf B S hS F).obj (op U)) :
    IsRegularSection B S hS F U s ↔ s ∈ ((structurePresheaf B S hS F).obj (op U))⁰

Tag 0EN5, a definition

Tag 0EN5 in the Stacks Project.

AlgebraicGeometry.Space.meromorphicSectionSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicSections.lean, line 148. The attribute's comment: “part (1)”.

The sheaf 𝒦_F(M) of meromorphic sections of a sheaf of 𝒪_F-modules M: the extension of scalars of M along 𝒪_F ⟶ 𝒦_F, sheafified.

noncomputable abbrev meromorphicSectionSheaf (hF : IsAlgebraicSpace B S hS F)
    (M : Modules.{u, max u z} B S hS F hF) :
    SheafOfModules.{max (u + 1) z}
      (Stacks.SheafOfModules.Tensor.ringSheaf (meromorphicRingedSite B S hS F hF).O)

AlgebraicGeometry.Space.MeromorphicSection, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicSections.lean, line 161. The attribute's comment: “part (2)”.

A meromorphic section of a sheaf of 𝒪_F-modules M is a global section of the sheaf 𝒦_F(M) of meromorphic sections of M.

noncomputable abbrev MeromorphicSection (hF : IsAlgebraicSpace B S hS F)
    (M : Modules.{u, max u z} B S hS F hF) : Type _

Tag 0EN6, a lemma

Tag 0EN6 in the Stacks Project.

AlgebraicGeometry.Space.isFractionRing_meromorphicFunctionSheaf_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicQuasicoherent.lean, line 343. The attribute's comment: “part (2): over an affine object of the small étale site the ring of meromorphic functions is the total ring of fractions of the ring of sections”.

For an affine object U of the small étale site of an algebraic space X satisfying hypotheses (a) and (b), the ring 𝒦_X(U) of meromorphic functions over U is the total ring of fractions of 𝒪_X(U).

theorem isFractionRing_meromorphicFunctionSheaf_obj
    (hwa : ∀ z ∈ weaklyAssociatedPointsOfSpace B S hS X, localRingDimension B S hS z = 0)
    (hfin : HasLocallyFiniteIrreducibleComponents B S hS X.1)
    (U : SmallEtale B S hS X.1) (hU : IsAffine (smallEtaleScheme B S hS X.1 U)) :
    letI : Algebra ((structurePresheaf B S hS X.1).obj (op U))
        ((meromorphicFunctionSheaf B S hS X.1 X.2).obj.obj (op U)) :=
      ((toMeromorphicFunctionSheaf B S hS X.1 X.2).hom.app (op U)).hom.toAlgebra
    IsFractionRing ((structurePresheaf B S hS X.1).obj (op U))
      ((meromorphicFunctionSheaf B S hS X.1 X.2).obj.obj (op U))

AlgebraicGeometry.Space.isQuasicoherent_meromorphicAlgebraSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicQuasicoherent.lean, line 389. The attribute's comment: “part (1): the sheaf of meromorphic functions is a quasi-coherent sheaf of algebras”.

For an algebraic space X satisfying hypotheses (a) and (b), the sheaf of meromorphic functions 𝒦_X is a quasi-coherent sheaf of 𝒪_X-algebras.

theorem isQuasicoherent_meromorphicAlgebraSheaf
    (hwa : ∀ z ∈ weaklyAssociatedPointsOfSpace B S hS X, localRingDimension B S hS z = 0)
    (hfin : HasLocallyFiniteIrreducibleComponents B S hS X.1) :
    (meromorphicAlgebraSheaf B S hS X).IsQuasicoherent

AlgebraicGeometry.Space.regularSectionsStalk_eq_nonZeroDivisors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicStalks.lean, line 408. The attribute's comment: “part (3): for a geometric point the germs of regular sections are exactly the nonzerodivisors of the étale local ring”.

Stacks 0EN6, part (3). Let X be an algebraic space over a scheme S such that every weakly associated point of X is a point of codimension 0 and every quasi-compact open of every étale scheme chart of X has finitely many irreducible components (the condition of Stacks 0BB1). Then for every geometric point x̄ of X the set 𝒮_x̄ of germs of regular sections is exactly the set of nonzerodivisors of the étale local ring 𝒪_{X, x̄}.

theorem regularSectionsStalk_eq_nonZeroDivisors (X : AlgebraicSpaces B S hS)
    (hwa : ∀ z ∈ weaklyAssociatedPointsOfSpace B S hS X, localRingDimension B S hS z = 0)
    (hfin : HasLocallyFiniteIrreducibleComponents B S hS X.1)
    (x : GeometricPoint B S hS X.1) :
    regularSectionsStalk x = (etaleLocalRing B S hS X.1 x)⁰

AlgebraicGeometry.Space.isFractionRing_meromorphicStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicStalks.lean, line 608. The attribute's comment: “part (4): for a geometric point the stalk of the sheaf of meromorphic functions is the total ring of fractions of the étale local ring”.

Stacks 0EN6, part (4). Let X be an algebraic space over a scheme S such that every weakly associated point of X is a point of codimension 0 and every quasi-compact open of every étale scheme chart of X has finitely many irreducible components (the condition of Stacks 0BB1). Then for every geometric point x̄ of X the stalk 𝒦_{X, x̄} of the sheaf of meromorphic functions is the total ring of fractions of the étale local ring 𝒪_{X, x̄}.

The stalk of 𝒦_X is the stalk of the presheaf of sectionwise localizations, which is the localization of 𝒪_{X, x̄} at 𝒮_x̄; by part (3) that multiplicative subset is exactly the set of nonzerodivisors of 𝒪_{X, x̄}.

theorem isFractionRing_meromorphicStalk
    (hwa : ∀ z ∈ weaklyAssociatedPointsOfSpace B S hS X, localRingDimension B S hS z = 0)
    (hfin : HasLocallyFiniteIrreducibleComponents B S hS X.1) :
    letI : Algebra (etaleLocalRing B S hS X.1 x) (meromorphicStalk B S hS X x) :=
      (toMeromorphicStalk B S hS X x).toAlgebra
    IsFractionRing (etaleLocalRing B S hS X.1 x) (meromorphicStalk B S hS X x)

Tag 0EN7, a lemma

Tag 0EN7 in the Stacks Project.

AlgebraicGeometry.Space.nonempty_meromorphicFunctionSheaf_iso_representedMeromorphicAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicRepresentableComparison.lean, line 373.

Stacks 0EN7. Let X be an algebraic space over S all of whose weakly associated points are points of codimension 0 and which satisfies the condition of Stacks 0BB1, and let X be representable by a scheme X₀. Then the sheaf of meromorphic functions 𝒦_X is, as a sheaf of 𝒪_X-algebras, the algebra on the small étale site of X associated to the quasi-coherent algebra 𝒦_{X₀} of meromorphic functions on X₀.

public theorem nonempty_meromorphicFunctionSheaf_iso_representedMeromorphicAlgebra
    (codimZero : ∀ z ∈ weaklyAssociatedPointsOfSpace B S hS X, localRingDimension B S hS z = 0)
    (finiteComponents : HasLocallyFiniteIrreducibleComponents B S hS X.1)
    (i : X.1 ≅ yoneda.obj T) :
    Nonempty (Under.mk (toMeromorphicFunctionSheaf B S hS X.1 X.2).hom ≅
      representedMeromorphicAlgebra B S hS X T codimZero finiteComponents i)

Tag 0EN8, a definition

Tag 0EN8 in the Stacks Project.

AlgebraicGeometry.Space.PullbacksMeromorphicSections, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicPullback.lean, line 145.

Stacks 0EN8. Pullbacks of meromorphic functions are defined for f : X ⟶ Y when, for every commuting square of an étale chart U of X over an étale chart V of Y, the pullback f^♯ along the underlying morphism of schemes carries every regular section of 𝒪_Y over V to a regular section of 𝒪_X over U.

abbrev PullbacksMeromorphicSections {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y) : Prop

Tag 0EN9, a lemma

Tag 0EN9 in the Stacks Project.

AlgebraicGeometry.Space.pullbacksMeromorphicSections_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicPullback.lean, line 156. The attribute's comment: “part (2): flat”. References: EGA IV (20.3.13), “flat: pullback defined”.

Stacks 0EN9, part (2). Pullbacks of meromorphic functions are defined along a flat morphism f : X ⟶ Y: the morphism of schemes underlying a commuting square of étale charts of f is flat, and pullbacks of meromorphic functions are defined along a flat morphism of schemes.

theorem pullbacksMeromorphicSections_of_flat {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hf : IsFlat B S hS f) : PullbacksMeromorphicSections B S hS f

AlgebraicGeometry.Space.pullbacksMeromorphicSections_of_mapsTo_codimensionZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicPullbackWeaklyAssociated.lean, line 70. The attribute's comment: “part (1): weakly associated points of X mapped to codimension-zero points of Y”.

Stacks 0EN9, part (1). Pullbacks of meromorphic functions are defined along a morphism f : X ⟶ Y of algebraic spaces carrying every weakly associated point of X to a point of codimension 0 of Y.

Over a commuting square of étale scheme charts the claim is the scheme-level criterion of Stacks 02OU: a weakly associated point of the chart of X lies over a weakly associated point of X, which is carried to a point of codimension 0 of Y, and such a point is a generic point of an irreducible component on the chart of Y above it.

theorem pullbacksMeromorphicSections_of_mapsTo_codimensionZero
    {X Y : AlgebraicSpaces B S hS} (f : X.1 ⟶ Y.1)
    (hf : ∀ x ∈ weaklyAssociatedPointsOfSpace B S hS X,
      localRingDimension B S hS (pointsMap B S hS X.1 f x) = 0) :
    PullbacksMeromorphicSections B S hS f

Tag 0ENA, a lemma

Tag 0ENA in the Stacks Project.

AlgebraicGeometry.Space.exists_codimensionZeroPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CodimensionZeroSchematicLocus.lean, line 361. The attribute's comment: “the assertion of the statement that the construction makes sense: the set of codimension-zero points is contained in the schematic locus, so that the local rings and the morphisms j_η are defined”.

Stacks 0ENA, the assertion that the construction makes sense. Let X be an algebraic space over a scheme S satisfying hypotheses (b) and (c) of Stacks 0ENA — the equivalent conditions of Stacks 0BB1, and representability of every codimension-zero point by a monomorphism from the spectrum of a field. Then X has a dense open subspace which is a scheme and whose point set contains the whole of X⁰.

Consequently the local rings 𝒪_{X, η} and the canonical morphisms j_η : Spec(𝒪_{X, η}) ⟶ X for η ∈ X⁰ are defined; they are AlgebraicGeometry.Space.CodimensionZeroPresentation.stalk and AlgebraicGeometry.Space.CodimensionZeroPresentation.fromSpecStalk.

theorem exists_codimensionZeroPresentation
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hfin : HasLocallyFiniteIrreducibleComponents B S hS X)
    (hmono : HasMonomorphicCodimensionZeroPoints B S hS X) :
    Nonempty (CodimensionZeroPresentation B S hS X)

AlgebraicGeometry.Space.codimensionZero_mem_schematicLocus_of_hasLocallyFiniteIrreducibleComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CodimensionZeroSchematicLocus.lean, line 387. The attribute's comment: “the assertion of the statement that the construction makes sense, read on the schematic locus of Tag 03JH”.

Stacks 0ENA, the assertion that the construction makes sense, stated with the schematic locus of Stacks 03JH: under hypotheses (b) and (c) of Stacks 0ENA every point of codimension 0 of X lies in the schematic locus.

The dense open subspace of AlgebraicGeometry.Space.exists_codimensionZeroPresentation is a representable open subspace, hence contained in the schematic locus.

theorem codimensionZero_mem_schematicLocus_of_hasLocallyFiniteIrreducibleComponents
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hfin : HasLocallyFiniteIrreducibleComponents B S hS X)
    (hmono : HasMonomorphicCodimensionZeroPoints B S hS X)
    (x : points B S hS X) (hx : localRingDimension B S hS x = 0) :
    x ∈ Set.range (pointsMap B S hS (schematicLocus B S hS X).toFunctor
      (schematicLocus B S hS X).ι)

AlgebraicGeometry.Space.CodimensionZeroPresentation.exists_codimensionZeroPresentation_isIso_genericPointComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicCodimensionZeroProduct.lean, line 373. The attribute's comment: “the first conclusion: the sheaf of meromorphic functions is the direct sum, and equally the product, over the codimension-zero points of the direct images of the local rings there, through the canonical comparisons”.

Stacks 0ENA, the first conclusion. Let X be an algebraic space over a scheme S such that

• (a) every weakly associated point of X is a point of codimension 0,
• (b) every quasi-compact open of every étale scheme chart of X has finitely many irreducible components, the condition of Stacks 0BB1, and
• (c) every point of codimension 0 of X is represented by a monomorphism from the spectrum of a field.

Then the local rings 𝒪_{X, η} at the points η ∈ X⁰ of codimension 0 and the canonical morphisms j_η : Spec(𝒪_{X, η}) ⟶ X are defined — this is the presentation P of the schematic locus whose existence is AlgebraicGeometry.Space.exists_codimensionZeroPresentation — and the sheaf of meromorphic functions 𝒦_X is both the direct sum and the product over X⁰ of the direct images j_{η, *}𝒪_{X, η}:

𝒦_X = ⨁_{η ∈ X⁰} j_{η, *}𝒪_{X, η} = ∏_{η ∈ X⁰} j_{η, *}𝒪_{X, η}.

The two identifications are the canonical comparisons: the one into the product has components the canonical maps 𝒦_X ⟶ j_{η, *}𝒪_{X, η} of AlgebraicGeometry.Space.CodimensionZeroPresentation.genericPointComparison, and the one out of the direct sum is CategoryTheory.Limits.sigmaPiComparison, the identity on the diagonal and zero off it.

theorem exists_codimensionZeroPresentation_isIso_genericPointComparison
    (hwa : ∀ z ∈ weaklyAssociatedPointsOfSpace B S hS X, localRingDimension B S hS z = 0)
    (hfin : HasLocallyFiniteIrreducibleComponents B S hS X.1)
    (hmono : HasMonomorphicCodimensionZeroPoints B S hS X.1) :
    ∃ P : CodimensionZeroPresentation B S hS X.1,
      IsIso P.genericPointModuleComparisonPi ∧
        letI : DecidableEq (CodimensionZeroPoints B S hS X.1) := Classical.decEq _
        letI := P.hasCoproduct_genericPointModule
        IsIso (sigmaPiComparison fun η : CodimensionZeroPoints B S hS X.1 =>
          P.genericPointModule η.2)

AlgebraicGeometry.Space.CodimensionZeroPresentation.exists_codimensionZeroPresentation_isIso_meromorphicSectionComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicCodimensionZeroSectionProduct.lean, line 380. The attribute's comment: “the second conclusion: for every quasi-coherent module the sheaf of its meromorphic sections is the direct sum, and equally the product, over the codimension-zero points of the direct images of its inverse images there, through the canonical comparisons”.

Stacks 0ENA, the second conclusion. Let X be an algebraic space over a scheme S such that

• (a) every weakly associated point of X is a point of codimension 0,
• (b) every quasi-compact open of every étale scheme chart of X has finitely many irreducible components, the condition of Stacks 0BB1, and
• (c) every point of codimension 0 of X is represented by a monomorphism from the spectrum of a field.

Then the local rings 𝒪_{X, η} at the points η ∈ X⁰ of codimension 0 and the canonical morphisms j_η : Spec(𝒪_{X, η}) ⟶ X are defined — this is the presentation P of the schematic locus whose existence is AlgebraicGeometry.Space.exists_codimensionZeroPresentation — and for every quasi-coherent 𝒪_X-module F the sheaf 𝒦_X(F) of meromorphic sections of F is both the direct sum and the product over X⁰ of the direct images j_{η, *}j_η^*F of the inverse images of F:

𝒦_X(F) = ⨁_{η ∈ X⁰} j_{η, *}j_η^*F = ∏_{η ∈ X⁰} j_{η, *}j_η^*F.

The two identifications are the canonical comparisons: the one into the product is AlgebraicGeometry.Space.CodimensionZeroPresentation.meromorphicSectionGenericPointComparisonPi, the transpose across sheafification of the family a ⊗ s ↦ a · s|_{U ×_X Spec(𝒪_{X, η})}, and the one out of the direct sum is CategoryTheory.Limits.sigmaPiComparison, the identity on the diagonal and zero off it.

theorem exists_codimensionZeroPresentation_isIso_meromorphicSectionComparison
    (hwa : ∀ z ∈ weaklyAssociatedPointsOfSpace B S hS X, localRingDimension B S hS z = 0)
    (hfin : HasLocallyFiniteIrreducibleComponents B S hS X.1)
    (hmono : HasMonomorphicCodimensionZeroPoints B S hS X.1) :
    ∃ P : CodimensionZeroPresentation B S hS X.1,
      ∀ F : Modules.{u, u} B S hS X.1 X.2, F.IsQuasicoherentOnSite →
        IsIso (P.meromorphicSectionGenericPointComparisonPi F) ∧
          letI : DecidableEq (CodimensionZeroPoints B S hS X.1) := Classical.decEq _
          letI := P.hasCoproduct_genericPointMeromorphicModule F
          IsIso (sigmaPiComparison fun η : CodimensionZeroPoints B S hS X.1 =>
            SheafOfModules.uliftObj.{_, _, _, _, u + 1}
              (P.genericPointMeromorphicModule η.2 F))

AlgebraicGeometry.Space.exists_ringEquiv_rationalFunctions_meromorphicFunction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SpaceRationalFunctionsMeromorphic.lean, line 475. The attribute's comment: “the third conclusion: the ring of rational functions of the space is its ring of meromorphic functions, R(X) = Γ(X, 𝒦_X), through the comparison that reads a rational function regular on a dense open subspace as a meromorphic function on every étale chart lying in that subspace”. References: EGA IV (20.1.13), “Algebraic clause only”.

Stacks 0ENA, the third conclusion. Let X be an algebraic space over a scheme S such that (a) every weakly associated point of X has codimension 0, (b) the irreducible components of X are locally finite, and (c) every codimension-zero point of X is representable by a monomorphism from the spectrum of a field. Then the ring R(X) of rational functions of X — the classes, modulo agreement on a dense open subspace, of morphisms to the relative affine line defined on a dense open subspace, of Stacks 0EMP — is the ring Γ(X, 𝒦_X) of meromorphic functions on X, the global sections of the sheaf of meromorphic functions of Stacks 0EN3.

The comparison is the canonical one: a rational function represented by a morphism ν regular on a dense open subspace W is sent to the meromorphic function whose value at an étale chart U lying in W is the image in 𝒦_X(U) of the coordinate of ν at U, and the displayed equation says exactly that. It is a ring homomorphism by AlgebraicGeometry.Space.rationalToMeromorphicRingHom, injective by AlgebraicGeometry.Space.injective_rationalToMeromorphic and surjective by AlgebraicGeometry.Space.surjective_rationalToMeromorphic.

theorem exists_ringEquiv_rationalFunctions_meromorphicFunction
    (hwa : ∀ z ∈ weaklyAssociatedPointsOfSpace B S hS X, localRingDimension B S hS z = 0)
    (hfin : HasLocallyFiniteIrreducibleComponents B S hS X.1)
    (hmono : HasMonomorphicCodimensionZeroPoints B S hS X.1) :
    ∃ e : rationalFunctions B S hS X.2 ≃+* MeromorphicFunction B S hS X.1 X.2,
      ∀ (f : PartialMap B S hS X.2 (affineLineFunctor B S hS))
        (U : SmallEtale B S hS X.1) (τ : yoneda.obj U.obj.left ⟶ f.domain.toFunctor),
        τ ≫ f.domain.ι = U.1.hom →
        (e (PartialMap.toRationalMap B S hS f)).val (op U) =
          ((toMeromorphicFunctionSheaf B S hS X.1 X.2).hom.app (op U)).hom
            (affineLineCoordinate B S hS (op U.obj.left)
              (f.hom.app (op U.obj.left) (yonedaEquiv τ)))

Tag 0ENB, a definition

Tag 0ENB in the Stacks Project.

AlgebraicGeometry.Space.IsRegularMeromorphicSection, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicSections.lean, line 168. References: EGA IV (20.1.8), “regular section defn”.

A meromorphic section s of a sheaf of 𝒪_F-modules L is regular when the induced map 𝒦_F ⟶ 𝒦_F(L), multiplication by s, is injective; this is tested on every étale chart of F.

noncomputable abbrev IsRegularMeromorphicSection (hF : IsAlgebraicSpace B S hS F)
    (L : Modules.{u, max u z} B S hS F hF)
    (s : MeromorphicSection.{u, z} B S hS F hF L) : Prop

Tag 0ENC, a lemma

Tag 0ENC in the Stacks Project.

AlgebraicGeometry.Space.isRegularMeromorphicSection_pullbackMeromorphicSectionOfGood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Chow/ProperPushforwardOfDivisorPullback.lean, line 149. The attribute's comment: “part (2) in the vocabulary of this chapter: the pullback f^*s of a regular meromorphic section of an invertible sheaf on a good algebraic space is regular”.

Stacks 0ENC, part (2), in this chapter's vocabulary. The pullback f^*s of a nonzero — that is, regular — meromorphic section of an invertible 𝒪_Y-module ℒ is again a nonzero meromorphic section, now of f^*ℒ.

theorem isRegularMeromorphicSection_pullbackMeromorphicSectionOfGood
    (hL : IsInvertibleSheaf D sY hY L)
    (hσ : IsRegularMeromorphicSection.{u, u} D.site D.base D.base_mem Y hY.1 L σ) :
    IsRegularMeromorphicSection.{u, u} D.site D.base D.base_mem X hX.1
      (pullbackSheaf D sY hY sX hX (spaceMorphismOfGood D sX hX sY hY (f := f)) L)
      (pullbackMeromorphicSectionOfGood D sX hX sY hY L σ hPull)

AlgebraicGeometry.Space.chartMeromorphicFunctionPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicFunctionsChartPullback.lean, line 140. The attribute's comment: “part (1), chartwise on the SHEAVES of meromorphic functions: the fraction rule a/b ↦ f♯a/f♯b over an étale chart diagram as a homomorphism 𝒦_Y(V) ⟶ 𝒦_X(U), where AlgebraicGeometry.Space.chartPullbackMeromorphicFunctions is the same rule on the presheaves of sectionwise localizations. This is the coefficient rule for part (1) read through the second of the two descriptions of 𝒦(F) in Stacks 0EN5, the sheafification of F ⊗_𝒪 𝒦, which is the one AlgebraicGeometry.Space.MeromorphicSection and hence part (2) use. The global map Γ(Y, 𝒦_Y(F)) ⟶ Γ(X, 𝒦_X(f^*F)) of part (1) is asserted for the first description by AlgebraicGeometry.Space.pullbackSheafifiedRegularSections, and for the second by AlgebraicGeometry.Space.pullbackMeromorphicSection, which is built over this rule. Part (2) is proved for an invertible module by AlgebraicGeometry.Space.isRegularMeromorphicSection_pullbackMeromorphicSection, over that same description, and is not asserted here”.

The chartwise pullback of meromorphic functions on the sheaves. Over a commuting square of étale charts U of X above V of Y the comparison 𝒦_Y ⟶ f_*𝒦_X projects to a homomorphism of commutative rings 𝒦_Y(V) ⟶ 𝒦_X(U).

noncomputable def chartMeromorphicFunctionPullback (d : ChartDiagram B S hS X.1 Y.1 f.hom) :
    (meromorphicFunctionSheaf B S hS Y.1 Y.2).obj.obj (op d.V) →+*
      (meromorphicFunctionSheaf B S hS X.1 X.2).obj.obj (op d.U)

AlgebraicGeometry.Space.chartPullbackMeromorphicFunctions, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicPullback.lean, line 238. The attribute's comment: “part (1), chartwise: the local fraction rule a/b ↦ f♯a/f♯b over an étale chart diagram, on the presheaf of sectionwise localizations. The global map Γ(Y, 𝒦_Y(F)) ⟶ Γ(X, 𝒦_X(f^*F)) of part (1) is asserted for ONE of the two spellings of 𝒦(F): AlgebraicGeometry.Space.pullbackSheafifiedRegularSections gives it with 𝒦(F) read as the first description in Stacks 0EN5, the sheafification of the presheaf of sectionwise localizations. It is asserted for AlgebraicGeometry.Space.MeromorphicSection, which realizes Stacks 0EN5 through the other description there, the sheafification of F ⊗_𝒪 𝒦, by AlgebraicGeometry.Space.pullbackMeromorphicSection. Stacks 0EMD, which identifies the two descriptions, is not proved and neither map uses it. Part (2), stated through AlgebraicGeometry.Space.IsRegularMeromorphicSection, is not asserted here; it is proved for an invertible module by AlgebraicGeometry.Space.isRegularMeromorphicSection_pullbackMeromorphicSection. Erratum: part (2) as printed reads 'invertible 𝒪_X-module', but pulling back along f : X ⟶ Y needs an 𝒪_Y-module, which is what the scheme-level form of the lemma, 02OY, says”.

The local fraction rule a/b ↦ f^♯a/f^♯b. When pullbacks of meromorphic functions are defined for f, the pullback along a chart diagram carries the sectionwise localization 𝒮_Y(V)⁻¹𝒪_Y(V) into 𝒮_X(U)⁻¹𝒪_X(U): a denominator regular over V pulls back to one regular over U, so the universal property of the localization applies.

noncomputable def chartPullbackMeromorphicFunctions
    (hf : PullbacksMeromorphicSections B S hS f) (d : ChartDiagram B S hS X Y f) :
    (regularSectionsSubpresheaf B S hS Y hY).localizationPresheaf.obj (op d.V) →+*
      (regularSectionsSubpresheaf B S hS X hX).localizationPresheaf.obj (op d.U)

AlgebraicGeometry.Space.fmapMeromorphicFunctions, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicPullback.lean, line 328. The attribute's comment: “part (1), chartwise: the fraction rule is canonical, being an f-map of Stacks 03G3 on the presheaves of sectionwise localizations. The global pullback map of part (1) is asserted for the sheafification of those presheaves, the first of the two descriptions of 𝒦 in Stacks 0EN5, by AlgebraicGeometry.Space.pullbackSheafifiedRegularSections, and for the second, AlgebraicGeometry.Space.MeromorphicSection, by AlgebraicGeometry.Space.pullbackMeromorphicSection. Part (2) is not asserted here; it is proved for an invertible module by AlgebraicGeometry.Space.isRegularMeromorphicSection_pullbackMeromorphicSection”.

The chartwise fraction rules assemble into an f-map of presheaves of sets from the sectionwise localization 𝒮_Y⁻¹𝒪_Y to 𝒮_X⁻¹𝒪_X, in the sense of Stacks 03G3: pullback of meromorphic functions is compatible with étale restriction of both charts of a diagram.

noncomputable def fmapMeromorphicFunctions (hf : PullbacksMeromorphicSections B S hS f) :
    FMap B S hS X Y f
      ((regularSectionsSubpresheaf B S hS X hX).localizationPresheaf ⋙
        CategoryTheory.forget CommRingCat.{u})
      ((regularSectionsSubpresheaf B S hS Y hY).localizationPresheaf ⋙
        CategoryTheory.forget CommRingCat.{u})

AlgebraicGeometry.Space.pullbackSheafifiedRegularSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicPullbackGlobalSections.lean, line 149. The attribute's comment: “part (1), for the first of the two descriptions of the sheaf of meromorphic sections in Stacks 0EN5: the global map Γ(Y, 𝒦_Y(F)) ⟶ Γ(X, 𝒦_X(f^*F)) with 𝒦(F) taken to be the sheafification of the presheaf of sectionwise localizations U ↦ 𝒮(U)⁻¹F(U). The same map for AlgebraicGeometry.Space.MeromorphicSection, which realizes Stacks 0EN5 through the other description there, the sheafification of the extension of scalars F ⊗_𝒪 𝒦, is AlgebraicGeometry.Space.pullbackMeromorphicSection. Stacks 0EMD, which identifies the two descriptions, is not proved and neither map uses it. Additivity of the map is not asserted, and neither is part (2), which is stated through AlgebraicGeometry.Space.IsRegularMeromorphicSection and proved for an invertible module by AlgebraicGeometry.Space.isRegularMeromorphicSection_pullbackMeromorphicSection”.

Stacks 0ENC, part (1), for the sheafification of the sectionwise localizations. When pullbacks of meromorphic functions are defined for f, there is a canonical map on global sections

Γ(Y, 𝒦_Y(M)) ⟶ Γ(X, 𝒦_X(f^*M))

with the sheaf of meromorphic sections taken as Stacks 0EN5 describes it, the sheafification of the presheaf of sectionwise localizations U ↦ 𝒮(U)⁻¹M(U).

It is the chartwise fraction rule m/b ↦ (f^*m)/(f^♯b) of AlgebraicGeometry.Space.chartPullbackMeromorphicSections, carried along three identifications: the descent of Stacks 03G4 for a presheaf of sections on the target (AlgebraicGeometry.Space.meromorphicSectionsDescendedHom), the extension of a morphism into a sheaf over the sheafification of its source (AlgebraicGeometry.Space.sheafifyForgetHomEquiv), and the identification of the global sections of a direct image with those of the sheaf (AlgebraicGeometry.Space.equivSectionsSpacesDirectImage).

Only the additive structure of the sectionwise localizations is used, so the map is produced on the underlying sets; it is a map of sets of global sections and is not here asserted to be additive.

noncomputable def pullbackSheafifiedRegularSections
    (hf : PullbacksMeromorphicSections B S hS f.hom) :
    (regularSectionsLocalizationModuleSheafSet B S hS Y.1 Y.2 M).obj.sections →
      (regularSectionsLocalizationModuleSheafSet B S hS X.1 X.2
        ((modulePullback B S hS f).obj M)).obj.sections

AlgebraicGeometry.Space.chartPullbackMeromorphicSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicPullbackModule.lean, line 202. The attribute's comment: “part (1), chartwise for an arbitrary sheaf of 𝒪_Y-modules F: the local fraction rule m/b ↦ (f^m)/(f♯b) on the sectionwise localizations over an étale chart diagram. This generalizes the structure-sheaf case AlgebraicGeometry.Space.chartPullbackMeromorphicFunctions from F = 𝒪_Y to an arbitrary F. The global map Γ(Y, 𝒦_Y(F)) ⟶ Γ(X, 𝒦_X(f^F)) of part (1) is asserted for ONE of the two spellings of 𝒦(F): AlgebraicGeometry.Space.pullbackSheafifiedRegularSections gives it with 𝒦(F) read as the first description in Stacks 0EN5, the sheafification of this presheaf of sectionwise localizations, and AlgebraicGeometry.Space.pullbackMeromorphicSection gives it for the other description there, the sheafification of F ⊗_𝒪 𝒦, which is the one AlgebraicGeometry.Space.MeromorphicSection uses. Stacks 0EMD, which identifies the two descriptions, is not proved and neither map uses it. Part (2), stated through AlgebraicGeometry.Space.IsRegularMeromorphicSection, is not asserted here; it is proved for an invertible module by AlgebraicGeometry.Space.isRegularMeromorphicSection_pullbackMeromorphicSection”.

The local fraction rule m/b ↦ (f^*m)/(f^♯b). When pullbacks of meromorphic functions are defined for f, the pullback along a chart diagram carries the sectionwise localization 𝒮_Y(V)⁻¹M(V) of a sheaf of 𝒪_Y-modules M into 𝒮_X(U)⁻¹(f^*M)(U): the numerator is pulled back by the chart component of the unit of the Stacks 03D7 adjunction and the denominator by the fraction rule on the structure sheaf, which inverts it.

noncomputable def chartPullbackMeromorphicSections
    (hf : PullbacksMeromorphicSections B S hS f.hom)
    (d : ChartDiagram B S hS X.1 Y.1 f.hom) :
    (regularSectionsLocalizationModule B S hS Y.1 Y.2 M).obj (op d.V) →+
      (regularSectionsLocalizationModule B S hS X.1 X.2
        ((modulePullback B S hS f).obj M)).obj (op d.U)

AlgebraicGeometry.Space.fmapMeromorphicSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicPullbackModule.lean, line 332. The attribute's comment: “part (1), chartwise for an arbitrary sheaf of 𝒪_Y-modules F: the fraction rule m/b ↦ (f^m)/(f♯b) is canonical, being an f-map of Stacks 03G3 from the presheaf of sectionwise localizations of F to that of f^F. This generalizes the structure-sheaf case AlgebraicGeometry.Space.fmapMeromorphicFunctions from F = 𝒪_Y to an arbitrary F. It is a statement about the presheaves of sectionwise localizations, not about their sheafifications; the global map Γ(Y, 𝒦_Y(F)) ⟶ Γ(X, 𝒦_X(f^*F)) of part (1) that this f-map descends to is AlgebraicGeometry.Space.pullbackSheafifiedRegularSections, which is part (1) with 𝒦(F) read as the first description in Stacks 0EN5, the sheafification of these sectionwise localizations. Part (1) for AlgebraicGeometry.Space.MeromorphicSection, which realizes Stacks 0EN5 through the other description there, the sheafification of F ⊗_𝒪 𝒦, is AlgebraicGeometry.Space.pullbackMeromorphicSection, built over the same rule taken over the sheaf 𝒦 instead of the presheaf 𝒮⁻¹𝒪. Part (2), stated through AlgebraicGeometry.Space.IsRegularMeromorphicSection, is not asserted here; it is proved for an invertible module by AlgebraicGeometry.Space.isRegularMeromorphicSection_pullbackMeromorphicSection”.

The chartwise fraction rules for a sheaf of 𝒪_Y-modules M assemble into an f-map of presheaves of sets from the sectionwise localization 𝒮_Y⁻¹M to 𝒮_X⁻¹(f^*M), in the sense of Stacks 03G3: the rule m/b ↦ (f^*m)/(f^♯b) is compatible with étale restriction of both charts of a diagram. This is the module-level form of AlgebraicGeometry.Space.fmapMeromorphicFunctions, which is the case M = 𝒪_Y.

noncomputable def fmapMeromorphicSections
    (hf : PullbacksMeromorphicSections B S hS f.hom) :
    FMap B S hS X.1 Y.1 f.hom
      ((regularSectionsLocalizationModule B S hS X.1 X.2
          ((modulePullback B S hS f).obj M)).presheaf ⋙
        CategoryTheory.forget AddCommGrpCat.{u})
      ((regularSectionsLocalizationModule B S hS Y.1 Y.2 M).presheaf ⋙
        CategoryTheory.forget AddCommGrpCat.{u})

AlgebraicGeometry.Space.pullbackMeromorphicSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicSectionGlobalPullback.lean, line 199. The attribute's comment: “part (1): the global map Γ(Y, 𝒦_Y(F)) ⟶ Γ(X, 𝒦_X(f^*F)) on AlgebraicGeometry.Space.MeromorphicSection, the meromorphic sections of Stacks 0EN5 as the library spells them -- global sections of the sheafification of F ⊗_𝒪 𝒦. AlgebraicGeometry.Space.pullbackSheafifiedRegularSections is the same map for the other description in Stacks 0EN5, the sheafification of the presheaf of sectionwise localizations. Additivity and semilinearity of this map are AlgebraicGeometry.Space.pullbackMeromorphicSection_eval_add and AlgebraicGeometry.Space.pullbackMeromorphicSection_eval_smul_chartDiagram, and global additivity is AlgebraicGeometry.Space.pullbackMeromorphicSection_add; part (2) for an invertible module is AlgebraicGeometry.Space.isRegularMeromorphicSection_pullbackMeromorphicSection”.

Stacks 0ENC, part (1). When pullbacks of meromorphic functions are defined for f, there is a canonical map on global meromorphic sections

Γ(Y, 𝒦_Y(M)) ⟶ Γ(X, 𝒦_X(f^*M))

with 𝒦(M) the sheaf of meromorphic sections of Stacks 0EN5, AlgebraicGeometry.Space.meromorphicSectionSheaf, and a meromorphic section a global section of it, AlgebraicGeometry.Space.MeromorphicSection.

It is the chartwise rule m ⊗ a ↦ (f^*m) ⊗ (f^♯a) of AlgebraicGeometry.Space.chartPullbackMeromorphicSectionsSheaf, carried along three identifications: the descent of Stacks 03G4 for a presheaf of sections on the target (AlgebraicGeometry.Space.meromorphicSectionSheafDescendedHom), the extension of a morphism into a sheaf over the sheafification of its source (AlgebraicGeometry.Space.sheafifyForgetHomEquiv), and the identification of the global sections of a direct image with those of the sheaf (AlgebraicGeometry.Space.equivSectionsSpacesDirectImage).

Only the additive structure of M ⊗_{𝒪} 𝒦 is used, so the map is produced on the underlying sets and nothing in the construction is a map of abelian groups. That it is nonetheless additive and 𝒦-semilinear is AlgebraicGeometry.Space.pullbackMeromorphicSection_eval_add and AlgebraicGeometry.Space.pullbackMeromorphicSection_eval_smul_chartDiagram, proved from its values; AlgebraicGeometry.Space.pullbackMeromorphicSection_add is global additivity against the group structure on global sections.

noncomputable def pullbackMeromorphicSection :
    MeromorphicSection.{u, u} B S hS Y.1 Y.2 M →
      MeromorphicSection.{u, u} B S hS X.1 X.2 ((modulePullback B S hS f).obj M)

AlgebraicGeometry.Space.pullbackMeromorphicSection_eval_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicSectionGlobalPullbackLinear.lean, line 297. The attribute's comment: “the algebra of the part (1) map, which its construction leaves unasserted: the global map on meromorphic sections is additive”.

The global pullback map of Stacks 0ENC, part (1) is additive. Let w be a meromorphic section of M whose value over every étale scheme chart of Y is the sum of the values of s and s' there. Then the value of the pullback of w over every étale scheme chart of X is the sum of the values of the pullbacks of s and s'.

A meromorphic section is a section of a sheaf of modules, a type carrying no module structure, so this is the assertion that the global map of part (1) is additive.

Every chart of X is covered by the charts of X of affine commuting squares (AlgebraicGeometry.Space.exists_affine_chartDiagram_ofArrows), over which the identity is AlgebraicGeometry.Space.pullbackMeromorphicSection_eval_add_chartDiagram.

theorem pullbackMeromorphicSection_eval_add
    (s s' w : MeromorphicSection.{u, u} B S hS Y.1 Y.2 M)
    (hw : ∀ V : SmallEtale B S hS Y.1, w.eval (op V) = s.eval (op V) + s'.eval (op V))
    (U : SmallEtale B S hS X.1) :
    (pullbackMeromorphicSection B S hS f M hf w).eval (op U) =
      (pullbackMeromorphicSection B S hS f M hf s).eval (op U) +
        (pullbackMeromorphicSection B S hS f M hf s').eval (op U)

AlgebraicGeometry.Space.pullbackMeromorphicSection_eval_smul_chartDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicSectionGlobalPullbackLinear.lean, line 334. The attribute's comment: “the algebra of the part (1) map, which its construction leaves unasserted: the global map on meromorphic sections is semilinear over the chartwise pullback of meromorphic functions. The coefficient over the chart of X of a commuting square of affine etale charts is the image of the coefficient over its chart of Y under AlgebraicGeometry.Space.chartMeromorphicPullbackHom; a single coefficient over all of X would need the global map on meromorphic functions, which is not available”.

The global pullback map of Stacks 0ENC, part (1) is semilinear over the chartwise pullback of meromorphic functions. Let d be a commuting square of affine étale scheme charts, d.U of X above d.V of Y, let c be a meromorphic function on d.V and let the meromorphic sections s and s' of M satisfy s|_{d.V} = c · s'|_{d.V}. Then over d.U

(f^*s)|_{d.U} = (f^♯c) · (f^*s')|_{d.U},

with f^♯ the chartwise pullback of meromorphic functions AlgebraicGeometry.Space.chartMeromorphicPullbackHom.

Over a covering family of d.U refining the sieve over which s' is an honest element of M ⊗_{𝒪_Y} 𝒦_Y both values are computed by AlgebraicGeometry.Space.pullbackMeromorphicSection_eval_chartDiagram, and the identity is that the chartwise rule carries a coefficient to its pullback.

theorem pullbackMeromorphicSection_eval_smul_chartDiagram
    (s s' : MeromorphicSection.{u, u} B S hS Y.1 Y.2 M)
    (d : ChartDiagram B S hS X.1 Y.1 f.hom)
    (hU : IsAffine ((BigFppfOver.toScheme B S hS).obj
      ((SmallEtale.toOver B S hS X.1).obj d.U)))
    (hV : IsAffine ((BigFppfOver.toScheme B S hS).obj
      ((SmallEtale.toOver B S hS Y.1).obj d.V)))
    (c : (Stacks.SheafOfModules.Tensor.ringSheaf (meromorphicRingedSite B S hS Y.1 Y.2).O).obj.obj
      (op d.V))
    (hc : s.eval (op d.V) = c • s'.eval (op d.V)) :
    (pullbackMeromorphicSection B S hS f M hf s).eval (op d.U) =
      chartMeromorphicRingedSitePullbackHom B S hS f hf d c •
        (pullbackMeromorphicSection B S hS f M hf s').eval (op d.U)

AlgebraicGeometry.Space.pullbackMeromorphicSection_sectionsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicSectionGlobalPullbackNatural.lean, line 203. The attribute's comment: “the algebra of the part (1) map, which its construction leaves unasserted: the global map on meromorphic sections is natural in the module, for the action of the sheaf of meromorphic sections on morphisms of modules”.

The global pullback of meromorphic sections is natural in the module: for a morphism φ : M ⟶ N of sheaves of 𝒪_Y-modules the pullback of the image of a meromorphic section of M under 𝒦_Y(φ) is the image of the pullback of that section under 𝒦_X(f^*φ).

theorem pullbackMeromorphicSection_sectionsMap (φ : M ⟶ N)
    (s : MeromorphicSection.{u, u} B S hS Y.1 Y.2 M) :
    pullbackMeromorphicSection B S hS f N hf
        (SheafOfModules.sectionsMap (meromorphicSectionSheafMap B S hS Y.1 Y.2 φ) s) =
      SheafOfModules.sectionsMap
        (meromorphicSectionSheafMap B S hS X.1 X.2 ((modulePullback B S hS f).map φ))
        (pullbackMeromorphicSection B S hS f M hf s)

AlgebraicGeometry.Space.isRegularMeromorphicSection_pullbackMeromorphicSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MeromorphicSectionPullbackRegular.lean, line 215. The attribute's comment: “part (2)”.

Let f : X ⟶ Y be a morphism of algebraic spaces for which pullbacks of meromorphic functions are defined, let L be an invertible 𝒪_Y-module and let s be a regular meromorphic section of L. Then the pullback f^*s is a regular meromorphic section of the invertible 𝒪_X-module f^*L.

theorem isRegularMeromorphicSection_pullbackMeromorphicSection (f : X ⟶ Y)
    (hf : PullbacksMeromorphicSections B S hS f.hom) (L : Modules.{u, u} B S hS Y.1 Y.2)
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible (structureCommRings B S hS Y)
      (structureRingSheaf B S hS Y).property L)
    (s : MeromorphicSection.{u, u} B S hS Y.1 Y.2 L)
    (hs : IsRegularMeromorphicSection.{u, u} B S hS Y.1 Y.2 L s) :
    IsRegularMeromorphicSection.{u, u} B S hS X.1 X.2 ((modulePullback B S hS f).obj L)
      (pullbackMeromorphicSection B S hS f L hf s)

Tag 0EPQ, a lemma

Tag 0EPQ in the Stacks Project.

AlgebraicGeometry.Space.exists_isRegularMeromorphicSection_of_isTrivialAtCodimensionZeroPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularMeromorphicSectionExistence.lean, line 299. The attribute's comment: “every invertible module on an algebraic space satisfying conditions (a), (b) and (c) of Tag 0ENA has a regular meromorphic section”.

Stacks 0EPQ. Let X be an algebraic space over a scheme S satisfying conditions (a), (b) and (c) of Stacks 0ENA — every weakly associated point of X has codimension 0, the irreducible components of X are locally finite, and every codimension-zero point of X is representable by a monomorphism from the spectrum of a field. Then every invertible 𝒪_X-module ℒ has a regular meromorphic section.

The choice of the generators s_η ∈ ℒ_η that the source makes is AlgebraicGeometry.Space.CodimensionZeroPresentation.nonempty_iso_unit_of_isInvertibleModule above, the triviality of an invertible module on the small étale site of Spec(𝒪_{X, η}), composed with AlgebraicGeometry.Space.modulePullbackInvertible. Those trivialisations give 𝒦_X ≅ 𝒦_X(ℒ) by CodimensionZeroPresentation.nonempty_uliftUnit_iso_meromorphicSectionSheaf, and an isomorphism 𝒦_X ≅ 𝒦_X(ℒ) produces a regular meromorphic section by AlgebraicGeometry.Space.exists_isRegularMeromorphicSection_of_nonempty_iso. See the implementation notes.

theorem exists_isRegularMeromorphicSection_of_isTrivialAtCodimensionZeroPoints
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hwa : ∀ z ∈ weaklyAssociatedPointsOfSpace B S hS (⟨X, hX⟩ : AlgebraicSpaces B S hS),
      localRingDimension B S hS z = 0)
    (hfin : HasLocallyFiniteIrreducibleComponents B S hS X)
    (hmono : HasMonomorphicCodimensionZeroPoints B S hS X)
    (L : Modules.{u, u} B S hS X hX)
    (hL : IsInvertibleModule (⟨X, hX⟩ : AlgebraicSpaces B S hS) L) :
    ∃ s : MeromorphicSection.{u, u} B S hS X hX L,
      IsRegularMeromorphicSection.{u, u} B S hS X hX L s

Sources

• Section 71.10, Tag 0EN2
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.meromorphicFunctionSheaf · AlgebraicGeometry.Space.MeromorphicFunction · AlgebraicGeometry.Space.isRegularSection_iff_mem_nonZeroDivisors · AlgebraicGeometry.Space.meromorphicSectionSheaf · AlgebraicGeometry.Space.MeromorphicSection · AlgebraicGeometry.Space.isFractionRing_meromorphicFunctionSheaf_obj · AlgebraicGeometry.Space.isQuasicoherent_meromorphicAlgebraSheaf · AlgebraicGeometry.Space.regularSectionsStalk_eq_nonZeroDivisors

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.