The Hodge Conjecture Formalization

4. The class of a subvariety🔗

4.1. The class to be constructed🔗

Let X be smooth of complex dimension d, and let Z\subseteq X be an irreducible closed subvariety of codimension p, with smooth locus Z_{\mathrm{reg}} and singular locus Z_{\mathrm{sing}}. Near a point of Z_{\mathrm{reg}}, holomorphic coordinates identify the pair (X,Z) with (\mathbb C^d,\mathbb C^{d-p}), so the cohomology of X with support in Z_{\mathrm{reg}} is locally one-dimensional in degree 2p and zero below. The complex structure orients the normal directions, and the orientation picks out a generator, the Thom class of the normal bundle. The class to be constructed is the global section of degree 2p that restricts to that generator in every chart,

\operatorname{cl}_X(Z)\in H^{2p}_Z(X;\mathbb Q),

and then, after forgetting the support, in H^{2p}(X;\mathbb Q).

The choice of generator is the essential point. Purity alone says that the local cohomology with support in degree 2p is one-dimensional, which fixes a line but not the multiplicity-one generator that a cycle class map needs. The formalization fixes the generator chart by chart using the complex orientation.

The whole construction stays in cohomology with support; no homology theory is involved, and the statement of the conjecture does not depend on one. Goresky, §8.11, gives the topological picture of a fundamental class this normalizes. Lee's Proposition 1.49 shows that a complex manifold carries a canonical orientation.

4.2. Step 1: the class on the smooth locus🔗

The smooth locus Z_{\mathrm{reg}} is closed in the open set X\setminus Z_{\mathrm{sing}}, where it is a smooth closed immersion of relative dimension d-p. Its codimension is recovered as d-(d-p)=p, which uses p\le d, a consequence of smoothness; this is what makes the natural-number subtraction in the types exact. Normal charts give local classes in degree 2p, these classes agree on overlaps, and they glue to a section of the sheaf of relative cohomology over X\setminus Z_{\mathrm{sing}}.

