43.23 Projections to 43.27 Pullback for a general…

Section43.23 Projections#

Section 43.23 of the Stacks Project, Tag 0B1N. 10 tags here are carried by 50 declarations of the repository (all in StacksFrontier) and 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0B1N, the section

Tag 0B1N in the Stacks Project.

Declarations registered for the tag:

• closedPointsEquivDual registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Intersection/Projections/ProjectionsSection.lean, line 47 (StacksFrontier): “section tag; the closed points of 𝐏(V) are the one-dimensional quotients V → L_p of V”.
• pointSubmodule registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Intersection/Projections/ProjectionsSection.lean, line 49 (StacksFrontier): “section tag; W_p = Ker(V → L_p), the degree-one forms vanishing at p”.
• projection registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Intersection/Projections/ProjectionsSection.lean, line 51 (StacksFrontier): “section tag; the projection r_p away from p, for the submodule W_p”.
• coe_mapDomain_pointSubmodule registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Intersection/Projections/ProjectionsSection.lean, line 53 (StacksFrontier): “section tag; the domain of definition of r_p is 𝐏(V) ∖ {p}”.

Tag 0B1P, a lemma

Tag 0B1P in the Stacks Project.

AlgebraicGeometry.ProjectiveSpaceOfModule.exists_isOpen_isFinite_projection_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Projective/FiniteProjection.lean, line 167.

Stacks Project, Tag 0B1P. Let V be a vector space of dimension n + 1 over an algebraically closed field and let X ⊆ 𝐏(V) be a closed subscheme with X ≠ 𝐏(V). Then there is a nonempty Zariski open U ⊆ 𝐏(V) such that for every closed point p ∈ U the projection r_p away from p is defined on X and the restriction r_p|_X : X ⟶ 𝐏(W_p) is a finite morphism.

The open is the complement of X, which is nonempty because a surjective closed immersion into the reduced scheme 𝐏(V) would be an isomorphism.

public theorem exists_isOpen_isFinite_projection_restrict [IsAlgClosed k] [FiniteDimensional k V]
    [Nontrivial V] {X : Scheme.{u}} (i : X ⟶ projectiveSpaceOfModule k V)
    [IsClosedImmersion i] (hX : ¬ IsIso i) :
    ∃ U : (projectiveSpaceOfModule k V).Opens,
      (U : Set (projectiveSpaceOfModule k V)).Nonempty ∧
      ∀ p ∈ U, IsClosed ({p} : Set (projectiveSpaceOfModule k V)) →
        ∃ j : X ⟶ (projectionDomain k V (pointSubmodule k V p)).toScheme,
          j ≫ (projectionDomain k V (pointSubmodule k V p)).ι = i ∧
            IsFinite (j ≫ projection k V (pointSubmodule k V p))

Tag 0B1Q, a lemma

Tag 0B1Q in the Stacks Project.

AlgebraicGeometry.ProjectiveSpaceOfModule.exists_isOpen_projection_isClosedImmersion_and_etaleAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Projective/GenericProjection.lean, line 641. The attribute's comment: “both parts, for a closed subvariety of the projective space of a vector space of dimension n + 1 over an algebraically closed field and a nonsingular point x of it, each part under its own dimension condition exactly as the source states it: (1) for dim X < n - 1 a nonempty Zariski open of centres p for which r_p|_X is an isomorphism over a neighbourhood of r_p(x), spelled as the restriction of r_p|_X over that neighbourhood being a closed immersion, which is the same thing since a closed immersion over an open R is an isomorphism onto its scheme-theoretic image r_p(X) ∩ R; (2) for dim X = n - 1 a nonempty Zariski open of centres p for which r_p|_X : X ⟶ 𝐏(W_p) is étale at x. Both parts also deliver the source's 'r_p is defined on X' as the lift j of the closed immersion i through the domain of definition of the projection away from p. WithBot ℕ∞ has no subtraction, so the two dimension conditions are written dim X + 1 < n and dim X + 1 = n.”.

Stacks Project, Tag 0B1Q. Let V be a vector space of dimension n + 1 over an algebraically closed field, let X ⊆ 𝐏(V) be a closed subvariety and let x be a nonsingular point of X. Then

1. if dim X < n - 1, there is a nonempty Zariski open U ⊆ 𝐏(V) such that for every closed point p ∈ U the projection r_p is defined on X and r_p|_X : X → r_p(X) is an isomorphism over an open neighbourhood of r_p(x);
2. if dim X = n - 1, there is a nonempty Zariski open U ⊆ 𝐏(V) such that for every closed point p ∈ U the projection r_p is defined on X and r_p|_X : X ⟶ 𝐏(W_p) is étale at x.

Each part keeps its own dimension condition as the hypothesis of its clause, as the source states them. That r_p is defined on X is the morphism j lifting the closed immersion i through the domain of definition of the projection away from p. In part (1) the isomorphism onto the image over a neighbourhood R of r_p(x) is spelled as r_p|_X restricted over R being a closed immersion, which is the same thing: a closed immersion over R is an isomorphism of its source onto its scheme-theoretic image, and that image is r_p(X) ∩ R. WithBot ℕ∞ has no subtraction, so dim X < n - 1 and dim X = n - 1 are written dim X + 1 < n and dim X + 1 = n.

public theorem exists_isOpen_projection_isClosedImmersion_and_etaleAt (n : ℕ)
    (hV : Module.finrank k V = n + 1)
    {X : Scheme.{u}} (i : X ⟶ projectiveSpaceOfModule k V) [IsClosedImmersion i]
    [IsVariety k (i ≫ projectiveSpaceOfModuleToSpec k V)]
    (x : X) (hxreg : x ∈ regularLocus X) :
    (topologicalKrullDim X + 1 < (n : WithBot ℕ∞) →
        ∃ U : (projectiveSpaceOfModule k V).Opens,
          (U : Set (projectiveSpaceOfModule k V)).Nonempty ∧
          ∀ p ∈ U, IsClosed ({p} : Set (projectiveSpaceOfModule k V)) →
            ∃ j : X ⟶ (projectionDomain k V (pointSubmodule k V p)).toScheme,
              j ≫ (projectionDomain k V (pointSubmodule k V p)).ι = i ∧
                ∃ R : (projectiveSpaceOfModule k ↥(pointSubmodule k V p)).Opens,
                  (j ≫ projection k V (pointSubmodule k V p)).base x ∈ R ∧
                  IsClosedImmersion ((j ≫ projection k V (pointSubmodule k V p)) ∣_ R)) ∧
      (topologicalKrullDim X + 1 = (n : WithBot ℕ∞) →
        ∃ U : (projectiveSpaceOfModule k V).Opens,
          (U : Set (projectiveSpaceOfModule k V)).Nonempty ∧
          ∀ p ∈ U, IsClosed ({p} : Set (projectiveSpaceOfModule k V)) →
            ∃ j : X ⟶ (projectionDomain k V (pointSubmodule k V p)).toScheme,
              j ≫ (projectionDomain k V (pointSubmodule k V p)).ι = i ∧
                EtaleAt (j ≫ projection k V (pointSubmodule k V p)) x)

Tag 0H8A, a lemma

Tag 0H8A in the Stacks Project.

AlgebraicGeometry.ProjectiveSpaceOfModule.exists_isOpen_forall_closedPoint_projection_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Projective/GenericProjectionLocalIsomorphism.lean, line 439.

Stacks Project, Tag 0H8A. Let V be a finite-dimensional vector space over an algebraically closed field k, let Z ⊆ X ⊆ 𝐏(V) be closed subvarieties with Z ≠ X and X ≠ 𝐏(V), and let x be a point of Z which is nonsingular on X. Then there is a nonempty Zariski open U ⊆ 𝐏(V) such that for every closed point p ∈ U the projection r_p is defined on Z and the morphism r_p|_Z : Z → r_p(Z) is an isomorphism over an open neighbourhood of r_p(x).

X is a closed subvariety, a closed immersion iX whose source is a variety over k; Z is an irreducible closed subscheme of X, the closed immersion e with e ≫ iX = iZ — this generalizes the source, which takes Z reduced as well. Z ≠ X and X ≠ 𝐏(V) are e and iX not being isomorphisms. That r_p is defined on Z is the lift j of iZ through the domain of definition of the projection away from p, and the isomorphism of Z onto r_p(Z) over a neighbourhood N of r_p(x) is spelled as r_p|_Z restricted over N being a closed immersion, which is the same thing: a closed immersion over N is an isomorphism of its source onto its scheme-theoretic image, and that image is r_p(Z) ∩ N.

public theorem exists_isOpen_forall_closedPoint_projection_restrict {Z X : Scheme.{u}}
    (iZ : Z ⟶ projectiveSpaceOfModule k V) [IsClosedImmersion iZ] [IrreducibleSpace Z]
    (iX : X ⟶ projectiveSpaceOfModule k V) [IsClosedImmersion iX]
    [IsVariety k (iX ≫ projectiveSpaceOfModuleToSpec k V)]
    (e : Z ⟶ X) (he : e ≫ iX = iZ) (hZX : ¬ IsIso e) (hX : ¬ IsIso iX)
    (x : Z) (hreg : e x ∈ regularLocus X) :
    ∃ U : (projectiveSpaceOfModule k V).Opens,
      (U : Set (projectiveSpaceOfModule k V)).Nonempty ∧
      ∀ p ∈ U, IsClosed ({p} : Set (projectiveSpaceOfModule k V)) →
        ∃ j : Z ⟶ (projectionDomain k V (pointSubmodule k V p)).toScheme,
          j ≫ (projectionDomain k V (pointSubmodule k V p)).ι = iZ ∧
          ∃ N : (projectiveSpaceOfModule k ↥(pointSubmodule k V p)).Opens,
            (j ≫ projection k V (pointSubmodule k V p)) x ∈ N ∧
            IsClosedImmersion ((j ≫ projection k V (pointSubmodule k V p)) ∣_ N)

Tag 0B1R, a lemma

Tag 0B1R in the Stacks Project.

AlgebraicGeometry.ProjectiveSpaceOfModule.exists_isOpen_inter_projectionCone_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/GenericProjectionIntersection.lean, line 130. The attribute's comment: “the decomposition Y ∩ r_p^{-1}(r_p(Z)) = (Y ∩ Z) ∪ E with E ⊆ Y closed, for every closed point p of a nonempty Zariski open subset of 𝐏(V), and the dimension bound dim E ≤ dim Y + dim Z + 1 - n carrying the hypothesis n ≤ dim Z + 1, that is for Z of codimension at most one, in which range the bound follows from E ⊆ Y; also carrying the hypothesis Y ∪ Z ≠ 𝐏(V), which the source leaves implicit and without which the asserted identity fails, the left-hand side missing p while Y ∩ Z contains it”.

For closed subsets Y and Z of 𝐏(V) whose union is not all of 𝐏(V), there is a nonempty Zariski open U such that for every closed point p ∈ U the intersection Y ∩ r_p^{-1}(r_p(Z)) is (Y ∩ Z) ∪ E with E ⊆ Y closed, and, in the range n ≤ dim Z + 1, with dim E ≤ dim Y + dim Z + 1 - n, where dim V = n + 1.

The decomposition and the closedness of E are proved for arbitrary closed Y and Z rather than only irreducible ones. The dimension bound is proved in the range n ≤ dim Z + 1, that is for Z of codimension at most one, where it already follows from E ⊆ Y; see the implementation notes for the incidence-variety argument that gives it in the remaining range, and for the one object it needs.

public theorem exists_isOpen_inter_projectionCone_eq [IsAlgClosed k] [Module.Finite k V]
    {n : ℕ} (hn : Module.finrank k V = n + 1)
    {Y Z : Set (projectiveSpaceOfModule k V)} (hY : IsClosed Y) (hZ : IsClosed Z)
    (hYZ : Y ∪ Z ≠ Set.univ)
    (hdimZ : (n : WithBot ℕ∞) ≤ topologicalKrullDim ↥Z + 1) :
    ∃ U : Set (projectiveSpaceOfModule k V), IsOpen U ∧ U.Nonempty ∧
      ∀ p ∈ U, IsClosed ({p} : Set (projectiveSpaceOfModule k V)) →
        ∃ E : Set (projectiveSpaceOfModule k V), IsClosed E ∧ E ⊆ Y ∧
          topologicalKrullDim ↥E + (n : WithBot ℕ∞) ≤
            topologicalKrullDim ↥Y + topologicalKrullDim ↥Z + 1 ∧
          Y ∩ projectionCone k V p Z = (Y ∩ Z) ∪ E

AlgebraicGeometry.ProjectiveSpaceOfModule.exists_isOpen_inter_projectionCone_eq_of_isClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/GenericProjectionIntersectionBound.lean, line 137. The attribute's comment: “the decomposition Y ∩ r_p^{-1}(r_p(Z)) = (Y ∩ Z) ∪ E with E ⊆ Y closed and the dimension bound dim E ≤ dim Y + dim Z + 1 - n, for every closed point p of a nonempty Zariski open subset of 𝐏(V); also carrying the hypothesis Y ∪ Z ≠ 𝐏(V), which the source leaves implicit and without which the asserted identity fails, the left-hand side missing p while Y ∩ Z contains it”.

Stacks Project, Tag 0B1R. For closed subsets Y and Z of 𝐏(V) whose union is not all of 𝐏(V), there is a nonempty Zariski open U such that for every closed point p ∈ U the intersection Y ∩ r_p^{-1}(r_p(Z)) is (Y ∩ Z) ∪ E with E ⊆ Y closed and dim E ≤ dim Y + dim Z + 1 - n, where dim V = n + 1.

The decomposition, the closedness of E and the dimension bound are all proved for arbitrary closed Y and Z rather than only irreducible ones; see the implementation notes for the incidence-variety argument behind the bound.

public theorem exists_isOpen_inter_projectionCone_eq_of_isClosed [IsAlgClosed k] [Module.Finite k V]
    {n : ℕ} (hn : Module.finrank k V = n + 1)
    {Y Z : Set (projectiveSpaceOfModule k V)} (hY : IsClosed Y) (hZ : IsClosed Z)
    (hYZ : Y ∪ Z ≠ Set.univ) :
    ∃ U : Set (projectiveSpaceOfModule k V), IsOpen U ∧ U.Nonempty ∧
      ∀ p ∈ U, IsClosed ({p} : Set (projectiveSpaceOfModule k V)) →
        ∃ E : Set (projectiveSpaceOfModule k V), IsClosed E ∧ E ⊆ Y ∧
          topologicalKrullDim ↥E + (n : WithBot ℕ∞) ≤
            topologicalKrullDim ↥Y + topologicalKrullDim ↥Z + 1 ∧
          Y ∩ projectionCone k V p Z = (Y ∩ Z) ∪ E

AlgebraicGeometry.ProjectiveSpaceOfModule.exists_isOpen_inter_projectionConeWithVertex_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/ProjectionConeWithVertex.lean, line 237. The attribute's comment: “the decomposition Y ∩ r_p^{-1}(r_p(Z)) = (Y ∩ Z) ∪ E with E ⊆ Y closed and dim E ≤ dim Y + dim Z + 1 - n, for every closed point p of a nonempty Zariski open subset of 𝐏(V), with no hypothesis beyond the closedness of Y and Z, reading r_p^{-1}(r_p(Z)) as the cone over Z with vertex p”.

Stacks 0B1R. Let V be a vector space of dimension n + 1 over an algebraically closed field and let Y, Z ⊆ 𝐏(V) be closed subsets. There is a nonempty Zariski open U ⊆ 𝐏(V) such that for every closed point p ∈ U

Y ∩ r_p^{-1}(r_p(Z)) = (Y ∩ Z) ∪ E

with E ⊆ Y closed and dim E ≤ dim Y + dim Z + 1 - n, where r_p^{-1}(r_p(Z)) is the cone over Z with vertex p.

