The Hodge Conjecture Formalization

3. Cycles and cohomology with support🔗

3.1. Cycles are indexed by generic points🔗

The coheight of a point x of a scheme is the codimension of its closure \overline{\{x\}}, an irreducible closed subset with generic point x. A codimension-p cycle is a locally finite integer combination of points of coheight p. The formalization uses this description throughout, in place of a separate type of subvarieties.

def codimensionCycleSubgroup (X : Scheme.{u}) (p : ℕ) : AddSubgroup (AlgebraicCycle X ℤ) where carrier c := ∀ x, c x ≠ 0 → coheight x = p zero_mem' x hx := (hx rfl).elim add_mem' := X✝:Over (Spec (CommRingCat.of ℂ))inst✝²:AlgebraicGeometry.IsIntegral X✝.leftinst✝¹:Smooth X✝.hominst✝:IsProjective X✝.homd:ℕp✝:ℕx:↥X✝.lefthx:coheight x = ↑p✝n:ℤX:Schemep:ℕ⊢ ∀ {a b : AlgebraicCycle X ℤ}, (a ∈ fun c ↦ ∀ (x : ↥X), c x ≠ 0 → coheight x = ↑p) → (b ∈ fun c ↦ ∀ (x : ↥X), c x ≠ 0 → coheight x = ↑p) → a + b ∈ fun c ↦ ∀ (x : ↥X), c x ≠ 0 → coheight x = ↑p X✝:Over (Spec (CommRingCat.of ℂ))inst✝²:AlgebraicGeometry.IsIntegral X✝.leftinst✝¹:Smooth X✝.hominst✝:IsProjective X✝.homd:ℕp✝:ℕx✝:↥X✝.lefthx✝:coheight x = ↑p✝n:ℤX:Schemep:ℕa:AlgebraicCycle X ℤb:AlgebraicCycle X ℤha:a ∈ fun c ↦ ∀ (x : ↥X), c x ≠ 0 → coheight x = ↑phb:b ∈ fun c ↦ ∀ (x : ↥X), c x ≠ 0 → coheight x = ↑px:↥Xhx:(a + b) x ≠ 0⊢ coheight x = ↑p X✝:Over (Spec (CommRingCat.of ℂ))inst✝²:AlgebraicGeometry.IsIntegral X✝.leftinst✝¹:Smooth X✝.hominst✝:IsProjective X✝.homd:ℕp✝:ℕx✝:↥X✝.lefthx✝:coheight x = ↑p✝n:ℤX:Schemep:ℕa:AlgebraicCycle X ℤb:AlgebraicCycle X ℤha:a ∈ fun c ↦ ∀ (x : ↥X), c x ≠ 0 → coheight x = ↑phb:b ∈ fun c ↦ ∀ (x : ↥X), c x ≠ 0 → coheight x = ↑px:↥Xhx:(a + b) x ≠ 0hax:a x = 0⊢ coheight x = ↑pX✝:Over (Spec (CommRingCat.of ℂ))inst✝²:AlgebraicGeometry.IsIntegral X✝.leftinst✝¹:Smooth X✝.hominst✝:IsProjective X✝.homd:ℕp✝:ℕx✝:↥X✝.lefthx✝:coheight x = ↑p✝n:ℤX:Schemep:ℕa:AlgebraicCycle X ℤb:AlgebraicCycle X ℤha:a ∈ fun c ↦ ∀ (x : ↥X), c x ≠ 0 → coheight x = ↑phb:b ∈ fun c ↦ ∀ (x : ↥X), c x ≠ 0 → coheight x = ↑px:↥Xhx:(a + b) x ≠ 0hax:¬a x = 0⊢ coheight x = ↑p X✝:Over (Spec (CommRingCat.of ℂ))inst✝²:AlgebraicGeometry.IsIntegral X✝.leftinst✝¹:Smooth X✝.hominst✝:IsProjective X✝.homd:ℕp✝:ℕx✝:↥X✝.lefthx✝:coheight x = ↑p✝n:ℤX:Schemep:ℕa:AlgebraicCycle X ℤb:AlgebraicCycle X ℤha:a ∈ fun c ↦ ∀ (x : ↥X), c x ≠ 0 → coheight x = ↑phb:b ∈ fun c ↦ ∀ (x : ↥X), c x ≠ 0 → coheight x = ↑px:↥Xhx:(a + b) x ≠ 0hax:a x = 0⊢ coheight x = ↑p exact hb x (X✝:Over (Spec (CommRingCat.of ℂ))inst✝²:AlgebraicGeometry.IsIntegral X✝.leftinst✝¹:Smooth X✝.hominst✝:IsProjective X✝.homd:ℕp✝:ℕx✝:↥X✝.lefthx✝:coheight x = ↑p✝n:ℤX:Schemep:ℕa:AlgebraicCycle X ℤb:AlgebraicCycle X ℤha:a ∈ fun c ↦ ∀ (x : ↥X), c x ≠ 0 → coheight x = ↑phb:b ∈ fun c ↦ ∀ (x : ↥X), c x ≠ 0 → coheight x = ↑px:↥Xhx:(a + b) x ≠ 0hax:a x = 0⊢ b x ≠ 0 All goals completed! 🐙) X✝:Over (Spec (CommRingCat.of ℂ))inst✝²:AlgebraicGeometry.IsIntegral X✝.leftinst✝¹:Smooth X✝.hominst✝:IsProjective X✝.homd:ℕp✝:ℕx✝:↥X✝.lefthx✝:coheight x = ↑p✝n:ℤX:Schemep:ℕa:AlgebraicCycle X ℤb:AlgebraicCycle X ℤha:a ∈ fun c ↦ ∀ (x : ↥X), c x ≠ 0 → coheight x = ↑phb:b ∈ fun c ↦ ∀ (x : ↥X), c x ≠ 0 → coheight x = ↑px:↥Xhx:(a + b) x ≠ 0hax:¬a x = 0⊢ coheight x = ↑p All goals completed! 🐙 neg_mem' := X✝:Over (Spec (CommRingCat.of ℂ))inst✝²:AlgebraicGeometry.IsIntegral X✝.leftinst✝¹:Smooth X✝.hominst✝:IsProjective X✝.homd:ℕp✝:ℕx:↥X✝.lefthx:coheight x = ↑p✝n:ℤX:Schemep:ℕ⊢ ∀ {x : AlgebraicCycle X ℤ}, (x ∈ fun c ↦ ∀ (x : ↥X), c x ≠ 0 → coheight x = ↑p) → -x ∈ fun c ↦ ∀ (x : ↥X), c x ≠ 0 → coheight x = ↑p X✝:Over (Spec (CommRingCat.of ℂ))inst✝²:AlgebraicGeometry.IsIntegral X✝.leftinst✝¹:Smooth X✝.hominst✝:IsProjective X✝.homd:ℕp✝:ℕx✝:↥X✝.lefthx✝:coheight x = ↑p✝n:ℤX:Schemep:ℕa:AlgebraicCycle X ℤha:a ∈ fun c ↦ ∀ (x : ↥X), c x ≠ 0 → coheight x = ↑px:↥Xhx:(-a) x ≠ 0⊢ coheight x = ↑p X✝:Over (Spec (CommRingCat.of ℂ))inst✝²:AlgebraicGeometry.IsIntegral X✝.leftinst✝¹:Smooth X✝.hominst✝:IsProjective X✝.homd:ℕp✝:ℕx✝:↥X✝.lefthx✝:coheight x = ↑p✝n:ℤX:Schemep:ℕa:AlgebraicCycle X ℤha:a ∈ fun c ↦ ∀ (x : ↥X), c x ≠ 0 → coheight x = ↑px:↥Xhx:(-a) x ≠ 0h:a x = 0⊢ (-a) x = 0 X✝:Over (Spec (CommRingCat.of ℂ))inst✝²:AlgebraicGeometry.IsIntegral X✝.leftinst✝¹:Smooth X✝.hominst✝:IsProjective X✝.homd:ℕp✝:ℕx✝:↥X✝.lefthx✝:coheight x = ↑p✝n:ℤX:Schemep:ℕa:AlgebraicCycle X ℤha:a ∈ fun c ↦ ∀ (x : ↥X), c x ≠ 0 → coheight x = ↑px:↥Xhx:(-a) x ≠ 0h:a x = 0⊢ -a x = 0 All goals completed! 🐙 noncomputable def codimensionCycleSubgroup.single {X : Scheme.{u}} {p : ℕ} (x : X) (hx : coheight x = p) (n : ℤ) : codimensionCycleSubgroup X p := X✝:Over (Spec (CommRingCat.of ℂ))inst✝²:AlgebraicGeometry.IsIntegral X✝.leftinst✝¹:Smooth X✝.hominst✝:IsProjective X✝.homd:ℕp✝:ℕx✝:↥X✝.lefthx✝:coheight x✝ = ↑p✝n✝:ℤX:Schemep:ℕx:↥Xhx:coheight x = ↑pn:ℤ⊢ ↥(codimensionCycleSubgroup X p) classical exact ⟨Function.locallyFinsuppWithin.single x n, X✝:Over (Spec (CommRingCat.of ℂ))inst✝²:AlgebraicGeometry.IsIntegral X✝.leftinst✝¹:Smooth X✝.hominst✝:IsProjective X✝.homd:ℕp✝:ℕx✝:↥X✝.lefthx✝:coheight x✝ = ↑p✝n✝:ℤX:Schemep:ℕx:↥Xhx:coheight x = ↑pn:ℤ⊢ Function.locallyFinsuppWithin.single x n ∈ codimensionCycleSubgroup X p X✝:Over (Spec (CommRingCat.of ℂ))inst✝²:AlgebraicGeometry.IsIntegral X✝.leftinst✝¹:Smooth X✝.hominst✝:IsProjective X✝.homd:ℕp✝:ℕx✝:↥X✝.lefthx✝:coheight x✝ = ↑p✝n✝:ℤX:Schemep:ℕx:↥Xhx:coheight x = ↑pn:ℤy:↥Xhy:(Function.locallyFinsuppWithin.single x n) y ≠ 0⊢ coheight y = ↑p X✝:Over (Spec (CommRingCat.of ℂ))inst✝²:AlgebraicGeometry.IsIntegral X✝.leftinst✝¹:Smooth X✝.hominst✝:IsProjective X✝.homd:ℕp✝:ℕx✝:↥X✝.lefthx✝:coheight x✝ = ↑p✝n✝:ℤX:Schemep:ℕx:↥Xhx:coheight x = ↑pn:ℤy:↥Xhy:(Function.locallyFinsuppWithin.single x n) y ≠ 0h:y = x⊢ coheight y = ↑pX✝:Over (Spec (CommRingCat.of ℂ))inst✝²:AlgebraicGeometry.IsIntegral X✝.leftinst✝¹:Smooth X✝.hominst✝:IsProjective X✝.homd:ℕp✝:ℕx✝:↥X✝.lefthx✝:coheight x✝ = ↑p✝n✝:ℤX:Schemep:ℕx:↥Xhx:coheight x = ↑pn:ℤy:↥Xhy:(Function.locallyFinsuppWithin.single x n) y ≠ 0h:¬y = x⊢ coheight y = ↑p X✝:Over (Spec (CommRingCat.of ℂ))inst✝²:AlgebraicGeometry.IsIntegral X✝.leftinst✝¹:Smooth X✝.hominst✝:IsProjective X✝.homd:ℕp✝:ℕx✝:↥X✝.lefthx✝:coheight x✝ = ↑p✝n✝:ℤX:Schemep:ℕx:↥Xhx:coheight x = ↑pn:ℤy:↥Xhy:(Function.locallyFinsuppWithin.single x n) y ≠ 0h:y = x⊢ coheight y = ↑p All goals completed! 🐙 X✝:Over (Spec (CommRingCat.of ℂ))inst✝²:AlgebraicGeometry.IsIntegral X✝.leftinst✝¹:Smooth X✝.hominst✝:IsProjective X✝.homd:ℕp✝:ℕx✝:↥X✝.lefthx✝:coheight x✝ = ↑p✝n✝:ℤX:Schemep:ℕx:↥Xhx:coheight x = ↑pn:ℤy:↥Xhy:(Function.locallyFinsuppWithin.single x n) y ≠ 0h:¬y = x⊢ coheight y = ↑p All goals completed! 🐙⟩