def cycleComponentSmoothClosedLiftCoclassSection (X : Over (Spec )) [IsIntegral X.left] [Smooth X.hom] [IsProjective X.hom] (x : X.left) {d p : } [SmoothOfRelativeDimension d X.hom] (hx : coheight x = p) : (supportRelativeCohomologySheaf (TopCat.of (ComplexPoint (cycleComponentSmoothLocusAmbientOpenOver X x))) (Set.range (Point.map (cycleComponentSmoothLocusClosedLiftOver X x))) (2 * p)).obj.obj (op ) := 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:Over (Spec (CommRingCat.of ))inst✝³:AlgebraicGeometry.IsIntegral X.leftinst✝²:Smooth X.hominst✝¹:IsProjective X.homx:X.leftd:p:inst✝:SmoothOfRelativeDimension d X.homhx:coheight x = p((supportRelativeCohomologySheaf (TopCat.of (ComplexPoint (cycleComponentSmoothLocusAmbientOpenOver X x))) (Set.range (Point.map (cycleComponentSmoothLocusClosedLiftOver X x))) (2 * p)).obj.obj (op )) 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:Over (Spec (CommRingCat.of ))inst✝³:AlgebraicGeometry.IsIntegral X.leftinst✝²:Smooth X.hominst✝¹:IsProjective X.homx:X.leftd:p:inst✝:SmoothOfRelativeDimension d X.homhx:coheight x = pthis:SmoothOfRelativeDimension (d - p) (cycleComponentSmoothClosedLiftStructureMap X x) := ···((supportRelativeCohomologySheaf (TopCat.of (ComplexPoint (cycleComponentSmoothLocusAmbientOpenOver X x))) (Set.range (Point.map (cycleComponentSmoothLocusClosedLiftOver X x))) (2 * p)).obj.obj (op )) 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:Over (Spec (CommRingCat.of ))inst✝³:AlgebraicGeometry.IsIntegral X.leftinst✝²:Smooth X.hominst✝¹:IsProjective X.homx:X.leftd:p:inst✝:SmoothOfRelativeDimension d X.homhx:coheight x = pthis:SmoothOfRelativeDimension (d - p) (cycleComponentSmoothClosedLiftStructureMap X x) := ···hdeg:d - (d - p) = p((supportRelativeCohomologySheaf (TopCat.of (ComplexPoint (cycleComponentSmoothLocusAmbientOpenOver X x))) (Set.range (Point.map (cycleComponentSmoothLocusClosedLiftOver X x))) (2 * p)).obj.obj (op )) All goals completed! 🐙 def cycleComponentSmoothSupportCoclassSection (X : Over (Spec )) [IsIntegral X.left] [Smooth X.hom] [IsProjective X.hom] (x : X.left) {d p : } [SmoothOfRelativeDimension d X.hom] (hx : coheight x = p) : (supportRelativeCohomologySheaf (TopCat.of (ComplexPoint X)) (cycleComponentSupport X x) (2 * p)).obj.obj (op (cycleComponentSmoothSupportAmbientOpen X x)) := supportRelativeCohomologySectionOnOpen (cycleComponentSmoothClosedLiftAmbientMap X x) (cycleComponentSmoothClosedLiftAmbientMap_isOpenEmbedding X x) (cycleComponentSupport X x) (Set.range (Point.map (cycleComponentSmoothLocusClosedLiftOver X x))) (cycleComponentSmoothClosedLiftAmbientMap_support X x) (2 * p) (cycleComponentSmoothSupportAmbientOpen X x) (cycleComponentSmoothClosedLiftAmbientMap_imageOpen X x) (cycleComponentSmoothClosedLiftCoclassSection X x (d := d) hx) AlgebraicGeometry.ComplexPoint.cycleComponentSmoothSupportCoclassSection_restrict (X : Over (Spec (CommRingCat.of ))) [AlgebraicGeometry.IsIntegral X.left] [Smooth X.hom] [IsProjective X.hom] (x : X.left) {d p : } [SmoothOfRelativeDimension d X.hom] (hx : coheight x = p) (V : Opens (ComplexPoint (cycleComponentSmoothLocusAmbientOpenOver X x))) (hV : .functor.obj V cycleComponentSmoothSupportAmbientOpen X x) : (ConcreteCategory.hom ((supportRelativeCohomologySheaf (TopCat.of (ComplexPoint X)) (cycleComponentSupport X x) (2 * p)).obj.map (homOfLE hV).op)) (cycleComponentSmoothSupportCoclassSection X x hx) = (ConcreteCategory.hom ((supportRelativeCohomologySheafOpenIso (cycleComponentSmoothClosedLiftAmbientMap X x) (cycleComponentSupport X x) (Set.range (Point.map (cycleComponentSmoothLocusClosedLiftOver X x))) (2 * p)).hom.hom.app (op V))) ((ConcreteCategory.hom ((supportRelativeCohomologySheaf (TopCat.of (ComplexPoint (cycleComponentSmoothLocusAmbientOpenOver X x))) (Set.range (Point.map (cycleComponentSmoothLocusClosedLiftOver X x))) (2 * p)).obj.map (homOfLE ).op)) (cycleComponentSmoothClosedLiftCoclassSection X x hx))#check AlgebraicGeometry.ComplexPoint.cycleComponentSmoothSupportCoclassSection_restrict

The restriction theorem says that on each chart the glued section is the class of that chart, exactly and not merely up to a nonzero rational multiple.

This section is nonzero whenever the smooth support has a complex point. Every neighborhood of that point contains a smaller normal chart, where the coclass evaluates to one on the normal class. It therefore stays nonzero under restriction to any neighborhood of that point, giving a nonzero germ and hence a nonzero glued section.

AlgebraicGeometry.ComplexPoint.smoothClosedSupportCoclassSection_ne_zero (X Y : Over (Spec (CommRingCat.of ))) (i : Y X) (m d : ) [SmoothOfRelativeDimension m Y.hom] [SmoothOfRelativeDimension d X.hom] [IsClosedImmersion (Over.Hom.left i)] (z : ComplexPoint Y) : smoothClosedSupportCoclassSection X Y i m d 0#check AlgebraicGeometry.ComplexPoint.smoothClosedSupportCoclassSection_ne_zero

The smooth locus of a component always has a complex point, so this applies to every component, in every codimension: the normalization does not silently produce zero anywhere.