No hypothesis beyond the closedness of Y and Z is needed, and in particular none on Y ∪ Z or on dim Z. The source asks for Y and Z to be closed subvarieties; the statement is proved here for arbitrary closed subsets, which is more general, a subvariety being an irreducible reduced closed subscheme.

The open subset produced is U₀ ∖ Z for U₀ the open of the general-fibre bound, when Z is neither empty nor everything; in those two degenerate cases the cone is respectively empty and everything, and E = ∅ serves over all of 𝐏(V). The subset E produced in the main case is the closure of (Y ∖ Z) ∩ r_p^{-1}(r_p(Z)), and its dimension is bounded through the incidence variety T = {(y, z, p) : y ∈ Y ∖ Z, z ∈ Z, p on the line joining y and z} exactly as in AlgebraicGeometry.ProjectiveSpaceOfModule.exists_isOpen_inter_projectionCone_eq_of_union_ne_univ, whose hypothesis p ∉ Y is not available here: the vertex p may well lie on Y, and when it does it is itself a point of (Y ∖ Z) ∩ r_p^{-1}(r_p(Z)) whose membership of the image of the fibre is witnessed by the collinear triple (p, z₀, p) for any closed point z₀ of Z.

With the punctured reading of r_p^{-1}(r_p(Z)) carried by AlgebraicGeometry.ProjectiveSpaceOfModule.projectionCone the statement is false, by AlgebraicGeometry.ProjectiveSpaceOfModule.not_exists_isOpen_inter_projectionCone_univ_eq, and the registrations of this tag on AlgebraicGeometry.ProjectiveSpaceOfModule.exists_isOpen_inter_projectionCone_eq carry the hypotheses that reading forces.

public theorem exists_isOpen_inter_projectionConeWithVertex_eq [IsAlgClosed k] [Module.Finite k V]
    {n : ℕ} (hn : Module.finrank k V = n + 1)
    {Y Z : Set (projectiveSpaceOfModule k V)} (hY : IsClosed Y) (hZ : IsClosed Z) :
    ∃ U : Set (projectiveSpaceOfModule k V), IsOpen U ∧ U.Nonempty ∧
      ∀ p ∈ U, IsClosed ({p} : Set (projectiveSpaceOfModule k V)) →
        ∃ E : Set (projectiveSpaceOfModule k V), IsClosed E ∧ E ⊆ Y ∧
          topologicalKrullDim ↥E + (n : WithBot ℕ∞) ≤
            topologicalKrullDim ↥Y + topologicalKrullDim ↥Z + 1 ∧
          Y ∩ projectionConeWithVertex k V p Z = (Y ∩ Z) ∪ E

Tag 0B2T, a lemma

Tag 0B2T in the Stacks Project.

AlgebraicGeometry.ProjectiveSpaceOfModule.exists_line_disjoint_and_isOpen_sweep, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Projective/AvoidingLines.lean, line 591. The attribute's comment: “the sweeping-out clause is read as the proof reads it: the avoiding lines through p cover the closed points of an open subset, their union itself being non-open at p”.

Stacks 0B2T. Let B be an irreducible closed subset of codimension at least two in the projective space of a nonzero finite-dimensional vector space over an algebraically closed field and let p be a closed point outside B. Then some projective line through p is disjoint from B, and the closed points other than p lying on such a line are exactly the closed points of a nonempty open subset of 𝐏(V), namely the complement of the cone over the image of B under the projection away from p. The union of the avoiding lines itself is not open: in a projective plane with B a point it contains p but no neighbourhood of p.

public theorem exists_line_disjoint_and_isOpen_sweep [IsAlgClosed k] [FiniteDimensional k V]
    [Nontrivial V]
    (B : IrreducibleCloseds (projectiveSpaceOfModule k V)) (hcodim : (2 : ℕ∞) ≤ codimension B)
    (p : projectiveSpaceOfModule k V)
    (hp : IsClosed ({p} : Set (projectiveSpaceOfModule k V)))
    (hpB : p ∉ (B : Set (projectiveSpaceOfModule k V))) :
    (∃ W : Submodule k V, Module.finrank k (V ⧸ W) = 2 ∧ p ∈ linearSubspace k V W ∧
        Disjoint (linearSubspace k V W) (B : Set (projectiveSpaceOfModule k V))) ∧
      ∃ U : Set (projectiveSpaceOfModule k V), IsOpen U ∧
        (∃ q ∈ U, IsClosed ({q} : Set (projectiveSpaceOfModule k V))) ∧
        ∀ q, IsClosed ({q} : Set (projectiveSpaceOfModule k V)) → q ≠ p →
          (q ∈ U ↔ ∃ W : Submodule k V, Module.finrank k (V ⧸ W) = 2 ∧
            p ∈ linearSubspace k V W ∧ q ∈ linearSubspace k V W ∧
            Disjoint (linearSubspace k V W) (B : Set (projectiveSpaceOfModule k V)))

Tag 0B2U, a lemma

Tag 0B2U in the Stacks Project.

AlgebraicGeometry.ProjectiveSpaceOfModule.projGenLinGroupEquivInvertibleClasses, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/ProjectiveLinearGroup.lean, line 219. The attribute's comment: “identification with the invertible open locus”.

PGL(V) is the invertible open locus of the projectivized endomorphism space. The quotient presentation of PGL(V) sends a projective linear transformation to the projective class of any of its linear representatives.

public noncomputable def projGenLinGroupEquivInvertibleClasses [Nontrivial V] :
    ProjGenLinGroup k V ≃ InvertibleEndomorphismClasses k V

AlgebraicGeometry.ProjectiveSpaceOfModule.projGenLinGroupEquivInvertibleClasses_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/ProjectiveLinearGroup.lean, line 226. The attribute's comment: “representative formula for the invertible locus”.

The equivalence with the invertible locus sends a projective linear transformation to the projective class of any of its linear representatives.

public theorem projGenLinGroupEquivInvertibleClasses_apply [Nontrivial V]
    (g : LinearMap.GeneralLinearGroup k V) (hg : (g : V →ₗ[k] V) ≠ 0) :
    ((projGenLinGroupEquivInvertibleClasses k V) (g : ProjGenLinGroup k V)).val =
      Projectivization.mk k (g : V →ₗ[k] V) hg

AlgebraicGeometry.ProjectiveSpaceOfModule.dualEndClosedPointsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/ProjectiveLinearGroup.lean, line 234. The attribute's comment: “closed-point identification for the parameter space”.

The closed points of P((End V)ᵛ) are the projective classes of endomorphisms. This is the parameter space of a linear projective transformation.

public noncomputable def dualEndClosedPointsEquiv [IsAlgClosed k] [Module.Finite k V] :
    ClosedPoints k (Module.Dual k (V →ₗ[k] V)) ≃ Projectivization k (V →ₗ[k] V)

AlgebraicGeometry.ProjectiveSpaceOfModule.dualEndClosedPointsEquiv_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/ProjectiveLinearGroup.lean, line 242. The attribute's comment: “annihilator formula for the parameter-space identification”.

The parameter point corresponding to a class of endomorphisms is cut out by the linear forms annihilating that class. This fixes the identification.

public theorem dualEndClosedPointsEquiv_apply [IsAlgClosed k] [Module.Finite k V]
    (p : ClosedPoints k (Module.Dual k (V →ₗ[k] V))) (φ : Module.Dual k (V →ₗ[k] V)) :
    SymmetricAlgebra.ι k (Module.Dual k (V →ₗ[k] V)) φ ∈ p.val.asHomogeneousIdeal ↔
      φ ((dualEndClosedPointsEquiv k V p).rep) = 0

AlgebraicGeometry.ProjectiveSpaceOfModule.parameterPointToProjGenLinGroup_of_rep, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/ProjectiveLinearGroup.lean, line 275. The attribute's comment: “parameter point to projective linear transformation”.

A parameter point represented by g names the class of g in PGL(V).

public theorem parameterPointToProjGenLinGroup_of_rep
    [Nontrivial V] [IsAlgClosed k] [Module.Finite k V]
    (p : InvertibleParameterPoints k V) (g : LinearMap.GeneralLinearGroup k V)
    (hg : (g : V →ₗ[k] V) ≠ 0)
    (hpg : (dualEndClosedPointsEquiv k V) p.val = Projectivization.mk k (g : V →ₗ[k] V) hg) :
    parameterPointToProjGenLinGroup k V p = (g : ProjGenLinGroup k V)

AlgebraicGeometry.ProjectiveSpaceOfModule.parameterPoint_smul_eq_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/ProjectiveLinearGroup.lean, line 290. The attribute's comment: “compatibility of the parameter-point action”.

On a parameter point represented by g, the morphism in the moving family is the action of the inverse element of PGL(V); the inversion accounts for the contravariance of Proj.

public theorem parameterPoint_smul_eq_map
    [Nontrivial V] [IsAlgClosed k] [Module.Finite k V]
    (p : InvertibleParameterPoints k V) (g : LinearMap.GeneralLinearGroup k V)
    (hg : (g : V →ₗ[k] V) ≠ 0)
    (hpg : (dualEndClosedPointsEquiv k V) p.val = Projectivization.mk k (g : V →ₗ[k] V) hg)
    (x : projectiveSpaceOfModule k V) :
    (parameterPointToProjGenLinGroup k V p)⁻¹ • x = map k V g x

AlgebraicGeometry.ProjectiveSpaceOfModule.projGenLinGroup_is_two_pretransitive, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/ProjectiveLinearGroup.lean, line 316.

Stacks Project, Tag 0B2U. The projective general linear group of a finite-dimensional vector space over an algebraically closed field acts doubly transitively on the closed points of its projective space.

public lemma projGenLinGroup_is_two_pretransitive [IsAlgClosed k] [Module.Finite k V] :
    MulAction.IsMultiplyPretransitive (ProjGenLinGroup k V) (ClosedPoints k V) 2

AlgebraicGeometry.ProjectiveSpaceOfModule.mapDomain_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/ProjMapComparison.lean, line 55. The attribute's comment: “the invertible locus has full projective domain”.

An invertible linear map has everywhere-defined projective morphism: the domain of definition of the induced graded ring homomorphism is all of P(V).

public theorem mapDomain_eq_top (g : LinearMap.GeneralLinearGroup k V) :
    mapDomain (fun n => SymPow.symmetricPower n k V) (fun n => SymPow.symmetricPower n k V)
      (SymPow.gradedSymAlgMap (g : V →ₗ[k] V)) = ⊤

AlgebraicGeometry.ProjectiveSpaceOfModule.mapDomain_ι_comp_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/ProjMapComparison.lean, line 63. The attribute's comment: “compatibility with the projective transformation family”.

On the domain of definition of the induced graded ring homomorphism, the morphism carrying the comparison maps on all twists is the action of g on P(V).

public theorem mapDomain_ι_comp_map (g : LinearMap.GeneralLinearGroup k V) :
    (mapDomain (fun n => SymPow.symmetricPower n k V) (fun n => SymPow.symmetricPower n k V)
          (SymPow.gradedSymAlgMap (g : V →ₗ[k] V))).ι ≫ map k V g =
      (projMapData (fun n => SymPow.symmetricPower n k V)
        (fun n => SymPow.symmetricPower n k V)
        (SymPow.gradedSymAlgMap (g : V →ₗ[k] V))).hom

Tag 0B2V, a lemma

Tag 0B2V in the Stacks Project.

MvPolynomial.irreducible_det_genericMatrix, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/Basic.lean, line 225.

Stacks Project, Tag 0B2V. The determinant of the generic square matrix of positive size over a field is an irreducible multivariate polynomial.

lemma irreducible_det_genericMatrix (k : Type*) [Field k] (n : ℕ) (hn : 0 < n) :
    Irreducible (Matrix.det (fun i j : Fin n ↦ MvPolynomial.X (i, j) :
      Matrix (Fin n) (Fin n) (MvPolynomial (Fin n × Fin n) k)))

Tag 0B2W, an equation

Tag 0B2W in the Stacks Project.

AlgebraicGeometry.ProjectiveSpaceOfModule.endDomain, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/EndomorphismProjection.lean, line 73. The attribute's comment: “the open U(ψ) over the point [g] of the parameter space, i.e. U(g)”.

The open U(g) on which the projective transformation attached to an endomorphism g of V is defined: the domain of definition of the morphism of projective spectra induced by Sym g.

public abbrev endDomain (g : V →ₗ[k] V) : (projectiveSpaceOfModule k V).Opens

AlgebraicGeometry.ProjectiveSpaceOfModule.endProjection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/EndomorphismProjection.lean, line 80. The attribute's comment: “the morphism r_ψ over the point [g] of the parameter space, i.e. r_g”.

The projective transformation r_g : 𝐏(V) ⊇ U(g) → 𝐏(V) attached to an endomorphism g of V: the morphism of projective spectra induced by Sym g on its domain of definition.

public def endProjection (g : V →ₗ[k] V) :
    (endDomain k V g).toScheme ⟶ projectiveSpaceOfModule k V

AlgebraicGeometry.ProjectiveSpaceOfModule.notMem_endDomain_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/EndomorphismProjection.lean, line 101. The attribute's comment: “the complement of U(g) is the image of the closed immersion 𝐏(Coker g) → 𝐏(V)”.

A point of 𝐏(V) lies outside U(g) exactly when it lies on the linear subspace cut out by the image of g, that is on 𝐏(Coker g) ⊆ 𝐏(V).

public theorem notMem_endDomain_iff (g : V →ₗ[k] V) (q : projectiveSpaceOfModule k V) :
    q ∉ endDomain k V g ↔ q ∈ linearSubspace k V (LinearMap.range g)

AlgebraicGeometry.ProjectiveSpaceOfModule.endProjection_eq_linearFunctionalPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/EndomorphismProjection.lean, line 150. The attribute's comment: “the value of r_g on a closed point, namely f ↦ f ∘ g”.

The morphism r_g sends the point cut out by a functional f on V to the point cut out by f ∘ g.

public theorem endProjection_eq_linearFunctionalPoint (g : V →ₗ[k] V)
    (y : (endDomain k V g).toScheme) (f : Module.Dual k V) (hf : f ≠ 0) (hfg : f ∘ₗ g ≠ 0)
    (hy : (y.val : projectiveSpaceOfModule k V) = linearFunctionalPoint k V f hf) :
    endProjection k V g y = linearFunctionalPoint k V (f ∘ₗ g) hfg

AlgebraicGeometry.ProjectiveSpaceOfModule.range_endProjection_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/EndomorphismProjection.lean, line 161. The attribute's comment: “the image of r_g is contained in the image of 𝐏(Im g) → 𝐏(V)”.

Every point in the image of r_g lies on the linear subspace cut out by the kernel of g, which is the image of 𝐏(Im g) → 𝐏(V).

public theorem range_endProjection_subset (g : V →ₗ[k] V) :
    Set.range (endProjection k V g).base ⊆ linearSubspace k V (LinearMap.ker g)

AlgebraicGeometry.ProjectiveSpaceOfModule.exists_endProjection_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/EndomorphismProjection.lean, line 186. The attribute's comment: “the image of r_g is the image of 𝐏(Im g) → 𝐏(V), on closed points”.

Over an algebraically closed field every closed point of the linear subspace cut out by the kernel of g — that is, of the image of 𝐏(Im g) → 𝐏(V) — is the image under r_g of a point of U(g).

public theorem exists_endProjection_eq [IsAlgClosed k] [Module.Finite k V] (g : V →ₗ[k] V)
    (q : projectiveSpaceOfModule k V)
    (hq : IsClosed ({q} : Set (projectiveSpaceOfModule k V)))
    (hmem : q ∈ linearSubspace k V (LinearMap.ker g)) :
    ∃ y : (endDomain k V g).toScheme, endProjection k V g y = q

AlgebraicGeometry.ProjectiveSpaceOfModule.endDomain_smul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/EndomorphismProjection.lean, line 227. The attribute's comment: “U(g) depends only on the point [g] of the parameter space”.