3.2. The support of a subvariety🔗

For a point x of X.left, cycleComponent X.left x is the reduced closed subscheme with underlying space \overline{\{x\}}, and cycleComponentι is its closed immersion into X.left. The support of the subvariety in X(\mathbb C) is the preimage of \overline{\{x\}} under the map from complex points to scheme points, and it is closed in the analytic topology.

def cycleComponent (X : Scheme) (x : X) : Scheme := (Scheme.IdealSheafData.vanishingIdeal (X := X) ⟨closure {x}, isClosed_closure⟩).subscheme def cycleComponentι (X : Scheme) (x : X) : cycleComponent X x ⟶ X := (Scheme.IdealSheafData.vanishingIdeal (X := X) ⟨closure {x}, isClosed_closure⟩).subschemeι def cycleComponentSupport (X : Over (Spec ↧ℂ)) [IsIntegral X.left] [Smooth X.hom] [IsProjective X.hom] (x : X.left) : Set (ComplexPoint X) := Point.underlying ⁻¹' closure {x} AlgebraicGeometry.isClosed_cycleComponentSupport (X : Over (Spec (CommRingCat.of ℂ))) [AlgebraicGeometry.IsIntegral X.left] [Smooth X.hom] [IsProjective X.hom] (x : ↥X.left) : IsClosed (cycleComponentSupport X x)#check AlgebraicGeometry.isClosed_cycleComponentSupport