AlgebraicGeometry.ComplexPoint.cycleComponentSmoothSupportCoclassSection_ne_zero (X : Over (Spec (CommRingCat.of ))) [AlgebraicGeometry.IsIntegral X.left] [Smooth X.hom] [IsProjective X.hom] (x : X.left) {d p : } [SmoothOfRelativeDimension d X.hom] (hx : coheight x = p) : cycleComponentSmoothSupportCoclassSection X x hx 0#check AlgebraicGeometry.ComplexPoint.cycleComponentSmoothSupportCoclassSection_ne_zero

Whether the resulting class in ordinary cohomology is nonzero is a different question, because forgetting support may kill it. That step is settled only for the generic point, at the end of this chapter, and in general it is cohomological purity; see What the repository proves about the statement.

4.3. Step 2: extension across the singular locus🔗

The singular locus Z_{\mathrm{sing}} has a finite filtration by closed subsets whose successive differences are smooth. Each layer has codimension at least p+1 in X, so its cohomology with support vanishes in degrees below 2(p+1), in particular in degrees 2p and 2p+1. The long exact sequence for the nested supports Z_{\mathrm{sing}}\subseteq Z then shows that restriction

H_Z^{2p}(X;\mathbb Q)\longrightarrow H_{Z_{\mathrm{reg}}}^{2p}(X\setminus Z_{\mathrm{sing}};\mathbb Q)

is an isomorphism. Its inverse extends the class of Step 1 uniquely to a class with support in all of Z.

