45.10 Further properties to 45.14 Weil cohomology theories…

Section45.10 Further properties #

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

Tag 0FHP, a lemma

Tag 0FHP in the Stacks Project.

Stacks.WeilCohomology.WeilData.trace_pt_eq_add_comp_pullTw, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/DisjointUnionTrace.lean, line 60.

Stacks Project, Tag 0FHP. Let X and Y be nonempty smooth projective schemes over k, both equidimensional of dimension d, and let c be a coproduct X ⨿ Y with coprojections i, j. Given (D0)–(D3) satisfying (A), (B) and (C), ∫_{X ⨿ Y} = ∫_X + ∫_Y, in the sense that ∫_{X ⨿ Y} = ∫_X ∘ i^* + ∫_Y ∘ j^* on H^{2d}(X ⨿ Y)(d).

theorem trace_pt_eq_add_comp_pullTw (hA : W.PoincareDuality) (hB : W.Kunneth)
    (hC : W.CycleClassAxiom hA.perfectPairing) {X Y : (SmoothProjectiveScheme k).FullSubcategory}
    {c : BinaryCofan X Y} (hc : IsColimit c) {d : ℕ} (hX : IsNonemptyEquidimensional X d)
    (hY : IsNonemptyEquidimensional Y d) :
    W.trace c.pt d (isNonemptyEquidimensional_pt hc hX hY) =
      W.trace X d hX ∘ₗ W.pullTw (Y := c.pt) c.inl _ _ +
        W.trace Y d hY ∘ₗ W.pullTw (Y := c.pt) c.inr _ _

Stacks.WeilCohomology.PoincareDualityPushforwardSetup.integration_eq_add_comp_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/FurtherProperties/TraceDisjointUnion.lean, line 186.

Stacks Project, Tag 0FHP. Additivity of the trace map over a disjoint union: ∫_{X ⨿ Y} = ∫_X + ∫_Y, as an identity between linear functionals on H^{2d}(X ⨿ Y), the two summands being the trace maps of the components precomposed with restriction along the coprojections.

theorem integration_eq_add_comp_pullback (i : X ⟶ Z) (j : Y ⟶ Z)
    (hdX : S.dimension X = S.dimension Z) (hdY : S.dimension Y = S.dimension Z)
    (hone : (S.H Z).one = S.pushforwardOne i hdX + S.pushforwardOne j hdY) :
    (S.integration Z).toLinearMap =
      (S.integration X).toLinearMap.comp
          ((ExternallyGraded.degreeCast (R := F) (X := (S.H X).piece)
              (show 2 * (S.dimension Z : ℤ) = 2 * (S.dimension X : ℤ) by omega)).comp
            (S.pullback i (2 * (S.dimension Z : ℤ)))) +
        (S.integration Y).toLinearMap.comp
          ((ExternallyGraded.degreeCast (R := F) (X := (S.H Y).piece)
              (show 2 * (S.dimension Z : ℤ) = 2 * (S.dimension Y : ℤ) by omega)).comp
            (S.pullback j (2 * (S.dimension Z : ℤ))))

Tag 0FHQ, a lemma

Tag 0FHQ in the Stacks Project.

Stacks.WeilCohomology.WeilData.grade_eq_bot_of_dimension_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/DimensionZero.lean, line 813. The attribute's comment: “part (1): H^i(X) = 0 for i ≠ 0, over the actual category of smooth projective schemes and the actual Weil data (D0)-(D3) satisfying (A), (B), (C)”.

Stacks 0FHQ (1): for data (D0)–(D3) satisfying (A), (B), (C) and X a smooth projective scheme of dimension zero over k, H^i(X) = 0 for i ≠ 0.

theorem grade_eq_bot_of_dimension_zero {n : ℤ} (hn : n ≠ 0) : W.grade X n = ⊥

Stacks.WeilCohomology.WeilData.finiteDimensional_H0_of_dimension_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/DimensionZero.lean, line 824. The attribute's comment: “part (2), finiteness: H^0(X) is finite dimensional over F”.

Stacks 0FHQ (2), finiteness: H^0(X) is a finite F-algebra, X of dimension zero.

theorem finiteDimensional_H0_of_dimension_zero : FiniteDimensional F (W.H0 X)

Stacks.WeilCohomology.WeilData.finrank_grade_zero_eq_degree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/DimensionZero.lean, line 838. The attribute's comment: “part (3): dim_F H^0(X) = deg(X → Spec k)”.

Stacks 0FHQ (3): dim_F H^0(X) = deg(X → Spec k), the degree being the rank of the finite flat structure morphism at the point of Spec k (Stacks 02KA, Scheme.Hom.finrank).

theorem finrank_grade_zero_eq_degree (s : Spec (.of k)) :
    Module.finrank F (W.grade X 0) = X.obj.hom.finrank s

Stacks.WeilCohomology.WeilData.isSeparable_H0_of_dimension_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/DimensionZero.lean, line 1038. The attribute's comment: “part (2), separability: H^0(X) is a separable F-algebra”.

Stacks 0FHQ (2), separability: H^0(X) is a separable F-algebra, X of dimension zero.

theorem isSeparable_H0_of_dimension_zero : Algebra.IsSeparable F (W.H0 X)

Stacks.WeilCohomology.WeilData.traceZero_eq_trace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/DimensionZero.lean, line 1046. The attribute's comment: “part (4): ∫_X : H^0(X) → F is the trace map”.

Stacks 0FHQ (4): ∫_X : H^0(X) → F is the trace map of the F-algebra H^0(X); here a ∈ H^0(X) enters ∫_X through H^0(X)(0) = H^0(X) ⊗_F F(0).

theorem traceZero_eq_trace (a : W.H0 X) :
    W.trace X 0 (isNonemptyEquidimensional_of_dimension_zero hX)
        ((W.twCoord X _ _).symm ⟨a.1, a.2⟩) = Algebra.trace F (W.H0 X) a

Stacks.WeilCohomology.WeilData.trace_cycleClass_fundamentalClass_of_dimension_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/DimensionZero.lean, line 1060. The attribute's comment: “part (6): ∫_X γ([X]) = deg(X → Spec k)”.

Stacks 0FHQ (6): ∫_X γ([X]) = deg(X → Spec k).

theorem trace_cycleClass_fundamentalClass_of_dimension_zero (s : Spec (.of k)) :
    W.trace X 0 (isNonemptyEquidimensional_of_dimension_zero hX)
        (W.cycleClass X 0 (fundamentalClass X)) = (X.obj.hom.finrank s : F)

Stacks.WeilCohomology.subsingleton_cohomology_of_dimension_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/FurtherProperties/DimensionZero.lean, line 277. The attribute's comment: “part (1): H^i(X) = 0 for i ≠ 0”.

Stacks Project, Tag 0FHQ, part (1). The cohomology of a smooth projective scheme of dimension zero over the base field vanishes in every nonzero degree.

theorem subsingleton_cohomology_of_dimension_zero (i : ℤ) (hi : i ≠ 0) : Subsingleton (HX i)

Stacks.WeilCohomology.finrank_cohomology_zero_eq_degree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/FurtherProperties/DimensionZero.lean, line 287. The attribute's comment: “part (3): dim_F H^0(X) = deg(X → Spec k)”.

Stacks Project, Tag 0FHQ, part (3). The degree-zero cohomology of a smooth projective scheme X of dimension zero over the base field has dimension deg(X → Spec(k)) over the coefficient field; the degree is the number n of copies of Y in the decomposition of X × Y.

theorem finrank_cohomology_zero_eq_degree : Module.finrank F (HX 0) = n

Stacks.WeilCohomology.integration_eq_trace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/FurtherProperties/DimensionZero.lean, line 332. The attribute's comment: “part (4): ∫_X is the trace map”.

Stacks Project, Tag 0FHQ, part (4). Integration on a smooth projective scheme of dimension zero over the base field is the trace map of the F-algebra H^0(X).

The hypothesis hint is the identity (∫_X a) · 1 = ∑_σ Spec(σ)^*a in H^0(Y), and e together with he is the isomorphism H^0(Y) ⊗_F H^0(X) ≅ H^0(Y)^Σ of H^0(Y)-algebras sending 1 ⊗ a to (Spec(σ)^*a)_σ. The right-hand side of hint is therefore the trace of 1 ⊗ a over H^0(Y), which is the image of the trace of a over F.

theorem integration_eq_trace : integration = Algebra.trace F A

Stacks.WeilCohomology.isSeparable_cohomology_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/FurtherProperties/DimensionZero.lean, line 385. The attribute's comment: “part (2): H^0(X) is a finite separable F-algebra”.

Stacks Project, Tag 0FHQ, part (2). The degree-zero cohomology of a smooth projective scheme of dimension zero over the base field is a finite separable algebra over the coefficient field; finiteness is the hypothesis [FiniteDimensional F A], which is axiom (A)(a).

Reducing the isomorphism e modulo a maximal ideal of B = H^0(Y) produces n characters of A = H^0(X) with values in the residue field L which span L^n over L; as A has dimension n over F by part (3), the resulting map A → L^n is injective, so A is reduced, and a reduced finite-dimensional algebra over a field of characteristic zero is separable.

theorem isSeparable_cohomology_zero : Algebra.IsSeparable F A

Stacks.WeilCohomology.cycleClass_fundamental_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/FurtherProperties/DimensionZero.lean, line 484. The attribute's comment: “part (5): γ([X]) = 1”.

Stacks Project, Tag 0FHQ, part (5). The cycle class of the fundamental class of a nonempty smooth projective scheme over the base field is the unit of its cohomology algebra.

The fundamental class of X is the pullback of the fundamental class of Spec(k) along the structure morphism (hfundamental); the cycle class map commutes with pullback by axiom (C)(a) (hcompat); the cycle class of the fundamental class of Spec(k) is the unit by Stacks 0FHE (hpt); and cohomological pullback preserves the unit (hone).

theorem cycleClass_fundamental_eq_one : cycleClass fundamental = 1

Stacks.WeilCohomology.integration_cycleClass_eq_degree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/FurtherProperties/DimensionZero.lean, line 519. The attribute's comment: “part (6): ∫_X γ([X]) = deg(X → Spec k)”.

Stacks Project, Tag 0FHQ, part (6). Integration of the cycle class of the fundamental class of a smooth projective scheme of dimension zero over the base field is its degree over the base field.

By part (5) that cycle class is the unit, by part (4) integration is the trace map, and the trace of the unit is the dimension of H^0(X) over the coefficient field, which is the degree by part (3).

theorem integration_cycleClass_eq_degree : integration (cycleClass fundamental) = (n : F)

Declarations registered for the tag:

Stacks.WeilCohomology.WeilData.cycleClass_fundamentalClass, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/DimensionZero.lean, line 1075 (StacksFrontier): “part (5): γ([X]) = 1, by 0FHF, for every smooth projective X”.

Tag 0FHR, a lemma

Tag 0FHR in the Stacks Project.

Stacks.WeilCohomology.WeilData.trace_cycleClass_eq_codimensionDegree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/ZeroCycleTraceDegree.lean, line 252.

Stacks 0FHR. Assume given data (D0)–(D3) satisfying (A), (B) and (C), and let X be a nonempty smooth projective scheme over k, equidimensional of dimension d. Then the diagram CH^d(X) --γ--> H^{2d}(X)(d) --∫_X--> F, CH^d(X) = CH_0(X) --deg--> 𝐙 → F commutes: ∫_X γ(β) = deg(β) for every β ∈ CH^d(X), where deg is the degree of zero cycles of Chow Homology, Section 0AZ0 (Stacks 0AZ1), on CH^d(X) = CH_0(X) (Stacks.WeilCohomology.codimensionDegree).

theorem trace_cycleClass_eq_codimensionDegree
    {X : (SmoothProjectiveScheme k).FullSubcategory} {d : ℕ}
    (hX : IsNonemptyEquidimensional X d) (β : codimensionChowGroup k X.obj.hom d) :
    W.trace X d hX (W.cycleClass X d β) = (codimensionDegree X d β : F)

Tag 0FHS, a lemma

Tag 0FHS in the Stacks Project.

Stacks.WeilCohomology.WeilData.finsum_negOnePow_finrank_eq_codimensionDegree_diag_mul_diag, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/EulerCharacteristic.lean, line 307. The attribute's comment: “the whole lemma: for (D0)-(D3) satisfying (A), (B), (C), F of characteristic 0, and X nonempty smooth projective over k, equidimensional of dimension d: the Euler characteristic ∑_i (-1)^i dim_F H^i(X) (over all i ∈ ℤ, of finite support) equals deg(Δ·Δ) for the intersection product of Tag 0FC0 of the class of the diagonal with itself in CH^{2d}(X × X), which equals deg(c_d(T_{X/k}) ∩ [X]) for the tangent sheaf T_{X/k} = Hom(Ω_{X/k}, O_X)”. References: SGA 7 XVI (2.1), “partial”.

Stacks 0FHS. Assume given (D0), (D1), (D2) and (D3) satisfying (A), (B) and (C), with F of characteristic zero. Let X be a nonempty smooth projective scheme over k, equidimensional of dimension d. Then

∑_i (-1)^i dim_F H^i(X) = deg(Δ · Δ) = deg(c_d(𝒯_{X/k})).

Here the sum runs over all i ∈ ℤ and has finite support (the first conclusion); Δ · Δ ∈ CH^{2d}(X × X) is the intersection product of Stacks 0FC0 (Stacks.Chow.codimensionIntersectionProduct) of the class [Δ] ∈ CH^d(X × X) of the diagonal with itself, and deg : CH^{2d}(X × X) = CH_0(X × X) → ℤ the degree of zero cycles (Stacks.WeilCohomology.codimensionDegree, Stacks 0AZ1); c_d(𝒯_{X/k}) ∈ A^d(X) is the d-th Chern class (Stacks 0ESW) of the tangent sheaf 𝒯_{X/k} = 𝓗om(Ω_{X/k}, 𝒪_X) (Stacks.WeilCohomology.SmoothProjectiveScheme.tangentSheaf), and its degree is that of the zero cycle class c_d(𝒯_{X/k}) ∩ [X] (Stacks.Chow.zeroDegree).

The proof is the source's. On the right, [Δ] · [Δ] = Δ_*(Δ^![Δ]) (Stacks 0FFE), Δ_* preserves degrees, and Δ^![Δ] = c_d(𝒩) ∩ [X] for the normal sheaf 𝒩 = 𝒞_{Δ}^∨ = 𝒯_{X/k} (Stacks 0FV9, the excess intersection formula for the Gysin map, with the conormal sheaf of the diagonal Ω_{X/k} by Stacks 08S2): codimensionDegree_diag_mul_diag and zeroDegree_regularImmersionGysin_diag. On the left, deg([Δ] · [Δ]) = ∫_{X × X} γ([Δ]) ∪ γ([Δ]) by Stacks 0FHR and (C)(c), = ∫_X Δ^*γ([Δ]) since γ([Δ]) = Δ_*1 (Stacks 0FHG, 0FHB), and writing γ([Δ]) = ∑ e_{i,j} ⊗ e'_{2d-i,j} (Stacks 0FHH) and using Remark 0FHD this is ∑_{i,j} ∫_X e_{i,j} ∪ e'_{2d-i,j} = ∑_i (-1)^i dim_F H^i(X).

theorem finsum_negOnePow_finrank_eq_codimensionDegree_diag_mul_diag :
    (Function.support fun i : ℤ ↦ (i.negOnePow : ℤ) * (Module.finrank F (W.grade X i) : ℤ)).Finite ∧
    (∑ᶠ i : ℤ, (i.negOnePow : ℤ) * (Module.finrank F (W.grade X i) : ℤ)) =
      codimensionDegree (prod X X) (d + d)
        (codimensionIntersectionProduct k (prod X X).obj.hom d d
          (closedSubschemeClass (prod X X).obj.hom (diag X).hom.left d)
          (closedSubschemeClass (prod X X).obj.hom (diag X).hom.left d)) ∧
    codimensionDegree (prod X X) (d + d)
        (codimensionIntersectionProduct k (prod X X).obj.hom d d
          (closedSubschemeClass (prod X X).obj.hom (diag X).hom.left d)
          (closedSubschemeClass (prod X X).obj.hom (diag X).hom.left d)) =
      zeroDegree k X.obj.hom (sub_self _)
        (chowCohomologyCap (fieldChowSituation k) (gysinSystemOfInvertible _) X.obj.hom d
          (totalChernOfFiniteLocallyFree (fieldChowSituation k) X.obj.hom (tangentSheaf X) d) d
          (fundamentalChowClass (fieldChowSituation k) X.obj.hom d))

Tag 0FHT, a lemma

Tag 0FHT in the Stacks Project.

AlgHom.exists_algEquiv_comp_eq_of_trace_sub_trace_eq_zsmul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/FurtherProperties/Basic.lean, line 458. The attribute's comment: “as printed the tag concludes σ = σ' from surjectivity of σ and σ' alone; Stacks.WeilCohomology.not_traceRelationStatement refutes that with F = ℝ, F' = A = ℂ, σ = id and σ' = complex conjugation. This declaration is the corrected statement, under the source's own hypotheses: σ' = θ ∘ σ for an F-algebra automorphism θ of F', equivalently Tr ∘ σ = Tr ∘ σ' together with ker σ = ker σ'”.

Stacks Project, Tag 0FHT, in the corrected form recorded as a Stacks erratum.

Over a field F of characteristic zero, let σ, σ' : A → F' be surjections from a finite F-algebra onto a finite separable F-algebra, and let σ i : A → F i be F-algebra maps to finite separable F-algebras. If
Tr_{F'/F} ∘ σ - Tr_{F'/F} ∘ σ' = n (∑ m i * Tr_{F i/F} ∘ σ i)
with n > 1 and the m i integers, then σ' = θ ∘ σ for an F-algebra automorphism θ of F'; equivalently Tr_{F'/F} ∘ σ = Tr_{F'/F} ∘ σ' and ker σ = ker σ'.

As printed, the tag concludes σ = σ'. That conclusion is refuted by Stacks.WeilCohomology.not_traceRelationStatement, which takes F = ℝ, F' = A = ℂ, σ = id and σ' = complex conjugation. An automorphism of F' is invisible to the trace relation, and the displayed conclusion is exactly what the relation does see.