A unit multiple of g has the same domain of definition U(g).

public theorem endDomain_smul (c : kˣ) (g : V →ₗ[k] V) :
    endDomain k V ((c : k) • g) = endDomain k V g

AlgebraicGeometry.ProjectiveSpaceOfModule.endProjection_smul_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/EndomorphismProjection.lean, line 235. The attribute's comment: “r_g depends only on the point [g] of the parameter space, on closed points”.

A unit multiple of g induces the same morphism r_g on the points cut out by linear functionals.

public theorem endProjection_smul_apply (c : kˣ) (g : V →ₗ[k] V)
    (y : (endDomain k V ((c : k) • g)).toScheme) (y' : (endDomain k V g).toScheme)
    (f : Module.Dual k V) (hf : f ≠ 0) (hfg : f ∘ₗ g ≠ 0)
    (hy : (y.val : projectiveSpaceOfModule k V) = linearFunctionalPoint k V f hf)
    (hy' : (y'.val : projectiveSpaceOfModule k V) = linearFunctionalPoint k V f hf) :
    endProjection k V ((c : k) • g) y = endProjection k V g y'

AlgebraicGeometry.ProjectiveSpaceOfModule.universalEndCoeff, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/UniversalEndomorphismFamily.lean, line 237. The attribute's comment: “the canonical map V → V ⊗ Eᵛ = Hom(E, V), v ↦ (g ↦ g v)”.

The canonical map V → (End V)ᵛ ⊗ V = Hom(End V, V) of the source, sending v to the evaluation g ↦ g v.

public def universalEndCoeff : V →ₗ[k] Module.Dual k (V →ₗ[k] V) ⊗[k] V

AlgebraicGeometry.ProjectiveSpaceOfModule.universalEnd, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/UniversalEndomorphismFamily.lean, line 246. The attribute's comment: “ψ over the affine parameter space Spec Sym(Eᵛ), the cone over 𝐏: the universal endomorphism of V ⊗ 𝒪, in place of the map of sheaves V ⊗ 𝒪_𝐏 → V ⊗ 𝒪_𝐏(1) over 𝐏”.

The universal endomorphism ψ of V ⊗ 𝒪 over the affine parameter space: the A-linear extension of the canonical map V → (End V)ᵛ ⊗ V ⊆ A ⊗ V. On the fibre over an endomorphism g it is g.

public def universalEnd :
    endParamRing k V ⊗[k] V →ₗ[endParamRing k V] endParamRing k V ⊗[k] V

AlgebraicGeometry.ProjectiveSpaceOfModule.universalEndDomain, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/UniversalEndomorphismFamily.lean, line 260. The attribute's comment: “U(ψ) ⊆ 𝐏(V ⊗ 𝒪_S) for S = Spec Sym(Eᵛ) the affine parameter space, the cone over 𝐏; the open over 𝐏 itself is AlgebraicGeometry.ProjectiveSpaceOfModule.universalEndSheafDomain, built there from the source's own ψ : V ⊗ 𝒪_𝐏 → V ⊗ 𝒪_𝐏(1) and not from this one by descent along 𝔸(E) ∖ {0} → 𝐏, which is constructed nowhere; what is not identified with 𝐏 × 𝐏(V) is its ambient 𝐏(V ⊗ 𝒪_𝐏(1))”.

The open U(ψ) of the universal family: the domain of definition of the morphism of relative projective spaces induced by Sym ψ over the affine parameter space.

public abbrev universalEndDomain :
    (projectiveSpaceOfModule (endParamRing k V) (endParamRing k V ⊗[k] V)).Opens

AlgebraicGeometry.ProjectiveSpaceOfModule.universalEndProjection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/UniversalEndomorphismFamily.lean, line 272. The attribute's comment: “r_ψ : U(ψ) → 𝐏(V ⊗ 𝒪_S) for S = Spec Sym(Eᵛ) the affine parameter space, the cone over 𝐏; the morphism over 𝐏 itself is AlgebraicGeometry.ProjectiveSpaceOfModule.universalEndSheafProjection, built there from the source's own ψ and not from this one by descent along 𝔸(E) ∖ {0} → 𝐏, which is constructed nowhere; what is not identified with 𝐏 × 𝐏(V) are its total spaces”.

The universal family r_ψ of projective transformations, 𝐏(V ⊗ 𝒪_S) ⊇ U(ψ) → 𝐏(V ⊗ 𝒪_S) over the affine space S of endomorphisms of V: the morphism of relative projective spaces induced by Sym ψ on its domain of definition.

public def universalEndProjection :
    (universalEndDomain k V).toScheme ⟶
      projectiveSpaceOfModule (endParamRing k V) (endParamRing k V ⊗[k] V)

AlgebraicGeometry.ProjectiveSpaceOfModule.endParamFibre_universalEnd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/UniversalEndomorphismFamily.lean, line 316. The attribute's comment: “the fibre of ψ over the parameter point of g is g”.

The fibre of the universal endomorphism over the parameter point of g is g. This is what makes universalEnd universal: the family it defines has r_g as its fibre over g.

public theorem endParamFibre_universalEnd (g : V →ₗ[k] V) (x : endParamRing k V ⊗[k] V) :
    endParamFibre k V g (universalEnd k V x) = g (endParamFibre k V g x)

AlgebraicGeometry.ProjectiveSpaceOfModule.endParamFibreHom_symAlgMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/UniversalEndomorphismFamily.lean, line 384. The attribute's comment: “the fibre of r_ψ over the parameter point of g is r_g, on the homogeneous coordinate rings: Sym ψ reduces to Sym g”.

Sym g is the fibre of Sym ψ over the parameter point of g. Reducing the universal graded endomorphism of Sym_A(V ⊗ A) along the point of the parameter space attached to an endomorphism g of V gives the graded endomorphism Sym g of Sym_k(V) out of which U(g) and r_g are built.

public theorem endParamFibreHom_symAlgMap (g : V →ₗ[k] V)
    (x : SymmetricAlgebra (endParamRing k V) (endParamRing k V ⊗[k] V)) :
    endParamFibreHom k V g (SymPow.symAlgMap (universalEnd k V) x) =
      SymPow.symAlgMap g (endParamFibreHom k V g x)

AlgebraicGeometry.ProjectiveSpaceOfModule.endParamFibreInclusion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/UniversalEndomorphismFamily.lean, line 477. The attribute's comment: “the inclusion of the fibre of 𝐏(V ⊗ 𝒪_S) over the parameter point of g”.

The fibre of the universal family over the parameter point of g: the morphism 𝐏(V) → 𝐏(V ⊗ 𝒪_S) induced by the specialization of the homogeneous coordinate ring, defined on all of 𝐏(V) by endParamFibreInclusionDomain_eq_top.

public def endParamFibreInclusion (g : V →ₗ[k] V) :
    (endParamFibreInclusionDomain k V g).toScheme ⟶
      projectiveSpaceOfModule (endParamRing k V) (endParamRing k V ⊗[k] V)

AlgebraicGeometry.ProjectiveSpaceOfModule.mem_universalEndDomain_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/UniversalEndomorphismFamily.lean, line 486. The attribute's comment: “U(g) is the fibre U(ψ) over the parameter point of g”.

U(g) is the fibre U(ψ) over the parameter point of g. A point of 𝐏(V), included as a point of the fibre of the relative projective space over the parameter point of g, lies in the domain of the universal family exactly when it lies in U(g), the domain of r_g.

public theorem mem_universalEndDomain_iff (g : V →ₗ[k] V)
    (y : (endParamFibreInclusionDomain k V g).toScheme) :
    (endParamFibreInclusion k V g).base y ∈ universalEndDomain k V ↔
      (y.val : projectiveSpaceOfModule k V) ∈ endDomain k V g

AlgebraicGeometry.ProjectiveSpaceOfModule.notMem_universalEndDomain_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/UniversalEndomorphismFamily.lean, line 535. The attribute's comment: “the complement of U(ψ) is the relative 𝐏(Coker ψ), as the vanishing of the degree-one forms in the image of ψ”.

The domain of the universal family. A point lies outside U(ψ) exactly when every degree-one form in the image of the universal endomorphism vanishes at it: the relative form of the description of the complement of U(g) as the image of 𝐏(Coker g) → 𝐏(V).

public theorem notMem_universalEndDomain_iff
    (q : projectiveSpaceOfModule (endParamRing k V) (endParamRing k V ⊗[k] V)) :
    q ∉ universalEndDomain k V ↔
      ∀ x : endParamRing k V ⊗[k] V,
        SymmetricAlgebra.ι (endParamRing k V) (endParamRing k V ⊗[k] V) (universalEnd k V x) ∈
          q.asHomogeneousIdeal

AlgebraicGeometry.ProjectiveSpaceOfModule.universalEndProjection_comp_toSpec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/UniversalEndomorphismFamily.lean, line 573. The attribute's comment: “r_ψ is a morphism over the parameter space S = Spec Sym(Eᵛ), the cone over 𝐏”.

The universal family is a family over the parameter space. The morphism r_ψ commutes with the two structure morphisms of the relative projective space 𝐏(V ⊗ 𝒪_S) to S = Spec Sym((End V)ᵛ), so it is a family of projective transformations parametrized by S and its fibres are morphisms of the fibres.

public theorem universalEndProjection_comp_toSpec :
    universalEndProjection k V ≫
        projectiveSpaceOfModuleToSpec (endParamRing k V) (endParamRing k V ⊗[k] V) =
      (universalEndDomain k V).ι ≫
        projectiveSpaceOfModuleToSpec (endParamRing k V) (endParamRing k V ⊗[k] V)

AlgebraicGeometry.ProjectiveSpaceOfModule.endParamFibreInclusion_comp_toSpec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/UniversalEndomorphismFamily.lean, line 596. The attribute's comment: “the fibre inclusion is a morphism over the parameter point of g”.

The fibre of the relative projective space over the parameter point of g is where 𝐏(V) goes. The inclusion ι_g : 𝐏(V) → 𝐏(V ⊗ 𝒪_S) is a morphism over the point of S attached to g, which is what makes it the inclusion of a fibre rather than merely a morphism.

public theorem endParamFibreInclusion_comp_toSpec (g : V →ₗ[k] V) :
    endParamFibreInclusion k V g ≫
        projectiveSpaceOfModuleToSpec (endParamRing k V) (endParamRing k V ⊗[k] V) =
      (endParamFibreInclusionDomain k V g).ι ≫ projectiveSpaceOfModuleToSpec k V ≫
        Spec.map (CommRingCat.ofHom (endParamPoint k V g).toRingHom)

AlgebraicGeometry.ProjectiveSpaceOfModule.fibreSquareIso_hom_comp_morphismRestrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/UniversalEndomorphismFamily.lean, line 653. The attribute's comment: “the fibre of r_ψ over the parameter point of g is r_g, as scheme morphisms”.

r_g is the fibre of r_ψ over the parameter point of g, as a square of scheme morphisms. Including the fibre 𝐏(V) into the relative projective space and then applying the universal family r_ψ is the same as applying r_g and then including the fibre: the square

U(g) --r_g--> 𝐏(V) --ι_g--> 𝐏(V ⊗ 𝒪_S), U(g) --ι_g--> U(ψ) --r_ψ--> 𝐏(V ⊗ 𝒪_S)

commutes, after the canonical identification fibreSquareIso of the two domains.

This is the composition law of Tag 01MZ applied to the two factorizations endParamFibreGradedHom_comp_gradedSymAlgMap of a single graded ring homomorphism.

public theorem fibreSquareIso_hom_comp_morphismRestrict (g : V →ₗ[k] V) :
    (fibreSquareIso k V g).hom ≫
        (endParamFibreInclusion k V g ∣_ universalEndDomain k V) ≫ universalEndProjection k V =
      (endProjection k V g ∣_ endParamFibreInclusionDomain k V g) ≫
        endParamFibreInclusion k V g

AlgebraicGeometry.ProjectiveSpaceOfModule.isPullback_universalFamilySpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/UniversalEndomorphismFamily.lean, line 672. The attribute's comment: “the total space of the family is the product 𝔸(E) × 𝐏(V), for 𝔸(E) = Spec Sym(Eᵛ) the cone over 𝐏; the source writes the displayed family on 𝐏 × 𝐏(V)”.

The relative projective space of the family is a product. The square formed by the projection 𝐏(V ⊗ 𝒪_S) ⟶ 𝐏(V) and the two structure morphisms is cartesian, so 𝐏(V ⊗ 𝒪_S) = S ×_{Spec k} 𝐏(V) with S = Spec Sym((End V)ᵛ) the affine space of endomorphisms. This is Stacks.ProjectiveSpaceBaseChange.isPullback_projectiveSpaceOfModuleToSpec for the base change of V along k → Sym((End V)ᵛ).

public theorem isPullback_universalFamilySpace :
    IsPullback (Stacks.ProjectiveSpaceBaseChange.map k (endParamRing k V) V)
      (projectiveSpaceOfModuleToSpec (endParamRing k V) (endParamRing k V ⊗[k] V))
      (projectiveSpaceOfModuleToSpec k V)
      (Spec.map (CommRingCat.ofHom (algebraMap k (endParamRing k V))))

AlgebraicGeometry.ProjectiveSpaceOfModule.universalFamilySpaceIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/UniversalEndomorphismFamily.lean, line 684. The attribute's comment: “the identification 𝐏(V ⊗ 𝒪_S) = 𝔸(E) × 𝐏(V) over the cone 𝔸(E) = Spec Sym(Eᵛ)”.

The total space of the family, as the product 𝔸(E) × 𝐏(V). The identification of 𝐏(V ⊗ 𝒪_S) with the fibre product of 𝐏(V) and the affine space of endomorphisms over Spec k, carried by isPullback_universalFamilySpace.

public def universalFamilySpaceIso :
    projectiveSpaceOfModule (endParamRing k V) (endParamRing k V ⊗[k] V) ≅
      Limits.pullback (projectiveSpaceOfModuleToSpec k V)
        (Spec.map (CommRingCat.ofHom (algebraMap k (endParamRing k V))))

AlgebraicGeometry.ProjectiveSpaceOfModule.universalEndSheafMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/UniversalFamilyOverProjectiveSpace.lean, line 469. The attribute's comment: “ψ : V ⊗ 𝒪_𝐏 → V ⊗ 𝒪_𝐏(1) over the projective parameter space 𝐏 = 𝐏(Eᵛ)”.

The map of sheaves ψ : V ⊗ 𝒪_𝐏 ⟶ V ⊗ 𝒪_𝐏(1) over the projective parameter space 𝐏 = 𝐏(Eᵛ), attached by the universal property of V ⊗ 𝒪_𝐏 to the canonical k-linear map V → Γ(𝐏, V ⊗ 𝒪_𝐏(1)).

def universalEndSheafMap :
    constantModule k (dualEndSpace k V) V ⟶
      twistObj k (dualEndSpace k V) (constantModule k (dualEndSpace k V) V) ((1 : ℕ) : ℤ)

AlgebraicGeometry.ProjectiveSpaceOfModule.universalEndSheafDomain, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/UniversalFamilyOverProjectiveSpace.lean, line 481. The attribute's comment: “U(ψ) ⊆ 𝐏(V ⊗ 𝒪_𝐏(1)) over the projective parameter space 𝐏 = 𝐏(Eᵛ); the identification of the twisted total space 𝐏(V ⊗ 𝒪_𝐏(1)) with the displayed 𝐏 × 𝐏(V) is not made, that being Tag 02NC over a base scheme, which this repository has only over a commutative ring”.

The open U(ψ) ⊆ 𝐏(V ⊗ 𝒪_𝐏(1)) of the universal family over the projective parameter space: Tag 07ZG's open for Sym ψ.

abbrev universalEndSheafDomain :
    (schemeProjectiveBundle
      (twistObj k (dualEndSpace k V) (constantModule k (dualEndSpace k V) V) ((1 : ℕ) : ℤ))
      (isQuasicoherentPieces_of_isQuasicoherent _)).scheme.Opens