AlgebraicGeometry.ComplexPoint.cycleComponentSingularBoundarySectionCohomology_isZero_cycleDegree (X : Over (Spec (CommRingCat.of ))) [AlgebraicGeometry.IsIntegral X.left] [Smooth X.hom] [IsProjective X.hom] (x : X.left) {d p : } [SmoothOfRelativeDimension d X.hom] (hx : coheight x = p) : IsZero ((((TopCat.Sheaf.supportEvaluation (TopCat.of (ComplexPoint X)) ).mapHomologicalComplex (ComplexShape.up )).obj (complexSupportInjectiveComplex X (cycleComponentSingularAnalyticClosedFiltration X x 0))).homology (2 * p))#check AlgebraicGeometry.ComplexPoint.cycleComponentSingularBoundarySectionCohomology_isZero_cycleDegree def cycleComponentSupportExtensionIso (X : Over (Spec )) [IsIntegral X.left] [Smooth X.hom] [IsProjective X.hom] (x : X.left) {d p : } [SmoothOfRelativeDimension d X.hom] (hx : coheight x = p) : ((((TopCat.Sheaf.supportEvaluation (TopCat.of (ComplexPoint X)) ).mapHomologicalComplex (.up )).obj (complexSupportInjectiveComplex X (cycleComponentAnalyticClosedSupport X x))).homology (2 * (p : ))) ((((TopCat.Sheaf.supportEvaluation (TopCat.of (ComplexPoint X)) (cycleComponentSmoothSupportAmbientOpen X x)).mapHomologicalComplex (.up )).obj (complexSupportInjectiveComplex X (cycleComponentAnalyticClosedSupport X x))).homology (2 * (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:Over (Spec (CommRingCat.of ))inst✝³:AlgebraicGeometry.IsIntegral X.leftinst✝²:Smooth X.hominst✝¹:IsProjective X.homx:X.leftd:p:inst✝:SmoothOfRelativeDimension d X.homhx:coheight x = p(((TopCat.Sheaf.supportEvaluation (TopCat.of (ComplexPoint X)) ).mapHomologicalComplex (ComplexShape.up )).obj (complexSupportInjectiveComplex X (cycleComponentAnalyticClosedSupport X x))).homology (2 * p) (((TopCat.Sheaf.supportEvaluation (TopCat.of (ComplexPoint X)) (cycleComponentSmoothSupportAmbientOpen X x)).mapHomologicalComplex (ComplexShape.up )).obj (complexSupportInjectiveComplex X (cycleComponentAnalyticClosedSupport X x))).homology (2 * 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:Over (Spec (CommRingCat.of ))inst✝³:AlgebraicGeometry.IsIntegral X.leftinst✝²:Smooth X.hominst✝¹:IsProjective X.homx:X.leftd:p:inst✝:SmoothOfRelativeDimension d X.homhx:coheight x = pthis:IsIso (HomologicalComplex.homologyMap (cycleComponentSupportSectionRestriction X x) (2 * p)) := ···(((TopCat.Sheaf.supportEvaluation (TopCat.of (ComplexPoint X)) ).mapHomologicalComplex (ComplexShape.up )).obj (complexSupportInjectiveComplex X (cycleComponentAnalyticClosedSupport X x))).homology (2 * p) (((TopCat.Sheaf.supportEvaluation (TopCat.of (ComplexPoint X)) (cycleComponentSmoothSupportAmbientOpen X x)).mapHomologicalComplex (ComplexShape.up )).obj (complexSupportInjectiveComplex X (cycleComponentAnalyticClosedSupport X x))).homology (2 * p) All goals completed! 🐙 def cycleComponentSupportedClassNormalizationIso (X : Over (Spec )) [IsIntegral X.left] [Smooth X.hom] [IsProjective X.hom] (x : X.left) {d p : } [SmoothOfRelativeDimension d X.hom] (hx : coheight x = p) : ((((TopCat.Sheaf.supportEvaluation (TopCat.of (ComplexPoint X)) ).mapHomologicalComplex (.up )).obj (complexSupportInjectiveComplex X (cycleComponentAnalyticClosedSupport X x))).homology (2 * (p : ))) (supportRelativeCohomologySheaf (TopCat.of (ComplexPoint X)) (cycleComponentSupport X x) (2 * p)).obj.obj (op (cycleComponentSmoothSupportAmbientOpen X 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:Over (Spec (CommRingCat.of ))inst✝³:AlgebraicGeometry.IsIntegral X.leftinst✝²:Smooth X.hominst✝¹:IsProjective X.homx:X.leftd:p:inst✝:SmoothOfRelativeDimension d X.homhx:coheight x = p(((TopCat.Sheaf.supportEvaluation (TopCat.of (ComplexPoint X)) ).mapHomologicalComplex (ComplexShape.up )).obj (complexSupportInjectiveComplex X (cycleComponentAnalyticClosedSupport X x))).homology (2 * p) (supportRelativeCohomologySheaf (TopCat.of (ComplexPoint X)) (cycleComponentSupport X x) (2 * p)).obj.obj (op (cycleComponentSmoothSupportAmbientOpen X 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:Over (Spec (CommRingCat.of ))inst✝³:AlgebraicGeometry.IsIntegral X.leftinst✝²:Smooth X.hominst✝¹:IsProjective X.homx:X.leftd:p:inst✝:SmoothOfRelativeDimension d X.homhx:coheight x = p(HomologicalComplex.homology (complexSupportInjectiveComplex X (cycleComponentAnalyticClosedSupport X x)) (2 * p)).obj.obj (op (cycleComponentSmoothSupportAmbientOpen X x)) (supportRelativeCohomologySheaf (TopCat.of (ComplexPoint X)) (cycleComponentSupport X x) (2 * p)).obj.obj (op (cycleComponentSmoothSupportAmbientOpen X 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:Over (Spec (CommRingCat.of ))inst✝³:AlgebraicGeometry.IsIntegral X.leftinst✝²:Smooth X.hominst✝¹:IsProjective X.homx:X.leftd:p:inst✝:SmoothOfRelativeDimension d X.homhx:coheight x = pe:(TopCat.Sheaf.supportEvaluation (TopCat.of (ComplexPoint X)) (cycleComponentSmoothSupportAmbientOpen X x)).obj (HomologicalComplex.homology (complexSupportInjectiveComplex X (cycleComponentAnalyticClosedSupport X x)) (2 * p)) (TopCat.Sheaf.supportEvaluation (TopCat.of (ComplexPoint X)) (cycleComponentSmoothSupportAmbientOpen X x)).obj (supportRelativeCohomologySheaf (TopCat.of (ComplexPoint X)) (↑(cycleComponentAnalyticClosedSupport X x)) (2 * p)) := (TopCat.Sheaf.supportEvaluation (TopCat.of (ComplexPoint X)) (cycleComponentSmoothSupportAmbientOpen X x)).mapIso (complexSupportInjectiveCohomologySheafIsoRelative X (cycleComponentAnalyticClosedSupport X x) (2 * p))(HomologicalComplex.homology (complexSupportInjectiveComplex X (cycleComponentAnalyticClosedSupport X x)) (2 * p)).obj.obj (op (cycleComponentSmoothSupportAmbientOpen X x)) (supportRelativeCohomologySheaf (TopCat.of (ComplexPoint X)) (cycleComponentSupport X x) (2 * p)).obj.obj (op (cycleComponentSmoothSupportAmbientOpen X 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:Over (Spec (CommRingCat.of ))inst✝³:AlgebraicGeometry.IsIntegral X.leftinst✝²:Smooth X.hominst✝¹:IsProjective X.homx:X.leftd:p:inst✝:SmoothOfRelativeDimension d X.homhx:coheight x = pe:(TopCat.Sheaf.supportEvaluation (TopCat.of (ComplexPoint X)) (cycleComponentSmoothSupportAmbientOpen X x)).obj (HomologicalComplex.homology (complexSupportInjectiveComplex X (cycleComponentAnalyticClosedSupport X x)) (2 * p)) (TopCat.Sheaf.supportEvaluation (TopCat.of (ComplexPoint X)) (cycleComponentSmoothSupportAmbientOpen X x)).obj (supportRelativeCohomologySheaf (TopCat.of (ComplexPoint X)) (↑(cycleComponentAnalyticClosedSupport X x)) (2 * p)) := (TopCat.Sheaf.supportEvaluation (TopCat.of (ComplexPoint X)) (cycleComponentSmoothSupportAmbientOpen X x)).mapIso (complexSupportInjectiveCohomologySheafIsoRelative X (cycleComponentAnalyticClosedSupport X x) (2 * p))he:(2 * p) = 2 * p(HomologicalComplex.homology (complexSupportInjectiveComplex X (cycleComponentAnalyticClosedSupport X x)) (2 * p)).obj.obj (op (cycleComponentSmoothSupportAmbientOpen X x)) (supportRelativeCohomologySheaf (TopCat.of (ComplexPoint X)) (cycleComponentSupport X x) (2 * p)).obj.obj (op (cycleComponentSmoothSupportAmbientOpen X 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:Over (Spec (CommRingCat.of ))inst✝³:AlgebraicGeometry.IsIntegral X.leftinst✝²:Smooth X.hominst✝¹:IsProjective X.homx:X.leftd:p:inst✝:SmoothOfRelativeDimension d X.homhx:coheight x = pe:(sheafToPresheaf (Opens.grothendieckTopology (ComplexPoint X)) AddCommGrpCat (evaluation (Opens (ComplexPoint X))ᵒᵖ AddCommGrpCat).obj (op (cycleComponentSmoothSupportAmbientOpen X x))).obj (HomologicalComplex.homology (complexSupportInjectiveComplex X (cycleComponentAnalyticClosedSupport X x)) (2 * p)) (sheafToPresheaf (Opens.grothendieckTopology (ComplexPoint X)) AddCommGrpCat (evaluation (Opens (ComplexPoint X))ᵒᵖ AddCommGrpCat).obj (op (cycleComponentSmoothSupportAmbientOpen X x))).obj (supportRelativeCohomologySheaf (TopCat.of (ComplexPoint X)) (↑(cycleComponentAnalyticClosedSupport X x)) (2 * p)) := (TopCat.Sheaf.supportEvaluation (TopCat.of (ComplexPoint X)) (cycleComponentSmoothSupportAmbientOpen X x)).mapIso (complexSupportInjectiveCohomologySheafIsoRelative X (cycleComponentAnalyticClosedSupport X x) (2 * p))he:(2 * p) = 2 * p(HomologicalComplex.homology (complexSupportInjectiveComplex X (cycleComponentAnalyticClosedSupport X x)) (2 * p)).obj.obj (op (cycleComponentSmoothSupportAmbientOpen X x)) (supportRelativeCohomologySheaf (TopCat.of (ComplexPoint X)) (cycleComponentSupport X x) (2 * p)).obj.obj (op (cycleComponentSmoothSupportAmbientOpen X 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:Over (Spec (CommRingCat.of ))inst✝³:AlgebraicGeometry.IsIntegral X.leftinst✝²:Smooth X.hominst✝¹:IsProjective X.homx:X.leftd:p:inst✝:SmoothOfRelativeDimension d X.homhx:coheight x = pe:(sheafToPresheaf (Opens.grothendieckTopology (ComplexPoint X)) AddCommGrpCat (evaluation (Opens (ComplexPoint X))ᵒᵖ AddCommGrpCat).obj (op (cycleComponentSmoothSupportAmbientOpen X x))).obj (HomologicalComplex.homology (complexSupportInjectiveComplex X (cycleComponentAnalyticClosedSupport X x)) (2 * p)) (sheafToPresheaf (Opens.grothendieckTopology (ComplexPoint X)) AddCommGrpCat (evaluation (Opens (ComplexPoint X))ᵒᵖ AddCommGrpCat).obj (op (cycleComponentSmoothSupportAmbientOpen X x))).obj (supportRelativeCohomologySheaf (TopCat.of (ComplexPoint X)) (↑(cycleComponentAnalyticClosedSupport X x)) (2 * p))he:(2 * p) = 2 * p(HomologicalComplex.homology (complexSupportInjectiveComplex X (cycleComponentAnalyticClosedSupport X x)) (2 * p)).obj.obj (op (cycleComponentSmoothSupportAmbientOpen X x)) (supportRelativeCohomologySheaf (TopCat.of (ComplexPoint X)) (cycleComponentSupport X x) (2 * p)).obj.obj (op (cycleComponentSmoothSupportAmbientOpen X x)) All goals completed! 🐙 AlgebraicGeometry.ComplexPoint.cycleComponentSupportedInjectiveClass_unique (X : Over (Spec (CommRingCat.of ))) [AlgebraicGeometry.IsIntegral X.left] [Smooth X.hom] [IsProjective X.hom] (x : X.left) {d p : } [SmoothOfRelativeDimension d X.hom] (hx : coheight x = p) (a : (CycleComponentSupportedCohomology X x p)) (ha : (ConcreteCategory.hom (cycleComponentSupportedClassNormalizationIso X x hx).hom) a = cycleComponentSmoothSupportCoclassSection X x hx) : a = cycleComponentSupportedInjectiveClass X x hx#check AlgebraicGeometry.ComplexPoint.cycleComponentSupportedInjectiveClass_unique