theorem AlgHom.exists_algEquiv_comp_eq_of_trace_sub_trace_eq_zsmul
    (F : Type u) [Field F] [CharZero F]
    (F' : Type v) [CommRing F'] [Algebra F F'] [FiniteDimensional F F']
    [Algebra.IsSeparable F F']
    (A : Type w) [CommRing A] [Algebra F A] [FiniteDimensional F A]
    {r : ℕ} (F_i : Fin r → Type x)
    [∀ i, CommRing (F_i i)] [∀ i, Algebra F (F_i i)]
    [∀ i, FiniteDimensional F (F_i i)] [∀ i, Algebra.IsSeparable F (F_i i)]
    (σ σ' : A →ₐ[F] F') (σ_i : ∀ i, A →ₐ[F] F_i i)
    (hσ : Function.Surjective σ) (hσ' : Function.Surjective σ')
    (n : ℤ) (hn : 1 < n) (m : Fin r → ℤ)
    (hrel :
      (Algebra.trace F F').comp σ.toLinearMap -
          (Algebra.trace F F').comp σ'.toLinearMap =
        n • ∑ i, m i • (Algebra.trace F (F_i i)).comp (σ_i i).toLinearMap) :
    (∃ θ : F' ≃ₐ[F] F', σ' = (θ : F' →ₐ[F] F').comp σ) ∧
      (Algebra.trace F F').comp σ.toLinearMap =
        (Algebra.trace F F').comp σ'.toLinearMap ∧
      RingHom.ker σ.toRingHom = RingHom.ker σ'.toRingHom

Tag 0FHU, a lemma

Tag 0FHU in the Stacks Project.

Stacks.WeilCohomology.WeilData.rationalPointChowClass_sub_ne_zsmul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/RationalPointIndivisibility.lean, line 1165. The attribute's comment: “for X smooth projective over a finite separable k'/k, viewed over k, with the actual CH_0(X) over k', the data (D0)-(D3) and axioms (A), (B), (C) over the actual category of smooth projective k-schemes; γ(x) is the family of the classes γ([x]) in every codimension”.

Stacks Project, Tag 0FHU. Assume given (D0), (D1), (D2) and (D3) satisfying (A), (B) and (C). Let k'/k be a finite separable extension, let X be a smooth projective scheme over k' and let x, x' ∈ X be k'-rational points. If γ(x) ≠ γ(x'), then [x] - [x'] is not divisible by any integer n > 1 in CH_0(X).

Here X is a scheme with a smooth projective structure morphism p : X ⟶ Spec k', and it is a smooth projective scheme over k through Spec k' ⟶ Spec k (ofOverField p hp), which is how the data (D0)–(D3) over k apply to it. The points are sections x, x' of p; [x], [x'] ∈ CH_0(X) are their classes in the Chow group of X over k' (rationalPointChowClass), and the divisibility is in that group. γ(x) is the family of the cohomology classes γ([x]) ∈ H^{2i}(X)(i) of the class [x] ∈ CH^i(X) of the closed subscheme x in every codimension i (rationalPointClass): on the part of X of dimension d containing x this is γ([x]) ∈ H^{2d}(X)(d), the other entries vanishing.

The proof is the source's. If x and x' lie in different parts of X of constant dimension, the degree on the part containing x separates them. Otherwise, on that part X_d, Stacks 0FH5 writes the class of every zero cycle as an integral combination of classes of closed points with separable residue field, Stacks 0FHG and Stacks 0FHQ identify a ↦ ∫ a ∪ γ([y]) on H^0(X_d) with Tr_{H^0(y)/F} ∘ i_y^*, Poincaré duality (A)(b) turns the divisibility into the trace relation of Stacks 0FHT, which forces i_x^* = i_{x'}^*, whence γ([x]) = γ([x']) on X_d; and by (C)(a), the Gysin map of an open immersion being restriction, and Stacks 0FHJ for X = X_d ⨿ (X ∖ X_d), γ(x) = γ(x') on X.

theorem rationalPointChowClass_sub_ne_zsmul [CharZero F] (hA : W.PoincareDuality)
    (hB : W.Kunneth) (hC : W.CycleClassAxiom hA.perfectPairing) {X : Scheme.{u}}
    (p : X ⟶ (fieldChowSituation k').S) [Smooth p] (hp : IsProjectiveMorphism p)
    (x x' : (fieldChowSituation k').S ⟶ X) (hx : x ≫ p = 𝟙 _) (hx' : x' ≫ p = 𝟙 _)
    (hne : (fun i : ℤ ↦ W.cycleClass (ofOverField p hp) i (rationalPointClass p hp x hx i)) ≠
      fun i : ℤ ↦ W.cycleClass (ofOverField p hp) i (rationalPointClass p hp x' hx' i))
    (n : ℤ) (hn : 1 < n) (c : chowGroup (fieldChowSituation k') p 0) :
    rationalPointChowClass k' p x hx - rationalPointChowClass k' p x' hx' ≠ n • c

Stacks.WeilCohomology.rationalPointChowClass_sub_ne_zsmul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/FurtherProperties/RationalPoints.lean, line 183. The attribute's comment: “(D0)-(D3), (A)-(C) as explicit arguments is the source's own hypothesis and this directory's convention, not a restriction; but hsep (Stacks 0FH5, not proved here) and htrace, htrace' (∫_X a ∪ γ([x]) = trace of i^*a, via 0FHG, 0FHB, 0FHQ(4)) are carried rather than derived, as is the reduction to irreducible X. Generalizations: no smoothness or projectivity on p; only pair.flip injectivity is used of (A)(b)”.

Stacks Project, Tag 0FHU. Let H^* be a Weil cohomology theory with coefficient field F of characteristic zero, let k'/k be a finite separable extension and let X be a smooth projective scheme over k'. If x and x' are k'-rational points of X with γ([x]) ≠ γ([x']), then [x] - [x'] is not divisible by any integer n > 1 in CH_0(X).

The cohomological data and the axioms it satisfies are the explicit arguments: [pair.IsPerfPair] is axiom (A)(b) for X, cycleClass is the cycle class map γ of (D2), the instances on F' = H^0(Spec k') are Stacks 0FHQ for Spec k' and are where separability of k'/k enters, hsplit and hsplit' are functoriality of (D1) along x ≫ p = id and x' ≫ p = id, htrace and htrace' identify ∫_X a ∪ γ([x]) with the trace of i^*a by Stacks 0FHG, the projection formula and Stacks 0FHQ part (4), and hsep is Stacks 0FH5 with those same inputs applied to the separable closed points it produces.

What is assumed and what is proved

Presenting (D0)-(D3) and (A)-(C) as explicit arguments is not a restriction: "assume given (D0)-(D3) satisfying (A), (B), (C)" is the source's own hypothesis, and the explicit-argument presentation is this directory's convention for it.

What is a restriction is that three further inputs are assumed rather than derived, where the source derives them from those axioms, because this library does not have them.

hsep is Stacks 0FH5, which is not proved in this library; it is a lemma of the chapter, not axiom data.

htrace and htrace' are the identification of ∫_X a ∪ γ([x]) with the trace of i^*a, which needs Stacks 0FHG, the projection formula of Stacks 0FHB and Stacks 0FHQ part (4) glued together on schemes.

The reduction to X irreducible of dimension d is absorbed into the single group T.

So the theorem is weaker than "the axioms imply the conclusion", and the attribute records that. Two departures go the other way and are genuine generalizations: no smoothness or projectivity is imposed on p, since those enter only through the pairing, the cycle class map and the trace identities, all of which are hypotheses here; and of axiom (A)(b) only injectivity of pair.flip is consumed.

theorem rationalPointChowClass_sub_ne_zsmul
    {k' : Type u} [Field k'] {X : Scheme.{u}}
    (p : X ⟶ (Stacks.Chow.fieldChowSituation k').S) [LocallyOfFiniteType p]
    (x x' : (Stacks.Chow.fieldChowSituation k').S ⟶ X)
    (hx : x ≫ p = 𝟙 (Stacks.Chow.fieldChowSituation k').S)
    (hx' : x' ≫ p = 𝟙 (Stacks.Chow.fieldChowSituation k').S)
    (F : Type v) [Field F] [CharZero F]
    (F' : Type w) [CommRing F'] [Algebra F F'] [FiniteDimensional F F']
    [Algebra.IsSeparable F F']
    (A : Type x) [CommRing A] [Algebra F A] [FiniteDimensional F A]
    (T : Type y) [AddCommGroup T] [Module F T]
    (pair : A →ₗ[F] T →ₗ[F] F) [pair.IsPerfPair]
    (cycleClass : Stacks.Chow.chowGroup (Stacks.Chow.fieldChowSituation k') p 0 →+ T)
    (pullback pullback' : A →ₐ[F] F') (structurePullback : F' →ₐ[F] A)
    (hsplit : pullback.comp structurePullback = AlgHom.id F F')
    (hsplit' : pullback'.comp structurePullback = AlgHom.id F F')
    (htrace : ∀ a : A, pair a (cycleClass (rationalPointChowClass k' p x hx)) =
      Algebra.trace F F' (pullback a))
    (htrace' : ∀ a : A, pair a (cycleClass (rationalPointChowClass k' p x' hx')) =
      Algebra.trace F F' (pullback' a))
    (hsep : ∀ c : Stacks.Chow.chowGroup (Stacks.Chow.fieldChowSituation k') p 0,
      IsSeparableTraceCombination.{v, x, z} F A (pair.flip (cycleClass c)))
    (hne : cycleClass (rationalPointChowClass k' p x hx) ≠
      cycleClass (rationalPointChowClass k' p x' hx'))
    (n : ℤ) (hn : 1 < n)
    (c : Stacks.Chow.chowGroup (Stacks.Chow.fieldChowSituation k') p 0) :
    rationalPointChowClass k' p x hx - rationalPointChowClass k' p x' hx' ≠ n • c

Tag 0FHV, a lemma

Tag 0FHV in the Stacks Project.

Stacks.WeilCohomology.WeilData.exists_cycleClass_comp_eq_comp_chowDegree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/PointClassDegree.lean, line 553. The attribute's comment: “for X smooth projective and geometrically irreducible over a finite separable k'/k, viewed over k, with the actual CH_0(X) over k' and its degree, the data (D0)-(D3) and axioms (A), (B), (C) over the actual category of smooth projective k-schemes”.

Stacks Project, Tag 0FHV. Assume given (D0), (D1), (D2) and (D3) satisfying (A), (B) and (C). Let k'/k be a finite separable extension and let X be a geometrically irreducible smooth projective scheme over k' of dimension d. Then γ : CH_0(X) → H^{2d}(X)(d) factors through deg : CH_0(X) → 𝐙.

Here X is a scheme with a smooth projective, geometrically irreducible structure morphism p : X ⟶ Spec k', viewed over k through Spec k' ⟶ Spec k (ofOverField p hp), which is how the data over k apply to it; "of dimension d" is topologicalKrullDim X = d. CH_0(X) is the Chow group of zero cycles of X over k' and deg its degree (Stacks 0AZ1, Stacks.Chow.chowDegree, read at the point s of Spec k'); γ is the cycle class map CH^d(X) → H^{2d}(X)(d) of (D2) composed with CH_0(X) = CH^d(X) (zeroCycleToCodimensionOfExtension).

The proof is the source's. By Stacks 0FH5 CH_0(X) is generated by the classes of closed points with separable residue field, and for two such points deg(x') γ([x]) = deg(x) γ([x']) (WeilData.residueDegree_smul_cycleClass_closedPointClass): over a finite separable extension into which both residue fields embed this comes from the rational-point step (Stacks 0FH7, Stacks 0FHU, (C)(b)) and (C)(b) along X_K ⟶ X.

theorem exists_cycleClass_comp_eq_comp_chowDegree [CharZero F]
    (hA : W.PoincareDuality) (hB : W.Kunneth) (hC : W.CycleClassAxiom hA.perfectPairing)
    {X : Scheme.{u}} (p : X ⟶ (fieldChowSituation k').S) [Smooth p] [GeometricallyIrreducible p]
    (hp : IsProjectiveMorphism p) {d : ℕ} (hd : topologicalKrullDim X = d)
    (s : (fieldChowSituation k').S) :
    haveI := isProper_of_isProjectiveMorphism p hp
    haveI : LocallyOfFiniteType
        (show (ofOverField (k := k) p hp).obj.left ⟶ (fieldChowSituation k').S from p) :=
      inferInstanceAs (LocallyOfFiniteType p)
    ∃ φ : ℤ →+ W.Tw (ofOverField p hp) (2 * d) d,
      (W.cycleClass (ofOverField p hp) d).comp
          (zeroCycleToCodimensionOfExtension (ofOverField p hp) p rfl d) =
        φ.comp (chowDegree (fieldChowSituation k') (fieldChowSituation_dimensionFunction k') p
          s)

Tag 0FHW, a lemma

Tag 0FHW in the Stacks Project.

Stacks.WeilCohomology.injective_pullback_of_isDominant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/FurtherProperties/DominantPullback.lean, line 171.

Stacks Project, Tag 0FHW. Let f : X ⟶ Y be a dominant morphism of irreducible smooth projective schemes over a field k, and let H^* be a Weil cohomology theory over k with coefficients in a field F of characteristic zero. Then f^* : H^i(Y) ⟶ H^i(X) is injective.

The cohomological data and the axioms the proof uses are the explicit arguments: the data and axioms at the base point Spec(k), the trace maps ∫_X, ∫_Y and the cup products of (D1) and (D3) with associativity, the unit law and multiplicativity of f^*, perfectness of the trace pairings of Y (axiom (A)), axiom (C)(a) for the structure morphism of Y and axiom (C)(b) for f. The identity γ([Y]) = 1 of Stacks 0FHF and the projection formula of Stacks 0FHB are derived from these, not assumed.

theorem injective_pullback_of_isDominant {k : Type u} [Field k] {F : Type*} [Field F]
    [CharZero F]
    (Hpt : ℤ → Type x) [∀ i : ℤ, AddCommGroup (Hpt i)] [∀ i : ℤ, Module F (Hpt i)]
    [∀ i : ℤ, FiniteDimensional F (Hpt i)]
    (HptZero : Type x) [CommRing HptZero] [Algebra F HptZero]
    (degreeZeroPoint : Hpt 0 ≃ₗ[F] HptZero)
    (kunnethPoint : ∀ n : ℤ,
      DirectSum ℤ (fun j : ℤ ↦ TensorProduct F (Hpt j) (Hpt (n - j))) ≃ₗ[F] Hpt n)
    (cycleClassPoint : chowGroup (fieldChowSituation k) (𝟙 _) 0 →+ HptZero)
    (integrationPoint : HptZero →ₗ[F] F)
    (integration_cycleClassPoint : integrationPoint
      (cycleClassPoint (fundamentalChowClass (fieldChowSituation k) (𝟙 _) 0)) = 1)
    (cycleClassPoint_mul :
      cycleClassPoint (fundamentalChowClass (fieldChowSituation k) (𝟙 _) 0) *
          cycleClassPoint (fundamentalChowClass (fieldChowSituation k) (𝟙 _) 0) =
        cycleClassPoint (fundamentalChowClass (fieldChowSituation k) (𝟙 _) 0))
    {X Y : Scheme.{u}} (sX : X ⟶ (fieldChowSituation k).S) [LocallyOfFiniteType sX]
    (sY : Y ⟶ (fieldChowSituation k).S) [Smooth sY] [IrreducibleSpace Y]
    (e : ℕ) (hd : AlgebraicGeometry.RelativeDimension sY e)
    (f : X ⟶ Y) [IsProper f] [IsDominant f] (hf : f ≫ sY = sX)
    {BX BY DXtop DYtop HXtop HYtop TopX TopY HX' HY' DX' : Type*}
    [AddCommGroup BX] [Module F BX] [AddCommGroup BY] [Module F BY]
    [AddCommGroup DXtop] [Module F DXtop] [AddCommGroup DYtop] [Module F DYtop]
    [AddCommGroup HXtop] [Module F HXtop] [AddCommGroup HYtop] [Module F HYtop]
    [AddCommGroup TopX] [Module F TopX] [AddCommGroup TopY] [Module F TopY]
    [AddCommGroup HX'] [Module F HX'] [AddCommGroup HY'] [Module F HY']
    [AddCommGroup DX'] [Module F DX']
    (integralX : TopX →ₗ[F] F) (integralY : TopY →ₗ[F] F)
    (cupTopX : HXtop →ₗ[F] DXtop →ₗ[F] TopX) (cupTopY : HYtop →ₗ[F] DYtop →ₗ[F] TopY)
    (cupX' : HX' →ₗ[F] DX' →ₗ[F] TopX) (cupY' : HY' →ₗ[F] BY →ₗ[F] TopY)
    [(cupTopY.compr₂ integralY).IsPerfPair] [(cupY'.compr₂ integralY).IsPerfPair]
    (cupX : BX →ₗ[F] DXtop →ₗ[F] DX') (cupY : BY →ₗ[F] DYtop →ₗ[F] BY)
    (cupLeftX : HX' →ₗ[F] BX →ₗ[F] HXtop) (cupLeftY : HY' →ₗ[F] BY →ₗ[F] HYtop)
    (one : DYtop)
    (cup_assoc_X : ∀ c b a, cupX' c (cupX b a) = cupTopX (cupLeftX c b) a)
    (cup_assoc_Y : ∀ c b a, cupY' c (cupY b a) = cupTopY (cupLeftY c b) a)
    (cupY_one : ∀ b, cupY b one = b)
    (pullbackB : BY →ₗ[F] BX) (pullbackTop : HYtop →ₗ[F] HXtop) (pullback' : HY' →ₗ[F] HX')
    (pullback_cup : ∀ c b, pullbackTop (cupLeftY c b) = cupLeftX (pullback' c) (pullbackB b))
    (pullbackPt : HptZero →ₗ[F] DYtop) (pullbackPt_one : pullbackPt 1 = one)
    (cycleClassX : chowGroup (fieldChowSituation k) sX (0 + (e : ℤ)) →+ DXtop)
    (cycleClassY : chowGroup (fieldChowSituation k) sY (0 + (e : ℤ)) →+ DYtop)
    (cycleClass_pullback : ∀ α,
      cycleClassY (flatPullbackChowOfRelativeDimension (fieldChowSituation k) sY (𝟙 _) sY
          (Category.comp_id sY) e hd 0 α) =
        pullbackPt (cycleClassPoint α))
    (cycleClass_pushforward : ∀ α,
      cycleClassY (properChowPushforward (fieldChowSituation k) sX sY f hf (0 + (e : ℤ))
          (properPushforwardFactorsThroughRationalEquivalence_of_isProper (fieldChowSituation k)
            sX sY f hf (0 + (e : ℤ))) α) =
        poincareDualPushforward (cupTopX.compr₂ integralX) (cupTopY.compr₂ integralY)
          pullbackTop (cycleClassX α)) :
    Function.Injective pullbackB

Tag 0FHX, a lemma

Tag 0FHX in the Stacks Project.

Stacks.WeilCohomology.WeilData.bijective_scalarExtensionMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/ScalarExtension.lean, line 692. The attribute's comment: “H^(X) ⊗_{H^0(Spec k')} H^0(Spec k'') = H^(X ×_{Spec k'} Spec k'') for the actual Weil data, X smooth projective over k', k''/k'/k finite separable”.

Stacks Project, Tag 0FHX. Assume given (D0)–(D3) satisfying (A), (B) and (C). Let k''/k'/k be finite separable algebras and let X be a smooth projective scheme over k'. Then the comparison map

H^*(X) ⊗_{H^0(Spec k')} H^0(Spec k'') ⟶ H^*(X ×_{Spec k'} Spec k''), a ⊗ b ↦ pr₁^*a ∪ pr₂^*b,

is bijective. Here H^*(X) is an H^0(Spec k')-algebra by pullback along X ⟶ Spec k', and X and X ×_{Spec k'} Spec k'' are smooth projective schemes over k.

theorem bijective_scalarExtensionMap [CharZero F] (hA : W.PoincareDuality) (hB : W.Kunneth)
    (hC : W.CycleClassAxiom hA.perfectPairing) :
    Function.Bijective (W.scalarExtensionMap π hπ (k'' := k''))

Stacks.WeilCohomology.WeilData.scalarExtensionAlgEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/ScalarExtension.lean, line 703. The attribute's comment: “the H^0(Spec k')-algebra isomorphism H^(X) ⊗_{H^0(Spec k')} H^0(Spec k'') ≃ H^(X ×_{Spec k'} Spec k'') for the actual Weil data”.

Stacks Project, Tag 0FHX, as an isomorphism of H^0(Spec k')-algebras: H^*(X) ⊗_{H^0(Spec k')} H^0(Spec k'') ≃ H^*(X ×_{Spec k'} Spec k''), a ⊗ b ↦ pr₁^*a ∪ pr₂^*b.

def scalarExtensionAlgEquiv [CharZero F] (hA : W.PoincareDuality) (hB : W.Kunneth)
    (hC : W.CycleClassAxiom hA.perfectPairing) :
    W.H (ofOver k π hπ) ⊗[W.H0 (spec k k')] W.H0 (spec k k'') ≃ₐ[W.H0 (spec k k')]
      W.H (baseChangeObj k π hπ (k'' := k''))

Stacks.WeilCohomology.bijective_scalarExtensionHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/FurtherProperties/ScalarExtension.lean, line 225. The attribute's comment: “the comparison map is bijective”.

Stacks Project, Tag 0FHX. Let k''/k'/k be finite separable algebras and let X be a smooth projective scheme over k'. Then the canonical map

H^*(X) ⊗_{H^0(Spec k')} H^0(Spec k'') ⟶ H^*(X ×_{Spec k'} Spec k'')

is bijective.

Write k' ⊗_k k'' = k'' × l and G = H^0(Spec l). Künneth together with additivity on a disjoint union, Stacks 0FHJ, decomposes H^0(Spec k') ⊗_F H^0(Spec k'') as H^0(Spec k'') × G with first projection the multiplication map, and decomposes H^*(X) ⊗_F H^0(Spec k'') as H^*(X ×_{Spec k'} Spec k'') × H^*(X ×_{Spec k'} Spec l) compatibly. The idempotent of the first decomposition corresponding to (0, 1) then identifies the two kernels.

theorem bijective_scalarExtensionHom (fM : M →ₐ[A] N₁)
    (kunneth : M ⊗[F] B ≃ₐ[F] N₁ × N₂)
    (kunneth_tmul : ∀ (m : M) (b : B),
      (kunneth (m ⊗ₜ[F] b)).1 = fM m * algebraMap B N₁ b)
    (split : A ⊗[F] B ≃ₐ[F] B × G)
    (split_fst : ∀ z : A ⊗[F] B, (split z).1 = tensorMulHom F A B z)
    (kunneth_split : ∀ z : A ⊗[F] B,
      kunneth (tensorActionHom F A B M z) =
        (algebraMap B N₁ (split z).1, algebraMap G N₂ (split z).2)) :
    Function.Bijective (scalarExtensionHom (B := B) fM)

Stacks.WeilCohomology.scalarExtensionEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/FurtherProperties/ScalarExtension.lean, line 247. The attribute's comment: “the scalar extension isomorphism”.

Stacks Project, Tag 0FHX. The scalar extension isomorphism

H^*(X) ⊗_{H^0(Spec k')} H^0(Spec k'') ≃ H^*(X ×_{Spec k'} Spec k'')

for k''/k'/k finite separable algebras and X smooth projective over k', given by a ⊗ b ↦ pr₁^*a ∪ pr₂^*b.

noncomputable def scalarExtensionEquiv (fM : M →ₐ[A] N₁)
    (kunneth : M ⊗[F] B ≃ₐ[F] N₁ × N₂)
    (kunneth_tmul : ∀ (m : M) (b : B),
      (kunneth (m ⊗ₜ[F] b)).1 = fM m * algebraMap B N₁ b)
    (split : A ⊗[F] B ≃ₐ[F] B × G)
    (split_fst : ∀ z : A ⊗[F] B, (split z).1 = tensorMulHom F A B z)
    (kunneth_split : ∀ z : A ⊗[F] B,
      kunneth (tensorActionHom F A B M z) =
        (algebraMap B N₁ (split z).1, algebraMap G N₂ (split z).2)) :
    M ⊗[A] B ≃ₐ[A] N₁

Sources

LeanStacks.WeilCohomology.WeilData.trace_pt_eq_add_comp_pullTw · Stacks.WeilCohomology.PoincareDualityPushforwardSetup.integration_eq_add_comp_pullback · Stacks.WeilCohomology.WeilData.grade_eq_bot_of_dimension_zero · Stacks.WeilCohomology.WeilData.finiteDimensional_H0_of_dimension_zero · Stacks.WeilCohomology.WeilData.finrank_grade_zero_eq_degree · Stacks.WeilCohomology.WeilData.isSeparable_H0_of_dimension_zero · Stacks.WeilCohomology.WeilData.traceZero_eq_trace · Stacks.WeilCohomology.WeilData.trace_cycleClass_fundamentalClass_of_dimension_zero

Section45.11 Weil cohomology theories, II #

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

Tag 0FI0, a lemma

Tag 0FI0 in the Stacks Project.

Stacks.WeilCohomology.WeilData.globalSections_criterion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/GlobalSectionsCriterion.lean, line 418. The attribute's comment: “(1) ⇔ (2), the finite separability of H^0(X), and (1) ⇔ (3) for X equidimensional of dimension d, on the actual Weil data (D0)-(D3) satisfying (A), (B), (C) over the actual category of smooth projective k-schemes”.

Stacks Project, Tag 0FI0. Assume given (D0), (D1), (D2) and (D3) satisfying (A), (B) and (C). Let X be a smooth projective scheme over k and k' = Γ(X, 𝒪_X). Then the following are equivalent:

there exist finitely many closed points x₁, …, x_r ∈ X whose residue fields are separable over k such that H^0(X) → H^0(x₁) ⊕ … ⊕ H^0(x_r) is injective (SeparablePointsDetectH0),

the map H^0(Spec(k')) → H^0(X) is an isomorphism.

If this is true, then H^0(X) is a finite separable algebra over F. If X is equidimensional of dimension d, then (1) and (2) are also equivalent to

the classes of closed points generate H^{2d}(X)(d) as a module over H^0(X) (PointClassesGenerate).

Here Spec(k') is the smooth projective k-scheme specGlobalSections X and the map in (2) is pullback along the canonical morphism X ⟶ Spec(k'); "equidimensional of dimension d" is RelativeDimension X.obj.hom d, which allows X = ∅.

theorem globalSections_criterion [CharZero F] (hA : W.PoincareDuality) (hB : W.Kunneth)
    (hC : W.CycleClassAxiom hA.perfectPairing) (X : (SmoothProjectiveScheme k).FullSubcategory) :
    (W.SeparablePointsDetectH0 X ↔ Function.Bijective (W.pullDeg (toSpecGlobalSections X) 0)) ∧
      (Function.Bijective (W.pullDeg (toSpecGlobalSections X) 0) →
        FiniteDimensional F (W.H0 X) ∧ Algebra.IsSeparable F (W.H0 X)) ∧
      ∀ d : ℕ, RelativeDimension X.obj.hom d →
        (W.SeparablePointsDetectH0 X ↔ W.PointClassesGenerate X d)

Tag 0FI1, a lemma

Tag 0FI1 in the Stacks Project.

Stacks.WeilCohomology.WeilData.exists_not_globalSections_criterion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/GlobalSectionsNegativeDegree.lean, line 128. The attribute's comment: “H^i(Y) ≠ 0 for some smooth projective Y and i < 0 gives a nonempty equidimensional smooth projective X for which conditions (1), (2), (3) of 0FI0 all fail, on the actual Weil data (D0)-(D3) satisfying (A), (B), (C) over the actual category of smooth projective k-schemes”.

Stacks Project, Tag 0FI1. Assume given (D0), (D1), (D2) and (D3) satisfying (A), (B) and (C). If there exists a smooth projective scheme Y over k such that H^i(Y) is nonzero for some i < 0, then there exists an equidimensional smooth projective scheme X over k such that the equivalent conditions of Stacks 0FI0 fail for X: (1) no finite family of closed points with separable residue fields detects H^0(X) (SeparablePointsDetectH0), (2) the map H^0(Spec Γ(X, 𝒪_X)) → H^0(X) is not an isomorphism, and (3) the classes of closed points do not generate H^{2d}(X)(d) as an H^0(X)-module (PointClassesGenerate), d the dimension of X. The scheme X is moreover nonempty.

theorem exists_not_globalSections_criterion [CharZero F] (hA : W.PoincareDuality)
    (hB : W.Kunneth) (hC : W.CycleClassAxiom hA.perfectPairing)
    (hneg : ∃ (Y : (SmoothProjectiveScheme k).FullSubcategory) (i : ℤ), i < 0 ∧ W.grade Y i ≠ ⊥) :
    ∃ (X : (SmoothProjectiveScheme k).FullSubcategory) (d : ℕ), IsNonemptyEquidimensional X d ∧
      ¬ W.SeparablePointsDetectH0 X ∧
      ¬ Function.Bijective (W.pullDeg (toSpecGlobalSections X) 0) ∧
      ¬ W.PointClassesGenerate X d

Tag 0FI2, a definition

Tag 0FI2 in the Stacks Project.

Declarations registered for the tag:

Stacks.WeilCohomology.WeilCohomologyTheory, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/WeilCohomologyTheoryTag.lean, line 37 (StacksFrontier): “Weil cohomology theory: data (D0)-(D3) on the smooth projective (01W8, not merely proper) k-schemes satisfying (A), (B), (C) of 0FHA and condition (2) of 0FI0 for every X, the equivalent condition (1) following by 0FI0. Generalized to any coefficient field F, with no [CharZero F]: with it, this is the source's notion. (B)(b) reads ∫_X ⊗ ∫_Y as zero off the top Künneth component H^{2d}(X)(d) ⊗ H^{2e}(Y)(e) of H^{2(d+e)}(X × Y)(d + e), the trace maps being extended by zero outside their degree as in 'Ad (A6)'”.

Tag 0FI3, a remark

Tag 0FI3 in the Stacks Project.

Stacks.WeilCohomology.WeilCohomologyTheory.factorwise_rank_one_of_geometricallyIrreducible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/ProductOfFieldsFactors.lean, line 428. The attribute's comment: “for H^ a Weil cohomology theory (0FI2), X geometrically irreducible smooth projective of dimension d over a finite separable k'/k, viewed over k, and H^0(Spec k') → ∏ F_i bijective for fields F_i: H^(X) and each H^n(X) are ∏_i of their base changes to the F_i by x ↦ (1 ⊗ x)_i; H^0(X) and H^{2d}(X) are free of rank 1 over H^0(Spec k'), with each factor of dimension 1 over F_i; M ⊗_{H^0(Spec k')} F_i is written F_i ⊗_{H^0(Spec k')} M; no CharZero F needed”.

Let H^* be a Weil cohomology theory (Definition 0FI2). Let X be a geometrically irreducible smooth projective scheme of dimension d over k', with k'/k a finite separable extension of fields. Suppose that H^0(Spec(k')) = F_1 × ⋯ × F_r for fields F_i. Then

H^*(X) = ∏_i H^*(X) ⊗_{H^0(Spec k')} F_i, by x ↦ (x ⊗ 1)_i, and likewise in each degree;

H^0(X) is free of rank 1 over ∏_i F_i, and each factor H^0(X) ⊗_{H^0(Spec k')} F_i has dimension 1 over F_i;

the same is true in degree 2d: H^{2d}(X) is free of rank 1 over ∏_i F_i, and each H^{2d}(X) ⊗_{H^0(Spec k')} F_i has dimension 1 over F_i.

Here X is a scheme with a smooth projective, geometrically irreducible structure morphism p : X ⟶ Spec k', viewed over k through Spec k' ⟶ Spec k (ofOver k p hp), Spec k' is the smooth projective k-scheme spec k k', and "of dimension d" is topologicalKrullDim X = d. H^*(X) is an H^0(Spec k')-algebra by pullback along X ⟶ Spec k', and H^n(X) is its degree n part (WeilData.gradeOverSpec). "H^0(Spec(k')) = F_1 × ⋯ × F_r" is a finite family of fields F_i, each an H^0(Spec k')-algebra, with H^0(Spec k') → ∏_i F_i bijective. The factor M ⊗_{H^0(Spec k')} F_i is written as the base change F_i ⊗_{H^0(Spec k')} M, which is the same module by the symmetry of the tensor product. The coefficient field F is not required to have characteristic zero.

theorem factorwise_rank_one_of_geometricallyIrreducible (W : WeilCohomologyTheory k F)
    {k' : Type u} [Field k'] [Algebra k k'] [FiniteDimensional k k'] [Algebra.IsSeparable k k']
    {X : Scheme.{u}} (p : X ⟶ Spec (.of k')) [Smooth p] [GeometricallyIrreducible p]
    (hp : IsProjectiveMorphism p) {d : ℕ} (hd : topologicalKrullDim X = d)
    {ι : Type*} [Fintype ι] [DecidableEq ι] (K : ι → Type*) [∀ i, Field (K i)]
    [∀ i, Algebra (W.H0 (spec k k')) (K i)]
    (hK : Function.Bijective (Pi.ringHom fun i ↦ algebraMap (W.H0 (spec k k')) (K i))) :
    Function.Bijective (fun (x : W.H (ofOver k p hp)) (i : ι) ↦
        (1 : K i) ⊗ₜ[W.H0 (spec k k')] x) ∧
      (∀ n : ℤ, Function.Bijective (fun (x : W.gradeOverSpec p hp n) (i : ι) ↦
        (1 : K i) ⊗ₜ[W.H0 (spec k k')] x)) ∧
      Nonempty (W.H0 (spec k k') ≃ₗ[W.H0 (spec k k')] W.gradeOverSpec p hp 0) ∧
      (∀ i, Module.finrank (K i) (K i ⊗[W.H0 (spec k k')] W.gradeOverSpec p hp 0) = 1) ∧
      Nonempty (W.H0 (spec k k') ≃ₗ[W.H0 (spec k k')] W.gradeOverSpec p hp (2 * d)) ∧
      (∀ i, Module.finrank (K i) (K i ⊗[W.H0 (spec k k')] W.gradeOverSpec p hp (2 * d)) = 1)

Tag 0GIJ, a proposition

Tag 0GIJ in the Stacks Project.

Stacks.WeilCohomology.WeilRealization.exists_globalSections_isoClassEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/WeilRealizationGlobalSections.lean, line 331. The attribute's comment: “a Weil cohomology theory is the same thing as a Q-linear symmetric monoidal functor G : M_k -> graded F-vector spaces with G(1(1)) nonzero only in degree -2 and G(h(Spec k')) -> G(h(X)) an isomorphism in degree 0 for k' = Gamma(X, O_X): a bijection of isomorphism classes, G corresponding to H^*(X) = G(h(X))”.

Stacks Project, Tag 0GIJ. Let k be a field and F a field of characteristic 0. A Weil cohomology theory (Definition 0FI2) is the same thing as a ℚ-linear symmetric monoidal functor G : M_k ⥤ graded F-vector spaces (Stacks.WeilCohomology.WeilRealization) such that

G(𝟏(1)) is nonzero only in degree -2, and

for every smooth projective X over k with k' = Γ(X, 𝒪_X) the map G(h(Spec k')) → G(h(X)) is an isomorphism in degree 0 (Stacks.WeilCohomology.WeilRealization.GlobalSections):

there is a bijection between isomorphism classes of such functors and isomorphism classes of Weil cohomology theories, sending the class of G to the class of the Weil cohomology theory H^*(X) = G(h(X)) of Stacks 0FHK.

theorem exists_globalSections_isoClassEquiv :
    ∃ e : Quotient ((isoSetoid k F).comap
          (Subtype.val : {G : WeilRealization k F // G.GlobalSections} → _)) ≃
        Quotient (WeilCohomologyTheory.isoSetoid k F),
      ∀ (G : {G : WeilRealization k F // G.GlobalSections}) (T : WeilCohomologyTheory k F),
        e (Quotient.mk _ G) = Quotient.mk _ T ↔
          (Quotient.mk (WeilDataAxioms.isoSetoid k F) G.1.toWeilDataAxioms =
            Quotient.mk _ T.toWeilDataAxioms)

Sources

LeanStacks.WeilCohomology.WeilData.globalSections_criterion · Stacks.WeilCohomology.WeilData.exists_not_globalSections_criterion · Stacks.WeilCohomology.WeilCohomologyTheory · Stacks.WeilCohomology.WeilCohomologyTheory.factorwise_rank_one_of_geometricallyIrreducible · Stacks.WeilCohomology.WeilRealization.exists_globalSections_isoClassEquiv

Section45.12 Chern classes #

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

Tag 0FI5, a proposition

Tag 0FI5 in the Stacks Project.

Stacks.WeilCohomology.existsUnique_isTotalChernClass_of_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/ChernClasses/KZeroRule.lean, line 598. The attribute's comment: “the proposition: existence and uniqueness of the rule c^A on all of K_0(Vect(X)), with its three properties, K_0(Vect(X)) being the Grothendieck group AlgebraicGeometry.VectorBundleKZero of Tag 0FDK and prod_{i >= 0} A^i(X) the family of components together with the clause mem_grade. NO constant rank and NO restriction to generators: properties (1) and (2) are stated for every element of K_0(Vect(X)) and the construction is for a module of arbitrary rank. The standing situation is the structure Stacks.WeilCohomology.ChernSetup -- the data the source fixes, with clause (1), clause (2), clause (3)(a), condition (1), condition (2), condition (4) and the source's grading A(X) = sum of the A^i(X) as isInternal_grade -- together with the three remaining conditions of the section, each in the source's own form: condition (3) at f^L itself; clause (3)(b) as the closure property IsBundleCompare at f^E itself; and clause (3)(c) as the closure property IsBundleEmbedding with condition (5) read at c_1^A(O_P(P')) for the divisor module characterized divisor-theoretically by IsSubbundleDivisorModule. NO hypothesis is read more strongly than the source states it: the invariance of the total Chern class under an isomorphism of modules, which K_0(Vect(X)) forces on any rule out of it and which a comparison of P(E) with P(E') would get only by asking clause (3)(b) at every E' isomorphic to f^E, is instead PROVED, as chernSeries_eq_of_iso, from multiplicativity in the short exact sequence 0 to E to E' to 0; the pseudofunctoriality coherence isomorphism h^(g^E) = (h . g)^E, which the source has for free, comes from the same theorem through pull_chernSeries_coeff_of_iso. The structure Stacks.WeilCohomology.ChernSituation is built inside the proof and is not an argument. PROVED here and in this directory, not assumed: the projective bundle with its flat projection, its invertible twist and its tautological sequence of kernel rank r, from clause (3)(a) (BundleObject.toBundleDatum); the rank-one case of that kernel rank (isFiniteLocallyFreeOfRank_kernel_of_epi_isInvertible_pred); condition (3) under an isomorphism of invertible modules (pull_c_1); condition (4) read with the grading (mem_grade_of_bundleFormula); the identification of twists along the induced morphism P(f^E) to P(E) (exists_bundleCompare) and along the induced closed immersion P(F) to P(E) (exists_divisorDatum); the source's identification O_P(P') = O_P(1) tensor (p^L)^{-1}, from the description of P(F) in P(E) as the zero scheme of a regular section (BundleObject.twistClass_eq_picardClassOf_add); clause (1), clause (2) and condition (2) with the local constancy of the rank, in the form 'A(X) is separated by, patched from and graded by its restrictions to the loci where E has constant rank' (eq_of_pull_constantRank, exists_pull_eq_constantRank, mem_grade_of_pull_constantRank, subsingleton_of_isEmpty); the construction of the Chern classes, equation 45.12.1.1, their centrality and homogeneity, their compatibility with pullback, the Whitney formula for an invertible submodule, multiplicativity in an arbitrary short exact sequence by induction on the rank, the arbitrary-rank total Chern class, the extension to K_0(Vect(X)) with the formal inverse, the three properties, and the uniqueness; the source's 'it suffices to check this after pulling back by P(E^dual) -- thus we may assume we have an invertible submodule L of E such that both E/L and F/L are finite locally free' (exists_splitInvertibleSub); the rank of the middle term of the sequence of clause (3)(c), from AlgebraicGeometry.SheafOfModules.rank_add_of_shortExact; and the first Chern class of the divisor class of that clause, from condition (3) with the additivity of c_1^A on Pic (c_1_divisorClass)”.

Stacks Project, Tag 0FI5. In the standing situation of Section 45.12 there is a unique rule which assigns to every object X of 𝒞 a total Chern class

c^A : K₀(Vect(X)) ⟶ ∏_{i ≥ 0} A^i(X)

such that (1) c^A(α + β) = c^A(α) c^A(β) and c^A(0) = 1, (2) f^* ∘ c^A = c^A ∘ f^* for a morphism f : X' ⟶ X of 𝒞, and (3) c^A([ℒ]) = 1 + c₁^A(ℒ) for ℒ ∈ Pic(X).

What the situation is. Stacks.WeilCohomology.ChernSetup is the source's own standing situation: the graded rings A(X) with the pullback ring maps and the additive c₁^A : Pic(X) ⟶ A¹(X) — the data the source fixes — together with clause (1), clause (2), clause (3)(a), condition (1), condition (2) and condition (4), and the grading A(X) = ⨁_{i ≥ 0} A^i(X) as isInternal_grade. Every field of it is a datum or a condition the source states; in particular Stacks.WeilCohomology.ChernSetup.bundleDatum — the projective bundle with its flat projection, its invertible twist and its tautological sequence — is a definition, built from clause (3)(a) by Stacks.WeilCohomology.BundleObject.toBundleDatum, and not a field.

The three remaining conditions of the section are the hypotheses here:

condition (3), f^*c₁^A(ℒ) = c₁^A(f^*ℒ), at f^*ℒ itself;

clause (3)(b), that the induced 𝐏(f^*ℰ) ⟶ 𝐏(ℰ) is a morphism of 𝒞 (Stacks.WeilCohomology.IsBundleCompare), at f^*ℰ itself and with nothing about twists;

clause (3)(c), that the induced closed immersion 𝐏(𝓕) ⟶ 𝐏(ℰ) is a morphism of 𝒞 (Stacks.WeilCohomology.IsBundleEmbedding), together with condition (5) read at c₁^A(𝒪_P(𝐏(𝓕))) for the divisor module characterized by Stacks.WeilCohomology.IsSubbundleDivisorModule.

No hypothesis is read more strongly than the source states it. In particular hcompare is clause (3)(b) at f^*ℰ itself. The invariance of the total Chern class under an isomorphism of modules, which K₀(Vect(X)) forces on any rule out of it and which a comparison of the projective bundles 𝐏(ℰ) and 𝐏(ℰ') would get only from a stronger reading of that clause, is instead the theorem Stacks.WeilCohomology.ChernSituation.chernSeries_eq_of_iso, proved from multiplicativity in the short exact sequence 0 ⟶ ℰ ⟶ ℰ' ⟶ 0 ⟶ 0. The pseudofunctoriality coherence isomorphism h^*(g^*ℰ) ≅ (h ≫ g)^*ℰ, which the source has for free by writing f^* as a strict functor, is handled by the same theorem through Stacks.WeilCohomology.ChernSituation.pull_chernSeries_coeff_of_iso.

The Stacks.WeilCohomology.ChernSituation the development is written over is assembled from these inside the proof, so it is not an argument of this statement. Everything the source derives rather than assumes is a theorem: condition (3) under an isomorphism of invertible modules (Stacks.WeilCohomology.ChernSituation.pull_c₁), condition (4) read with the grading (Stacks.WeilCohomology.SourceChernSetup.mem_grade_of_bundleFormula), the identifications of twists along the two induced morphisms (Stacks.WeilCohomology.ChernSituation.exists_bundleCompare and Stacks.WeilCohomology.ChernSituation.exists_divisorDatum), and 𝒪_P(𝐏(𝓕)) ≅ 𝒪_P(1) ⊗ (p^*ℒ)^{⊗ -1} (Stacks.WeilCohomology.BundleObject.twistClass_eq_picardClassOf_add).

theorem existsUnique_isTotalChernClass_of_source (𝔄 : SourceChernSetup.{u, v, v₁, w} C S)
    (hpull : PullbackFirstChernCondition 𝔄) (hcompare : BundleCompareClause 𝔄)
    (hdivisor : DivisorDatumClause 𝔄) :
    ∃! c : ∀ X : C, VectorBundleKZero (S.obj X) → ℕ → 𝔄.A X,
    IsTotalChernClassOnLocallyFree 𝔄.toChernSetup c

Stacks.WeilCohomology.eq_of_isTotalChernClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/ChernClasses/TotalChernClass.lean, line 226. The attribute's comment: “uniqueness, for the class of a module of constant rank; the existence half of the rule on all of K₀ needs condition (5), which ChernSetup does not carry, and property (2) is stated on generators — see the module documentation”.

The uniqueness half of Stacks Tag 0FI5. Properties (1), (2) and (3) determine the total Chern class of the class of a finite locally free module of constant rank: any two rules with those properties agree there.

The splitting principle of Tag 0FI7 supplies p : P ⟶ X with p^* injective on A and a filtration of p^*ℰ with invertible successive quotients. That filtration writes [p^*ℰ] as a sum of classes of invertible modules in K₀(Vect(P)), where properties (1) and (3) determine the total Chern class; property (2) identifies the result with p^*c^A([ℰ]), and p^* is injective.

theorem eq_of_isTotalChernClass {𝔄 : ChernSetup.{u, v, v₁, w} C S}
    {c c' : ∀ X : C, VectorBundleKZero (S.obj X) → ℕ → 𝔄.A X}
    (hc : IsTotalChernClass 𝔄 c) (hc' : IsTotalChernClass 𝔄 c') (X : C)
    (E : (S.obj X).Modules) (r : ℕ)
    (hE : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E r) (n : ℕ) :
    c X (VectorBundleKZero.classOf (S.obj X) E) n =
      c' X (VectorBundleKZero.classOf (S.obj X) E) n

Stacks.WeilCohomology.ChernSetup.chernClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/ChernClasses/TotalChernClass.lean, line 274. The attribute's comment: “the Chern classes of one finite locally free module of constant positive rank; not yet the rule on K₀”.

The Chern classes c_j^A(ℰ) of a finite locally free module of constant rank r + 1. The zeroth is 1, those in degrees 1, …, r + 1 are the entries of chernTuple with the signs of equation 45.12.1.1, and the rest vanish.

This is the construction half of Tag 0FI5 for a single module: a real body, the inverse of the bijection of condition (4) applied to an explicit element. It is not yet a rule on K₀(Vect(X)); see the module documentation.

def chernClass (j : ℕ) : 𝔄.A X

Stacks.WeilCohomology.ChernSetup.sum_chernClass_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/ChernClasses/TotalChernClass.lean, line 300. The attribute's comment: “equation 45.12.1.1, the relation defining the Chern classes”.

Equation 45.12.1.1, the relation that defines the Chern classes: ∑_{i=0}^{r+1} (-1)^i c₁^A(𝒪_P(1))^i ∪ p^*c^A_{r+1-i}(ℰ) = 0 in A(𝐏(ℰ)).

The term at i = r + 1 is (-1)^{r+1} c₁^A(𝒪_P(1))^{r+1}, because c_0^A(ℰ) = 1; the terms below it reproduce the projective bundle formula applied to the tuple, the two signs cancelling, and that is -(-1)^{r+1} c₁^A(𝒪_P(1))^{r+1} by construction.

theorem sum_chernClass_eq_zero :
    ∑ i : Fin (r + 2), ((-1 : ℤ) ^ (i : ℕ)) •
        (𝔄.c₁ (𝔄.bundleDatum X E r hE).bundle (𝔄.bundleDatum X E r hE).twistClass ^ (i : ℕ) *
          𝔄.pull (𝔄.bundleDatum X E r hE).proj (𝔄.chernClass X E r hE (r + 1 - (i : ℕ)))) = 0

Tag 0FI7, a lemma

Tag 0FI7 in the Stacks Project.

Stacks.WeilCohomology.ChernSetup.exists_injective_hasInvertibleFiltration, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/ChernClasses/SplittingPrinciple.lean, line 276. The attribute's comment: “the ranks are constant, as in the source; see the module documentation for the clauses of the standing situation that ChernSetup transcribes”.

The splitting principle, Stacks Tag 0FI7. In the standing situation of Section 45.12, let X be an object of 𝒞 and let ℰ_i be a finite collection of locally free 𝒪_X-modules of ranks r_i. There is a morphism p : P ⟶ X of 𝒞 such that p^* : A(X) ⟶ A(P) is injective and each p^*ℰ_i has a filtration of length r_i whose successive quotients are invertible 𝒪_P-modules. The projection is moreover flat.

The induction is on ∑ rᵢ. If every rank is at most one the identity of X already works, each ℰ_i being zero or invertible. Otherwise some rᵢ exceeds one; the projective bundle of ℰ_i gives p : P ⟶ X with its tautological sequence 0 ⟶ 𝓕 ⟶ p^*ℰ_i ⟶ 𝒪_P(1) ⟶ 0, and p^* is injective by the projective bundle formula. The inductive hypothesis applied to 𝓕 together with the p^*ℰ_{i'} for i' ≠ i produces q : Q ⟶ P, and q ≫ p is the required morphism: flatness of S q keeps the tautological sequence exact after pullback, so the filtration of q^*𝓕 extends by one step to one of q^*p^*ℰ_i.

theorem exists_injective_hasInvertibleFiltration (𝔄 : ChernSetup.{u, v, v₁, w} C S) (X : C)
    (I : Type*) [Finite I] (E : I → (S.obj X).Modules) (r : I → ℕ)
    (hE : ∀ i, AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} (E i) (r i)) :
    ∃ (P : C) (p : P ⟶ X), Flat (S.map p) ∧ Function.Injective (𝔄.pull p) ∧
      ∀ i, HasInvertibleFiltration (S.obj P)
        ((Scheme.Modules.pullback (S.map p)).obj (E i)) (r i)

Tag 0FI8, a lemma

Tag 0FI8 in the Stacks Project.

Stacks.WeilCohomology.ChernSetup.chernClass_tensorObj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/ChernClasses/Twist.lean, line 267. The attribute's comment: “the comparison 𝐏(ℰ) ≅ 𝐏(ℰ ⊗ ℒ) of projective bundles and its effect on the tautological class are hypotheses, the situation carrying no functoriality of 𝐏; the rank is constant and that of ℰ ⊗ ℒ is assumed; see the module documentation”.

Let ℰ be a finite locally free 𝒪_X-module of constant rank r + 1 and let ℒ be an invertible 𝒪_X-module, with ℰ ⊗ ℒ again of rank r + 1. Then for i ≤ r + 1 c^A_i(ℰ ⊗ ℒ) = ∑_{j=0}^{i} binom(r + 1 - i + j, j) c^A_{i-j}(ℰ) ∪ c₁^A(ℒ)^j, given an isomorphism g : 𝐏(ℰ) ≅ 𝐏(ℰ ⊗ ℒ) over X under which c₁^A(𝒪_{𝐏(ℰ ⊗ ℒ)}(1)) pulls back to c₁^A(𝒪_{𝐏(ℰ)}(1)) + p^*c₁^A(ℒ).

theorem chernClass_tensorObj (𝔄 : ChernSetup.{u, v, v₁, w} C S) (X : C)
    (E L : (S.obj X).Modules) (r : ℕ)
    (hE : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E (r + 1))
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible (S.obj X).presheaf
      (S.obj X).ringCatSheaf.2 L)
    (hEL : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
      (Scheme.Modules.tensorObjRingedSpace (S.obj X) E L) (r + 1))
    (g : (𝔄.bundleDatum X E r hE).bundle ≅
      (𝔄.bundleDatum X (Scheme.Modules.tensorObjRingedSpace (S.obj X) E L) r hEL).bundle)
    (hg : g.hom ≫ (𝔄.bundleDatum X
        (Scheme.Modules.tensorObjRingedSpace (S.obj X) E L) r hEL).proj =
      (𝔄.bundleDatum X E r hE).proj)
    (htwist : 𝔄.pull g.hom
        (𝔄.c₁ (𝔄.bundleDatum X (Scheme.Modules.tensorObjRingedSpace (S.obj X) E L) r hEL).bundle
          (𝔄.bundleDatum X
            (Scheme.Modules.tensorObjRingedSpace (S.obj X) E L) r hEL).twistClass) =
      𝔄.c₁ (𝔄.bundleDatum X E r hE).bundle (𝔄.bundleDatum X E r hE).twistClass +
        𝔄.pull (𝔄.bundleDatum X E r hE).proj (𝔄.c₁ X (picardClassOf (S.obj X) L hL)))
    (i : ℕ) (hi : i ≤ r + 1) :
    𝔄.chernClass X (Scheme.Modules.tensorObjRingedSpace (S.obj X) E L) r hEL i =
      ∑ j ∈ Finset.range (i + 1), (r + 1 - i + j).choose j •
        (𝔄.chernClass X E r hE (i - j) * 𝔄.c₁ X (picardClassOf (S.obj X) L hL) ^ j)

Stacks.WeilCohomology.IsTotalChernClassOnLocallyFree.apply_classOf_tensorObj_invertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/ChernClasses/TwistFormula.lean, line 180. The attribute's comment: “for every rule c^A with the three properties of Tag 0FI5 (by that proposition there is exactly one), at the Chern classes c^A_i(E) = the i-th component of c^A([E]); E of constant rank r, L invertible, i <= r. Unconditional: no comparison of projective bundles is assumed; the proof is the splitting principle 0FI7 instead of Constructions 02NC”.

Stacks Project, Tag 0FI8: the Chern classes of a twist. In the standing situation of Section 45.12, let c^A be a rule with the three properties of Tag 0FI5, let ℰ be a finite locally free 𝒪_X-module of constant rank r and ℒ an invertible 𝒪_X-module. Then for i ≤ r

c^A_i(ℰ ⊗ ℒ) = ∑_{j=0}^{i} binom(r - i + j, j) c^A_{i-j}(ℰ) ∪ c₁^A(ℒ)^j,

where c^A_i(ℱ) is the i-th component of c^A([ℱ]). By the splitting principle, Tag 0FI7, after an injective pullback ℰ has Chern roots x_1, …, x_r and ℰ ⊗ ℒ the roots x_k + t with t the pullback of c₁^A(ℒ); the formula is then Stacks.WeilCohomology.esymm_map_add_const.

theorem apply_classOf_tensorObj_invertible (hc : IsTotalChernClassOnLocallyFree 𝔄 c) (X : C)
    (E L : (S.obj X).Modules) (r : ℕ)
    (hE : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E r)
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible (S.obj X).presheaf
      (S.obj X).ringCatSheaf.2 L) (i : ℕ) (hi : i ≤ r) :
    c X (VectorBundleKZero.classOf (S.obj X)
        (Scheme.Modules.tensorObjRingedSpace (S.obj X) E L)) i =
      ∑ j ∈ Finset.range (i + 1), (r - i + j).choose j •
        (c X (VectorBundleKZero.classOf (S.obj X) E) (i - j) *
          𝔄.c₁ X (picardClassOf (S.obj X) L hL) ^ j)

Stacks.WeilCohomology.chernClass_tensorObjRingedSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/ChernClasses/TwistUnconditional.lean, line 422. The attribute's comment: “for E of constant rank r + 1 and every i, the binomial coefficient binom(r - i + j, j) written (r + 1 + j - i).choose j in N, which agrees with it wherever the term c_{i-j}(E) is nonzero. The situation is SourceChernSetup with the source's condition (3), clause (3)(b) and clause (3)(c) (QuotientBundleEmbeddingClause, the closure property for an arbitrary surjection), each as the source states it. PROVED, not assumed: the comparison of P(E) with P(E tensor L) inside the category and g^c_1(O(1)) = c_1(O(1)) + p^c_1(L) (exists_bundleTensor_comparison, from Tag 02NC exists_bundleTensorIso, Tag 01CD and Tag 01CX), and the rank of E tensor L. The rule c^A on K_0 and an arbitrary finite locally free E are ChernSituation.totalChernClass_classOf_tensorObjRingedSpace and ChernSituation.pull_totalChernClass_classOf_tensorObjRingedSpace”.

Stacks Project, Tag 0FI8. In the standing situation of Section 45.12, let ℰ be a finite locally free 𝒪_X-module of constant rank r + 1 and ℒ an invertible 𝒪_X-module. Then for every i c^A_i(ℰ ⊗ ℒ) = ∑_{j=0}^{i} binom(r + 1 - i + j, j) c^A_{i-j}(ℰ) ∪ c₁^A(ℒ)^j, the binomial coefficient written (r + 1 + j - i).choose j (see the module documentation).

The situation is Stacks.WeilCohomology.SourceChernSetup with the source's condition (3), clause (3)(b) and clause (3)(c), each in the source's own form. The comparison of 𝐏(ℰ) with 𝐏(ℰ ⊗ ℒ) and its effect on c₁^A(𝒪(1)) are proved (Stacks.WeilCohomology.exists_bundleTensor_comparison, from Tag 02NC), and so is the rank of ℰ ⊗ ℒ.

theorem chernClass_tensorObjRingedSpace (𝔄 : SourceChernSetup.{u, v, v₁, w} C S)
    (hpull : PullbackFirstChernCondition 𝔄) (hcompare : BundleCompareClause 𝔄)
    (hquot : QuotientBundleEmbeddingClause 𝔄) (X : C) (E L : (S.obj X).Modules) (r : ℕ)
    (hE : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E (r + 1))
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible (S.obj X).presheaf
      (S.obj X).ringCatSheaf.2 L) (i : ℕ) :
    𝔄.chernClass X (Scheme.Modules.tensorObjRingedSpace (S.obj X) E L) r
        (isFiniteLocallyFreeOfRank_tensorObjRingedSpace_of_isInvertible E L (r + 1) hE hL) i =
      ∑ j ∈ Finset.range (i + 1), (r + 1 + j - i).choose j •
        (𝔄.chernClass X E r hE (i - j) * 𝔄.c₁ X (picardClassOf (S.obj X) L hL) ^ j)

Stacks.WeilCohomology.ChernSituation.totalChernClass_classOf_tensorObjRingedSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/ChernClasses/TwistUnconditional.lean, line 543. The attribute's comment: “for the rule c^A of Tag 0FI5 (ChernSituation.totalChernClass on K_0(Vect(X))), E of constant rank r, r = 0 included, and every i; binom(r - i + j, j) written (r + j - i).choose j in N, which agrees with it wherever c_{i-j}(E) is nonzero. The situation is ChernSituation, the source's clauses and conditions each in the source's form, with the source's clause (3)(c) for an arbitrary surjection (QuotientBundleEmbeddingClause). The comparison of P(E) with P(E tensor L) and the rank of E tensor L are proved; see chernClass_tensorObjRingedSpace”.

Stacks Project, Tag 0FI8, for the rule c^A of Tag 0FI5. In the standing situation, for ℰ finite locally free of constant rank r (r = 0 included) and ℒ invertible, c^A_i([ℰ ⊗ ℒ]) = ∑_{j=0}^{i} binom(r - i + j, j) c^A_{i-j}([ℰ]) ∪ c₁^A(ℒ)^j for every i.

theorem totalChernClass_classOf_tensorObjRingedSpace
    (hquot : QuotientBundleEmbeddingClause 𝔖.toSourceChernSetup) (X : C)
    (E L : (S.obj X).Modules) (r : ℕ)
    (hE : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E r)
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible (S.obj X).presheaf
      (S.obj X).ringCatSheaf.2 L) (i : ℕ) :
    𝔖.totalChernClass X
        (VectorBundleKZero.classOf (S.obj X) (Scheme.Modules.tensorObjRingedSpace (S.obj X) E L))
        i =
      ∑ j ∈ Finset.range (i + 1), (r + j - i).choose j •
        (𝔖.totalChernClass X (VectorBundleKZero.classOf (S.obj X) E) (i - j) *
          𝔖.c₁ X (picardClassOf (S.obj X) L hL) ^ j)

Stacks.WeilCohomology.ChernSituation.pull_totalChernClass_classOf_tensorObjRingedSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/ChernClasses/TwistUnconditional.lean, line 578. The attribute's comment: “for the rule c^A of Tag 0FI5 and an ARBITRARY finite locally free E: the formula holds after pullback along every morphism f : Z to X of the category along which E has constant rank r, which by condition (2) (ChernSituation.eq_of_pull_one) determines c^A_i(E tensor L); binom(r - i + j, j) written (r + j - i).choose j in N, which agrees with it wherever c_{i-j}(f^E) is nonzero. The situation is ChernSituation with the source's clause (3)(c) for an arbitrary surjection (QuotientBundleEmbeddingClause). Proved, not assumed: the comparison of P(E) with P(E tensor L), the rank of E tensor L, and f^(E tensor L) = f^E tensor f^L (Tag 01CD)”.

Stacks Project, Tag 0FI8, for the rule c^A of Tag 0FI5 and an arbitrary finite locally free module. In the standing situation, let ℰ be finite locally free, of possibly non-constant rank, and ℒ invertible. On every object f : Z ⟶ X over X on which ℰ has constant rank r, f^*c^A_i([ℰ ⊗ ℒ]) = ∑_{j=0}^{i} binom(r - i + j, j) f^*c^A_{i-j}([ℰ]) ∪ f^*c₁^A(ℒ)^j.

The source's r is the rank of ℰ, and its proof begins "by the construction of c^A_i we may assume ℰ has constant rank r": the formula is read on the loci of constant rank, and by condition (2) these determine A(X) (Stacks.WeilCohomology.ChernSituation.eq_of_pull_one).

theorem pull_totalChernClass_classOf_tensorObjRingedSpace
    (hquot : QuotientBundleEmbeddingClause 𝔖.toSourceChernSetup) (X : C)
    (E L : (S.obj X).Modules)
    (hE : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u}
      (R := (S.obj X).ringCatSheaf) E)
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible (S.obj X).presheaf
      (S.obj X).ringCatSheaf.2 L) (Z : C) (f : Z ⟶ X) (r : ℕ)
    (hr : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
      ((Scheme.Modules.pullback (S.map f)).obj E) r) (i : ℕ) :
    𝔖.pull f (𝔖.totalChernClass X
        (VectorBundleKZero.classOf (S.obj X) (Scheme.Modules.tensorObjRingedSpace (S.obj X) E L))
        i) =
      ∑ j ∈ Finset.range (i + 1), (r + j - i).choose j •
        (𝔖.pull f (𝔖.totalChernClass X (VectorBundleKZero.classOf (S.obj X) E) (i - j)) *
          𝔖.pull f (𝔖.c₁ X (picardClassOf (S.obj X) L hL)) ^ j)

Tag 0FI9, a proposition

Tag 0FI9 in the Stacks Project.

Stacks.WeilCohomology.eq_of_isChernCharacter, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/ChernClasses/ChernCharacter.lean, line 167. The attribute's comment: “uniqueness, for the class of a module of constant rank; the existence half needs the locally constant rank r^A, which is indexed by condition (2) of the situation, and the Chern classes of Tag 0FI5 on all of K₀, and property (2) is stated on generators — see the module documentation”.

The uniqueness half of Stacks Tag 0FI9. Properties (1), (2) and (3) determine the Chern character of the class of a finite locally free module of constant rank: any two rules with those properties agree there.

The splitting principle of Tag 0FI7 supplies p : P ⟶ X with p^* injective on A and a filtration of p^*ℰ with invertible successive quotients. That filtration writes [p^*ℰ] as a sum of classes of invertible modules in K₀(Vect(P)), where additivity and the value on an invertible module determine the Chern character; property (2) identifies the result with p^*ch^A([ℰ]), and p^* is injective.

theorem eq_of_isChernCharacter {𝔄 : ChernSetup.{u, v, v₁, w} C S}
    [∀ X : C, Algebra ℚ (𝔄.A X)]
    {ch ch' : ∀ X : C, VectorBundleKZero (S.obj X) → ℕ → 𝔄.A X}
    (hch : IsChernCharacter 𝔄 ch) (hch' : IsChernCharacter 𝔄 ch') (X : C)
    (E : (S.obj X).Modules) (r : ℕ)
    (hE : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E r) (n : ℕ) :
    ch X (VectorBundleKZero.classOf (S.obj X) E) n =
      ch' X (VectorBundleKZero.classOf (S.obj X) E) n

Stacks.WeilCohomology.existsUnique_isChernCharacter_of_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/ChernClasses/ChernCharacterExistence.lean, line 788. The attribute's comment: “the unique rule ch^A : K₀(Vect(X)) ⟶ ∏_{i ≥ 0} A^i(X) with properties (1), (2) and (3), both halves, on all of K₀(Vect(X)) and with no restriction on the rank, in the standing situation of Section 45.12 read with 𝐐-coefficients. The standing situation is the structure Stacks.WeilCohomology.ChernSetup -- the data the source fixes, with clause (1), clause (2), clause (3)(a), condition (1), condition (2), condition (4) and the source's grading A(X) = sum of the A^i(X) -- together with the section's three remaining conditions (PullbackFirstChernCondition, BundleCompareClause, DivisorDatumClause), each in the source's own form, and the 𝐐-coefficients as an algebra structure with the rationals lying in A^0(X). The structures Stacks.WeilCohomology.ChernSituation and RationalChernSituation are built inside the proof and are not arguments. PROVED and not assumed: the total Chern classes of Tag 0FI5, which the source's own proof cites as Proposition 45.12.1 (Stacks.WeilCohomology.ChernSituation.isTotalChernClass_totalChernClass); the rank class r^A, which is Stacks.WeilCohomology.SourceChernSetup.rankClass, constructed from condition (2) as the source constructs it, with its membership in A^0(X) and its compatibility with pullback along an arbitrary morphism; and the projective bundle with its flat projection, invertible twist and tautological sequence, from clause (3)(a). Property (2) is stated on the generators, which IsChernCharacterOnLocallyFree.map_pull_kzero upgrades to the source's form, read against the CONSTRUCTED pullback homomorphism AlgebraicGeometry.VectorBundleKZero.pullbackRingHom of K₀(Vect(-)). NO hypothesis is read more strongly than the source states it: BundleCompareClause is clause (3)(b) at f^E itself, and the invariance of the total Chern class under an isomorphism of modules, together with the pseudofunctoriality coherence isomorphism h^(g^E) = (h . g)^E, are PROVED (chernSeries_eq_of_iso, pull_chernSeries_coeff_of_iso) rather than obtained by asking that clause at every module isomorphic to f^*E”.

In the standing situation of Section 45.12, read with 𝐐-coefficients, there is exactly one rule assigning to every object X of 𝒞 a Chern character

ch^A : K₀(Vect(X)) ⟶ ∏_{i ≥ 0} A^i(X)

which is a ring map, is compatible with pullback, and sends an invertible module ℒ to exp(c₁^A(ℒ)).

The situation is a Stacks.WeilCohomology.SourceChernSetup together with the section's three remaining conditions as the hypotheses hpull, hcompare and hdivisor (Stacks.WeilCohomology.PullbackFirstChernCondition, Stacks.WeilCohomology.BundleCompareClause, Stacks.WeilCohomology.DivisorDatumClause), and the 𝐐-coefficients are the ℚ-algebra structure together with hq, which says that the rationals lie in A^0(X).

theorem existsUnique_isChernCharacter_of_source (𝔄 : SourceChernSetup.{u, v, v₁, w} C S)
    [∀ X : C, Algebra ℚ (𝔄.A X)]
    (hq : ∀ (X : C) (q : ℚ), algebraMap ℚ (𝔄.A X) q ∈ 𝔄.grade X 0)
    (hpull : PullbackFirstChernCondition 𝔄) (hcompare : BundleCompareClause 𝔄)
    (hdivisor : DivisorDatumClause 𝔄) :
    ∃! ch : ∀ X : C, VectorBundleKZero (S.obj X) → ℕ → 𝔄.A X,
    IsChernCharacterOnLocallyFree 𝔄.toChernSetup ch

Stacks.WeilCohomology.eq_of_isChernCharacterOnLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/ChernClasses/ChernCharacterUniqueness.lean, line 168. The attribute's comment: “uniqueness, on all of K₀(Vect(X)) and with no restriction on the rank: two rules with properties (1), (2) and (3) are equal. Property (2) is stated on the generators, which IsChernCharacterOnLocallyFree.map_pull_kzero upgrades to the source's form, read against the CONSTRUCTED pullback homomorphism AlgebraicGeometry.VectorBundleKZero.pullbackRingHom of K₀(Vect(-))”.

The uniqueness half of Stacks Tag 0FI9. Properties (1), (2) and (3) determine the Chern character on all of K₀(Vect(X)): any two rules with those properties are equal.

theorem eq_of_isChernCharacterOnLocallyFree {𝔄 : SourceChernSetup.{u, v, v₁, w} C S}
    [∀ X : C, Algebra ℚ (𝔄.A X)]
    {ch ch' : ∀ X : C, VectorBundleKZero (S.obj X) → ℕ → 𝔄.A X}
    (hch : IsChernCharacterOnLocallyFree 𝔄.toChernSetup ch)
    (hch' : IsChernCharacterOnLocallyFree 𝔄.toChernSetup ch') (X : C)
    (α : VectorBundleKZero (S.obj X)) (n : ℕ) :
    ch X α n = ch' X α n

Tag 0FIA, a lemma

Tag 0FIA in the Stacks Project.

Stacks.WeilCohomology.chernClass_secondAdams_kZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/ChernClasses/AdamsEigenvaluesKZero.lean, line 191. The attribute's comment: “the identity c^A_i(psi^2(alpha)) = 2^i c^A_i(alpha) for EVERY element alpha of K_0(Vect(X)) and a module of ARBITRARY rank -- the source's own statement, with no restriction to generators and no constant rank: the reduction to the generators is eq_of_convolutive_of_eq_classOf and the reduction to constant rank is the source's decomposition of X by the rank, ChernSetup.eq_of_pull_constantRank. The rule c^A is the predicate IsTotalChernClassOnLocallyFree of Tag 0FI5, which exactly one rule satisfies (existsUnique_isTotalChernClass_of_source), so fixing it by that predicate is the source's 'let c^A be as in Proposition 45.12.1'. psi^2 is named by the two properties Tag 0FEJ gives it, its value on an invertible module and its commutation with the pullback of K_0(Vect(-)), and the identity is proved for every ring endomorphism with those two properties; this repository CONSTRUCTS such a map, VectorBundleKZero.secondAdamsRingHom, and the two properties are verified for it in chernClass_secondAdams_secondAdamsRingHom. The pullback of K_0(Vect(-)) is NOT named by a property: it is the constructed ring homomorphism VectorBundleKZero.pullbackRingHom, with its defining property pullback_classOf, and property (2) is read against it by IsTotalChernClassOnLocallyFree.map_pull_kZero. psi^2([L]) = [L tensor L] is read in Pic, where addition is the tensor product by Tag 01CX (picardClassOf_tensorObjRingedSpace)”.

Stacks Project, Tag 0FIA for the total Chern class. The second Adams operator scales the degree-n part of the total Chern class by 2^n: c^A_n(ψ²(α)) = 2^n c^A_n(α) for every α ∈ K₀(Vect(X)).

The rule c^A is the one of Tag 0FI5, named by Stacks.WeilCohomology.IsTotalChernClassOnLocallyFree, and ψ² is named by the two properties Tag 0FEJ gives it. The pullback of K₀(Vect(-)) is the constructed AlgebraicGeometry.VectorBundleKZero.pullbackRingHom; see the module documentation.

theorem chernClass_secondAdams_kZero
    {c : ∀ X : C, VectorBundleKZero (S.obj X) → ℕ → 𝔄.A X}
    (hc : IsTotalChernClassOnLocallyFree 𝔄.toChernSetup c)
    (hψpull : ∀ {X Y : C} (f : X ⟶ Y) (α : VectorBundleKZero (S.obj Y)),
      VectorBundleKZero.pullbackRingHom (S.map f) (ψ Y α) =
        ψ X (VectorBundleKZero.pullbackRingHom (S.map f) α))
    (hψinv : ∀ (X : C) (L : (S.obj X).Modules)
      (hL : AlgebraicGeometry.SheafOfModules.IsInvertible (S.obj X).presheaf
        (S.obj X).ringCatSheaf.2 L),
      ∃ (M : (S.obj X).Modules) (hM : AlgebraicGeometry.SheafOfModules.IsInvertible
        (S.obj X).presheaf (S.obj X).ringCatSheaf.2 M),
        ψ X (VectorBundleKZero.classOf (S.obj X) L) =
            VectorBundleKZero.classOf (S.obj X) M ∧
          picardClassOf (S.obj X) M hM = 2 • picardClassOf (S.obj X) L hL)
    (X : C) (α : VectorBundleKZero (S.obj X)) (n : ℕ) :
    c X (ψ X α) n = (2 ^ n : ℕ) • c X α n

Stacks.WeilCohomology.chernCharacter_secondAdams_kZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/ChernClasses/AdamsEigenvaluesKZero.lean, line 258. The attribute's comment: “the identity ch^A_i(psi^2(alpha)) = 2^i ch^A_i(alpha) for EVERY element alpha of K_0(Vect(X)) and a module of ARBITRARY rank -- the source's own statement, with no restriction to generators and no constant rank: the reduction to the generators is VectorBundleKZero.addHom_ext and the reduction to constant rank is the source's decomposition of X by the rank, ChernSetup.eq_of_pull_constantRank. The rule ch^A is the predicate IsChernCharacterOnLocallyFree of Tag 0FI9, which exactly one rule satisfies (existsUnique_isChernCharacter_of_source), so fixing it by that predicate is the source's 'let ch^A be as in Proposition 45.12.4'. psi^2 is named by the two properties Tag 0FEJ gives it, its value on an invertible module and its commutation with the pullback of K_0(Vect(-)), and the identity is proved for every ring endomorphism with those two properties; this repository CONSTRUCTS such a map, VectorBundleKZero.secondAdamsRingHom, and the two properties are verified for it in chernCharacter_secondAdams_secondAdamsRingHom. The pullback of K_0(Vect(-)) is NOT named by a property: it is the constructed ring homomorphism VectorBundleKZero.pullbackRingHom, with its defining property pullback_classOf, and property (2) is read against it by IsChernCharacterOnLocallyFree.map_pull_kzero. psi^2([L]) = [L tensor L] is read in Pic, where addition is the tensor product by Tag 01CX (picardClassOf_tensorObjRingedSpace)”.

Stacks Project, Tag 0FIA for the Chern character. The second Adams operator scales the degree-n part of the Chern character by 2^n: ch^A_n(ψ²(α)) = 2^n ch^A_n(α) for every α ∈ K₀(Vect(X)).

The rule ch^A is the one of Tag 0FI9, named by Stacks.WeilCohomology.IsChernCharacterOnLocallyFree, and ψ² is named by the two properties Tag 0FEJ gives it. The pullback of K₀(Vect(-)) is the constructed AlgebraicGeometry.VectorBundleKZero.pullbackRingHom; see the module documentation.

theorem chernCharacter_secondAdams_kZero [∀ X : C, Algebra ℚ (𝔄.A X)]
    {ch : ∀ X : C, VectorBundleKZero (S.obj X) → ℕ → 𝔄.A X}
    (hch : IsChernCharacterOnLocallyFree 𝔄.toChernSetup ch)
    (hψpull : ∀ {X Y : C} (f : X ⟶ Y) (α : VectorBundleKZero (S.obj Y)),
      VectorBundleKZero.pullbackRingHom (S.map f) (ψ Y α) =
        ψ X (VectorBundleKZero.pullbackRingHom (S.map f) α))
    (hψinv : ∀ (X : C) (L : (S.obj X).Modules)
      (hL : AlgebraicGeometry.SheafOfModules.IsInvertible (S.obj X).presheaf
        (S.obj X).ringCatSheaf.2 L),
      ∃ (M : (S.obj X).Modules) (hM : AlgebraicGeometry.SheafOfModules.IsInvertible
        (S.obj X).presheaf (S.obj X).ringCatSheaf.2 M),
        ψ X (VectorBundleKZero.classOf (S.obj X) L) =
            VectorBundleKZero.classOf (S.obj X) M ∧
          picardClassOf (S.obj X) M hM = 2 • picardClassOf (S.obj X) L hL)
    (X : C) (α : VectorBundleKZero (S.obj X)) (n : ℕ) :
    ch X (ψ X α) n = (2 ^ n : ℕ) • ch X α n

Sources

Section45.13 Exterior powers and K-groups #

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

Tag 0FIC, a lemma

Tag 0FIC in the Stacks Project.

AlgebraicGeometry.VectorBundleKZero.exists_lambdaOperations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/LambdaOperations.lean, line 547. The attribute's comment: “all three clauses, granted one hypothesis: the filtration of ⋀ⁿ along a short exact sequence of finite locally free modules, which the library does not construct. The pullback homomorphism of K₀(Vect(-)), whose construction the source omits, is also a hypothesis”. References: SGA 6 0 (2.9), “partial”; SGA 6 V (2.2.1), “Second conjunct only”.

Stacks Project, Tag 0FIC. Let X be a scheme. There are maps λ^r : K₀(Vect(X)) → K₀(Vect(X)) which send [ℰ] to [⋀^r ℰ] when ℰ is a finite locally free 𝒪_X-module and which are compatible with pullbacks.

All three clauses of the source are present: the operations are produced as a family of maps, the second conjunct is their value on the class of a finite locally free module, and the third is their commutation with any ring map of Grothendieck rings realising pullback of finite locally free modules.

The sole hypothesis ExteriorPowersData X is the geometric input of the source's proof: the filtration of ⋀ⁿ along a short exact sequence, which the library does not construct. Finite local freeness of ⋀ⁿ ℰ and the comparison f^*(⋀^r ℰ) ≅ ⋀^r(f^*ℰ) of Tag 01CI are not assumed; both are proved.

theorem exists_lambdaOperations (X : Scheme.{u}) (h : ExteriorPowersData X) :
    ∃ lam : ℕ → VectorBundleKZero X → VectorBundleKZero X,
      (∀ (r : ℕ) (E : X.Modules), IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) E →
          lam r (classOf X E) = classOf X (Scheme.Modules.exteriorPower E (r : ℤ))) ∧
        (∀ (Y : Scheme.{u}) (f : Y ⟶ X) (hY : ExteriorPowersData Y)
            (p : VectorBundleKZero X →+* VectorBundleKZero Y),
          (∀ E : X.Modules, IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) E →
              p (classOf X E) = classOf Y ((Scheme.Modules.pullback f).obj E)) →
            (∀ E : X.Modules, IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) E →
              IsFiniteLocallyFree.{u, u, u} (R := Y.ringCatSheaf)
                ((Scheme.Modules.pullback f).obj E)) →
              ∀ (r : ℕ) (a : VectorBundleKZero X),
                lambdaOperation hY r (p a) = p (lambdaOperation h r a))

AlgebraicGeometry.VectorBundleKZero.exists_lambdaOperations_pullbackRingHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/LambdaOperationsScheme.lean, line 290. The attribute's comment: “the maps λ^r on K₀(Vect(X)) for every scheme X, their value λ^r[ℰ] = [⋀^r ℰ] on finite locally free modules, and their compatibility with pullback λ^r ∘ f^* = f^* ∘ λ^r for the pullback ring map f^* of K₀(Vect(-)); no hypothesis”. References: SGA 6 X (1.2), “clause (1.2.1)”.

Stacks Project, Tag 0FIC. Let X be a scheme. There are maps λ^r : K₀(Vect(X)) → K₀(Vect(X)) which send [ℰ] to [⋀^r ℰ] when ℰ is a finite locally free 𝒪_X-module and which are compatible with pullbacks: for every morphism of schemes f : Y ⟶ X, λ^r ∘ f^* = f^* ∘ λ^r, where f^* is the pullback ring map pullbackRingHom f.

The family is X ↦ lambdaOperation (exteriorPowersData X), so nothing is assumed: the filtration relation the construction consumes is exteriorPowersData, and the pullback map is the one constructed in StacksFrontier.AlgebraicGeometry.Chow.VectorBundleKZeroPullback.

theorem exists_lambdaOperations_pullbackRingHom :
    ∃ lam : ∀ X : Scheme.{u}, ℕ → VectorBundleKZero X → VectorBundleKZero X,
      (∀ (X : Scheme.{u}) (r : ℕ) (E : X.Modules),
          IsFiniteLocallyFree.{u, u, u} (R := X.ringCatSheaf) E →
            lam X r (classOf X E) = classOf X (Scheme.Modules.exteriorPower E (r : ℤ))) ∧
        (∀ {X Y : Scheme.{u}} (f : Y ⟶ X) (r : ℕ) (a : VectorBundleKZero X),
          lam Y r (pullbackRingHom f a) = pullbackRingHom f (lam X r a))

Sources

LeanAlgebraicGeometry.VectorBundleKZero.exists_lambdaOperations · AlgebraicGeometry.VectorBundleKZero.exists_lambdaOperations_pullbackRingHom

Section45.14 Weil cohomology theories, III #

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

Tag 0FIE, a lemma

Tag 0FIE in the Stacks Project.

Stacks.WeilCohomology.eq_of_cohomologicalChernCharacter, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/CohomologicalChernCharacter.lean, line 238. The attribute's comment: “uniqueness, for the class of a finite locally free module of constant rank: two rules compatible with pullbacks and taking the value exp(c₁^H(ℒ)) on an invertible module agree there. Constant rank is the source's reduction by condition (2) of the situation of Section 45.12, which ChernSetup does not transcribe, and the pullback homomorphism of K₀(Vect(-)), which this repository does not construct, is a hypothesis”.

The uniqueness half of Stacks Tag 0FIE. Two rules assigning to every object X of 𝒞 a ring homomorphism K₀(Vect(X)) ⟶ ∏_{i ≥ 0} H^{2i}(X)(i), compatible with pullbacks and taking the value exp(c_1^H(ℒ)) on every invertible module, agree on the class of every finite locally free module of constant rank.

The splitting principle of Tag 0FI7 supplies p : P ⟶ X with p^* injective on A and a filtration of p^*ℰ with invertible successive quotients. That filtration writes [p^*ℰ] as a sum of classes of invertible modules in K₀(Vect(P)), where additivity and the prescribed value determine the character; compatibility with pullbacks identifies the result with p^*ch^H([ℰ]), and p^* is injective.

theorem eq_of_cohomologicalChernCharacter
    (hκ : ∀ {X Y : C} (f : X ⟶ Y) (E : (S.obj Y).Modules),
      Stacks.FiniteLocallyFree.IsFiniteLocallyFree.{u, u, u} E →
        κ f (VectorBundleKZero.classOf (S.obj Y) E) =
          VectorBundleKZero.classOf (S.obj X) ((Scheme.Modules.pullback (S.map f)).obj E))
    {ch ch' : ∀ X : C, VectorBundleKZero (S.obj X) →+* PowerSeries (𝔄.A X)}
    (hpull : ∀ {X Y : C} (f : X ⟶ Y) (α : VectorBundleKZero (S.obj Y)),
      PowerSeries.map (𝔄.pull f) (ch Y α) = ch X (κ f α))
    (hpull' : ∀ {X Y : C} (f : X ⟶ Y) (α : VectorBundleKZero (S.obj Y)),
      PowerSeries.map (𝔄.pull f) (ch' Y α) = ch' X (κ f α))
    (hinv : ∀ (X : C) (L : (S.obj X).Modules)
      (hL : AlgebraicGeometry.SheafOfModules.IsInvertible (S.obj X).presheaf
        (S.obj X).ringCatSheaf.2 L),
      ch X (VectorBundleKZero.classOf (S.obj X) L) =
        expFirstChernClass 𝔄 X (picardClassOf (S.obj X) L hL))
    (hinv' : ∀ (X : C) (L : (S.obj X).Modules)
      (hL : AlgebraicGeometry.SheafOfModules.IsInvertible (S.obj X).presheaf
        (S.obj X).ringCatSheaf.2 L),
      ch' X (VectorBundleKZero.classOf (S.obj X) L) =
        expFirstChernClass 𝔄 X (picardClassOf (S.obj X) L hL))
    (X : C) (E : (S.obj X).Modules) (r : ℕ)
    (hE : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} E r) :
    ch X (VectorBundleKZero.classOf (S.obj X) E) =
      ch' X (VectorBundleKZero.classOf (S.obj X) E)

Stacks.WeilCohomology.exists_cohomologicalChernCharacter, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/CohomologicalChernCharacter.lean, line 287. The attribute's comment: “existence: the rule, as a ring homomorphism out of K₀(Vect(X)) into ∏_{i ≥ 0} H^{2i}(X)(i), together with its grading, its compatibility with pullbacks and its value exp(c₁^H(ℒ)) on an invertible module. The cohomological Chern character of a single finite locally free module, which Tag 0FI9's existence half constructs from the locally constant rank r^A and the Chern classes of Tag 0FI5 on all of K₀ — neither available here, both resting on condition (2) of the situation, which ChernSetup does not transcribe — is a hypothesis, as is the pullback homomorphism of K₀(Vect(-))”.

The existence half of Stacks Tag 0FIE. The cohomological Chern character of a single finite locally free module extends to a ring homomorphism ch^H : K₀(Vect(X)) ⟶ ∏_{i ≥ 0} H^{2i}(X)(i) for every object X of 𝒞, which is graded, compatible with pullbacks, and takes the value exp(c_1^H(ℒ)) on an invertible module.

The extension is Tag 0FEM's universal property of the Grothendieck ring, applied to the given additive, multiplicative and unital assignment; the grading and the compatibility with pullbacks pass from the generators to all of K₀(Vect(X)) because the graded series form a subgroup and because both sides of the pullback equation are additive.

theorem exists_cohomologicalChernCharacter
    (hκ : ∀ {X Y : C} (f : X ⟶ Y) (E : (S.obj Y).Modules),
      Stacks.FiniteLocallyFree.IsFiniteLocallyFree.{u, u, u} E →
        κ f (VectorBundleKZero.classOf (S.obj Y) E) =
          VectorBundleKZero.classOf (S.obj X) ((Scheme.Modules.pullback (S.map f)).obj E))
    (chM : ∀ X : C, (S.obj X).Modules → PowerSeries (𝔄.A X))
    (hzero : ∀ (X : C) (M : (S.obj X).Modules),
      ¬ Stacks.FiniteLocallyFree.IsFiniteLocallyFree.{u, u, u} M → chM X M = 0)
    (hadd : ∀ (X : C) {E F G : (S.obj X).Modules} (f : E ⟶ F) (g : F ⟶ G) (w : f ≫ g = 0),
      Stacks.FiniteLocallyFree.IsFiniteLocallyFree.{u, u, u} E →
        Stacks.FiniteLocallyFree.IsFiniteLocallyFree.{u, u, u} F →
          Stacks.FiniteLocallyFree.IsFiniteLocallyFree.{u, u, u} G →
            Mono f → Epi g → (ShortComplex.mk f g w).Exact →
              chM X F = chM X E + chM X G)
    (hmul : ∀ (X : C) (M N : (S.obj X).Modules),
      Stacks.FiniteLocallyFree.IsFiniteLocallyFree.{u, u, u} M →
        Stacks.FiniteLocallyFree.IsFiniteLocallyFree.{u, u, u} N →
          chM X (Scheme.Modules.tensorObjRingedSpace (S.obj X) M N) = chM X M * chM X N)
    (hone : ∀ X : C, chM X (SheafOfModules.unit (S.obj X).ringCatSheaf) = 1)
    (hgrade : ∀ (X : C) (M : (S.obj X).Modules), chM X M ∈ gradedPowerSeries 𝔄 X)
    (hinvM : ∀ (X : C) (L : (S.obj X).Modules)
      (hL : AlgebraicGeometry.SheafOfModules.IsInvertible (S.obj X).presheaf
        (S.obj X).ringCatSheaf.2 L),
      chM X L = expFirstChernClass 𝔄 X (picardClassOf (S.obj X) L hL))
    (hpullM : ∀ {X Y : C} (f : X ⟶ Y) (E : (S.obj Y).Modules),
      Stacks.FiniteLocallyFree.IsFiniteLocallyFree.{u, u, u} E →
        PowerSeries.map (𝔄.pull f) (chM Y E) =
          chM X ((Scheme.Modules.pullback (S.map f)).obj E))
    (hflf : ∀ {X Y : C} (f : X ⟶ Y) (E : (S.obj Y).Modules),
      Stacks.FiniteLocallyFree.IsFiniteLocallyFree.{u, u, u} E →
        Stacks.FiniteLocallyFree.IsFiniteLocallyFree.{u, u, u}
          ((Scheme.Modules.pullback (S.map f)).obj E)) :
    ∃ ch : ∀ X : C, VectorBundleKZero (S.obj X) →+* PowerSeries (𝔄.A X),
      (∀ (X : C) (M : (S.obj X).Modules),
          Stacks.FiniteLocallyFree.IsFiniteLocallyFree.{u, u, u} M →
          ch X (VectorBundleKZero.classOf (S.obj X) M) = chM X M) ∧
        (∀ (X : C) (α : VectorBundleKZero (S.obj X)), ch X α ∈ gradedPowerSeries 𝔄 X) ∧
          (∀ {X Y : C} (f : X ⟶ Y) (α : VectorBundleKZero (S.obj Y)),
            PowerSeries.map (𝔄.pull f) (ch Y α) = ch X (κ f α)) ∧
            ∀ (X : C) (L : (S.obj X).Modules)
              (hL : AlgebraicGeometry.SheafOfModules.IsInvertible (S.obj X).presheaf
                (S.obj X).ringCatSheaf.2 L),
              ch X (VectorBundleKZero.classOf (S.obj X) L) =
                expFirstChernClass 𝔄 X (picardClassOf (S.obj X) L hL)

Stacks.WeilCohomology.eq_of_cohomologicalChernCharacter', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/CohomologicalChernCharacterConstructed.lean, line 180. The attribute's comment: “uniqueness: two rules assigning to every object a ring homomorphism out of K₀(Vect(X)), compatible with pullbacks and taking the value exp(c₁^H(ℒ)) on an invertible module, agree on every class and at every object. Every input is discharged here: compatibility with pullbacks is read against the CONSTRUCTED pullback homomorphism AlgebraicGeometry.VectorBundleKZero.pullbackRingHom of K₀(Vect(-))”.

The uniqueness half of Stacks Tag 0FIE. Two rules assigning to every object X of 𝒞 a ring homomorphism K₀(Vect(X)) ⟶ ∏_{i ≥ 0} H^{2i}(X)(i), compatible with pullbacks and taking the value exp(c_1^H(ℒ)) on every invertible module, are equal: they agree on every class of K₀(Vect(X)), for every object X of 𝒞.

Both rules are additive, so it is enough that they agree on the classes [ℰ] of finite locally free modules, which generate K₀(Vect(X)). For ℰ of constant rank that is eq_classOf_of_isFiniteLocallyFreeOfRank, read off the splitting principle. An arbitrary ℰ is reduced to that case by Stacks.WeilCohomology.SourceChernSetup.exists_clopenRankPieces: restriction to the finitely many loci where the rank of ℰ is constant is injective on A(X) by condition (2) of the situation, and both rules commute with those restrictions.

theorem eq_of_cohomologicalChernCharacter'
    {ch ch' : ∀ X : C, VectorBundleKZero (S.obj X) →+* PowerSeries (𝔄.A X)}
    (hpull : ∀ {X Y : C} (f : X ⟶ Y) (α : VectorBundleKZero (S.obj Y)),
      PowerSeries.map (𝔄.pull f) (ch Y α) = ch X (VectorBundleKZero.pullbackRingHom (S.map f) α))
    (hpull' : ∀ {X Y : C} (f : X ⟶ Y) (α : VectorBundleKZero (S.obj Y)),
      PowerSeries.map (𝔄.pull f) (ch' Y α) = ch' X (VectorBundleKZero.pullbackRingHom (S.map f) α))
    (hinv : ∀ (X : C) (L : (S.obj X).Modules)
      (hL : AlgebraicGeometry.SheafOfModules.IsInvertible (S.obj X).presheaf
        (S.obj X).ringCatSheaf.2 L),
      ch X (VectorBundleKZero.classOf (S.obj X) L) =
        expFirstChernClass 𝔄.toChernSetup X (picardClassOf (S.obj X) L hL))
    (hinv' : ∀ (X : C) (L : (S.obj X).Modules)
      (hL : AlgebraicGeometry.SheafOfModules.IsInvertible (S.obj X).presheaf
        (S.obj X).ringCatSheaf.2 L),
      ch' X (VectorBundleKZero.classOf (S.obj X) L) =
        expFirstChernClass 𝔄.toChernSetup X (picardClassOf (S.obj X) L hL))
    (X : C) (α : VectorBundleKZero (S.obj X)) :
    ch X α = ch' X α

Stacks.WeilCohomology.exists_cohomologicalChernCharacter_of_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/CohomologicalChernCharacterConstructed.lean, line 527. The attribute's comment: “existence: the rule, as a ring homomorphism out of K₀(Vect(X)) into ∏_{i ≥ 0} H^{2i}(X)(i), together with its grading, its compatibility with the CONSTRUCTED pullback homomorphism AlgebraicGeometry.VectorBundleKZero.pullbackRingHom of K₀(Vect(-)) and its value exp(c₁^H(ℒ)) on an invertible module, stated over the data and the conditions of Sections 45.12 and 45.14 themselves and over NO structure argument. The standing situation is the structure Stacks.WeilCohomology.ChernSetup -- the data the source fixes, with clause (1), clause (2), clause (3)(a), condition (1), condition (2), condition (4) and the source's grading A(X) = sum of the A^i(X) as isInternal_grade -- together with the section's three remaining conditions: condition (3) at f^L itself, in the source's own form (PullbackFirstChernCondition); clause (3)(b) as the closure property IsBundleCompare at f^E itself, in the source's own form (BundleCompareClause); clause (3)(c) as the closure property IsBundleEmbedding with condition (5) read at c_1^A(O_P(P')) for the divisor module characterized divisor-theoretically by IsSubbundleDivisorModule (DivisorDatumClause); and the Q-structure of A as data (D0) and (D1) of Section 45.14 read for A, that is Stacks.WeilCohomology.ChernSetup.IsRationallyGraded. The structure Stacks.WeilCohomology.ChernSituation is built inside the proof by Stacks.WeilCohomology.chernSituationOfSource and is not an argument, and no RationalChernSituation occurs. PROVED and not assumed: the cohomological Chern character of a single finite locally free module, which the source's proof cites from Tag 0FI9's existence half and which Stacks.WeilCohomology.exists_cohomologicalChernCharacter leaves open as chM with seven properties, discharged here by Stacks.WeilCohomology.chernCharacterOfModule and its seven lemmas; the total Chern classes of Tag 0FI5 those rest on, at the constructed situation (ChernSituation.isTotalChernClass_totalChernClass); the rank class r^A, which is Stacks.WeilCohomology.SourceChernSetup.rankClass, built from condition (2); the pullback homomorphism of K_0(Vect(-)), which is AlgebraicGeometry.VectorBundleKZero.pullbackRingHom; the Whitney formula this half needs, proved from clause (3)(c) with condition (5); and the one-degree form of the Q-structure, the rationals lying in A^0(X), DERIVED from (D0) and (D1) by Stacks.WeilCohomology.ChernSetup.algebraMap_mem_grade_zero_of_isRationallyGraded. Nothing outside the data and the conditions of Sections 45.12 and 45.14 is assumed, and NO hypothesis is read more strongly than the source states it: the invariance of the total Chern class under an isomorphism of modules, which K_0(Vect(X)) forces on any rule out of it and which a comparison of P(E) with P(E') would get only by asking clause (3)(b) at every module isomorphic to f^E, is PROVED (chernSeries_eq_of_iso), as is the pseudofunctoriality coherence isomorphism h^(g^E) = (h . g)^E (pull_chernSeries_coeff_of_iso)”.

Stacks Project, Tag 0FIE, existence half. In the standing situation of Section 45.12, read with the 𝐐-structure data (D0) and (D1) of Section 45.14 give, there is a rule assigning to every object X of 𝒞 a ring homomorphism

ch^H : K₀(Vect(X)) ⟶ ∏_{i ≥ 0} H^{2i}(X)(i)

which is graded, is compatible with pullbacks, and takes the value exp(c_1^H(ℒ)) on every invertible module. With Stacks.WeilCohomology.eq_of_cohomologicalChernCharacter' for uniqueness this is the tag.

What the situation is. Stacks.WeilCohomology.ChernSetup is the source's own standing situation — the data the source fixes, with clause (1), clause (2), clause (3)(a), condition (1), condition (2), condition (4) and the grading A(X) = ⨁_{i ≥ 0} A^i(X); in particular Stacks.WeilCohomology.ChernSetup.bundleDatum is a definition and not a field. The section's three remaining conditions, each in the source's own form, are the arguments hpull, hcompare and hdivisor (Stacks.WeilCohomology.PullbackFirstChernCondition, Stacks.WeilCohomology.BundleCompareClause, Stacks.WeilCohomology.DivisorDatumClause), and the 𝐐-structure is the ℚ-algebra structure on the A X together with Stacks.WeilCohomology.ChernSetup.IsRationallyGraded, which is data (D0) and (D1) of Section 45.14 read for A. The Stacks.WeilCohomology.ChernSituation the development is written over is assembled from those three by Stacks.WeilCohomology.chernSituationOfSource inside the proof, so it is not an argument of this statement, and no Stacks.WeilCohomology.RationalChernSituation occurs: condition (5), together with clause (3)(c), is the argument hdivisor rather than a field, and the one-degree form of the 𝐐-structure is derived by Stacks.WeilCohomology.ChernSetup.algebraMap_mem_grade_zero_of_isRationallyGraded.

All three conditions are in the source's own form. In particular Stacks.WeilCohomology.BundleCompareClause is clause (3)(b) at f^*ℰ itself, and not at every ℰ' carrying an isomorphism f^*ℰ ≅ ℰ' — that reading would be a closure property clauses (1), (2) and (3) do not give, since at f = 𝟙 X it is the closure of 𝒞 under the 𝐏(ℰ') ⟶ 𝐏(ℰ) induced by an arbitrary ℰ ≅ ℰ'. The invariance of the total Chern class under an isomorphism of modules, which K₀(Vect(X)) forces on any rule out of it, and the pseudofunctoriality coherence isomorphism h^*(g^*ℰ) ≅ (h ∘ g)^*ℰ, which the source has for free, are both theorems: Stacks.WeilCohomology.ChernSituation.chernSeries_eq_of_iso and Stacks.WeilCohomology.ChernSituation.pull_chernSeries_coeff_of_iso.

Nothing is assumed beyond that data and those conditions. The cohomological Chern character of a single finite locally free module, which the source's proof of this tag cites from the existence half of Tag 0FI9 and which Stacks.WeilCohomology.exists_cohomologicalChernCharacter leaves open as chM with seven properties, is Stacks.WeilCohomology.chernCharacterOfModule with its seven lemmas; the total Chern classes of Tag 0FI5 those rest on are Stacks.WeilCohomology.ChernSituation.isTotalChernClass_totalChernClass at the constructed situation; the rank class r^A is Stacks.WeilCohomology.SourceChernSetup.rankClass, built from condition (2); and the pullback homomorphism of K₀(Vect(-)) is AlgebraicGeometry.VectorBundleKZero.pullbackRingHom.

theorem exists_cohomologicalChernCharacter_of_source (𝔄 : SourceChernSetup.{u, v, v₁, w} C S)
    [∀ X : C, Algebra ℚ (𝔄.A X)] (hgr : 𝔄.IsRationallyGraded)
    (hpull : PullbackFirstChernCondition 𝔄) (hcompare : BundleCompareClause 𝔄)
    (hdivisor : DivisorDatumClause 𝔄) :
    ∃ ch : ∀ X : C, VectorBundleKZero (S.obj X) →+* PowerSeries (𝔄.A X),
      (∀ (X : C) (M : (S.obj X).Modules),
          Stacks.FiniteLocallyFree.IsFiniteLocallyFree.{u, u, u} M →
          ch X (VectorBundleKZero.classOf (S.obj X) M) =
            chernCharacterOfModule (𝔄 := 𝔄) (chernSituationOfSource 𝔄 hpull hcompare
              hdivisor).isTotalChernClass_totalChernClass X M) ∧
        (∀ (X : C) (α : VectorBundleKZero (S.obj X)), ch X α ∈ gradedPowerSeries 𝔄.toChernSetup X) ∧
          (∀ {X Y : C} (f : X ⟶ Y) (α : VectorBundleKZero (S.obj Y)),
            PowerSeries.map (𝔄.pull f) (ch Y α) =
              ch X (VectorBundleKZero.pullbackRingHom (S.map f) α)) ∧
            ∀ (X : C) (L : (S.obj X).Modules)
              (hL : AlgebraicGeometry.SheafOfModules.IsInvertible (S.obj X).presheaf
                (S.obj X).ringCatSheaf.2 L),
              ch X (VectorBundleKZero.classOf (S.obj X) L) =
                expFirstChernClass 𝔄.toChernSetup X (picardClassOf (S.obj X) L hL)

Stacks.WeilCohomology.FirstChernClassData.existsUnique_cohomologicalChernCharacter, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/WeilChernCharacter.lean, line 334. The attribute's comment: “under exactly (D0), (D1), (D2') and (A1)-(A4), for all smooth projective schemes over k (not necessarily irreducible or nonempty), with the tensor-defined Tate twists: existence and uniqueness of the rule K_0(Vect(X)) -> prod_{i >= 0} H^{2i}(X)(i), a ring homomorphism for the cup product of the product. (D1) is Z-graded as in the chapter's conventions; the proof uses condition (4) of Section 45.12 only through injectivity and the resolution of the top power, which is what (A3) gives on A when H^* has negative-degree classes”.

Stacks Project, Tag 0FIE. Assume given data (D0), (D1), (D2') satisfying axioms (A1), (A2), (A3) and (A4). There is a unique rule which assigns to every smooth projective X over k a ring homomorphism

ch^H : K₀(Vect(X)) ⟶ ∏_{i ≥ 0} H^{2i}(X)(i)

compatible with pullbacks such that ch^H(ℒ) = exp(c₁^H(ℒ)) for every invertible 𝒪_X-module ℒ.

The twists are the tensor-defined ones, Stacks.WeilCohomology.tateTwist. A family (a_i)_{i ≥ 0} with a_i ∈ H^*(X)(i) lies in ∏_{i ≥ 0} H^{2i}(X)(i) when each a_i lies in the image of H^{2i}(X)(i). The ring structure of the product is the cup product Stacks.WeilCohomology.FirstChernClassData.cupConv, (a ∪ b)_n = ∑_{i + j = n} a_i ∪ b_j, with unit Stacks.WeilCohomology.FirstChernClassData.oneConv; a ring homomorphism is an additive, multiplicative and unital map. Compatibility with pullbacks is f^* ∘ ch^H = ch^H ∘ f^*, the pullback of K₀(Vect(-)) being AlgebraicGeometry.VectorBundleKZero.pullbackRingHom, and exp(c₁^H(ℒ)) = ∑_n (1/n!) c₁^H(ℒ)^n is Stacks.WeilCohomology.FirstChernClassData.expTw.

The proof is the source's: Proposition 45.12.4 (Tag 0FI9) for the category of smooth projective schemes over k, the functor A : X ↦ ⨁_{i ≥ 0} H^{2i}(X)(i) and c₁^H, whose standing assumptions are (A1)–(A4). The projective bundle formula is used in the weak form that (A3) provides when H^* is nonzero in negative degrees; see the module documentation.

theorem existsUnique_cohomologicalChernCharacter [CharZero F] (hA1 : 𝔇.CoproductAxiom)
    (hA2 : 𝔇.PullbackAxiom) (hA3 : 𝔇.ProjectiveBundleAxiom) (hA4 : 𝔇.DivisorAxiom) :
    ∃! ch : ∀ X : (SmoothProjectiveScheme k).FullSubcategory,
        VectorBundleKZero ((toScheme k).obj X) → ∀ n : ℕ, tateTwist F 𝔇.tate (𝔇.H X) n,
      (∀ X α (n : ℕ), ch X α n ∈
          LinearMap.range (tateTwistMap (L := 𝔇.tate) (𝔇.grade X (2 * (n : ℤ))).subtype n)) ∧
        (∀ X α β, ch X (α + β) = ch X α + ch X β) ∧
        (∀ X α β, ch X (α * β) = 𝔇.cupConv X (ch X α) (ch X β)) ∧
        (∀ X, ch X 1 = 𝔇.oneConv X) ∧
        (∀ {X Y : (SmoothProjectiveScheme k).FullSubcategory} (f : X ⟶ Y) α (n : ℕ),
          ch X (VectorBundleKZero.pullbackRingHom ((toScheme k).map f) α) n =
            𝔇.pullTw f n (ch Y α n)) ∧
          ∀ X (L : ((toScheme k).obj X).Modules)
            (hL : AlgebraicGeometry.SheafOfModules.IsInvertible ((toScheme k).obj X).presheaf
              ((toScheme k).obj X).ringCatSheaf.2 L),
            ch X (VectorBundleKZero.classOf _ L) = 𝔇.expTw X (𝔇.c₁ X (picardClassOf _ L hL))

Tag 0FIF, a lemma

Tag 0FIF in the Stacks Project.

Stacks.WeilCohomology.FirstChernClassData.existsUnique_codimensionCycleClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/ChernClassCycleClassIntegral.lean, line 302. The attribute's comment: “the integral form: existence and uniqueness, under exactly (D0), (D1), (D2') and (A1)-(A4), of γ on the integral Chow groups CH^i(X) = prod_d CH_{d-i}(X_d) of every smooth projective X over k, with values in H^{2i}(X)(i), additive, multiplicative for the intersection product of 0FC0 and the cup product, γ([X]) = 1, compatible with the codimension-graded Gysin pullbacks f^! of 0FF3, and with γ(ch(α)) = ch^H(α) read through CH -> CH ⊗ Q (the Q-linear extension of γ sends ch(α) ∩ [X] to ch^H(α), ch^H as in 0FIE). Derived from the rational form existsUnique_cycleClassMap; nothing is assumed”.

Stacks Project, Tag 0FIF, on the integral Chow ring. Assume given (D0), (D1), (D2') satisfying axioms (A1), (A2), (A3) and (A4). There is a unique rule which assigns to every smooth projective X over k a graded ring homomorphism

γ : CH^*(X) ⟶ ⨁_{i ≥ 0} H^{2i}(X)(i)

compatible with pullbacks such that γ(ch(α)) = ch^H(α) for α ∈ K₀(Vect(X)).

CH^*(X) = ⨁_i CH^i(X) is the integral Chow ring, CH^i(X) = ∏_d CH_{d-i}(X_d) with the intersection product of Chow Homology, Section 0FC0, and unit the fundamental class [X]; pullback is the Gysin map f^! of Chow Homology, Tag 0FF3, graded by codimension. A graded ring homomorphism is given by its components γ : CH^i(X) ⟶ H^{2i}(X)(i): additive, multiplicative for the cup product, and sending [X] to 1. The equation γ(ch(α)) = ch^H(α) involves the rational class ch(α) ∩ [X] ∈ CH^*(X) ⊗ 𝐐 and is read through CH^*(X) ⟶ CH^*(X) ⊗ 𝐐: the 𝐐-linear extension γ_𝐐 of γ to CH^*(X) ⊗ 𝐐 (an additive map agreeing with γ on the integral classes) satisfies γ_𝐐(ch(α) ∩ [X]) = ch^H(α), ch^H being the cohomological Chern character of Tag 0FIE.

theorem existsUnique_codimensionCycleClass (hA1 : 𝔇.CoproductAxiom) (hA2 : 𝔇.PullbackAxiom)
    (hA3 : 𝔇.ProjectiveBundleAxiom) (hA4 : 𝔇.DivisorAxiom) :
    ∃! γ : ∀ (X : (SmoothProjectiveScheme k).FullSubcategory) (i : ℕ),
        codimensionChowGroup k X.obj.hom i →+ tateTwist F 𝔇.tate (𝔇.H X) i,
      (∀ (X : (SmoothProjectiveScheme k).FullSubcategory) (i : ℕ)
          (a : codimensionChowGroup k X.obj.hom i),
        γ X i a ∈
          LinearMap.range (tateTwistMap (L := 𝔇.tate) (𝔇.grade X (2 * (i : ℤ))).subtype i)) ∧
      (∀ (X : (SmoothProjectiveScheme k).FullSubcategory) (i j : ℕ)
          (a : codimensionChowGroup k X.obj.hom i)
        (b : codimensionChowGroup k X.obj.hom j),
        γ X (i + j) (codimensionIntersectionProduct k X.obj.hom i j a b) =
          tateCup 𝔇.finrank_tate (𝔇.cup X) i j (i + j) (by push_cast; ring) (γ X i a)
            (γ X j b)) ∧
      (∀ X : (SmoothProjectiveScheme k).FullSubcategory, γ X 0 (fundamentalClass X) = 𝔇.unitTw X) ∧
      (∀ {X Y : (SmoothProjectiveScheme k).FullSubcategory} (f : X ⟶ Y) (i : ℕ)
        (b : codimensionChowGroup k Y.obj.hom i),
        γ X i (codimensionGysin X.obj.hom Y.obj.hom (w f) i b) = 𝔇.pullTw f i (γ Y i b)) ∧
      ∀ ch : ∀ X : (SmoothProjectiveScheme k).FullSubcategory,
          VectorBundleKZero ((toScheme k).obj X) → ∀ n : ℕ, tateTwist F 𝔇.tate (𝔇.H X) n,
        𝔇.IsCohomologicalChernCharacter ch →
        ∃ γℚ : ∀ X : (SmoothProjectiveScheme k).FullSubcategory,
            smoothRationalChowRing (k := k) X.obj.hom → ∀ n : ℕ, tateTwist F 𝔇.tate (𝔇.H X) n,
          (∀ (X : (SmoothProjectiveScheme k).FullSubcategory)
              (α β : smoothRationalChowRing (k := k) X.obj.hom),
            γℚ X (α + β) = γℚ X α + γℚ X β) ∧
          (∀ (X : (SmoothProjectiveScheme k).FullSubcategory) (i : ℕ)
              (a : codimensionChowGroup k X.obj.hom i),
            γℚ X (smoothChowEquiv X.obj.hom (codimensionToRationalChow k X.obj.hom i a)) i =
              γ X i a ∧
            ∀ n : ℕ, n ≠ i →
              γℚ X (smoothChowEquiv X.obj.hom (codimensionToRationalChow k X.obj.hom i a)) n =
                0) ∧
          ∀ (X : (SmoothProjectiveScheme k).FullSubcategory)
              (a : VectorBundleKZero ((toScheme k).obj X)),
            γℚ X (rationalChernCharacterAlgEquiv (isRegular_of_smooth_over_field X.obj.hom)
              (exists_bounds_relativeDimension_fieldChowSituation k X.obj.hom) (1 ⊗ₜ[ℤ] a)) =
              ch X a

Stacks.WeilCohomology.FirstChernClassData.existsUnique_cycleClassMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/ChernClassCycleClassMap.lean, line 339. The attribute's comment: “existence and uniqueness, under exactly (D0), (D1), (D2') and (A1)-(A4) (FirstChernClassData with its four axioms), for all smooth projective X over k: γ on CH^(X) ⊗ Q (the actual rational Chow group of X with the intersection product of Chow Homology, Section 0FEX, and its codimension grading) is graded, additive, multiplicative and unital for the cup product of prod_i H^{2i}(X)(i), compatible with the actual Gysin pullbacks f^!, and γ(ch(α) ∩ [X]) = ch^H(α) for every α in K_0(Vect(X)) and the ch^H of Tag 0FIE. The source prints the last equation as ch^H(α) = γ(ch(α)), which typechecks only after capping with [X], and takes γ on CH^(X); its proof defines γ on CH^*(X) ⊗ Q, where the equation lives, and so does this statement. 0FEY, 0FEM, 0FF8, 0FEN, 0FEX and 0FIA are proved, not assumed”.

Stacks Project, Tag 0FIF. Assume given (D0), (D1), (D2') satisfying axioms (A1), (A2), (A3) and (A4). There is a unique rule which assigns to every smooth projective X over k a graded ring homomorphism

γ : CH^*(X) ⊗ 𝐐 ⟶ ⨁_{i ≥ 0} H^{2i}(X)(i)

compatible with pullbacks such that γ(ch(α) ∩ [X]) = ch^H(α) for α ∈ K₀(Vect(X)), ch^H being the cohomological Chern character of Tag 0FIE.

CH^*(X) ⊗ 𝐐 is CH_*(X) ⊗ 𝐐 with the intersection product of Chow Homology, Section 0FEX, and its codimension grading; pullback is the Gysin map f^! of Chow Homology, Tag 0FF3; ch(α) ∩ [X] is the isomorphism of Chow Homology, Tags 0FEY and 0FEM. A value of γ is a family (γ(α)_n)_{n ≥ 0}, γ(α)_n ∈ H^*(X)(n); graded means that a class of codimension i has γ(α)_i ∈ H^{2i}(X)(i) and all other components zero (so γ(α) ∈ ⨁_{i ≥ 0} H^{2i}(X)(i)), and the ring structure of the target is the cup product cupConv with unit oneConv, as in Tag 0FIE. The rule ch^H is quantified over: Tag 0FIE says exactly one rule has its properties.

theorem existsUnique_cycleClassMap (hA1 : 𝔇.CoproductAxiom) (hA2 : 𝔇.PullbackAxiom)
    (hA3 : 𝔇.ProjectiveBundleAxiom) (hA4 : 𝔇.DivisorAxiom) :
    ∃! γ : ∀ X : (SmoothProjectiveScheme k).FullSubcategory,
        smoothRationalChowRing (k := k) X.obj.hom → ∀ n : ℕ, tateTwist F 𝔇.tate (𝔇.H X) n,
      (∀ (X : (SmoothProjectiveScheme k).FullSubcategory) (i : ℕ)
          (α : smoothRationalChowRing (k := k) X.obj.hom),
        (smoothChowEquiv X.obj.hom).symm α ∈
            codimensionChowSubmodule (fieldChowSituation k) X.obj.hom i →
          γ X α i ∈
              LinearMap.range (tateTwistMap (L := 𝔇.tate) (𝔇.grade X (2 * (i : ℤ))).subtype i) ∧
            ∀ n : ℕ, n ≠ i → γ X α n = 0) ∧
      (∀ (X : (SmoothProjectiveScheme k).FullSubcategory)
          (α β : smoothRationalChowRing (k := k) X.obj.hom),
        γ X (α + β) = γ X α + γ X β) ∧
      (∀ (X : (SmoothProjectiveScheme k).FullSubcategory)
          (α β : smoothRationalChowRing (k := k) X.obj.hom),
        γ X (α * β) = 𝔇.cupConv X (γ X α) (γ X β)) ∧
      (∀ (X : (SmoothProjectiveScheme k).FullSubcategory), γ X 1 = 𝔇.oneConv X) ∧
      (∀ {X Y : (SmoothProjectiveScheme k).FullSubcategory} (f : X ⟶ Y)
          (α : smoothRationalChowRing (k := k) Y.obj.hom) (n : ℕ),
        γ X (smoothGysinRingHom X.obj.hom Y.obj.hom (w f) α) n = 𝔇.pullTw f n (γ Y α n)) ∧
      ∀ ch : ∀ X : (SmoothProjectiveScheme k).FullSubcategory,
          VectorBundleKZero ((toScheme k).obj X) → ∀ n : ℕ, tateTwist F 𝔇.tate (𝔇.H X) n,
        𝔇.IsCohomologicalChernCharacter ch → ∀ (X : (SmoothProjectiveScheme k).FullSubcategory)
          (a : VectorBundleKZero ((toScheme k).obj X)),
          γ X (rationalChernCharacterAlgEquiv (isRegular_of_smooth_over_field X.obj.hom)
            (exists_bounds_relativeDimension_fieldChowSituation k X.obj.hom) (1 ⊗ₜ[ℤ] a)) =
            ch X a

Stacks.WeilCohomology.CycleClassSetup.isCycleClassRule_cycleClassMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/CycleClassMap.lean, line 204. The attribute's comment: “existence: the rule, constructed rather than chosen, together with its three properties — graded, compatible with pullbacks, and γ(ch(α) ∩ [X]) = ch^H(α). The source prints that equation as ch^H(α) = γ(ch(α)), which typechecks only after capping with [X]; the form proved is the one the source's own proof defines, and γ is correspondingly taken on CH^*(X) ⊗ ℚ, where the equation lives. Tag 0FIE (ch^H), Tags 0FEY and 0FEM (the ring isomorphism K₀(Vect(X)) ⊗ ℚ ≅ CH^*(X) ⊗ ℚ), Tag 0FEJ (ψ²) and Tags 0FEX and 0FIA (the two eigenvalue statements) are hypotheses, carried by CycleClassSetup”.

The existence half of Stacks Tag 0FIF. The transported cohomological Chern character is graded, compatible with pullbacks, and satisfies γ(ch(α) ∩ [X]) = ch^H(α).

The grading is the source's Adams operator argument: a class of codimension i answers to a 2^i-eigenvector of ψ², whose cohomological Chern character lies in H^{2i}(X)(i) by Tag 0FIA. Compatibility with pullbacks is that of ch^H and of the Chern character isomorphism, the latter transported through its inverse. The defining equation holds by construction.

theorem isCycleClassRule_cycleClassMap : IsCycleClassRule S S.cycleClassMap

Stacks.WeilCohomology.eq_of_isCycleClassRule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/CycleClassMap.lean, line 224. The attribute's comment: “uniqueness: the defining equation γ(ch(α) ∩ [X]) = ch^H(α) alone determines the rule, the Chern character isomorphism of Tags 0FEY and 0FEM being surjective. As in the existence half the equation is the corrected form of the source's ch^H(α) = γ(ch(α)) and γ is taken on CH^*(X) ⊗ ℚ”.

The uniqueness half of Stacks Tag 0FIF. Two rules with the three properties are equal.

Only the defining equation is used: the Chern character isomorphism of Tags 0FEY and 0FEM is surjective, so a rule is determined by its values on the classes ch(α) ∩ [X].

theorem eq_of_isCycleClassRule {S : CycleClassSetup.{v, v₁, w} C}
    {γ γ' : ∀ X : C, S.CH X →+* S.A X} (h : IsCycleClassRule S γ) (h' : IsCycleClassRule S γ') :
    γ = γ'

Tag 0FIH, a lemma

Tag 0FIH in the Stacks Project.

Stacks.WeilCohomology.SmoothProjectiveScheme.exists_blowup_relations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/BlowupRelationGeneral.lean, line 856.

Lemma 0FIH. Let b : X' ⟶ X be the blowing up of a smooth projective scheme X over k (not necessarily equidimensional) in a smooth closed subscheme i : Z ⟶ X, with exceptional divisor j : E ⟶ X' and π : E ⟶ Z. Assume that some element of K_0(Vect(X)) restricts on Z to the class of 𝒞_{Z/X}, and that every irreducible component of Z has codimension r ≥ 1 in X (its generic point has coheight r in X). Then there is a cycle θ ∈ CH^{r-1}(X') such that

b^![Z] = [E] · θ in CH^r(X'), with b^! the Gysin map of Stacks 0FF3 and · the intersection product of Stacks 0FC0, both graded by codimension; and

π_*(j^!θ) = [Z]: for every e, on the part X'_{e+1} of X' of dimension e + 1 the Gysin map of the regular immersion j (Stacks.Chow.regularImmersionPartGysin) carries θ to a class of CH_{e-(r-1)}(E ×_{X'} X'_{e+1}) whose pushforward to Z is the fundamental class [Z]_{e-(r-1)}, the sum of the components of Z of dimension e - (r - 1).

Since CH_*(E) is the direct sum of the CH_*(E ×_{X'} X'_d), the piece over X'_0 is empty, and [Z] = ∑_m [Z]_m, the second family of equalities is π_*(j^!θ) = [Z] in CH_*(Z) = ⊕_m CH_m(Z). The source writes [Z] ∈ CH^r(Z); as π_*j^!θ has codimension 0 in Z, this is the fundamental class [Z] ∈ CH^0(Z). The hypothesis r ≥ 1 is implicit in the source (θ ∈ CH^{r-1}(X')): for r = 0 and Z nonempty, Z is a union of components of X, E is empty and π_*(j^!θ) = 0 ≠ [Z].

The cycle is θ = c_{r-1}(b^*α^∨ - [𝒪_{X'}(E)]) ∩ [X'] (Stacks.WeilCohomology.SmoothProjectiveScheme.blowupTheta), as in the source.

theorem exists_blowup_relations {r : ℕ} (hr0 : 0 < r)
    (hr : ∀ z : Z.obj.left, closure ({z} : Set Z.obj.left) ∈ irreducibleComponents Z.obj.left →
      Order.coheight (i.hom.left z) = r)
    (hK : ∃ α : VectorBundleKZero X.obj.left,
      VectorBundleKZero.pullback i.hom.left α = classOf _ (centreConormal i)) :
    ∃ θ : codimensionChowGroup k (blowupObj i).obj.hom ((r - 1 : ℕ) : ℤ),
      codimensionGysin (blowupObj i).obj.hom X.obj.hom (Over.w (blowupHom i).hom) (r : ℤ)
          (closedSubschemeClass X.obj.hom i.hom.left (r : ℤ)) ≍
        codimensionIntersectionProduct k (blowupObj i).obj.hom 1 ((r - 1 : ℕ) : ℤ)
          (closedSubschemeClass (blowupObj i).obj.hom (exceptionalHom i).hom.left 1) θ ∧
      ∀ e : ℕ, properChowPushforward (fieldChowSituation k)
          (pullback.fst (exceptionalHom i).hom.left (dimPart (blowupObj i).obj.hom (e + 1)).ι ≫
            (exceptionalHom i).hom.left ≫ (blowupObj i).obj.hom)
          Z.obj.hom
          (pullback.fst (exceptionalHom i).hom.left (dimPart (blowupObj i).obj.hom (e + 1)).ι ≫
            (exceptionalProj i).hom.left)
          (by rw [Category.assoc, Over.w (exceptionalProj i).hom, Over.w (exceptionalHom i).hom])
          ((e : ℤ) - ((r - 1 : ℕ) : ℤ))
          (properPushforwardFactorsThroughRationalEquivalence_of_isProper _ _ _ _ _ _)
          (regularImmersionPartGysin (blowupObj i).obj.hom (exceptionalHom i).hom.left
            (isRegularImmersion_of_isClosedImmersion (exceptionalHom i)) e (e + 1)
            ((r - 1 : ℕ) : ℤ) (θ (e + 1))) =
        fundamentalChowClass (fieldChowSituation k) Z.obj.hom ((e : ℤ) - ((r - 1 : ℕ) : ℤ))

Tag 0FII, a lemma

Tag 0FII in the Stacks Project.

Stacks.WeilCohomology.FirstChernClassData.IsCohomologicalChernCharacter.cup_codimensionCycleClass_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/CycleClassCupVanishingGeneral.lean, line 370. The attribute's comment: “for any smooth projective X and smooth closed Z all of whose irreducible components have codimension r, with [C_{Z/X}] restricted from K_0(X): a|_Z = 0 implies γ([Z]) ∪ a = 0, γ the cycle class map of 0FIF; the case r = 0 by (A1)”.

Stacks Project, Lemma 0FII. Let (D0), (D1), (D2') satisfy (A1)–(A4) and (A7), with γ the cycle class map of Tag 0FIF. Let X be a smooth projective scheme over k and i : Z ⟶ X a smooth closed subscheme every irreducible component of which has codimension r in X, such that the class of 𝒞_{Z/X} in K_0(Z) is the restriction of an element of K_0(X). If a ∈ H^*(X) restricts to 0 on Z, then γ([Z]) ∪ a = 0, written a ∪ γ([Z]) with γ([Z]) twisted.

"Every irreducible component of Z has codimension r" is read at the generic points of the components: the codimension in X of the closure of the image of such a point is its coheight. For r ≥ 1 the proof is the source's, on each part of X of constant dimension (mul_κ_codimensionCycleClass_eq_zero_of_pos). For r = 0 the source's argument does not apply, Z not being nowhere dense; there Z is open and closed (isOpenImmersion_of_coheight_eq_zero) and (A1) gives the vanishing directly (cup_codimensionCycleClass_eq_zero_of_isOpenImmersion).

theorem cup_codimensionCycleClass_eq_zero (hA1 : 𝔇.CoproductAxiom)
    (hA3 : 𝔇.ProjectiveBundleAxiom) (hA4 : 𝔇.DivisorAxiom) (hA7 : 𝔇.BlowupAxiom)
    {Z X : (SmoothProjectiveScheme k).FullSubcategory} (i : Z ⟶ X) [IsClosedImmersion i.hom.left]
    (r : ℕ)
    (hr : ∀ z : Z.obj.left, closure ({z} : Set Z.obj.left) ∈ irreducibleComponents Z.obj.left →
      Order.coheight (i.hom.left z) = r)
    (hK : ∃ α : VectorBundleKZero X.obj.left,
      VectorBundleKZero.pullback i.hom.left α = VectorBundleKZero.classOf _ (centreConormal i))
    (a : 𝔇.H X) (ha : 𝔇.pull i a = 0) :
    tateCupLeft (𝔇.cup X) (r : ℤ) a
      (h.codimensionCycleClass X r (closedSubschemeClass X.obj.hom i.hom.left r)) = 0

Stacks.WeilCohomology.FirstChernClassData.IsCohomologicalChernCharacter.codimensionCycleClass_cup_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/CycleClassCupVanishingGeneral.lean, line 394. The attribute's comment: “in the source's order γ([Z]) ∪ a = 0, for any smooth projective X and smooth closed Z all of whose irreducible components have codimension r, with [C_{Z/X}] restricted from K_0(X), and a|_Z = 0; γ the cycle class map of 0FIF”.

Stacks Project, Lemma 0FII, in the source's order: γ([Z]) ∪ a = 0. Here γ([Z]) ∪ a is the cup product with the twisted class on the left, tateCupLeft of the flipped cup product. It follows from cup_codimensionCycleClass_eq_zero by graded commutativity of H^*(X), γ([Z]) having even degree 2r.

theorem codimensionCycleClass_cup_eq_zero (hA1 : 𝔇.CoproductAxiom)
    (hA3 : 𝔇.ProjectiveBundleAxiom) (hA4 : 𝔇.DivisorAxiom) (hA7 : 𝔇.BlowupAxiom)
    {Z X : (SmoothProjectiveScheme k).FullSubcategory} (i : Z ⟶ X) [IsClosedImmersion i.hom.left]
    (r : ℕ)
    (hr : ∀ z : Z.obj.left, closure ({z} : Set Z.obj.left) ∈ irreducibleComponents Z.obj.left →
      Order.coheight (i.hom.left z) = r)
    (hK : ∃ α : VectorBundleKZero X.obj.left,
      VectorBundleKZero.pullback i.hom.left α = VectorBundleKZero.classOf _ (centreConormal i))
    (a : 𝔇.H X) (ha : 𝔇.pull i a = 0) :
    tateCupLeft (𝔇.cup X).flip (r : ℤ) a
      (h.codimensionCycleClass X r (closedSubschemeClass X.obj.hom i.hom.left r)) = 0

Tag 0FIJ, a lemma

Tag 0FIJ in the Stacks Project.

Stacks.WeilCohomology.FirstChernClassData.IsCohomologicalChernCharacter.poincareDuality_toWeilData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/PoincareDualityWeilThree.lean, line 127. The attribute's comment: “axiom (A) for the data of (A1)-(A7), with trace map λ of (A6) and γ the cycle class map of 0FIF”.

Stacks Project, Lemma 0FIJ. Let (D0), (D1), (D2') satisfy axioms (A1)–(A7). Then axiom (A) of Section 0FHA holds with ∫_X = λ as in axiom (A6): for X nonempty and equidimensional of dimension d, H^i(X) is finite dimensional and H^i(X) × H^{2d-i}(X)(d) ⟶ F, (a, b) ↦ λ(a ∪ b), is a perfect pairing.

theorem poincareDuality_toWeilData : (h.toWeilData hA1 hA3 hA5 hA6).PoincareDuality

Tag 0FIK, a remark

Tag 0FIK in the Stacks Project.

Stacks.WeilCohomology.FirstChernClassData.IsCohomologicalChernCharacter.trace_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/TraceUniqueness.lean, line 196. The attribute's comment: “uniqueness of the trace map λ of (A6): two linear maps H^{2d}(X)(d) → F normalized by (1 ⊗ λ)γ([Δ]) = 1 are equal, for X nonempty equidimensional of dimension d and γ the cycle class map of 0FIF”.

Stacks Project, Remark 0FIK: uniqueness of the trace map. Let (D0), (D1), (D2') satisfy (A1)–(A7), with γ the cycle class map of Tag 0FIF, and let X be a nonempty smooth projective scheme over k, equidimensional of dimension d. Then a linear map λ : H^{2d}(X)(d) ⟶ F with (1 ⊗ λ)γ([Δ]) = 1 as in axiom (A6) is unique.

The axioms used are (A1), (A3), (A4), (A5) and (A7), through the identity γ([Δ]) ∪ p₁^*a = γ([Δ]) ∪ p₂^*a (key_diagonalClass); (A2) enters through γ itself.

theorem trace_unique (hA1 : 𝔇.CoproductAxiom) (hA3 : 𝔇.ProjectiveBundleAxiom)
    (hA4 : 𝔇.DivisorAxiom) (hA5 : 𝔇.KunnethAxiom) (hA7 : 𝔇.BlowupAxiom)
    (X : (SmoothProjectiveScheme k).FullSubcategory) (d : ℕ) (hX : IsNonemptyEquidimensional X d)
    (lam lam' : tateTwist F 𝔇.tate (𝔇.grade X (2 * (d : ℤ))) d →ₗ[F] F)
    (hlam : 𝔇.traceContract hA5 X d lam
      (h.codimensionCycleClass (prod X X) d (diagonalClass X d)) = 1)
    (hlam' : 𝔇.traceContract hA5 X d lam'
      (h.codimensionCycleClass (prod X X) d (diagonalClass X d)) = 1) :
    lam = lam'

Stacks.WeilCohomology.FirstChernClassData.IsCohomologicalChernCharacter.bijective_diagonalContract, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/TraceUniqueness.lean, line 217. The attribute's comment: “γ([Δ]) ∈ ⊕_i H^i(X) ⊗ H^{2d-i}(X)(d) defines a perfect duality between H^i(X) and H^{2d-i}(X)(d): contraction against its (i, 2d-i) Künneth component is a bijection (H^{2d-i}(X)(d))^* → H^i(X), for X nonempty equidimensional of dimension d”.

Stacks Project, Remark 0FIK: γ([Δ]) defines a perfect duality between H^i(X) and H^{2d-i}(X)(d). Let (D0), (D1), (D2') satisfy (A1)–(A7), with γ the cycle class map of Tag 0FIF, and let X be a nonempty smooth projective scheme over k, equidimensional of dimension d. For i + j = 2d, contraction against the (i, j) Künneth component of γ([Δ]), μ ↦ (1 ⊗ μ)γ([Δ])_{i,j}, is a bijection (H^j(X)(d))^* ⟶ H^i(X).

theorem bijective_diagonalContract (hA1 : 𝔇.CoproductAxiom) (hA3 : 𝔇.ProjectiveBundleAxiom)
    (hA4 : 𝔇.DivisorAxiom) (hA5 : 𝔇.KunnethAxiom)
    (hA6 : 𝔇.TraceAxiomFor hA5 h.codimensionCycleClass) (hA7 : 𝔇.BlowupAxiom)
        (X : (SmoothProjectiveScheme k).FullSubcategory) (d : ℕ)
    (hX : IsNonemptyEquidimensional X d) {i j : ℤ} (hij : i + j = 2 * (d : ℤ)) :
    Function.Bijective (𝔇.diagonalContract hA5 X d
      (h.codimensionCycleClass (prod X X) d (diagonalClass X d)) i j)

Stacks.WeilCohomology.diagonalDuality, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/TraceMap.lean, line 156. The attribute's comment: “the perfect duality that γ([Δ]) defines between H^i(X) and H^{2d-i}(X)(d); the left-dual structure of H^*(X) produced by Lemma 45.14.5, Tag 0FIJ, is carried as the hypothesis ExactPairing V W, as the remark itself directs”.

Stacks Project, Tag 0FIK. The class γ([Δ]) defines a perfect duality between H^i(X) and H^{2d - i}(X)(d): contracting its degree-i Künneth component against a linear functional on H^{2d - i}(X)(d) is a linear isomorphism onto H^i(X).

Here V i is H^i(X), W (-i) is H^{2d - i}(X)(d), and the left-dual structure is the one Lemma 45.14.5, Tag 0FIJ, produces, whose coevaluation is multiplication by γ([Δ]). The inverse is the pairing of Tag 0FFV, recorded in diagonalDuality_symm_apply.

noncomputable def diagonalDuality (i : ℤ) : (W (-i) →ₗ[F] F) ≃ₗ[F] V i

Stacks.WeilCohomology.traceMap_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/TraceMap.lean, line 185. The attribute's comment: “uniqueness of the trace map ∫_X = λ of axiom (A6), the remark's conclusion; the normalisation (id ⊗ λ) γ([Δ]) = 1 is axiom (A6) and the left-dual structure is Lemma 45.14.5, Tag 0FIJ”.

Stacks Project, Tag 0FIK. The trace map is unique: an F-linear map λ : H^{2d}(X)(d) → F satisfying the normalisation (id ⊗ λ) γ([Δ]) = 1 of axiom (A6) is determined by that equation, because contraction of γ([Δ]) against a functional is injective in degree 0. This is what licenses the notation ∫_X for it.

theorem traceMap_unique (one : V 0) {lam lam' : W 0 →ₗ[F] F}
    (hlam : diagonalDuality V W 0 lam = one) (hlam' : diagonalDuality V W 0 lam' = one) :
    lam = lam'

Tag 0FIL, a lemma

Tag 0FIL in the Stacks Project.

Stacks.WeilCohomology.WeilChernData.kunneth_toWeilData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/KunnethWeilThree.lean, line 422. The attribute's comment: “axiom (B) of 0FHA for the data of (A1)-(A7): the Künneth map is an isomorphism and ∫_{X×Y} = ∫_X ⊗ ∫_Y, with ∫ = λ of (A6) and γ the cycle class map of 0FIF”.

Stacks Project, Lemma 0FIL. Let (D0), (D1), (D2') be data satisfying axioms (A1)–(A7) of Section 45.14. Then axiom (B) of Section 0FHA holds for the data (D0)–(D3) they define (WeilChernData.toWeilData: γ the cycle class map of Tag 0FIF, ∫_X = λ the trace map of (A6)): for smooth projective X, Y over k, (a) H^*(X) ⊗_F H^*(Y) ⟶ H^*(X × Y), α ⊗ β ↦ pr₁^*α ∪ pr₂^*β, is an isomorphism, and (b) if X and Y are nonempty and equidimensional, ∫_{X × Y} = ∫_X ⊗ ∫_Y via (a).

theorem kunneth_toWeilData (𝔚 : WeilChernData k F) : 𝔚.toWeilData.Kunneth

Tag 0FIM, a lemma

Tag 0FIM in the Stacks Project.

Stacks.WeilCohomology.WeilChernData.cycleClassPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/CycleClassPointWeilThree.lean, line 115.

Stacks Project, Lemma 0FIM. Assume given data (D0), (D1) and (D2') satisfying axioms (A1)–(A7). Then axiom (C)(d) of Section 0FHA holds for the data of Section 0FHA they define: ∫_{Spec k} γ([Spec k]) = 1, where γ is the cycle class map of Tag 0FIF and ∫ = λ is the trace map of axiom (A6).

theorem cycleClassPoint : 𝔚.toWeilData.CycleClassPoint

Tag 0FIN, a lemma

Tag 0FIN in the Stacks Project.

Stacks.WeilCohomology.WeilChernData.cycleClass_equidimensionalPushforward_bundleProj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/ProjectiveBundlePushforward.lean, line 309. The attribute's comment: “the whole lemma, under exactly (A1)-(A7) (WeilChernData): for p : P(E) -> X with E of rank r + 1 >= 1 and X nonempty equidimensional, gamma(p_ alpha) = p_ gamma(alpha) for every alpha in CH^i(P), with the pushforward of Section 0FHA for toWeilData; nothing assumed”.

Stacks Project, Lemma 0FIN. Let (D0), (D1), (D2') satisfy axioms (A1)–(A7), let ℰ be a finite locally free module of rank r + 1 ≥ 1 on a nonempty equidimensional smooth projective X over k and p : P = 𝐏(ℰ) ⟶ X its projective bundle, as in axiom (A3). Then γ commutes with pushforward along p: for P and X of dimensions e and d and α ∈ CH^i(P), γ(p_*α) = p_*γ(α) in H^{2j}(X)(j), j = i + d - e, where p_*α is proper pushforward of cycles and p_*γ(α) the pushforward on cohomology of Section 0FHA, for the data WeilChernData.toWeilData (∫_X = λ of (A6), γ of Tag 0FIF). This is clause (C)(b), WeilData.CycleClassPushforward, for the morphism p.

theorem cycleClass_equidimensionalPushforward_bundleProj {d e : ℕ}
    (hX : IsNonemptyEquidimensional X d) (hP : IsNonemptyEquidimensional (bundle X E r) e)
    (i j : ℤ) (hij : j = i + d - e) (α : codimensionChowGroup k (bundle X E r).obj.hom i) :
    𝔚.toWeilData.cycleClass X j (equidimensionalPushforward (bundleProj X E r) e d i j hij α) =
      𝔚.toWeilData.pushforward 𝔚.perfectPairing (bundleProj X E r) hP hX (2 * i) i
        (2 * j) j (by omega) (by omega) (𝔚.toWeilData.cycleClass (bundle X E r) i α)

Tag 0FVR, a lemma

Tag 0FVR in the Stacks Project.

Stacks.WeilCohomology.WeilChernData.untwistTrace_one_spec_galois, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/GaloisTraceDegree.lean, line 374. The attribute's comment: “the source's statement on the actual data (D0), (D1), (D2') satisfying (A1)-(A7) (WeilChernData, with γ of 0FIF): every λ normalised as in (A6) at Spec(k'), i.e. ∫_{Spec(k')} (unique by 0FIK), takes the unit class to [k' : k]; the nonvanishing of H^*(Spec(k')) needed to cancel the unit is derived from (A3), (A4), (A5)”.

Stacks Project, Tag 0FVR. Assume given data (D0), (D1), (D2') satisfying axioms (A1)–(A7), and let k'/k be a finite Galois extension. Then ∫_{Spec(k')} 1 = [k' : k]: every F-linear map λ : H^0(Spec(k'))(0) ⟶ F with (id ⊗ λ) γ([Δ]) = 1 (axiom (A6), γ the cycle class map of Tag 0FIF; such a λ is unique by Remark 0FIK and is ∫_{Spec(k')}) takes the unit class to [k' : k].

theorem untwistTrace_one_spec_galois
    (lam : tateTwist F 𝔚.tate (𝔚.grade (spec k k') (2 * ((0 : ℕ) : ℤ))) (0 : ℕ) →ₗ[F] F)
    (hlam : 𝔚.traceContract 𝔚.kunneth (spec k k') 0 lam
      (𝔚.γ (prod (spec k k') (spec k k')) 0 (diagonalClass (spec k k') 0)) = 1) :
    𝔚.untwistTrace (spec k k') 0 lam 1 = (Module.finrank k k' : F)

Stacks.WeilCohomology.WeilChernData.toWeilData_trace_one_spec_galois, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/GaloisTraceDegree.lean, line 388. The attribute's comment: “the same for the trace map ∫ of 𝔚.toWeilData, the λ of (A6)”.

Stacks 0FVR for the trace map ∫_X of the data of Section 0FHA defined by 𝔚: ∫_{Spec(k')} 1 = [k' : k].

theorem toWeilData_trace_one_spec_galois :
    𝔚.untwistTrace (spec k k') 0 (𝔚.toWeilData.trace (spec k k') 0
      (isNonemptyEquidimensional_of_dimension_zero
        (FirstChernClassData.topologicalKrullDim_spec_field (k := k) (K' := k')))) 1 =
      (Module.finrank k k' : F)

Stacks.WeilCohomology.integration_one_eq_finrank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/GaloisExtension.lean, line 100. The attribute's comment: “the value of the trace map of axiom (A6) on the unit class of the spectrum of a finite Galois extension; the part of the data (D0), (D1), (D2') and of the axioms (A1) -- (A7) the argument consumes is carried as hypotheses, as elsewhere in Section 45.14, and the decomposition of the self-product into Galois translates of the diagonal is the hypothesis decomposition”.

Stacks Project, Tag 0FVR. For a finite Galois extension k'/k the trace map ∫_{Spec(k')} = λ of axiom (A6) takes the unit class to the degree of the extension: ∫_{Spec(k')} 1 = [k' : k].

Here A is H^0(Spec(k')), nonzero because Spec(k') is nonempty, and A ⊗_F A is the cohomology of Spec(k') × Spec(k') in the same degree by axioms (A5) and (A1); CH is the group of cycles on the self-product, carrying the fundamental class fund and the class diag of the diagonal. The hypothesis decomposition is the source's identity of cycles Spec(k') × Spec(k') = ∐_{σ ∈ Gal(k'/k)} (Spec(σ) × id)^{-1} Δ, and normalization is the equation of axiom (A6) that characterises λ. The module documentation reads each hypothesis against the data (D0), (D1), (D2') and the axioms.

theorem integration_one_eq_finrank
    (k k' : Type u) [Field k] [Field k'] [Algebra k k']
    [FiniteDimensional k k'] [IsGalois k k']
    {F : Type uF} [Field F] {A : Type uA} [Ring A] [Algebra F A] [Nontrivial A]
    {CH : Type uC} [AddCommGroup CH]
    (fund diag : CH)
    (cyclePull : (k' ≃ₐ[k] k') → CH →+ CH)
    (gamma : CH →+ A ⊗[F] A)
    (pullback : (k' ≃ₐ[k] k') → A →ₗ[F] A)
    (decomposition : fund = ∑ σ : k' ≃ₐ[k] k', cyclePull σ diag)
    (gamma_fund : gamma fund = (1 : A) ⊗ₜ[F] (1 : A))
    (gamma_cyclePull : ∀ (σ : k' ≃ₐ[k] k') (c : CH),
      gamma (cyclePull σ c) = TensorProduct.map (pullback σ) LinearMap.id (gamma c))
    (pullback_one : ∀ σ : k' ≃ₐ[k] k', pullback σ 1 = 1)
    (lam : A →ₗ[F] F)
    (normalization : tensorContractRight lam (gamma diag) = (1 : A)) :
    lam 1 = (Module.finrank k k' : F)

Tag 0FIP, a lemma

Tag 0FIP in the Stacks Project.

Stacks.WeilCohomology.WeilChernData.cycleClassPushforward_of_closedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/CycleClassPushforwardOfClosedImmersion.lean, line 52. The attribute's comment: “the whole lemma, under exactly (A1)-(A7) (WeilChernData): if i_*(1) = gamma([Z]) for every closed immersion i : Z -> X of nonempty equidimensional smooth projective schemes over k, then gamma commutes with pushforward (axiom (C)(b) for toWeilData); nothing assumed”.

Stacks Project, Lemma 0FIP. Assume given data (D0), (D1), (D2') satisfying axioms (A1)–(A7). In order to show that γ commutes with pushforward (axiom (C)(b) of Section 0FHA for the data 𝔚.toWeilData) it suffices to show that i_*(1) = γ([Z]) in H^{2c}(X)(c), c = d - e, whenever i : Z ⟶ X is a closed immersion of nonempty smooth projective equidimensional schemes over k, of dimensions e and d. Here [Z] ∈ CH^c(X) is the class of the closed subscheme Z and i_* the pushforward on cohomology defined by Poincaré duality.

theorem cycleClassPushforward_of_closedImmersion
    (hi : ∀ {Z X : (SmoothProjectiveScheme k).FullSubcategory} (i : Z ⟶ X)
      [IsClosedImmersion i.hom.left] {e d : ℕ} (hZ : IsNonemptyEquidimensional Z e)
      (hX : IsNonemptyEquidimensional X d) (c : ℤ) (hc : c = d - e),
      𝔚.toWeilData.pushforward 𝔚.perfectPairing i hZ hX 0 0 (2 * c) c (by omega) (by omega)
          (𝔚.toWeilData.unitTw Z 0 0 rfl) =
        𝔚.toWeilData.cycleClass X c (closedSubschemeClass X.obj.hom i.hom.left c)) :
    𝔚.toWeilData.CycleClassPushforward 𝔚.perfectPairing

Tag 0FIQ, a lemma

Tag 0FIQ in the Stacks Project.

Stacks.WeilCohomology.WeilChernData.pushforwardCompatible_fst_grassmannian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/GrassmannianProjectionPushforward.lean, line 130. The attribute's comment: “the whole lemma, under exactly (A1)-(A7) (WeilChernData): for l < n (so in particular 0 < l < n) and X nonempty equidimensional, gamma commutes with pushforward along p : X × G(l, n) -> X, gamma(p_ alpha) = p_ gamma(alpha) for every alpha in CH^i(X × G(l, n)), with the pushforward of Section 0FHA for toWeilData; nothing assumed”.

Let data (D0), (D1), (D2') satisfy axioms (A1)–(A7) of Section 45.14 (WeilChernData), with γ the cycle class map of Tag 0FIF and the pushforward on cohomology of Section 45.9 built from the trace maps λ of (A6) (WeilChernData.toWeilData, Poincaré duality being Lemma 0FIJ). For integers l < n (in particular 0 < l < n) and a smooth projective scheme X over k, γ commutes with pushforward along the projection p : X × G(l, n) ⟶ X: whenever X is nonempty and equidimensional of dimension d and X × G(l, n) of dimension d', γ(p_*α) = p_*γ(α) in H^{2q}(X)(q) for every α ∈ CH^i(X × G(l, n)), q = i + d - d'.

theorem pushforwardCompatible_fst_grassmannian {l n : ℕ} (hln : l < n)
    (X : (SmoothProjectiveScheme k).FullSubcategory) :
    𝔚.toWeilData.PushforwardCompatible 𝔚.perfectPairing
      (fst X (SmoothProjectiveScheme.grassmannian k l n))

Tag 0FIR, a lemma

Tag 0FIR in the Stacks Project.

Stacks.WeilCohomology.WeilChernData.cycleClassPushforward_of_extendableConormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/CycleClassPushforwardOfExtendableConormal.lean, line 65. The attribute's comment: “the whole lemma, under exactly (A1)-(A7) (WeilChernData): if i_*(1) = gamma([Z]) for every closed immersion i : Z -> X of nonempty equidimensional smooth projective schemes over k whose conormal class in K_0(Z) is the pullback of a class in K_0(X), then gamma commutes with pushforward (axiom (C)(b) for toWeilData); nothing assumed”.

Stacks Project, Lemma 0FIR. Assume given data (D0), (D1), (D2') satisfying axioms (A1)–(A7). In order to show that γ commutes with pushforward (axiom (C)(b) of Section 0FHA for the data 𝔚.toWeilData) it suffices to show that i_*(1) = γ([Z]) in H^{2c}(X)(c), c = d - e, whenever i : Z ⟶ X is a closed immersion of nonempty smooth projective equidimensional schemes over k, of dimensions e and d, such that the class of the conormal sheaf 𝒞_{Z/X} in K₀(Z) is the pullback of a class in K₀(X). Here [Z] ∈ CH^c(X) is the class of the closed subscheme Z and i_* the pushforward on cohomology defined by Poincaré duality.

theorem cycleClassPushforward_of_extendableConormal
    (hi : ∀ {Z X : (SmoothProjectiveScheme k).FullSubcategory} (i : Z ⟶ X)
      [IsClosedImmersion i.hom.left]
      {e d : ℕ} (hZ : IsNonemptyEquidimensional Z e) (hX : IsNonemptyEquidimensional X d)
      (c : ℤ) (hc : c = d - e),
      (∃ β : VectorBundleKZero X.obj.left, pullbackRingHom i.hom.left β =
        classOf Z.obj.left (Stacks.Conormal.conormalSheaf i.hom.left)) →
      𝔚.toWeilData.pushforward 𝔚.perfectPairing i hZ hX 0 0 (2 * c) c (by omega) (by omega)
          (𝔚.toWeilData.unitTw Z 0 0 rfl) =
        𝔚.toWeilData.cycleClass X c (closedSubschemeClass X.obj.hom i.hom.left c)) :
    𝔚.toWeilData.CycleClassPushforward 𝔚.perfectPairing

Tag 0FVS, a lemma

Tag 0FVS in the Stacks Project.

Stacks.WeilCohomology.FirstChernClassData.injective_pull_specMap_of_nontrivial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/SeparableExtensionCohomology.lean, line 402. The attribute's comment: “the source's statement, on the actual data (D0), (D1), (D2') over smooth projective k-schemes: with H^(Spec K) ≠ 0 for a finite normal separable K ⊇ k'' (a normal closure), H^(Spec k') ⟶ H^*(Spec k'') is injective, from (A1) and (A5)”.

For finite separable field extensions k''/k'/k and a finite normal separable extension K/k containing k'' (for instance a normal closure of k''/k) with H^*(Spec(K)) ≠ 0, pullback H^*(Spec(k')) ⟶ H^*(Spec(k'')) is injective, under axioms (A1) and (A5) (the source assumes (A1)–(A7)); in particular it is injective on H^0.

theorem injective_pull_specMap_of_nontrivial (hA1 : 𝔇.CoproductAxiom) (hA5 : 𝔇.KunnethAxiom)
    {k' : Type u} [Field k'] [Algebra k k'] [FiniteDimensional k k'] [Algebra.IsSeparable k k']
    {k'' : Type u} [Field k''] [Algebra k k''] [FiniteDimensional k k''] [Algebra.IsSeparable k k'']
    (incl : k' →ₐ[k] k'') {E : Type u} [Field E] [Algebra k E] [FiniteDimensional k E]
    [Algebra.IsSeparable k E] [Normal k E] (ι : k'' →ₐ[k] E) (hE : Nontrivial (𝔇.H (spec k E))) :
    Function.Injective (𝔇.pull (specMap incl))

Stacks.WeilCohomology.FirstChernClassData.injective_pull_specMap_of_axioms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/SeparableExtensionCohomology.lean, line 463. The attribute's comment: “unconditional form: the nonvanishing hypothesis is derived from (A3), (A4), (A5)”.

For finite separable field extensions k''/k'/k, pullback H^*(Spec(k')) ⟶ H^*(Spec(k'')) is injective under axioms (A1), (A3), (A4) and (A5), F having characteristic zero: the hypothesis H^0(Spec(K)) ≠ 0 of the source is a consequence of the axioms (Stacks.WeilCohomology.FirstChernClassData.nontrivial_H_spec). This is the form in which the proof of Stacks 0FIS uses 0FVS.

theorem injective_pull_specMap_of_axioms [CharZero F] (hA1 : 𝔇.CoproductAxiom)
    (hA3 : 𝔇.ProjectiveBundleAxiom) (hA4 : 𝔇.DivisorAxiom) (hA5 : 𝔇.KunnethAxiom)
    {k' : Type u} [Field k'] [Algebra k k'] [FiniteDimensional k k'] [Algebra.IsSeparable k k']
    {k'' : Type u} [Field k''] [Algebra k k''] [FiniteDimensional k k''] [Algebra.IsSeparable k k'']
    (incl : k' →ₐ[k] k'') : Function.Injective (𝔇.pull (specMap incl))

Stacks.WeilCohomology.injective_pullback_of_separable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/SeparableExtension.lean, line 417. The attribute's comment: “injectivity on cohomology for a tower of finite separable field extensions; the Künneth decomposition of Spec(k') x Spec(K) as a product over the embeddings, the functoriality relations, and the nonvanishing of the cohomology of Spec(K) are derived from the functor of (D1) together with axioms (A1), (A5), (A6) and (C)(b), which are explicit arguments here, as elsewhere in Section 45.14”.

Let k''/k'/k be finite separable field extensions. Then pullback H^0(Spec(k')) → H^0(Spec(k'')) is injective.

Here H is the cohomology functor of (D1), read on the spectra of finite étale k-algebras; since these schemes are zero dimensional, H^0 is the total cohomology H^*. The hypothesis kunneth is axiom (A5) and disjointUnion is axiom (A1); traceMap is the trace map ∫_{Spec(L)} of axiom (A6) for the zero-dimensional scheme Spec(L), cycleClass is the cycle class map γ of (D2') on the zero cycles of Spec(L), free of rank one on [Spec(L)], and traceMap_cycleClass is axiom (C)(b) for the structure morphism of Spec(L), which evaluates that trace on γ(n · [Spec(L)]) as its degree n · [L : k].

theorem injective_pullback_of_separable
    (k k' k'' : Type u) [Field k] [Field k'] [Field k'']
    [Algebra k k'] [Algebra k k''] [Algebra k' k''] [IsScalarTower k k' k'']
    [FiniteDimensional k k'] [Algebra.IsSeparable k k']
    [FiniteDimensional k' k''] [Algebra.IsSeparable k' k'']
    (F : Type v) [Field F] [CharZero F] (H : FinEtaleAlg k ⥤ CommAlgCat.{w} F)
    (kunneth : ∀ X Y : FinEtaleAlg k, Function.Bijective (finEtaleKunnethMap H X Y))
    (disjointUnion : ∀ (ι : Type u) [Fintype ι] (X : ι → FinEtaleAlg k),
      Function.Bijective (componentRestriction H X))
    (cycleClass : ∀ (L : Type u) [Field L] [Algebra k L] (hfin : Module.Finite k L)
      (hsep : Algebra.IsSeparable k L), ℤ →+ H.obj (ofField k L hfin hsep))
    (traceMap : ∀ (L : Type u) [Field L] [Algebra k L] (hfin : Module.Finite k L)
      (hsep : Algebra.IsSeparable k L), H.obj (ofField k L hfin hsep) →ₗ[F] F)
    (traceMap_cycleClass : ∀ (L : Type u) [Field L] [Algebra k L]
      (hfin : Module.Finite k L) (hsep : Algebra.IsSeparable k L) (n : ℤ),
      traceMap L hfin hsep (cycleClass L hfin hsep n) =
        (n : F) * (Module.finrank k L : F)) :
    Function.Injective (H.map (algHomMk (X := ofField k k' inferInstance inferInstance)
      (Y := ofField k k'' (Module.Finite.trans k' k'') (Algebra.IsSeparable.trans k k' k''))
      (IsScalarTower.toAlgHom k k' k'')))

Tag 0FIS, a lemma

Tag 0FIS in the Stacks Project.

Stacks.WeilCohomology.integration_comp_pullback_eq_integration, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/BlowupPushforward.lean, line 149. The attribute's comment: “integration agrees with integration after pullback to the blowup”.

Stacks Project, Tag 0FIS. For a blowup b : X' ⟶ X of a nonempty equidimensional smooth projective scheme of dimension d in a nowhere dense smooth centre, integration over X' after pullback is integration over X: both satisfy the normalization (1 ⊗ ∫)(η) = 1 of (A6) against the degree-zero Künneth component of the diagonal class of X, which determines the trace map.

theorem integration_comp_pullback_eq_integration
    (pullbackZero : A →ₗ[F] A') (pullbackTop : T →ₗ[F] T') (restrict : A' →ₗ[F] P)
    (one : A) (one' : A') (integration : T →ₗ[F] F) (integration' : T' →ₗ[F] F)
    (η : A ⊗[F] T) (η' : A' ⊗[F] T')
    (restrict_injective : Function.Injective restrict)
    (pullbackZero_injective : Function.Injective pullbackZero)
    (pullbackZero_one : pullbackZero one = one')
    (restrict_eq : TensorProduct.map (restrict ∘ₗ pullbackZero) pullbackTop η =
      TensorProduct.map restrict LinearMap.id η')
    (normalization : tensorContractRight integration η = one)
    (normalization' : tensorContractRight integration' η' = one')
    (nondegenerate : Function.Injective fun μ : T →ₗ[F] F => tensorContractRight μ η) :
    integration' ∘ₗ pullbackTop = integration

Stacks.WeilCohomology.pushforwardOne_blowup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/BlowupPushforward.lean, line 175.

Stacks Project, Tag 0FIS. For a blowup b : X' ⟶ X of a nonempty equidimensional smooth projective scheme of dimension d in a nowhere dense smooth centre, the Poincaré-dual pushforward carries the unit class of X' to the unit class of X: b_*(1) = 1.

theorem pushforwardOne_blowup
    (pullbackZero : A →ₗ[F] A') (pullbackTop : T →ₗ[F] T') (restrict : A' →ₗ[F] P)
    (one : A) (one' : A') (integration : T →ₗ[F] F) (integration' : T' →ₗ[F] F)
    (pairing : T →ₗ[F] A →ₗ[F] F) [pairing.IsPerfPair] (pairing' : T' →ₗ[F] A' →ₗ[F] F)
    (η : A ⊗[F] T) (η' : A' ⊗[F] T')
    (restrict_injective : Function.Injective restrict)
    (pullbackZero_injective : Function.Injective pullbackZero)
    (pullbackZero_one : pullbackZero one = one')
    (restrict_eq : TensorProduct.map (restrict ∘ₗ pullbackZero) pullbackTop η =
      TensorProduct.map restrict LinearMap.id η')
    (normalization : tensorContractRight integration η = one)
    (normalization' : tensorContractRight integration' η' = one')
    (nondegenerate : Function.Injective fun μ : T →ₗ[F] F => tensorContractRight μ η)
    (pairing_one : ∀ β, pairing β one = integration β)
    (pairing_one' : ∀ β, pairing' β one' = integration' β) :
    poincareDualPushforward pairing' pairing pullbackTop one' = one

Stacks.WeilCohomology.FirstChernClassData.trace_comp_pullGradeTw_blowupHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/BlowupPushforwardOne.lean, line 203. The attribute's comment: “∫_{X'} ∘ b^ = ∫_X on H^{2d}(X)(d) for the blowing up in a nowhere dense smooth centre, the trace maps being the λ of (A6) and γ the cycle class map of 0FIF, under (A1)-(A8); the form b_(1) = 1 of the statement is this identity read through Poincaré duality”.

Stacks Project, Tag 0FIS. Let data (D0), (D1), (D2') satisfy axioms (A1)–(A8) of Section 45.14 (of which (A1), (A3), (A4), (A5), (A7), (A8) are used), with γ the cycle class map of Tag 0FIF. Let b : X' ⟶ X be the blowing up of a smooth projective scheme X over k, nonempty and equidimensional of dimension d, in a nowhere dense smooth centre Z ⊆ X. Then the trace map ∫_{X'} of X' composed with b^* : H^{2d}(X)(d) ⟶ H^{2d}(X')(d) is the trace map ∫_X of X: for the linear maps λ, λ' of axiom (A6) for X and X' (unique by Remark 0FIK), λ' ∘ b^* = λ. This is the identity the source's proof establishes ("∫_X is equal to ∫_{X'} composed with the pullback map"), equivalent to b_*(1) = 1 for the pushforward of Section 45.9 built from these trace maps.

theorem trace_comp_pullGradeTw_blowupHom (h : 𝔇.IsCohomologicalChernCharacter ch)
    (hA1 : 𝔇.CoproductAxiom) (hA3 : 𝔇.ProjectiveBundleAxiom) (hA4 : 𝔇.DivisorAxiom)
    (hA5 : 𝔇.KunnethAxiom) (hA7 : 𝔇.BlowupAxiom) (hA8 : 𝔇.GlobalSectionsAxiom)
    {Z X : (SmoothProjectiveScheme k).FullSubcategory} (i : Z ⟶ X) [IsClosedImmersion i.hom.left]
    (hZ : IsNowhereDense (Set.range i.hom.left.base)) {d : ℕ}
    (hX : IsNonemptyEquidimensional X d)
    (lam : tateTwist F 𝔇.tate (𝔇.grade X (2 * (d : ℤ))) d →ₗ[F] F)
    (lam' : tateTwist F 𝔇.tate (𝔇.grade (blowupObj i) (2 * (d : ℤ))) d →ₗ[F] F)
    (hlam : 𝔇.traceContract hA5 X d lam
      (h.codimensionCycleClass (prod X X) d (diagonalClass X d)) = 1)
    (hlam' : 𝔇.traceContract hA5 (blowupObj i) d lam'
      (h.codimensionCycleClass (prod (blowupObj i) (blowupObj i)) d
        (diagonalClass (blowupObj i) d)) = 1) :
    lam' ∘ₗ 𝔇.pullGradeTw (blowupHom i) (2 * (d : ℤ)) d = lam

Stacks.WeilCohomology.FirstChernClassData.pushforward_unitTw_blowupHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/BlowupPushforwardOne.lean, line 229. The attribute's comment: “b_*(1) = 1 for the blowing up in a nowhere dense smooth centre, for the pushforward of Section 45.9 attached to the data of (A1)-(A8) with the trace maps of (A6) and γ of 0FIF”.

Stacks Project, Tag 0FIS: b_*(1) = 1. Let data (D0), (D1), (D2') satisfy axioms (A1)–(A8) of Section 45.14 (of which (A1), (A3)–(A8) are used), γ the cycle class map of Tag 0FIF, and let W be the data (D0)–(D3) of Section 45.9 they define, with trace maps the λ of (A6) (IsCohomologicalChernCharacter.toWeilData), which satisfy axiom (A) by Lemma 0FIJ. Let b : X' ⟶ X be the blowing up of a smooth projective scheme X over k, nonempty and equidimensional of dimension d, in a nowhere dense smooth centre. Then the pushforward b_* : H^0(X') ⟶ H^0(X) of Section 45.9 sends 1 to 1.

theorem pushforward_unitTw_blowupHom (h : 𝔇.IsCohomologicalChernCharacter ch)
    (hA1 : 𝔇.CoproductAxiom) (hA3 : 𝔇.ProjectiveBundleAxiom) (hA4 : 𝔇.DivisorAxiom)
    (hA5 : 𝔇.KunnethAxiom) (hA6 : 𝔇.TraceAxiomFor hA5 h.codimensionCycleClass)
    (hA7 : 𝔇.BlowupAxiom) (hA8 : 𝔇.GlobalSectionsAxiom)
    {Z X : (SmoothProjectiveScheme k).FullSubcategory} (i : Z ⟶ X) [IsClosedImmersion i.hom.left]
    (hZ : IsNowhereDense (Set.range i.hom.left.base)) {d : ℕ}
    (hX : IsNonemptyEquidimensional X d) :
    (h.toWeilData hA1 hA3 hA5 hA6).pushforward
        (h.poincareDuality_toWeilData hA1 hA3 hA5 hA6 hA4 hA7).perfectPairing (blowupHom i)
        (isNonemptyEquidimensional_blowupObj i hX hZ) hX 0 0 0 0 rfl rfl
        ((h.toWeilData hA1 hA3 hA5 hA6).unitTw (blowupObj i) 0 0 rfl) =
      (h.toWeilData hA1 hA3 hA5 hA6).unitTw X 0 0 rfl

Tag 0FIT, a lemma

Tag 0FIT in the Stacks Project.

Stacks.WeilCohomology.WeilChernData.cycleClassPushforward_of_globalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/CycleClassPushforwardGlobalSections.lean, line 144. The attribute's comment: “the whole lemma, under exactly (A1)-(A8): WeilChernData bundles (A1)-(A7) and the only hypothesis is (A8) GlobalSections; conclusion: gamma commutes with pushforward (axiom (C)(b) for toWeilData) for every morphism of nonempty equidimensional smooth projective schemes; nothing assumed, (A9) is not used”.

Tag 0FIT: for data (D0), (D1), (D2') satisfying axioms (A1)–(A8) (a WeilChernData, which bundles (A1)–(A7), and (A8) GlobalSections), the cycle class map γ commutes with pushforward: axiom (C)(b) of Section 0FHA for WeilChernData.toWeilData, i.e. γ(f_*α) = f_*γ(α) for every morphism f : X ⟶ Y of nonempty equidimensional smooth projective schemes over k and every α ∈ CH^p(X). This is Lemma 0FIP's reduction (cycleClassPushforward_of_grassmannian) applied to pushforward_unitTw_eq_cycleClass_of_globalSections. The source's proof cites (A9) for j_*1 = γ([E]); here that step is cycleClass_exceptional_eq_pushforward_unitTw_of_lt, proved from (A1)–(A8).

theorem cycleClassPushforward_of_globalSections (hA8 : 𝔚.GlobalSections) :
    𝔚.toWeilData.CycleClassPushforward 𝔚.perfectPairing

Tag 0FIU, a proposition

Tag 0FIU in the Stacks Project.

Stacks.WeilCohomology.WeilChernData.exists_weilCohomologyTheory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/Concrete/WeilCohomologyTheoryOfWeilChern.lean, line 85. The attribute's comment: “the whole proposition, under exactly (A1)-(A8): WeilChernData bundles (A1)-(A7) and the only hypothesis is (A8) GlobalSections; conclusion: a Weil cohomology theory (Definition 0FI2) whose data (D0)-(D3) are F(1), H^*, gamma of 0FIF and the trace of (A6); nothing assumed, (A9) is not used”.

Proposition 0FIU: data (D0), (D1), (D2') satisfying (A1)–(A8) give a Weil cohomology theory: there is a Weil cohomology theory (Definition 0FI2) whose data (D0)–(D3) are 𝔚.toWeilData, i.e. the given F(1) and H^*, the cycle class map γ of Tag 0FIF and the trace map ∫_X = λ of axiom (A6).

theorem exists_weilCohomologyTheory (hA8 : 𝔚.GlobalSections) :
    ∃ T : WeilCohomologyTheory k F, T.toWeilData = 𝔚.toWeilData

Tag 0FVT, a lemma

Tag 0FVT in the Stacks Project.

Stacks.WeilCohomology.exists_axioms_of_fieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/WeilCohomology/BaseFieldExtension/Descent.lean, line 215.

Stacks Tag 0FVT. Let k'/k be an extension of fields and F'/F an extension of fields of characteristic zero. Let 𝔇 = (F(1), H^*, c₁^H) be data (D0), (D1), (D2') for k and F and 𝔚' = (F'(1), (H')^*, c₁^{H'}) data (D0), (D1), (D2') for k' and F', given with an isomorphism F(1) ⊗_F F' ≅ F'(1) and isomorphisms H^*(X) ⊗_F F' ≅ (H')^*(X_{k'}) of graded F'-algebras, functorial in the smooth projective scheme X over k, under which c₁^H and c₁^{H'} correspond (Φ, a Stacks.WeilCohomology.FieldExtensionComparison). If F'(1), (H')^*, c₁^{H'} satisfy (A1)–(A9) — (A1)–(A7) being the fields of Stacks.WeilCohomology.WeilChernData, (A8) GlobalSections, (A9) DivisorTrace — then F(1), H^*, c₁^H satisfy (A1)–(A9): (A1)–(A5), (A6) for the cycle class map γ of Tag 0FIF of the data 𝔇 (which (A1)–(A4) determine), (A7), (A8), and (A9) for that γ.

theorem exists_axioms_of_fieldExtension [CharZero F] [CharZero F'] (𝔇 : FirstChernClassData k F)
    (𝔚' : WeilChernData k' F') (Φ : FieldExtensionComparison 𝔇 𝔚'.toFirstChernClassData)
    (h8 : 𝔚'.GlobalSections) (h9 : 𝔚'.DivisorTrace) :
    ∃ (hA1 : 𝔇.CoproductAxiom) (hA2 : 𝔇.PullbackAxiom) (hA3 : 𝔇.ProjectiveBundleAxiom)
      (hA4 : 𝔇.DivisorAxiom) (hA5 : 𝔇.KunnethAxiom),
      𝔇.TraceAxiomFor hA5 (𝔇.cycleClassOf hA1 hA2 hA3 hA4) ∧ 𝔇.BlowupAxiom ∧
        𝔇.GlobalSectionsAxiom ∧ 𝔇.DivisorTraceAxiomFor hA5 (𝔇.cycleClassOf hA1 hA2 hA3 hA4)

Sources

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

45.10 Further properties to 45.14 Weil cohomology theories…

Section45.10 Further properties#

Tag 0FHP, a lemma

Tag 0FHQ, a lemma

Tag 0FHR, a lemma

Tag 0FHS, a lemma

Tag 0FHT, a lemma

Tag 0FHU, a lemma

What is assumed and what is proved

Tag 0FHV, a lemma

Tag 0FHW, a lemma

Tag 0FHX, a lemma

Sources

Section45.11 Weil cohomology theories, II#

Tag 0FI0, a lemma

Tag 0FI1, a lemma

Tag 0FI2, a definition

Tag 0FI3, a remark

Tag 0GIJ, a proposition

Sources

Section45.12 Chern classes#

Tag 0FI5, a proposition

Tag 0FI7, a lemma

Tag 0FI8, a lemma

Tag 0FI9, a proposition

Tag 0FIA, a lemma

Sources

Section45.13 Exterior powers and K-groups#

Tag 0FIC, a lemma

Sources

Section45.14 Weil cohomology theories, III#

Tag 0FIE, a lemma

Tag 0FIF, a lemma

Tag 0FIH, a lemma

Tag 0FII, a lemma

Tag 0FIJ, a lemma

Tag 0FIK, a remark

Tag 0FIL, a lemma

Tag 0FIM, a lemma

Tag 0FIN, a lemma

Tag 0FVR, a lemma

Tag 0FIP, a lemma

Tag 0FIQ, a lemma

Tag 0FIR, a lemma

Tag 0FVS, a lemma

Tag 0FIS, a lemma

Tag 0FIT, a lemma

Tag 0FIU, a proposition

Tag 0FVT, a lemma

Sources

Section45.10 Further properties #

Section45.11 Weil cohomology theories, II #

Section45.12 Chern classes #

Section45.13 Exterior powers and K-groups #

Section45.14 Weil cohomology theories, III #