AlgebraicGeometry.ProjectiveSpaceOfModule.universalEndSheafProjection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/UniversalFamilyOverProjectiveSpace.lean, line 494. The attribute's comment: “r_ψ : U(ψ) → 𝐏(V ⊗ 𝒪_𝐏) over the projective parameter space 𝐏 = 𝐏(Eᵛ); the target 𝐏(V ⊗ 𝒪_𝐏) is identified with the displayed 𝐏 × 𝐏(V) over 𝐏, but the source 𝐏(V ⊗ 𝒪_𝐏(1)) is not, that being Tag 02NC over a base scheme, so r_ψ is not yet a partially defined self-map of one scheme”.

The universal family of projective transformations over the projective parameter space, 𝐏(V ⊗ 𝒪_𝐏(1)) ⊇ U(ψ) --r_ψ--> 𝐏(V ⊗ 𝒪_𝐏): the partially defined morphism of relative projective spaces that Tag 07ZG attaches to Sym ψ.

def universalEndSheafProjection :
    (universalEndSheafDomain k V).toScheme ⟶
      (schemeProjectiveBundle (constantModule k (dualEndSpace k V) V)
        (isQuasicoherentPieces_of_isQuasicoherent _)).scheme

AlgebraicGeometry.ProjectiveSpaceOfModule.universalEndSheafProjection_comp_toBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/UniversalFamilyOverProjectiveSpace.lean, line 503. The attribute's comment: “the universal family over 𝐏 = 𝐏(Eᵛ) is a morphism over 𝐏”.

The universal family is a family over the parameter space 𝐏: r_ψ is a morphism over 𝐏, so it is a family of maps of the fibres and not merely a morphism of schemes.

theorem universalEndSheafProjection_comp_toBase :
    universalEndSheafProjection k V ≫
        schemeProjectiveBundleToBase (constantModule k (dualEndSpace k V) V)
          (isQuasicoherentPieces_of_isQuasicoherent _) =
      (universalEndSheafDomain k V).ι ≫
        schemeProjectiveBundleToBase
          (twistObj k (dualEndSpace k V)
            (constantModule k (dualEndSpace k V) V) ((1 : ℕ) : ℤ))
          (isQuasicoherentPieces_of_isQuasicoherent _)

AlgebraicGeometry.ProjectiveSpaceOfModule.exists_iso_pullback_universalEndTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/UniversalFamilyProductSpace.lean, line 176. The attribute's comment: “the identification 𝐏(V ⊗ 𝒪_𝐏) = 𝐏 × 𝐏(V) over the projective parameter space 𝐏 = 𝐏(Eᵛ), the target of r_ψ; the second factor is the projective bundle of Ṽ over Spec k”.

The target of Tag 0B2W's universal family is the product 𝐏 × 𝐏(V). The relative projective space 𝐏(V ⊗ 𝒪_𝐏) over the projective parameter space 𝐏 = 𝐏(Eᵛ) is the fibre product of 𝐏 with the projective space of V over Spec k, by an isomorphism over 𝐏.

This is the first of the two identifications Tag 0B2W's display uses, and it is the base change of a relative homogeneous spectrum (Tag 01O3) along the structure morphism of 𝐏, which is not an affine morphism and over which nothing is assumed.

public theorem exists_iso_pullback_universalEndTarget :
    ∃ e : (Stacks.SymGraded.schemeProjectiveBundle
          (constantModule k (dualEndSpace k V) V)
          (Stacks.SymGraded.isQuasicoherentPieces_of_isQuasicoherent _)).scheme ≅
        pullback (projectiveSpaceOfModuleToSpec k (dualEndSpace k V))
          (Stacks.SymGraded.schemeProjectiveBundle
            (AlgebraicGeometry.tilde (ModuleCat.of (CommRingCat.of k) V))
            (Stacks.SymGraded.isQuasicoherentPieces_of_isQuasicoherent _)).toBase,
      e.hom ≫ pullback.fst (projectiveSpaceOfModuleToSpec k (dualEndSpace k V))
          (Stacks.SymGraded.schemeProjectiveBundle
            (AlgebraicGeometry.tilde (ModuleCat.of (CommRingCat.of k) V))
            (Stacks.SymGraded.isQuasicoherentPieces_of_isQuasicoherent _)).toBase =
        (Stacks.SymGraded.schemeProjectiveBundle
          (constantModule k (dualEndSpace k V) V)
          (Stacks.SymGraded.isQuasicoherentPieces_of_isQuasicoherent _)).toBase

AlgebraicGeometry.ProjectiveSpaceOfModule.exists_isPullback_universalEndTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/UniversalFamilyProductSpace.lean, line 204. The attribute's comment: “the identification 𝐏(V ⊗ 𝒪_𝐏) = 𝐏 × 𝐏(V) as a cartesian square over Spec k, the affine-cone product identification carried over to the projective parameter space 𝐏 = 𝐏(Eᵛ)”.

The target of Tag 0B2W's universal family is the product 𝐏 × 𝐏(V), as a cartesian square. The projection of 𝐏(V ⊗ 𝒪_𝐏) to 𝐏, the comparison with the projective space of V over Spec k and the two structure morphisms form a cartesian square.

This is the statement AlgebraicGeometry.ProjectiveSpaceOfModule.isPullback_universalFamilySpace over the projective parameter space 𝐏 instead of over the affine cone 𝔸(E).

public theorem exists_isPullback_universalEndTarget :
    ∃ q : (Stacks.SymGraded.schemeProjectiveBundle
          (constantModule k (dualEndSpace k V) V)
          (Stacks.SymGraded.isQuasicoherentPieces_of_isQuasicoherent _)).scheme ⟶
        (Stacks.SymGraded.schemeProjectiveBundle
          (AlgebraicGeometry.tilde (ModuleCat.of (CommRingCat.of k) V))
          (Stacks.SymGraded.isQuasicoherentPieces_of_isQuasicoherent _)).scheme,
      IsPullback (Stacks.SymGraded.schemeProjectiveBundle
          (constantModule k (dualEndSpace k V) V)
          (Stacks.SymGraded.isQuasicoherentPieces_of_isQuasicoherent _)).toBase q
        (projectiveSpaceOfModuleToSpec k (dualEndSpace k V))
        (Stacks.SymGraded.schemeProjectiveBundle
          (AlgebraicGeometry.tilde (ModuleCat.of (CommRingCat.of k) V))
          (Stacks.SymGraded.isQuasicoherentPieces_of_isQuasicoherent _)).toBase

AlgebraicGeometry.ProjectiveSpaceOfModule.exists_iso_pullback_universalEndTarget_comp_toBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/UniversalFamilyProductSpace.lean, line 228. The attribute's comment: “r_ψ followed by the identification of its target with 𝐏 × 𝐏(V) is a morphism over 𝐏, the first projection of the product”.

The universal family is a family over 𝐏 read on the product. Composing AlgebraicGeometry.ProjectiveSpaceOfModule.universalEndSheafProjection_comp_toBase with the identification of the target with 𝐏 × 𝐏(V): the first projection of the product, pulled back along r_ψ and the identification, is the projection of U(ψ) to 𝐏.

public theorem exists_iso_pullback_universalEndTarget_comp_toBase :
    ∃ e : (Stacks.SymGraded.schemeProjectiveBundle
          (constantModule k (dualEndSpace k V) V)
          (Stacks.SymGraded.isQuasicoherentPieces_of_isQuasicoherent _)).scheme ≅
        pullback (projectiveSpaceOfModuleToSpec k (dualEndSpace k V))
          (Stacks.SymGraded.schemeProjectiveBundle
            (AlgebraicGeometry.tilde (ModuleCat.of (CommRingCat.of k) V))
            (Stacks.SymGraded.isQuasicoherentPieces_of_isQuasicoherent _)).toBase,
      (universalEndSheafProjection k V ≫ e.hom) ≫
          pullback.fst (projectiveSpaceOfModuleToSpec k (dualEndSpace k V))
            (Stacks.SymGraded.schemeProjectiveBundle
              (AlgebraicGeometry.tilde (ModuleCat.of (CommRingCat.of k) V))
              (Stacks.SymGraded.isQuasicoherentPieces_of_isQuasicoherent _)).toBase =
        (universalEndSheafDomain k V).ι ≫
          Stacks.SymGraded.schemeProjectiveBundleToBase
            (twistObj k (dualEndSpace k V)
              (constantModule k (dualEndSpace k V) V) ((1 : ℕ) : ℤ))
            (Stacks.SymGraded.isQuasicoherentPieces_of_isQuasicoherent _)

AlgebraicGeometry.ProjectiveSpaceOfModule.exists_iso_universalEndFamily_selfMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/UniversalFamilySelfMap.lean, line 144. The attribute's comment: “the universal family of projective transformations as the displayed partially defined self-map of 𝐏 × 𝐏(V): both total spaces identified with the product over 𝐏, U(ψ) as an open subscheme of the product, and r_ψ as a morphism of the product over 𝐏”.

[Stacks, Tag 0B2W]. The universal family of projective transformations of a finite-dimensional vector space V over a field k, read as the partially defined self-map

𝐏 × 𝐏(V) ⊇ U(ψ) --r_ψ--> 𝐏 × 𝐏(V)

of the product of the parameter space 𝐏 = 𝐏(Eᵛ), E = End(V), with the projective space of V, as the source displays it.

Both total spaces of the family built in AlgebraicGeometry.ProjectiveSpaceOfModule.universalEndSheafProjection — the twisted 𝐏(V ⊗ 𝒪_𝐏(1)) and the untwisted 𝐏(V ⊗ 𝒪_𝐏) — are isomorphic to 𝐏 × 𝐏(V) by isomorphisms over 𝐏; under the first of them the domain of definition U(ψ) becomes an open subscheme of 𝐏 × 𝐏(V), and r_ψ, read through the second, is a morphism from that open subscheme to 𝐏 × 𝐏(V) over 𝐏, hence a family of partially defined self-maps of 𝐏(V) indexed by 𝐏.

theorem exists_iso_universalEndFamily_selfMap :
    ∃ (α : (schemeProjectiveBundle (twistObj k (dualEndSpace k V)
          (constantModule k (dualEndSpace k V) V) ((1 : ℕ) : ℤ))
          (isQuasicoherentPieces_of_isQuasicoherent _)).scheme ≅ universalProductSpace k V)
      (β : (schemeProjectiveBundle (constantModule k (dualEndSpace k V) V)
          (isQuasicoherentPieces_of_isQuasicoherent _)).scheme ≅ universalProductSpace k V),
      α.hom ≫ universalProductToParam k V =
          schemeProjectiveBundleToBase (twistObj k (dualEndSpace k V)
            (constantModule k (dualEndSpace k V) V) ((1 : ℕ) : ℤ))
            (isQuasicoherentPieces_of_isQuasicoherent _) ∧
        β.hom ≫ universalProductToParam k V =
          schemeProjectiveBundleToBase (constantModule k (dualEndSpace k V) V)
            (isQuasicoherentPieces_of_isQuasicoherent _) ∧
        IsOpenImmersion ((universalEndSheafDomain k V).ι ≫ α.hom) ∧
        (universalEndSheafProjection k V ≫ β.hom) ≫ universalProductToParam k V =
          ((universalEndSheafDomain k V).ι ≫ α.hom) ≫ universalProductToParam k V

Tag 0B1S, a lemma

Tag 0B1S in the Stacks Project.