The compact interface names the supported group and the smooth-locus section group. The extension map takes any such section to its unique global supported class, using the proved isomorphism above. Applying it to the normalized smooth-locus section gives the component class.

AlgebraicGeometry.ComplexPoint.CycleComponentSupportedCohomology (X : Over (Spec (CommRingCat.of ))) [AlgebraicGeometry.IsIntegral X.left] [Smooth X.hom] [IsProjective X.hom] (x : X.left) (p : ) : AddCommGrpCat#check AlgebraicGeometry.ComplexPoint.CycleComponentSupportedCohomology AlgebraicGeometry.ComplexPoint.CycleComponentSmoothCoclassSections (X : Over (Spec (CommRingCat.of ))) [AlgebraicGeometry.IsIntegral X.left] [Smooth X.hom] [IsProjective X.hom] (x : X.left) (p : ) : AddCommGrpCat#check AlgebraicGeometry.ComplexPoint.CycleComponentSmoothCoclassSections AlgebraicGeometry.ComplexPoint.cycleComponentExtendSmoothCoclass (X : Over (Spec (CommRingCat.of ))) [AlgebraicGeometry.IsIntegral X.left] [Smooth X.hom] [IsProjective X.hom] (x : X.left) {d p : } [SmoothOfRelativeDimension d X.hom] (hx : coheight x = p) : (CycleComponentSmoothCoclassSections X x p) →+ (CycleComponentSupportedCohomology X x p)#check AlgebraicGeometry.ComplexPoint.cycleComponentExtendSmoothCoclass AlgebraicGeometry.ComplexPoint.cycleComponentExtendSmoothCoclass_normalization (X : Over (Spec (CommRingCat.of ))) [AlgebraicGeometry.IsIntegral X.left] [Smooth X.hom] [IsProjective X.hom] (x : X.left) {d p : } [SmoothOfRelativeDimension d X.hom] (hx : coheight x = p) (s : (CycleComponentSmoothCoclassSections X x p)) : (ConcreteCategory.hom (cycleComponentSupportedClassNormalizationIso X x hx).hom) ((cycleComponentExtendSmoothCoclass X x hx) s) = s#check AlgebraicGeometry.ComplexPoint.cycleComponentExtendSmoothCoclass_normalization AlgebraicGeometry.ComplexPoint.cycleComponentExtendSmoothCoclass_unique (X : Over (Spec (CommRingCat.of ))) [AlgebraicGeometry.IsIntegral X.left] [Smooth X.hom] [IsProjective X.hom] (x : X.left) {d p : } [SmoothOfRelativeDimension d X.hom] (hx : coheight x = p) (s : (CycleComponentSmoothCoclassSections X x p)) (a : (CycleComponentSupportedCohomology X x p)) (ha : (ConcreteCategory.hom (cycleComponentSupportedClassNormalizationIso X x hx).hom) a = s) : a = (cycleComponentExtendSmoothCoclass X x hx) s#check AlgebraicGeometry.ComplexPoint.cycleComponentExtendSmoothCoclass_unique example [SmoothOfRelativeDimension d X.hom] : CycleComponentSupportedCohomology X x p := cycleComponentExtendSmoothCoclass X x (d := d) hx (cycleComponentSmoothSupportCoclassSection X x (d := d) hx)