Only the ambient variety is assumed smooth. A subvariety may be singular, and the construction of its class in the next section handles that case from the start.

3.3. Cohomology with support🔗

Let Z\subseteq X(\mathbb C) be closed, with open complement j:U\hookrightarrow X(\mathbb C). Cohomology with support in Z sits in the distinguished triangle

R\Gamma_Z(X,\mathbb Q_X)\longrightarrow R\Gamma(X,\mathbb Q_X) \longrightarrow R\Gamma(U,\mathbb Q_U)\xrightarrow{+1}.

The formalization builds the first term as a homotopy fibre. It resolves the constant sheaf \underline{\mathbb Q}_U injectively, pushes the resolution forward along j, maps \underline{\mathbb Q}_X to the result, and takes the mapping cone shifted by -1. Hypercohomology of this complex is H^n_Z(X;\mathbb Q), and the connecting map of the triangle is forgetSupport, the map H^n_Z(X;\mathbb Q)\to H^n(X;\mathbb Q).

abbrev rationalCohomologyWithSupportComplex (X : Over (Spec ↧ℂ)) (Z : Set (ComplexPoint X)) : CochainComplex (AnalyticAdditiveSheaf X) ℤ := CochainComplex.mappingCone (rationalRestrictionComplexInt X Z) abbrev RationalCohomologyWithSupport (X : Over (Spec ↧ℂ)) (Z : Set (ComplexPoint X)) (n : ℤ) : Type 1 := Hypercohomology X (rationalCohomologyWithSupportComplex X Z) (n - 1) def forgetSupport (X : Over (Spec ↧ℂ)) (Z : Set (ComplexPoint X)) (n : ℤ) : RationalCohomologyWithSupport X Z n →+ H^n(X; ℚ) where toFun α := α.comp (forgetSupportShiftedHom X Z) (X✝:Over (Spec (CommRingCat.of ℂ))inst✝²:AlgebraicGeometry.IsIntegral X✝.leftinst✝¹:Smooth X✝.hominst✝:IsProjective X✝.homd:ℕp:ℕx:↥X✝.lefthx:coheight x = ↑pn✝:ℤX:Over (Spec (CommRingCat.of ℂ))Z:Set (ComplexPoint X)n:ℤα:RationalCohomologyWithSupport X Z n⊢ 1 + (n - 1) = n All goals completed! 🐙) map_zero' := X✝:Over (Spec (CommRingCat.of ℂ))inst✝²:AlgebraicGeometry.IsIntegral X✝.leftinst✝¹:Smooth X✝.hominst✝:IsProjective X✝.homd:ℕp:ℕx:↥X✝.lefthx:coheight x = ↑pn✝:ℤX:Over (Spec (CommRingCat.of ℂ))Z:Set (ComplexPoint X)n:ℤ⊢ Localization.SmallShiftedHom.comp 0 (forgetSupportShiftedHom X Z) ⋯ = 0 X✝:Over (Spec (CommRingCat.of ℂ))inst✝²:AlgebraicGeometry.IsIntegral X✝.leftinst✝¹:Smooth X✝.hominst✝:IsProjective X✝.homd:ℕp:ℕx:↥X✝.lefthx:coheight x = ↑pn✝:ℤX:Over (Spec (CommRingCat.of ℂ))Z:Set (ComplexPoint X)n:ℤ⊢ (Localization.SmallShiftedHom.equiv (analyticQuasiIsomorphisms X) DerivedCategory.Q) (Localization.SmallShiftedHom.comp 0 (forgetSupportShiftedHom X Z) ⋯) = (Localization.SmallShiftedHom.equiv (analyticQuasiIsomorphisms X) DerivedCategory.Q) 0 All goals completed! 🐙 map_add' α β := X✝:Over (Spec (CommRingCat.of ℂ))inst✝²:AlgebraicGeometry.IsIntegral X✝.leftinst✝¹:Smooth X✝.hominst✝:IsProjective X✝.homd:ℕp:ℕx:↥X✝.lefthx:coheight x = ↑pn✝:ℤX:Over (Spec (CommRingCat.of ℂ))Z:Set (ComplexPoint X)n:ℤα:RationalCohomologyWithSupport X Z nβ:RationalCohomologyWithSupport X Z n⊢ Localization.SmallShiftedHom.comp (α + β) (forgetSupportShiftedHom X Z) ⋯ = Localization.SmallShiftedHom.comp α (forgetSupportShiftedHom X Z) ⋯ + Localization.SmallShiftedHom.comp β (forgetSupportShiftedHom X Z) ⋯ X✝:Over (Spec (CommRingCat.of ℂ))inst✝²:AlgebraicGeometry.IsIntegral X✝.leftinst✝¹:Smooth X✝.hominst✝:IsProjective X✝.homd:ℕp:ℕx:↥X✝.lefthx:coheight x = ↑pn✝:ℤX:Over (Spec (CommRingCat.of ℂ))Z:Set (ComplexPoint X)n:ℤα:RationalCohomologyWithSupport X Z nβ:RationalCohomologyWithSupport X Z n⊢ (Localization.SmallShiftedHom.equiv (analyticQuasiIsomorphisms X) DerivedCategory.Q) (Localization.SmallShiftedHom.comp (α + β) (forgetSupportShiftedHom X Z) ⋯) = (Localization.SmallShiftedHom.equiv (analyticQuasiIsomorphisms X) DerivedCategory.Q) (Localization.SmallShiftedHom.comp α (forgetSupportShiftedHom X Z) ⋯ + Localization.SmallShiftedHom.comp β (forgetSupportShiftedHom X Z) ⋯) All goals completed! 🐙

For the triangle and the exact sequence of a pair see Goresky, §§7.14–7.15; for the derived-functor description see the Stacks Project, §20.21.