AlgebraicGeometry.ProjectiveSpaceOfModule.exists_isOpen_forall_closedPoint_line_isGood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/GeneralLineProperIntersection.lean, line 279. The attribute's comment: “both clauses (1) X ⊆ U(g) and (2) g(X) intersects Y properly, along a general line through [id_V]; 'general' is read as in Tag 0B2T, namely that there is a nonempty Zariski open subset of the parameter space 𝐏 = 𝐏((End V)ᵛ) each of whose closed points lies with [id_V] on such a line; carrying as hypotheses that the bad locus is an irreducible closed subset of 𝐏 (stronger than the source's 'B is closed', irreducibility being what the formalization of Tag 0B2T asks of it) of codimension at least two (the source's dim(B) ≤ dim(𝐏) - 2), which together are everything the source's proof establishes between those two steps and need the family of projective transformations over 𝐏 in the source's product form 𝐏 × 𝐏(V), which is not available: the family over 𝐏 itself is AlgebraicGeometry.ProjectiveSpaceOfModule.universalEndSheafProjection, but neither of its total spaces is identified with 𝐏 × 𝐏(V) and its fibre over [g] is not compared with r_g; the source's own '[id_V] ∉ B by assumption' is proved rather than carried; clause (2) is the dimension criterion defining Tag 0AZQ read on the image set r_g(X), which agrees with IntersectProperly whenever that image is the underlying set of a closed subvariety; the hypotheses X ≠ 𝐏(V) and X ∩ Y ≠ ∅ are recorded and unused, entering only the carried steps”.

Stacks Project, Tag 0B1S. With X, Y closed subvarieties of 𝐏(V) which intersect properly, X ≠ 𝐏(V) and X ∩ Y ≠ ∅, suppose the bad locus in the parameter space 𝐏 = 𝐏((End V)ᵛ) is a closed subvariety B of codimension at least two. Then for a general line ℓ ⊆ 𝐏 through [id_V] — that is, for a line through [id_V] and any closed point of a nonempty Zariski open subset of 𝐏 — every representative g of every closed point of ℓ satisfies X ⊆ U(g) and makes r_g(X) intersect Y properly.

public theorem exists_isOpen_forall_closedPoint_line_isGood [Nontrivial V]
    (X Y : IrreducibleCloseds (projectiveSpaceOfModule k V)) (hXY : IntersectProperly X Y)
    (_hXne : (X : Set (projectiveSpaceOfModule k V)) ≠ Set.univ)
    (_hXYne : ((X : Set (projectiveSpaceOfModule k V)) ∩
      (Y : Set (projectiveSpaceOfModule k V))).Nonempty)
    (B : IrreducibleCloseds (projectiveSpaceOfModule k (ParameterModule k V)))
    (hB : (B : Set (projectiveSpaceOfModule k (ParameterModule k V))) =
      badParameterLocus k V (X : Set (projectiveSpaceOfModule k V))
        (Y : Set (projectiveSpaceOfModule k V)))
    (hcodim : (2 : ℕ∞) ≤ codimension B) :
    ∃ U : Set (projectiveSpaceOfModule k (ParameterModule k V)), IsOpen U ∧ U.Nonempty ∧
      ∀ q ∈ U, IsClosed ({q} : Set (projectiveSpaceOfModule k (ParameterModule k V))) →
        ∃ L : Submodule k (ParameterModule k V),
          Module.finrank k (ParameterModule k V ⧸ L) = 2 ∧
          identityParameterPoint k V ∈ linearSubspace k (ParameterModule k V) L ∧
          q ∈ linearSubspace k (ParameterModule k V) L ∧
          ∀ p : ClosedPoints k (ParameterModule k V),
            (p : projectiveSpaceOfModule k (ParameterModule k V)) ∈
              linearSubspace k (ParameterModule k V) L →
            ∀ g : V →ₗ[k] V, RepresentsParameterPoint k V p g →
              IsGoodEndomorphism k V (X : Set (projectiveSpaceOfModule k V))
                (Y : Set (projectiveSpaceOfModule k V)) g

AlgebraicGeometry.ProjectiveSpaceOfModule.exists_isOpen_closedPoint_line_isGood_of_codimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/GeneralLineProperIntersectionOfCodimension.lean, line 232. The attribute's comment: “both clauses (1) X ⊆ U(g) and (2) g(X) intersects Y properly, along a general line through [id_V], in the form that assumes a bound on the bad locus: 'general' is read as in Tag 0B2T, namely that there is a nonempty Zariski open subset of the parameter space 𝐏 = 𝐏((End V)ᵛ) each of whose closed points lies with [id_V] on such a line, and clause (2) is the dimension criterion defining Tag 0AZQ read on the image set r_g(X), which agrees with IntersectProperly whenever that image is the underlying set of a closed subvariety. The bad-locus bound is discharged, and the tag registered for both clauses at the source's own hypotheses alone, by AlgebraicGeometry.ProjectiveSpaceOfModule.exists_isOpen_forall_closedPoint_line_isGood of StacksFrontier.AlgebraicGeometry.Intersection.Projections.TransitionDominant; this form keeps its place here, upstream of the incidence-correspondence construction that the discharge needs”.

Stacks Project, Tag 0B1S. With X, Y closed subvarieties of 𝐏(V) which intersect properly, X ≠ 𝐏(V) and X ∩ Y ≠ ∅, suppose the bad locus in the parameter space 𝐏 = 𝐏((End V)ᵛ) is contained in a closed subset B of 𝐏 which has codimension at least two at each of its points and does not contain [id_V]. Then for a general line ℓ ⊆ 𝐏 through [id_V] — that is, for a line through [id_V] and any closed point of a nonempty Zariski open subset of 𝐏 — every representative g of every closed point of ℓ satisfies X ⊆ U(g) and makes r_g(X) intersect Y properly.

Containment and not equality, together with [id_V] ∉ B: that is all the genericity argument uses, and it is what the clause-(1) and clause-(2) loci of …ProjectiveSpaceOfModule.exists_isClosed_two_le_codimension_badParameterLocus_subset supply — their union is a superset of the bad locus, the codimension bound being available only there. With the equality [id_V] ∉ B would follow from [id_V] being closed and good, so the hypothesis is stated separately; the proper intersection of X and Y, which is what makes [id_V] good, is accordingly recorded and not used.

B is not asked to be irreducible: that strengthening is unsatisfiable for some admissible pairs, by AlgebraicGeometry.ProjectiveSpaceOfModule.not_exists_irreducible_badParameterLocus.

public theorem exists_isOpen_closedPoint_line_isGood_of_codimension [Nontrivial V]
    (X Y : IrreducibleCloseds (projectiveSpaceOfModule k V)) (_hXY : IntersectProperly X Y)
    (hXne : (X : Set (projectiveSpaceOfModule k V)) ≠ Set.univ)
    (_hXYne : ((X : Set (projectiveSpaceOfModule k V)) ∩
      (Y : Set (projectiveSpaceOfModule k V))).Nonempty)
    (B : Set (projectiveSpaceOfModule k (ParameterModule k V))) (hBc : IsClosed B)
    (hB : ∀ p : ClosedPoints k (ParameterModule k V),
      (p : projectiveSpaceOfModule k (ParameterModule k V)) ∈
          badParameterLocus k V (X : Set (projectiveSpaceOfModule k V))
            (Y : Set (projectiveSpaceOfModule k V)) →
        (p : projectiveSpaceOfModule k (ParameterModule k V)) ∈ B)
    (hBid : identityParameterPoint k V ∉ B)
    (hcodim : ∀ x ∈ B, (2 : ℕ∞) ≤ codimension (IrreducibleCloseds.closureSingleton x)) :
    ∃ U : Set (projectiveSpaceOfModule k (ParameterModule k V)), IsOpen U ∧ U.Nonempty ∧
      ∀ q ∈ U, IsClosed ({q} : Set (projectiveSpaceOfModule k (ParameterModule k V))) →
        ∃ L : Submodule k (ParameterModule k V),
          Module.finrank k (ParameterModule k V ⧸ L) = 2 ∧
          identityParameterPoint k V ∈ linearSubspace k (ParameterModule k V) L ∧
          q ∈ linearSubspace k (ParameterModule k V) L ∧
          ∀ p : ClosedPoints k (ParameterModule k V),
            (p : projectiveSpaceOfModule k (ParameterModule k V)) ∈
              linearSubspace k (ParameterModule k V) L →
            ∀ g : V →ₗ[k] V, RepresentsParameterPoint k V p g →
              IsGoodEndomorphism k V (X : Set (projectiveSpaceOfModule k V))
                (Y : Set (projectiveSpaceOfModule k V)) g

AlgebraicGeometry.ProjectiveSpaceOfModule.exists_isOpen_forall_closedPoint_line_isGood_of_intersectProperly, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/TransitionDominant.lean, line 778. The attribute's comment: “both clauses (1) X ⊆ U(g) and (2) g(X) intersects Y properly, along a general line through [id_V]; 'general' is read as in Tag 0B2T, namely that there is a nonempty Zariski open subset of the parameter space 𝐏 = 𝐏((End V)ᵛ) each of whose closed points lies with [id_V] on such a line; clause (2) is the dimension criterion defining Tag 0AZQ read on the image set r_g(X), which agrees with IntersectProperly whenever that image is the underlying set of a closed subvariety”.

Stacks Project, Tag 0B1S. Let X, Y be closed subvarieties of 𝐏(V) which intersect properly, with X ≠ 𝐏(V) and X ∩ Y ≠ ∅. Then for a general line ℓ ⊆ 𝐏 = 𝐏((End V)ᵛ) through [id_V] — that is, for a line through [id_V] and any closed point of a nonempty Zariski open subset of 𝐏 — every representative g of every closed point of ℓ satisfies

• clause (1) X ⊆ U(g), so that r_g is defined on the whole of X, and
• clause (2) r_g(X) intersects Y properly,

both being the predicate AlgebraicGeometry.ProjectiveSpaceOfModule.IsGoodEndomorphism.

The hypotheses are exactly the source's, and all three do work: X ≠ 𝐏(V) gives 2 ≤ dim_k V, which is what makes the determinant hypersurface a proper closed subset of 𝐏 (at dim_k V = 1 it is the whole of 𝐏); X ∩ Y ≠ ∅ together with the proper intersection gives dim 𝐏(V) ≤ dim X + dim Y, which is what makes r_g(X) meet Y at all and hence the projection of the incidence correspondence to 𝐏 surjective (without it, two disjoint lines in 𝐏³ satisfy IntersectProperly vacuously and the conclusion fails).

public theorem exists_isOpen_forall_closedPoint_line_isGood_of_intersectProperly
    (X Y : IrreducibleCloseds (projectiveSpaceOfModule k V)) (hXY : IntersectProperly X Y)
    (hXne : (X : Set (projectiveSpaceOfModule k V)) ≠ Set.univ)
    (hXYne : ((X : Set (projectiveSpaceOfModule k V)) ∩
      (Y : Set (projectiveSpaceOfModule k V))).Nonempty) :
    ∃ U : Set (projectiveSpaceOfModule k (ParameterModule k V)), IsOpen U ∧ U.Nonempty ∧
      ∀ q ∈ U, IsClosed ({q} : Set (projectiveSpaceOfModule k (ParameterModule k V))) →
        ∃ L : Submodule k (ParameterModule k V),
          Module.finrank k (ParameterModule k V ⧸ L) = 2 ∧
          identityParameterPoint k V ∈ linearSubspace k (ParameterModule k V) L ∧
          q ∈ linearSubspace k (ParameterModule k V) L ∧
          ∀ p : ClosedPoints k (ParameterModule k V),
            (p : projectiveSpaceOfModule k (ParameterModule k V)) ∈
              linearSubspace k (ParameterModule k V) L →
            ∀ g : V →ₗ[k] V, RepresentsParameterPoint k V p g →
              IsGoodEndomorphism k V (X : Set (projectiveSpaceOfModule k V))
                (Y : Set (projectiveSpaceOfModule k V)) g

Sources

• Section 43.23, Tag 0B1N
• AxiomMath/Stacks at 5ed82d14

LeanclosedPointsEquivDual · pointSubmodule · projection · coe_mapDomain_pointSubmodule · AlgebraicGeometry.ProjectiveSpaceOfModule.exists_isOpen_isFinite_projection_restrict · AlgebraicGeometry.ProjectiveSpaceOfModule.exists_isOpen_projection_isClosedImmersion_and_etaleAt · AlgebraicGeometry.ProjectiveSpaceOfModule.exists_isOpen_forall_closedPoint_projection_restrict · AlgebraicGeometry.ProjectiveSpaceOfModule.exists_isOpen_inter_projectionCone_eq

Section43.24 Moving Lemma#

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

Tag 0B0E, a lemma

Tag 0B0E in the Stacks Project.

AlgebraicGeometry.ProjectiveSpaceOfModule.exists_intersectProperly_torFormulaCycleIntersectionProduct_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/MovingLemma/KeyLemma.lean, line 1024. The attribute's comment: “the whole lemma. X ⊂ 𝐏^N is read as ⊆, so dim X = N is covered: there X is the whole of 𝐏(V) and the conclusion holds with C = Z and an empty family of Z_j, which is the empty case of the source's chain of projections. The non-strict dimension clause is registered in the disjunctive form dim (Z_j ∩ T_i) ≤ dim (Z ∩ T_i) ∨ dim (Z_j ∩ T_i) + n ≤ d + d' — written additively because WithBot ℕ∞ has no subtraction — which is what condition (4) of the source's proof yields and which implies the source's own first inequality wherever Tag 0AZP makes it true, namely whenever Z ∩ T_i is nonempty; in the bottom case Z ∩ T_i = ∅ the source's first inequality is refuted by a nonsingular quadric surface in 𝐏^3 with Z and T_1 two distinct lines of one ruling, written out in this module's implementation notes, and the second disjunct is what holds there. The strict clause is as the source has it, and is vacuous exactly on that bottom case”.

Stacks Project, Tag 0B0E. Let X ⊆ 𝐏(V) be a nonsingular closed subvariety of dimension n of the projective space of a vector space of dimension N + 1 over an algebraically closed field; let Z ⊆ X be a closed subvariety of dimension d < n, and let T_i ⊆ X be finitely many closed subvarieties of dimension d' < n. Then there is a closed subvariety C ⊆ 𝐏(V) whose prime cycle intersects that of X properly, with

C · X = [Z] + ∑ m_j [Z_j]

in the Tor-formula intersection product of Section 0B08, where the Z_j ⊆ X are irreducible closed of dimension d, distinct from Z, with nonzero multiplicities, and where

• dim (Z_j ∩ T_i) ≤ dim (Z ∩ T_i) or dim (Z_j ∩ T_i) + n ≤ d + d', and
• dim (Z_j ∩ T_i) < dim (Z ∩ T_i) whenever Z does not intersect T_i properly inside X.

The first clause is the disjunction that condition (4) of the source's proof yields; its first disjunct is the source's own inequality, which Tag 0AZP supplies from the second whenever Z ∩ T_i is nonempty, and which alone would be false in the bottom case Z ∩ T_i = ∅ — see the quadric-surface counterexample in the implementation notes of this module. The second clause is vacuous exactly on that bottom case and needs no guard.

public theorem exists_intersectProperly_torFormulaCycleIntersectionProduct_eq
    (k V : Type u) [Field k] [IsAlgClosed k] [AddCommGroup V] [Module k V]
    [FiniteDimensional k V] [Nontrivial V] [DecidableEq (projectiveSpaceOfModule k V)]
    {N n d d' : ℕ} (hV : Module.finrank k V = N + 1)
    {X : Scheme.{u}} (iX : X ⟶ projectiveSpaceOfModule k V) [IsClosedImmersion iX]
    [IsVariety k (iX ≫ projectiveSpaceOfModuleToSpec k V)] (hXreg : IsRegular X)
    (hdimX : topologicalKrullDim X = (n : WithBot ℕ∞))
    (hd : d < n) (hd' : d' < n)
    (Z : Set X) (hZcl : IsClosed Z) (hZirr : IsIrreducible Z)
    (hZd : topologicalKrullDim ↥Z = (d : WithBot ℕ∞))
    {ι : Type*} [Finite ι] (T : ι → Set X) (hTcl : ∀ i, IsClosed (T i))
    (hTirr : ∀ i, IsIrreducible (T i))
    (hTd : ∀ i, topologicalKrullDim ↥(T i) = (d' : WithBot ℕ∞))
    (XC ZC : IrreducibleCloseds (projectiveSpaceOfModule k V))
    (TC : ι → IrreducibleCloseds (projectiveSpaceOfModule k V))
    (hXC : (XC : Set (projectiveSpaceOfModule k V)) = Set.range iX.base)
    (hZC : (ZC : Set (projectiveSpaceOfModule k V)) = iX.base '' Z)
    (hTC : ∀ i, (TC i : Set (projectiveSpaceOfModule k V)) = iX.base '' (T i)) :
    ∃ (C : IrreducibleCloseds (projectiveSpaceOfModule k V))
      (S : Finset (IrreducibleCloseds (projectiveSpaceOfModule k V)))
      (m : IrreducibleCloseds (projectiveSpaceOfModule k V) → ℤ),
      AlgebraicCycle.IntersectProperly
          (Function.locallyFinsuppWithin.single C.isIrreducible.genericPoint (1 : ℤ))
          (Function.locallyFinsuppWithin.single XC.isIrreducible.genericPoint (1 : ℤ)) ∧
        TorFormula.torFormulaCycleIntersectionProduct (fieldChowSituation k)
            (projectiveSpaceOfModuleToSpec k V) (isRegular_projectiveSpaceOfModule k V) (d : ℤ)
            (Function.locallyFinsuppWithin.single C.isIrreducible.genericPoint (1 : ℤ))
            (Function.locallyFinsuppWithin.single XC.isIrreducible.genericPoint (1 : ℤ)) =
          Function.locallyFinsuppWithin.single ZC.isIrreducible.genericPoint (1 : ℤ) +
            ∑ W ∈ S, m W • Function.locallyFinsuppWithin.single
              W.isIrreducible.genericPoint (1 : ℤ) ∧
        ZC ∉ S ∧ (∀ W ∈ S, m W ≠ 0) ∧
        (∀ W ∈ S, (W : Set (projectiveSpaceOfModule k V)) ⊆
          (XC : Set (projectiveSpaceOfModule k V))) ∧
        (∀ W ∈ S, topologicalKrullDim (W : Set (projectiveSpaceOfModule k V)) =
          (d : WithBot ℕ∞)) ∧
        (∀ W ∈ S, ∀ i,
          topologicalKrullDim ↥((W : Set (projectiveSpaceOfModule k V)) ∩
                (TC i : Set (projectiveSpaceOfModule k V))) ≤
              topologicalKrullDim ↥((ZC : Set (projectiveSpaceOfModule k V)) ∩
                (TC i : Set (projectiveSpaceOfModule k V))) ∨
            topologicalKrullDim ↥((W : Set (projectiveSpaceOfModule k V)) ∩
                  (TC i : Set (projectiveSpaceOfModule k V))) + (n : WithBot ℕ∞) ≤
              (d : WithBot ℕ∞) + (d' : WithBot ℕ∞)) ∧
        (∀ W ∈ S, ∀ i,
          ¬ (topologicalKrullDim ↥((ZC : Set (projectiveSpaceOfModule k V)) ∩
                  (TC i : Set (projectiveSpaceOfModule k V))) +
                topologicalKrullDim (XC : Set (projectiveSpaceOfModule k V)) ≤
              topologicalKrullDim (ZC : Set (projectiveSpaceOfModule k V)) +
                topologicalKrullDim (TC i : Set (projectiveSpaceOfModule k V))) →
            topologicalKrullDim ↥((W : Set (projectiveSpaceOfModule k V)) ∩
                (TC i : Set (projectiveSpaceOfModule k V))) <
              topologicalKrullDim ↥((ZC : Set (projectiveSpaceOfModule k V)) ∩
                (TC i : Set (projectiveSpaceOfModule k V))))

Tag 0B1T, a lemma

Tag 0B1T in the Stacks Project.

AlgebraicGeometry.ProjectiveSpaceOfModule.endProjectionImage_eq_of_represents_identity, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/MovingLemma.lean, line 183. The attribute's comment: “clause (2), C'_0 = C, in the fibrewise form of this module: the fibre of the family over 0 = [id_V] is r_g(C) for g a representative of [id_V], and that translate is C itself; the family C' and hence the scheme-theoretic reading of the equality are not constructed, see the implementation notes”.

Clause (2) of the Moving Lemma: the fibre over 0 is C. Every endomorphism representing the point [id_V] of the parameter space is a unit scalar multiple of the identity, so the translate it induces is the identity on subsets of 𝐏(V).

public theorem endProjectionImage_eq_of_represents_identity [Nontrivial V]
    {p : ClosedPoints k (ParameterModule k V)}
    (hp : (p : projectiveSpaceOfModule k (ParameterModule k V)) = identityParameterPoint k V)
    {g : V →ₗ[k] V} (hg : RepresentsParameterPoint k V p g)
    (S : Set (projectiveSpaceOfModule k V)) :
    endProjectionImage k V g S = S

AlgebraicGeometry.ProjectiveSpaceOfModule.exists_movingFamily_of_subvariety_fixed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/MovingLemmaFixedPoints.lean, line 172. The attribute's comment: “the whole lemma, at the source's hypotheses and no others, over the source's fixed 𝐏^1 with its fixed points: C a closed subvariety of 𝐏^N = 𝐏(V) (an irreducible closed subset with its reduced structure), X a subvariety of 𝐏^N (an irreducible locally closed subset, not necessarily closed), T i ⊆ X finitely many closed subvarieties of X (irreducible, closed in X), C and X intersecting properly; for every projective line 𝐏^1 = 𝐏(W), dim_k W = 2, and every pair of distinct closed points 0, ∞ of it, a closed subvariety C' of 𝐏^1 × 𝐏^N with (1) C' → 𝐏^1 dominant, read as density of the image; (2) C'_0 = C scheme theoretically: the ideal sheaf of the reduced closed subscheme on C' pulled back along the section of 𝐏^1 × 𝐏^N → 𝐏^N at 0 is the ideal sheaf of the reduced closed subscheme on C; (3) C' and X × 𝐏^1 intersect properly; (4) C'_∞ intersects each T i properly. Proper intersection is the dimension criterion of Definition 0AZQ read on the subsets”.

Stacks Project, Tag 0B1T, over a given projective line with given points 0 ≠ ∞. Let C be a closed subvariety of 𝐏^N = 𝐏(V), X a subvariety of 𝐏^N (irreducible and locally closed, not necessarily closed), T i ⊆ X finitely many closed subvarieties of X, and assume C and X intersect properly. Let 𝐏^1 = 𝐏(W), dim_k W = 2, and let 0 ≠ ∞ be closed points of it. Then there is a closed subvariety C' of 𝐏^1 × 𝐏^N such that

1. C' → 𝐏^1 is dominant;
2. C'_0 = C scheme theoretically;
3. C' and X × 𝐏^1 intersect properly;
4. C'_∞ properly intersects each T i.

Proper intersection is the dimension criterion of Definition 0AZQ read on the subsets. The instance Nontrivial W is implied by dim_k W = 2 and is there only because the products and sections of 𝐏(W) are stated under it. The family of AlgebraicGeometry.ProjectiveSpaceOfModule.exists_movingFamily_of_subvariety is transported along an isomorphism of projective lines carrying its points to the given ones.

public theorem exists_movingFamily_of_subvariety_fixed
    (C : IrreducibleCloseds (projectiveSpaceOfModule k V))
    (X : Set (projectiveSpaceOfModule k V)) (hX : IsLocallyClosed X) (hXirr : IsIrreducible X)
    (hCX : topologicalKrullDim ↥((C : Set (projectiveSpaceOfModule k V)) ∩ X) +
        topologicalKrullDim (projectiveSpaceOfModule k V) ≤
      topologicalKrullDim ↥(C : Set (projectiveSpaceOfModule k V)) + topologicalKrullDim ↥X)
    {ι : Type*} [Finite ι] (T : ι → Set (projectiveSpaceOfModule k V))
    (hTX : ∀ i, T i ⊆ X) (hTc : ∀ i, IsClosed {x : X | x.1 ∈ T i})
    (hTirr : ∀ i, IsIrreducible (T i))
    (W : Type u) [AddCommGroup W] [Module k W] [FiniteDimensional k W] [Nontrivial W]
    (hW : Module.finrank k W = 2) (zero infty : projectiveSpaceOfModule k W)
    (hzero : IsClosed ({zero} : Set (projectiveSpaceOfModule k W)))
    (hinfty : IsClosed ({infty} : Set (projectiveSpaceOfModule k W))) (hne : zero ≠ infty) :
    ∃ Cfam : IrreducibleCloseds (lineProduct k V W),
      closure ((lineProductLine k V W).base '' (Cfam : Set (lineProduct k V W))) = Set.univ ∧
      (Scheme.IdealSheafData.vanishingIdeal
            (⟨Cfam, Cfam.isClosed'⟩ : Closeds (lineProduct k V W))).comap
          (lineProductSection k V W zero hzero) =
        Scheme.IdealSheafData.vanishingIdeal
          (⟨C, C.isClosed'⟩ : Closeds (projectiveSpaceOfModule k V)) ∧
      topologicalKrullDim ↥((Cfam : Set (lineProduct k V W)) ∩ lineProductConstant k V W X) +
          topologicalKrullDim (lineProduct k V W) ≤
        topologicalKrullDim ↥(Cfam : Set (lineProduct k V W)) +
          topologicalKrullDim ↥(lineProductConstant k V W X) ∧
      ∀ i, topologicalKrullDim
            ↥(lineProductFibre k V W infty hinfty (Cfam : Set (lineProduct k V W)) ∩ T i) +
          topologicalKrullDim (projectiveSpaceOfModule k V) ≤
        topologicalKrullDim
            ↥(lineProductFibre k V W infty hinfty (Cfam : Set (lineProduct k V W))) +
          topologicalKrullDim ↥(T i)

AlgebraicGeometry.ProjectiveSpaceOfModule.exists_isOpen_forall_closedPoint_line_moving_of_codimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/Projections/MovingLemmaOfCodimension.lean, line 190. The attribute's comment: “clauses (1), (3) and (4), read on the fibres, in the form that assumes bounds on the two bad loci: 𝐏^1 is the source's own line ℓ ⊆ 𝐏 = 𝐏((End V)ᵛ) through [id_V] and the fibre C'_[g] is the translate r_g(C), so that (1) 'C' → 𝐏^1 is dominant' is read as 'the fibre over every closed point of ℓ is nonempty', (3) as 'r_g(C) intersects X properly for every representative g of every closed point of ℓ' and (4) as 'r_g(C) intersects each T i properly for every representative g of the ∞ point of ℓ'; clause (2) is endProjectionImage_eq_of_represents_identity of this module; 'general' is read as in Tags 0B2T and 0B1S, namely that there is a nonempty Zariski open subset of 𝐏 each of whose closed points is the ∞ point of such a line; proper intersection is the dimension criterion defining Tag 0AZQ read on the image set r_g(C), as in Tag 0B1S; X is taken closed in this form, Lemma 0B1S being formalized for a pair of closed subvarieties. The two bad-locus bounds are discharged by AlgebraicGeometry.ProjectiveSpaceOfModule .exists_isOpen_forall_closedPoint_line_moving_of_intersectProperly of StacksFrontier.AlgebraicGeometry.Intersection.Projections.MovingFamilyMain, and the tag is registered for all four clauses about the family C' over 𝐏^1 at the source's own hypotheses on C, X (not necessarily closed) and the T i, clause (2) scheme theoretically, on AlgebraicGeometry.ProjectiveSpaceOfModule.exists_movingFamily_of_subvariety_fixed of StacksFrontier.AlgebraicGeometry.Intersection.Projections.MovingLemmaFixedPoints; this form keeps its place here, upstream of the incidence-correspondence construction that either discharge needs”.

Stacks Project, Tag 0B1T. Let C, X be closed subvarieties of 𝐏(V) which intersect properly, with C ≠ 𝐏(V) and C ∩ X ≠ ∅, and let T i ⊆ X be a finite collection of closed subvarieties. Suppose the bad locus of (C, X) in the parameter space 𝐏 = 𝐏((End V)ᵛ) is contained in a closed subset B which has codimension at least two at each of its points and does not contain [id_V], and that for each i the bad locus of (C, T i) is contained in a closed subset BT i other than all of 𝐏. Then for a general line ℓ ⊆ 𝐏 through [id_V] — that is, for the line through [id_V] and any closed point ∞ of a nonempty Zariski open subset of 𝐏 — the four clauses of the source hold of the family whose fibre over a point [g] of ℓ is the translate r_g(C): that family is dominant over ℓ, because r_g(C) is nonempty for every representative g of every closed point of ℓ; its fibre over 0 = [id_V] is C; it meets the constant family X × ℓ properly, because r_g(C) meets X properly at every closed point of ℓ; and its fibre over ∞ meets each T i properly.

Both families of hypotheses are carried, this module being upstream of either discharge, which is why Tag 0B1T is registered not here but on the form over 𝐏^1 …ProjectiveSpaceOfModule.exists_movingFamily_of_subvariety_fixed of StacksFrontier.AlgebraicGeometry.Intersection.Projections.MovingLemmaFixedPoints, which states all four clauses about the family itself at the source's hypotheses alone.

public theorem exists_isOpen_forall_closedPoint_line_moving_of_codimension [Nontrivial V]
    (C X : IrreducibleCloseds (projectiveSpaceOfModule k V)) (hCX : IntersectProperly C X)
    (hCne : (C : Set (projectiveSpaceOfModule k V)) ≠ Set.univ)
    (hCXne : ((C : Set (projectiveSpaceOfModule k V)) ∩
      (X : Set (projectiveSpaceOfModule k V))).Nonempty)
    {ι : Type*} [Finite ι] (T : ι → IrreducibleCloseds (projectiveSpaceOfModule k V))
    (_hTX : ∀ i, (T i : Set (projectiveSpaceOfModule k V)) ⊆
      (X : Set (projectiveSpaceOfModule k V)))
    (B : Set (projectiveSpaceOfModule k (ParameterModule k V))) (hBc : IsClosed B)
    (hB : ∀ p : ClosedPoints k (ParameterModule k V),
      (p : projectiveSpaceOfModule k (ParameterModule k V)) ∈
          badParameterLocus k V (C : Set (projectiveSpaceOfModule k V))
            (X : Set (projectiveSpaceOfModule k V)) →
        (p : projectiveSpaceOfModule k (ParameterModule k V)) ∈ B)
    (hBid : identityParameterPoint k V ∉ B)
    (hcodim : ∀ x ∈ B, (2 : ℕ∞) ≤ codimension (IrreducibleCloseds.closureSingleton x))
    (BT : ι → Set (projectiveSpaceOfModule k (ParameterModule k V)))
    (hBT : ∀ i, IsClosed (BT i)) (hBTne : ∀ i, BT i ≠ Set.univ)
    (hBTbad : ∀ (i) (p : ClosedPoints k (ParameterModule k V)),
      (p : projectiveSpaceOfModule k (ParameterModule k V)) ∈
          badParameterLocus k V (C : Set (projectiveSpaceOfModule k V))
            (T i : Set (projectiveSpaceOfModule k V)) →
        (p : projectiveSpaceOfModule k (ParameterModule k V)) ∈ BT i) :
    ∃ U : Set (projectiveSpaceOfModule k (ParameterModule k V)), IsOpen U ∧ U.Nonempty ∧
      ∀ q ∈ U, IsClosed ({q} : Set (projectiveSpaceOfModule k (ParameterModule k V))) →
        ∃ L : Submodule k (ParameterModule k V),
          Module.finrank k (ParameterModule k V ⧸ L) = 2 ∧
          identityParameterPoint k V ∈ linearSubspace k (ParameterModule k V) L ∧
          q ∈ linearSubspace k (ParameterModule k V) L ∧
          (∀ p : ClosedPoints k (ParameterModule k V),
            (p : projectiveSpaceOfModule k (ParameterModule k V)) ∈
              linearSubspace k (ParameterModule k V) L →
            ∀ g : V →ₗ[k] V, RepresentsParameterPoint k V p g →
              (endProjectionImage k V g (C : Set (projectiveSpaceOfModule k V))).Nonempty ∧
                IsGoodEndomorphism k V (C : Set (projectiveSpaceOfModule k V))
                  (X : Set (projectiveSpaceOfModule k V)) g) ∧
          (∀ p : ClosedPoints k (ParameterModule k V),
            (p : projectiveSpaceOfModule k (ParameterModule k V)) =
              identityParameterPoint k V →
            ∀ g : V →ₗ[k] V, RepresentsParameterPoint k V p g →
              endProjectionImage k V g (C : Set (projectiveSpaceOfModule k V)) =
                (C : Set (projectiveSpaceOfModule k V))) ∧
          ∀ p : ClosedPoints k (ParameterModule k V),
            (p : projectiveSpaceOfModule k (ParameterModule k V)) = q →
            ∀ g : V →ₗ[k] V, RepresentsParameterPoint k V p g → ∀ i,
              IsGoodEndomorphism k V (C : Set (projectiveSpaceOfModule k V))
                (T i : Set (projectiveSpaceOfModule k V)) g

Tag 0B1U, a lemma

Tag 0B1U in the Stacks Project.

AlgebraicGeometry.exists_rationallyEquivalent_forall_intersectProperly, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/MovingLemma/MovingCycles.lean, line 97. The attribute's comment: “for a finite family of cycles β i of arbitrary dimensions s i in place of the single s-cycle β, which is the case of a one-element family; r and the s i are arbitrary integers. Nonsingular is IsRegular X, projective variety is IsProjectiveVariety, cycles are the graded cycle groups Stacks.Chow.CycleGroup over Spec k, rational equivalence is Tag 02RW and proper intersection is Definition 0AZQ. The proof replaces the source's degeneration of the cone C in 𝐏^N × 𝐏^1 (Tags 0B1T, 0B1M, 0B07) by the flat pullback along the finite projection π : X → 𝐏^n of the proof of Tag 0B0E, which is flat by miracle flatness, together with moving π(Z) inside 𝐏^n”.

Stacks Project, Tag 0B1U, for a finite family of cycles. Let X be a nonsingular projective variety over an algebraically closed field, let α be an r-cycle on X and let β i be finitely many cycles on X, of dimensions s i. Then there is an r-cycle α' with α' ∼_rat α which intersects every β i properly. This is the case of exists_rationallyEquivalent_forall_intersectProperly_of_isQuasiProjectiveVariety for a projective variety.

public theorem exists_rationallyEquivalent_forall_intersectProperly (k : Type u) [Field k]
    [IsAlgClosed k] {X : Scheme.{u}} (sX : X ⟶ Spec (.of k)) [IsProjectiveVariety k sX]
    (hX : IsRegular X) {r : ℤ} (α : CycleGroup (fieldChowSituation k) sX r)
    {ι : Type*} [Finite ι] (s : ι → ℤ) (β : ∀ i, CycleGroup (fieldChowSituation k) sX (s i)) :
    ∃ α' : CycleGroup (fieldChowSituation k) sX r,
      RationallyEquivalent (fieldChowSituation k) sX r α' α ∧
        ∀ i, AlgebraicCycle.IntersectProperly α'.1 (β i).1

AlgebraicGeometry.exists_rationallyEquivalent_intersectProperly, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/MovingLemma/MovingCycles.lean, line 115. The attribute's comment: “as stated: nonsingular is IsRegular X, projective variety is IsProjectiveVariety, cycles are the graded cycle groups Stacks.Chow.CycleGroup over Spec k, rational equivalence is Tag 02RW and proper intersection is Definition 0AZQ; r and s are arbitrary integers”.

Stacks Project, Tag 0B1U. Let X be a nonsingular projective variety over an algebraically closed field, let α be an r-cycle and β an s-cycle on X. Then there is an r-cycle α' with α' ∼_rat α which intersects β properly.

public theorem exists_rationallyEquivalent_intersectProperly (k : Type u) [Field k]
    [IsAlgClosed k] {X : Scheme.{u}} (sX : X ⟶ Spec (.of k)) [IsProjectiveVariety k sX]
    (hX : IsRegular X) {r s : ℤ} (α : CycleGroup (fieldChowSituation k) sX r)
    (β : CycleGroup (fieldChowSituation k) sX s) :
    ∃ α' : CycleGroup (fieldChowSituation k) sX r,
      RationallyEquivalent (fieldChowSituation k) sX r α' α ∧
        AlgebraicCycle.IntersectProperly α'.1 β.1

Sources

• Section 43.24, Tag 0B0D
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.ProjectiveSpaceOfModule.exists_intersectProperly_torFormulaCycleIntersectionProduct_eq · AlgebraicGeometry.ProjectiveSpaceOfModule.endProjectionImage_eq_of_represents_identity · AlgebraicGeometry.ProjectiveSpaceOfModule.exists_movingFamily_of_subvariety_fixed · AlgebraicGeometry.ProjectiveSpaceOfModule.exists_isOpen_forall_closedPoint_line_moving_of_codimension · AlgebraicGeometry.exists_rationallyEquivalent_forall_intersectProperly · AlgebraicGeometry.exists_rationallyEquivalent_intersectProperly

Section43.25 Intersection products and rational equivalence#

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

Tag 0B60, a lemma

Tag 0B60 in the Stacks Project.

Stacks.Intersection.RationalEquivalence.rationallyEquivalent_intersectionProduct_fibreCycle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/RationalEquivalence/FibreSpecialCase.lean, line 1164. The attribute's comment: “the whole lemma with the fibre cycles in their dimension s, as the proof and Tag 0B1V use it, at the source's own data: X a nonsingular variety over an algebraically closed field (the chapter's convention, Tag 0AZ8) of dimension dX, W ⊆ X × P^1 an integral closed subscheme of dimension s + 1 dominating P^1, a, b closed points of P^1 with fibres W_a, W_b read in X as in Tag 0B07, and V the closure of a point of dimension r with dim (V ∩ W_a) and dim (V ∩ W_b) at most r + s - dX, the proper intersection of Tag 0AZQ written additively. The conclusion is that [V] · [W_a]_s and [V] · [W_b]_s are rationally equivalent (Tag 02RW), the products being those of Tag 0B08 in the integer expected dimension r + s - dX. The source prints [W_a]_r; the fibre has dimension s, and the statement as printed is rationallyEquivalent_intersectionProduct_fibreCycle_dimension_r.”.

Stacks Project, Tag 0B60. Let X be a nonsingular variety over an algebraically closed field, of dimension dX. Let W ⊆ X × ℙ¹ be a closed subvariety of dimension s + 1 dominating ℙ¹, let a, b be closed points of ℙ¹ and let W_a, W_b be the fibres of W over them, viewed as closed subschemes of X. Let V ⊆ X be the closure of a point v, of dimension r, meeting W_a and W_b properly. Then [V] · [W_a]_s ∼_rat [V] · [W_b]_s.

theorem rationallyEquivalent_intersectionProduct_fibreCycle [DecidableEq X] (hX : IsRegular X)
    (dX r s : ℕ) (hdX : topologicalKrullDim X = (dX : WithBot ℕ∞))
    (W : (projectiveLineProduct f).IdealSheafData) [IsIntegral W.subscheme]
    (hW : topologicalKrullDim (W.support : Set (projectiveLineProduct f)) =
      ((s + 1 : ℕ) : WithBot ℕ∞))
    [IsDominant (W.subschemeι ≫
      pullback.snd f (relativeProjectiveLine (Spec (.of k)) ↘ Spec (.of k)))]
    (a b : relativeProjectiveLine (Spec (.of k))) (ha : IsClosed {a}) (hb : IsClosed {b})
    (v : X) (hv : topologicalKrullDim (closure ({v} : Set X)) = (r : WithBot ℕ∞))
    (hVa : topologicalKrullDim (↥(closure ({v} : Set X) ∩
        Set.range (W.comap (closedPointSection k rfl a ha f)).subschemeι)) +
        (dX : WithBot ℕ∞) ≤ ((r + s : ℕ) : WithBot ℕ∞))
    (hVb : topologicalKrullDim (↥(closure ({v} : Set X) ∩
        Set.range (W.comap (closedPointSection k rfl b hb f)).subschemeι)) +
        (dX : WithBot ℕ∞) ≤ ((r + s : ℕ) : WithBot ℕ∞)) :
    letI : IsLocallyNoetherian X := isLocallyNoetherian_of_isRegular hX
    RationallyEquivalent (fieldChowSituation k) f ((r : ℤ) + s - dX)
      ⟨torFormulaCycleIntersectionProduct (fieldChowSituation k) f hX ((r : ℤ) + s - dX)
          (Function.locallyFinsuppWithin.single v 1)
          (cycleAssociatedToClosedSubscheme (fieldChowSituation k) f
            (W.comap (closedPointSection k rfl a ha f)).subschemeι s).1,
        torFormulaCycleIntersectionProduct_mem_cyclesOfDimension
          (fieldChowSituation k) f hX _ _ _⟩
      ⟨torFormulaCycleIntersectionProduct (fieldChowSituation k) f hX ((r : ℤ) + s - dX)
          (Function.locallyFinsuppWithin.single v 1)
          (cycleAssociatedToClosedSubscheme (fieldChowSituation k) f
            (W.comap (closedPointSection k rfl b hb f)).subschemeι s).1,
        torFormulaCycleIntersectionProduct_mem_cyclesOfDimension
          (fieldChowSituation k) f hX _ _ _⟩

Stacks.Intersection.RationalEquivalence.rationallyEquivalent_intersectionProduct_fibreCycle_dimension_r, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/RationalEquivalence/FibreSpecialCase.lean, line 1330. The attribute's comment: “as printed, with [W_a]_r and [W_b]_r, the fibre cycles in the dimension r of V, the products being those of Tag 0B08 in the integer expected dimension r + r - dX; the data are those of rationallyEquivalent_intersectionProduct_fibreCycle, the fibres being pure of dimension s by Tag 02RK.”.

Stacks Project, Tag 0B60, as printed. The statement with the fibre cycles [W_a]_r and [W_b]_r in the dimension r of V, as the source writes it. The fibres are pure of dimension s (Tag 02RK), so for r ≠ s both cycles vanish, and for r = s this is Stacks.Intersection.RationalEquivalence.rationallyEquivalent_intersectionProduct_fibreCycle.

theorem rationallyEquivalent_intersectionProduct_fibreCycle_dimension_r [DecidableEq X]
    (hX : IsRegular X)
    (dX r s : ℕ) (hdX : topologicalKrullDim X = (dX : WithBot ℕ∞))
    (W : (projectiveLineProduct f).IdealSheafData) [IsIntegral W.subscheme]
    (hW : topologicalKrullDim (W.support : Set (projectiveLineProduct f)) =
      ((s + 1 : ℕ) : WithBot ℕ∞))
    [IsDominant (W.subschemeι ≫
      pullback.snd f (relativeProjectiveLine (Spec (.of k)) ↘ Spec (.of k)))]
    (a b : relativeProjectiveLine (Spec (.of k))) (ha : IsClosed {a}) (hb : IsClosed {b})
    (v : X) (hv : topologicalKrullDim (closure ({v} : Set X)) = (r : WithBot ℕ∞))
    (hVa : topologicalKrullDim (↥(closure ({v} : Set X) ∩
        Set.range (W.comap (closedPointSection k rfl a ha f)).subschemeι)) +
        (dX : WithBot ℕ∞) ≤ ((r + s : ℕ) : WithBot ℕ∞))
    (hVb : topologicalKrullDim (↥(closure ({v} : Set X) ∩
        Set.range (W.comap (closedPointSection k rfl b hb f)).subschemeι)) +
        (dX : WithBot ℕ∞) ≤ ((r + s : ℕ) : WithBot ℕ∞)) :
    letI : IsLocallyNoetherian X := isLocallyNoetherian_of_isRegular hX
    RationallyEquivalent (fieldChowSituation k) f ((r : ℤ) + r - dX)
      ⟨torFormulaCycleIntersectionProduct (fieldChowSituation k) f hX ((r : ℤ) + r - dX)
          (Function.locallyFinsuppWithin.single v 1)
          (cycleAssociatedToClosedSubscheme (fieldChowSituation k) f
            (W.comap (closedPointSection k rfl a ha f)).subschemeι r).1,
        torFormulaCycleIntersectionProduct_mem_cyclesOfDimension
          (fieldChowSituation k) f hX _ _ _⟩
      ⟨torFormulaCycleIntersectionProduct (fieldChowSituation k) f hX ((r : ℤ) + r - dX)
          (Function.locallyFinsuppWithin.single v 1)
          (cycleAssociatedToClosedSubscheme (fieldChowSituation k) f
            (W.comap (closedPointSection k rfl b hb f)).subschemeι r).1,
        torFormulaCycleIntersectionProduct_mem_cyclesOfDimension
          (fieldChowSituation k) f hX _ _ _⟩

Tag 0B1V, a theorem

Tag 0B1V in the Stacks Project.

AlgebraicGeometry.TorFormula.torFormulaCycleIntersectionProduct_mem_rationalEquivalences, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/MovingLemma/RationalEquivalenceProduct.lean, line 160. The attribute's comment: “the whole theorem, for a nonsingular projective variety X of dimension n over an algebraically closed field: for an r-cycle α and an s-cycle β meeting properly (Tag 0AZQ) with α rationally equivalent to zero, the Tag 0B08 product α · β is a rationally trivial (r + s - n)-cycle”.

Stacks Project, Tag 0B1V. Let X be a nonsingular projective variety of dimension n over an algebraically closed field k. Let α be an r-cycle and β an s-cycle on X which intersect properly, so that α · β is defined, and assume α ∼_rat 0. Then α · β ∼_rat 0.

The product is the intersection product of Tag 0B08, an (r + s - n)-cycle.

theorem torFormulaCycleIntersectionProduct_mem_rationalEquivalences (k : Type u) [Field k]
    [IsAlgClosed k] {X : Scheme.{u}} (p : X ⟶ Spec (.of k)) [IsProjectiveVariety k p]
    (hX : IsRegular X) {n : ℕ} (hn : topologicalKrullDim X = (n : WithBot ℕ∞)) {r s : ℤ}
    (α : CycleGroup (fieldChowSituation k) p r) (β : CycleGroup (fieldChowSituation k) p s)
    (hαβ : AlgebraicCycle.IntersectProperly α.1 β.1)
    (hα : α ∈ rationalEquivalences (fieldChowSituation k) p r) :
    haveI : IsLocallyNoetherian X := isLocallyNoetherian_of_isRegular hX
    (⟨torFormulaCycleIntersectionProduct (fieldChowSituation k) p hX (r + s - n) α.1 β.1,
        torFormulaCycleIntersectionProduct_mem_cyclesOfDimension (fieldChowSituation k) p hX
          (r + s - n) α.1 β.1⟩ :
      CycleGroup (fieldChowSituation k) p (r + s - n)) ∈
      rationalEquivalences (fieldChowSituation k) p (r + s - n)

Tag 0B61, a remark

Tag 0B61 in the Stacks Project.

AlgebraicGeometry.ProjectiveSpaceOfModule.exists_intersectProperly_cycleComap_torFormulaCycleIntersectionProduct_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/MovingLemma/KeyLemma.lean, line 770. The attribute's comment: “the variant of the moving lemma 0B0E stated there, for an arbitrary open subscheme U ⟶ X of the nonsingular locus of a closed subvariety X ⊆ 𝐏(V) (the source's U = X^reg), with the dimensions of the T_i allowed to vary; (C · X)|_U is the coefficientwise inverse image of the cycle C · X along U ⟶ X ⟶ 𝐏(V); the non-strict dimension clause is the disjunction dim (Z_j ∩ T_i) ≤ dim (Z ∩ T_i) or dim (Z_j ∩ T_i) + n ≤ d + d', as for 0B0E, because the source's inequality fails when Z ∩ T_i is empty”.

Stacks Project, Remark 0B61: the moving lemma on an open subset of the nonsingular locus. Let X ⊆ 𝐏(V) be a closed subvariety of dimension n of the projective space of a vector space of dimension N + 1 over an algebraically closed field, let U ⊆ X be an open subscheme contained in the nonsingular locus X^{reg}, given as an open immersion j₀ : U ⟶ X (written Y ⟶ X below), let Z ⊆ U be a closed subvariety of dimension d < n, and let T_i ⊆ U be finitely many closed subvarieties, T_i of dimension d' i < n. Then there is a closed subvariety C ⊆ 𝐏(V) whose prime cycle intersects that of X properly, with

(C · X)|_U = [Z] + ∑ m_j [Z_j]

in the Tor-formula intersection product of Section 0B08, where C · X is supported on C ∩ X, the Z_j ⊆ U are irreducible closed of dimension d, distinct from Z, with nonzero multiplicities, and where, inside U,

• dim (Z_j ∩ T_i) ≤ dim (Z ∩ T_i) or dim (Z_j ∩ T_i) + n ≤ d + d' i, and
• dim (Z_j ∩ T_i) < dim (Z ∩ T_i) whenever Z does not intersect T_i properly in U.

The restriction of C · X to U is its coefficientwise inverse image Stacks.Chow.cycleComap along U ⟶ X ⟶ 𝐏(V). U = X^{reg} is the statement of Remark 0B61, U a quasi-projective variety embedded in a closed subvariety X of 𝐏(V) is the form the remark's 0B1U and 0B1V use, and j₀ = 𝟙 X for a nonsingular X is Lemma 0B0E; the dimensions d' i may vary with i, the source's single d' being the constant family.

The first clause departs from the source's text, because the source's clause is false. The source asks for dim (Z_j ∩ T_i) ≤ dim (Z ∩ T_i) outright. When Z ∩ T_i = ∅ this demands Z_j ∩ T_i = ∅ for every j, and that fails already for the projective Lemma 0B0E, where U = X = X^{reg}. Take X ⊆ 𝐏^3 a nonsingular quadric surface (n = 2) and Z, T_1 two distinct lines of one ruling (d = d' = 1), so that Z ∩ T_1 = ∅. A C as in the conclusion must be a surface: if dim C ≤ 1 then C ∩ X is finite and Z does not occur in C · X, and if C = 𝐏^3 then C · X has no component of dimension 1. A surface C meets the line T_1, and every component of C ∩ X through such a point has dimension exactly 1, so it occurs in C · X with a positive multiplicity and meets T_1; it is neither Z nor any admissible Z_j. The argument is written out in full in the implementation notes of this module. The disjunction is what condition (4) of the source's proof gives, and its first disjunct is the source's inequality whenever Z ∩ T_i is nonempty, by Tag 0AZP; in the empty case the second disjunct dim (Z_j ∩ T_i) + n ≤ d + d' i is what holds. The second clause is as the source has it, and is vacuous exactly in the empty case.

public theorem exists_intersectProperly_cycleComap_torFormulaCycleIntersectionProduct_eq
    (k V : Type u) [Field k] [IsAlgClosed k] [AddCommGroup V] [Module k V]
    [FiniteDimensional k V] [Nontrivial V] [DecidableEq (projectiveSpaceOfModule k V)]
    {N n d : ℕ} (hV : Module.finrank k V = N + 1)
    {X : Scheme.{u}} (iX : X ⟶ projectiveSpaceOfModule k V) [IsClosedImmersion iX]
    [IsVariety k (iX ≫ projectiveSpaceOfModuleToSpec k V)]
    (hdimX : topologicalKrullDim X = (n : WithBot ℕ∞)) (hd : d < n)
    {Y : Scheme.{u}} (j₀ : Y ⟶ X) [IsOpenImmersion j₀] (hU : Set.range j₀.base ⊆ regularLocus X)
    [DecidableEq Y]
    (Z : IrreducibleCloseds Y)
    (hZd : topologicalKrullDim (Z : Set Y) = (d : WithBot ℕ∞))
    {ι : Type*} [Finite ι] (T : ι → IrreducibleCloseds Y) {d' : ι → ℕ}
    (hd' : ∀ i, d' i < n)
    (hTd : ∀ i, topologicalKrullDim (T i : Set Y) = (d' i : WithBot ℕ∞))
    (XC : IrreducibleCloseds (projectiveSpaceOfModule k V))
    (hXC : (XC : Set (projectiveSpaceOfModule k V)) = Set.range iX.base) :
    ∃ (C : IrreducibleCloseds (projectiveSpaceOfModule k V))
      (S : Finset (IrreducibleCloseds Y)) (m : IrreducibleCloseds Y → ℤ),
      AlgebraicCycle.IntersectProperly
          (Function.locallyFinsuppWithin.single C.isIrreducible.genericPoint (1 : ℤ))
          (Function.locallyFinsuppWithin.single XC.isIrreducible.genericPoint (1 : ℤ)) ∧
        cycleComap j₀ j₀.isOpenEmbedding.injective
            (cycleComap iX iX.isClosedEmbedding.injective
              (TorFormula.torFormulaCycleIntersectionProduct (fieldChowSituation k)
                (projectiveSpaceOfModuleToSpec k V) (isRegular_projectiveSpaceOfModule k V)
                (d : ℤ)
                (Function.locallyFinsuppWithin.single C.isIrreducible.genericPoint (1 : ℤ))
                (Function.locallyFinsuppWithin.single XC.isIrreducible.genericPoint (1 : ℤ)))) =
          Function.locallyFinsuppWithin.single Z.isIrreducible.genericPoint (1 : ℤ) +
            ∑ W ∈ S, m W • Function.locallyFinsuppWithin.single
              W.isIrreducible.genericPoint (1 : ℤ) ∧
        (∀ p : projectiveSpaceOfModule k V,
          TorFormula.torFormulaCycleIntersectionProduct (fieldChowSituation k)
              (projectiveSpaceOfModuleToSpec k V) (isRegular_projectiveSpaceOfModule k V) (d : ℤ)
              (Function.locallyFinsuppWithin.single C.isIrreducible.genericPoint (1 : ℤ))
              (Function.locallyFinsuppWithin.single XC.isIrreducible.genericPoint (1 : ℤ)) p ≠
              0 →
            p ∈ (C : Set (projectiveSpaceOfModule k V)) ∩
              (XC : Set (projectiveSpaceOfModule k V))) ∧
        Z ∉ S ∧ (∀ W ∈ S, m W ≠ 0) ∧
        (∀ W ∈ S, topologicalKrullDim (W : Set Y) = (d : WithBot ℕ∞)) ∧
        (∀ W ∈ S, ∀ i,
          topologicalKrullDim ↥((W : Set Y) ∩ (T i : Set Y)) ≤
              topologicalKrullDim ↥((Z : Set Y) ∩ (T i : Set Y)) ∨
            topologicalKrullDim ↥((W : Set Y) ∩ (T i : Set Y)) +
                (n : WithBot ℕ∞) ≤ (d : WithBot ℕ∞) + (d' i : WithBot ℕ∞)) ∧
        (∀ W ∈ S, ∀ i, ¬ AlgebraicGeometry.IntersectProperly Z (T i) →
          topologicalKrullDim ↥((W : Set Y) ∩ (T i : Set Y)) <
            topologicalKrullDim ↥((Z : Set Y) ∩ (T i : Set Y)))

AlgebraicGeometry.exists_rationallyEquivalent_forall_intersectProperly_of_isQuasiProjectiveVariety, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/MovingLemma/MovingCycles.lean, line 64. The attribute's comment: “Lemma 0B1U for a nonsingular quasi-projective variety, which the remark asserts with the same proof; for a finite family of cycles β i of arbitrary dimensions s i in place of a single s-cycle, and with r and the s i arbitrary integers. Nonsingular is IsRegular X, quasi-projective variety is IsQuasiProjectiveVariety, cycles are the graded cycle groups Stacks.Chow.CycleGroup over Spec k, rational equivalence is Tag 02RW and proper intersection is Definition 0AZQ. The moving lemma is run on X as an open subset of the nonsingular locus of its closure in projective space, which is the version of Tag 0B0E the remark describes”.

Remark 0B61: the moving lemma for a nonsingular quasi-projective variety, for a finite family of cycles. Let X be a nonsingular quasi-projective variety over an algebraically closed field, let α be an r-cycle on X and let β i be finitely many cycles on X, of dimensions s i. Then there is an r-cycle α' with α' ∼_rat α which intersects every β i properly.

X is an open subscheme of a closed subvariety X̄ ⊆ 𝐏(k^{N+1}) (exists_isOpenImmersion_projectiveSpaceOfModule_of_isQuasiProjectiveVariety), contained in the nonsingular locus of X̄ because X is nonsingular, and the moving lemma on such an open subset is isMovableOff_of_isOpenImmersion.

public theorem exists_rationallyEquivalent_forall_intersectProperly_of_isQuasiProjectiveVariety
    (k : Type u) [Field k] [IsAlgClosed k] {X : Scheme.{u}} (sX : X ⟶ Spec (.of k))
    [IsQuasiProjectiveVariety k sX] (hX : IsRegular X) {r : ℤ}
    (α : CycleGroup (fieldChowSituation k) sX r)
    {ι : Type*} [Finite ι] (s : ι → ℤ) (β : ∀ i, CycleGroup (fieldChowSituation k) sX (s i)) :
    ∃ α' : CycleGroup (fieldChowSituation k) sX r,
      RationallyEquivalent (fieldChowSituation k) sX r α' α ∧
        ∀ i, AlgebraicCycle.IntersectProperly α'.1 (β i).1

AlgebraicGeometry.TorFormula.torFormulaCycleIntersectionProduct_mem_rationalEquivalences_of_isQuasiProjectiveVariety, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/MovingLemma/RationalEquivalenceProduct.lean, line 196. The attribute's comment: “Theorem 0B1V for a nonsingular quasi-projective variety X of dimension n over an algebraically closed field, which the remark asserts with the same proof: for an r-cycle α and an s-cycle β meeting properly (Tag 0AZQ) with α rationally equivalent to zero, the Tag 0B08 product α · β is a rationally trivial (r + s - n)-cycle. Quasi-projective variety is IsQuasiProjectiveVariety; the argument is run on X as an open subset of the nonsingular locus of its closure in projective space, the version of Tag 0B0E the remark describes”.

Stacks Project, Tag 0B61 for Theorem 0B1V. Let X be a nonsingular quasi-projective variety of dimension n over an algebraically closed field k. Let α be an r-cycle and β an s-cycle on X which intersect properly, and assume α ∼_rat 0. Then α · β ∼_rat 0.

X is an open subscheme of a closed subvariety X̄ ⊆ 𝐏^N of the same dimension, inside the nonsingular locus of X̄, and the proof of Tag 0B1V runs on such an open subscheme.

theorem torFormulaCycleIntersectionProduct_mem_rationalEquivalences_of_isQuasiProjectiveVariety
    (k : Type u) [Field k] [IsAlgClosed k] {X : Scheme.{u}} (p : X ⟶ Spec (.of k))
    [IsQuasiProjectiveVariety k p] (hX : IsRegular X) {n : ℕ}
    (hn : topologicalKrullDim X = (n : WithBot ℕ∞)) {r s : ℤ}
    (α : CycleGroup (fieldChowSituation k) p r) (β : CycleGroup (fieldChowSituation k) p s)
    (hαβ : AlgebraicCycle.IntersectProperly α.1 β.1)
    (hα : α ∈ rationalEquivalences (fieldChowSituation k) p r) :
    haveI : IsLocallyNoetherian X := isLocallyNoetherian_of_isRegular hX
    (⟨torFormulaCycleIntersectionProduct (fieldChowSituation k) p hX (r + s - n) α.1 β.1,
        torFormulaCycleIntersectionProduct_mem_cyclesOfDimension (fieldChowSituation k) p hX
          (r + s - n) α.1 β.1⟩ :
      CycleGroup (fieldChowSituation k) p (r + s - n)) ∈
      rationalEquivalences (fieldChowSituation k) p (r + s - n)

Sources

• Section 43.25, Tag 0B0F
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Intersection.RationalEquivalence.rationallyEquivalent_intersectionProduct_fibreCycle · Stacks.Intersection.RationalEquivalence.rationallyEquivalent_intersectionProduct_fibreCycle_dimension_r · AlgebraicGeometry.TorFormula.torFormulaCycleIntersectionProduct_mem_rationalEquivalences · AlgebraicGeometry.ProjectiveSpaceOfModule.exists_intersectProperly_cycleComap_torFormulaCycleIntersectionProduct_eq · AlgebraicGeometry.exists_rationallyEquivalent_forall_intersectProperly_of_isQuasiProjectiveVariety · AlgebraicGeometry.TorFormula.torFormulaCycleIntersectionProduct_mem_rationalEquivalences_of_isQuasiProjectiveVariety

Section43.27 Pullback for a general morphism#

Section 43.27 of the Stacks Project, Tag 0B0H. 1 tag here is carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0B2X, a lemma

Tag 0B2X in the Stacks Project.

Stacks.Intersection.ChowRing.chowPullback_eq_flatPullbackChow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/ChowRing/Pullback.lean, line 703. The attribute's comment: “part (4): for flat f of relative dimension e, the pullback f^* of Tag 0B0H is the flat pullback CH_k(Y) → CH_{k+e}(X) of Section 43.9”.

Stacks 0B2X, part (4): for flat f the pullback is flat pullback. If f is flat of relative dimension e, then f^* = f^*_{flat} : CH_k(Y) ⟶ CH_{k+e}(X).

theorem chowPullback_eq_flatPullbackChow [Flat f] (e : ℕ)
    (he : topologicalKrullDim X = topologicalKrullDim Y + (e : WithBot ℕ∞)) {k : ℤ}
    (hkm : k + dX = dY + (k + e)) :
    letI : LocallyOfFiniteType f := locallyOfFiniteType_of_isVariety_comp K sX sY f hf
    chowPullback K sX sY hX hY hdX hdY f hf hkm =
      flatPullbackChowOfRelativeDimension (fieldChowSituation K) sX sY f hf e
        (relativeDimension_of_flat_of_isVariety K sX sY f hf e he) k

Stacks.Intersection.ChowRing.chowMulFun_properChowPushforward_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/ChowRing/Pullback.lean, line 850. The attribute's comment: “part (3): the projection formula f_*(α) · β = f_*(α · f^*β) on Chow groups, for α ∈ CH_r(X) and β ∈ CH_k(Y), f^*β ∈ CH_m(X) with k + dim X = dim Y + m, and both products in CH_n with r + m = dim X + n”. References: SGA 7 XVII (5.2), “partial”.

Stacks 0B2X, part (3): the projection formula f_*(a) · b = f_*(a · f^*b). With s the graph, s_*(a · f^*b) = s_*(a) · pr_Y^* b on X × Y by the remark on graphs, and f_* = pr_{Y,*} ∘ s_*, so this is the flat projection formula (Tag 0B10) for pr_Y.

theorem chowMulFun_properChowPushforward_eq {r k m n : ℤ} (hkm : k + dX = dY + m)
    (hn : r + m = dX + n) (a : chowGroup (fieldChowSituation K) sX r)
    (b : chowGroup (fieldChowSituation K) sY k) :
    letI := isProper_of_comp_eq f hf
    chowMulFun K sY hY n
        (properChowPushforward (fieldChowSituation K) sX sY f hf r
          (properPushforwardFactorsThroughRationalEquivalence_of_isProper (fieldChowSituation K)
            sX sY f hf r) a) b =
      properChowPushforward (fieldChowSituation K) sX sY f hf n
        (properPushforwardFactorsThroughRationalEquivalence_of_isProper (fieldChowSituation K)
          sX sY f hf n)
        (chowMulFun K sX hX n a (chowPullback K sX sY hX hY hdX hdY f hf hkm b))

Stacks.Intersection.ChowRing.chowPullback_isRingHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/ChowRing/Pullback.lean, line 948. The attribute's comment: “part (1): f^* : CH^*(Y) → CH^*(X) is a ring map, stated as the existence of a ring homomorphism between the Chow rings ⨁_c CH^c which is f^* on each graded piece CH^c(Y) = CH_{dim Y - c}(Y) → CH^c(X) = CH_{dim X - c}(X); the content is chowPullback_chowMulFun (f^*(a · b) = f^*a · f^*b) and chowPullback_fundamentalClass (f^*[Y] = [X])”.

Stacks Project, Tag 0B2X, part (1). Let f : X ⟶ Y be a morphism of nonsingular projective varieties over an algebraically closed field (the chapter's convention, Tag 0AZ8). Then the pullback f^* : CH^*(Y) ⟶ CH^*(X) of Section 43.23 (Tag 0B0H) is a ring map: there is a ring homomorphism between the Chow rings of Section 43.21 (Tag 0B0G) which is f^* on every graded piece CH^c(Y) ⟶ CH^c(X).

theorem chowPullback_isRingHom :
    ∃ φ : ChowRing K sY hY dY hdY →+* ChowRing K sX hX dX hdX,
      ∀ (c : ℕ) (a : ChowGrade K sY dY hY hdY c),
        φ (DirectSum.of _ c a) =
          DirectSum.of _ c (chowPullback K sX sY hX hY hdX hdY f hf (k := (dY : ℤ) - c)
            (m := (dX : ℤ) - c) (by ring) a)

Stacks.Intersection.ChowRing.chowPullback_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Intersection/ChowRing/PullbackComposition.lean, line 396. The attribute's comment: “part (2): (g ∘ f)^* = f^* ∘ g^* for a composable pair of morphisms of nonsingular projective varieties, on Chow groups CH_k(Z) → CH_l(Y) → CH_m(X) with k + dim Y = dim Z + l, l + dim X = dim Y + m”.

Stacks Project, Tag 0B2X, part (2). For morphisms f : X ⟶ Y and g : Y ⟶ Z of nonsingular projective varieties, (g ∘ f)^* = f^* ∘ g^* on Chow groups. On W = (X × Y) × Z, f^*(g^*c) = pr_{X,*}(q₁₂^*[Γ_f] · q₂₃^*[Γ_g] · q₃^* c) by base change (Tag 02RG), the projection formula for q₁₂ (Tag 0B10) and Tag 0B0Z; the product q₁₂^*[Γ_f] · q₂₃^*[Γ_g] is the transversal intersection {(x, f(x), g(f(x)))}, which q₁₃ maps isomorphically onto Γ_{g ∘ f}, and the projection formula for q₁₃ gives (g ∘ f)^* c.

theorem chowPullback_comp {k l m : ℤ} (hkl : k + dY = dZ + l) (hlm : l + dX = dY + m)
    (hkm : k + dX = dZ + m) (c : chowGroup (fieldChowSituation K) sZ k) :
    chowPullback K sX sZ hX hZ hdX hdZ (f ≫ g) (by rw [Category.assoc, hg, hf]) hkm c =
      chowPullback K sX sY hX hY hdX hdY f hf hlm
        (chowPullback K sY sZ hY hZ hdY hdZ g hg hkl c)

Sources

• Section 43.27, Tag 0B0H
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Intersection.ChowRing.chowPullback_eq_flatPullbackChow · Stacks.Intersection.ChowRing.chowMulFun_properChowPushforward_eq · Stacks.Intersection.ChowRing.chowPullback_isRingHom · Stacks.Intersection.ChowRing.chowPullback_comp

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.