4.4. Step 3: from support to ordinary cohomology🔗

The extension is a class in the cohomology of an injective resolution with supports. Transporting it through the comparison with the mapping-cone model of the previous section gives the class of the subvariety in cohomology with support, and forgetting the support gives its class in ordinary cohomology, which is the class the statement uses.

def cycleComponentSheafSupportedClass (X : Over (Spec )) [IsIntegral X.left] [Smooth X.hom] [IsProjective X.hom] (x : X.left) {d p : } [SmoothOfRelativeDimension d X.hom] (hx : coheight x = p) : RationalCohomologyWithSupport X (cycleComponentSupport X x) (2 * (p : )) := (rationalSupportAddEquivSupportedInjectiveHomology X (cycleComponentSupport X x) (cycleComponentAnalyticClosedSupport X x).isClosed (2 * (p : ))).symm (cycleComponentSupportedInjectiveClass X x (d := d) hx) def cycleComponentSheafClass (X : Over (Spec )) [IsIntegral X.left] [Smooth X.hom] [IsProjective X.hom] (x : X.left) {d p : } [SmoothOfRelativeDimension d X.hom] (hx : coheight x = p) : H^(2 * (p : ))(X; ) := (rationalCohomologyAddEquivAmbientInjectiveHomology X (2 * (p : ))).symm (HomologicalComplex.homologyMap (TopCat.Sheaf.supportRestrictionSectionsComplexShortComplex (TopCat.of (ComplexPoint X)) (cycleComponentAnalyticClosedSupport X x).compl (ambientRationalInjectiveComplex X)).f (2 * (p : )) (cycleComponentSupportedInjectiveClass X x (d := d) hx)) AlgebraicGeometry.ComplexPoint.cycleComponentSheafClass_eq_forgetSupport (X : Over (Spec (CommRingCat.of ))) [AlgebraicGeometry.IsIntegral X.left] [Smooth X.hom] [IsProjective X.hom] (x : X.left) {d p : } [SmoothOfRelativeDimension d X.hom] (hx : coheight x = p) : cycleComponentSheafClass X x hx = (ComplexPoint.forgetSupport X (cycleComponentSupport X x) (2 * p)) (cycleComponentSheafSupportedClass X x hx)#check AlgebraicGeometry.ComplexPoint.cycleComponentSheafClass_eq_forgetSupport

Both definitions take only the variety, the generic point, its coheight, and the dimension d as arguments.

For the generic point of X itself, the support is all of X(\mathbb C), so forgetting support is an isomorphism. The nonzero normalized section therefore gives a nonzero class in H^0(X;\mathbb Q) in every dimension, without assuming analytic connectedness.

AlgebraicGeometry.ComplexPoint.cycleComponentSheafClass_genericPoint_ne_zero (X : Over (Spec (CommRingCat.of ))) [AlgebraicGeometry.IsIntegral X.left] [Smooth X.hom] [IsProjective X.hom] (d : ) [SmoothOfRelativeDimension d X.hom] : cycleComponentSheafClass X (genericPoint X.left) 0#check AlgebraicGeometry.ComplexPoint.cycleComponentSheafClass_genericPoint_ne_zero