Documentation

Atlas.GeometryOfManifolds.code.PontrjaginObstructions

Algebraic data of the intersection form of a closed oriented $4$-manifold: second Betti number $b_2 = b_2^+ + b_2^-$, signature $\sigma = b_2^+ - b_2^-$, parity, and a symmetric bilinear form on $H^2(M; \mathbb{Z}) \cong \mathbb{Z}^{b_2}$.

Instances For

    An almost-complex structure $J$ on a smooth $4$-manifold (placeholder, witnessing existence).

    • mk' :: (
      • )
      Instances For

        Topological data attached to a closed smooth $4$-manifold $M$: its intersection form Q and Euler characteristic $\chi(M) = 2 + b_2(M)$ (for simply connected $M$).

        Instances

          Chern and Pontrjagin number data for a closed $4$-manifold equipped with an almost complex structure: $c_1^2 \cdot [M]$, $c_2 \cdot [M]$, with $c_2 = \chi(M)$.

          Instances For

            First Pontrjagin number $p_1 \cdot [M] = c_1^2 - 2 c_2$, the Whitney sum relation for an almost complex $4$-manifold.

            Instances For

              The rearranged Chern–Pontrjagin relation: $c_1^2 = 2 c_2 + p_1$.

              Data of a closed oriented $4$-manifold: Pontrjagin number $p_1$, Betti numbers $b_2^\pm$, signature $\sigma$, and a symmetric intersection form on $H^2 \cong \mathbb{Z}^{b_2}$.

              Instances For

                Hirzebruch signature theorem (axiomatized): $p_1 \cdot [M] = 3 \sigma(M)$ for closed oriented $4$-manifolds.

                Hirzebruch signature theorem (Theorem 1 of the chapter): $p_1(TM) \cdot [M] = 3 \sigma(M)$.

                Build closed-oriented manifold data from Chern–Pontrjagin data plus topological data.

                Instances For

                  Bundled data for a closed oriented almost-complex $4$-manifold: the underlying topology, Euler number $\chi$, $c_1^2$, $c_2 = \chi$, and the Whitney relation $p_1 = c_1^2 - 2c_2$.

                  Instances For

                    The Chern–Pontrjagin relation $c_1^2 = 2 c_2 + p_1$ for closed almost complex $4$-manifolds.

                    Construct the bundled closed Chern–Pontrjagin data from HasChernPontrjaginData together with Mfd4Topology, assuming the simply-connected case.

                    Instances For

                      Corollary 1 (closed form): $c_1^2 \cdot [M] = 2 \chi(M) + 3 \sigma(M)$, obtained by combining the Chern–Pontrjagin relation with the Hirzebruch signature theorem.

                      Corollary 1: for a closed almost complex $4$-manifold, $c_1^2 \cdot [M] = 2 \chi(M) + 3 \sigma(M)$.

                      Generic algebraic data needed to state the almost-complex existence criterion: rank of $H^2$, Euler number $\chi$, signature $\sigma$, and a symmetric bilinear pairing modeling the intersection form $Q$.

                      Instances For

                        The square $\alpha^2 \cdot [M] = Q(\alpha, \alpha)$ evaluated via the bilinear pairing.

                        Instances For

                          Self-pairing $Q([A], [A])$ of a homology class with itself under the intersection form.

                          Instances For

                            Witness that an almost complex structure J has first Chern class with prescribed coordinates in the basis of $H^2(M; \mathbb{Z})$.

                            Instances For
                              theorem almost_complex_structure_criterion {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace (Fin 4)) M] [IsManifold (modelWithCornersSelf (EuclideanSpace (Fin 4))) M] [CompactSpace M] (obsData : AlmostComplexObstructionDataGeneral M) (α : Fin obsData.rank_H2) :
                              (∃ (J : Mfd4AlmostComplexStr M) (hc : HasFirstChernClassGeneral J obsData), hc.c₁_coords = α) obsData.square_eval α = 2 * obsData.euler + 3 * obsData.signature ∀ (A : Fin obsData.rank_H2), obsData.pairing α A % 2 = obsData.Q_selfpairing A % 2

                              Theorem 2 (almost-complex existence): there exists an almost complex structure $J$ on $M^4$ with $\alpha = c_1(TM, J)$ iff $\alpha^2 \cdot [M] = 2\chi + 3\sigma$ and $\alpha \cdot [A] \equiv Q([A], [A]) \pmod 2$ for every $[A] \in H_2(M; \mathbb{Z})$.

                              Obstruction data for an almost-complex structure, tied to the ambient Mfd4Topology: the rank of $H^2$ matches $b_2(M)$, and a symmetric pairing models the intersection form.

                              Instances For

                                Forget the link to Mfd4Topology and produce general almost-complex obstruction data.

                                Instances For

                                  Witness that an almost complex structure J has a first Chern class with the given integer coordinates in the obstruction basis.

                                  Instances For
                                    theorem not_sum_of_two_squares_14 (a b : ) :
                                    a ^ 2 + b ^ 2 14

                                    Number-theoretic lemma: $14$ is not a sum of two integer squares, used in the obstruction argument for $\mathbb{CP}^2 \# \mathbb{CP}^2$.

                                    theorem CP2_CP2_no_acs_full {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace (Fin 4)) M] [IsManifold (modelWithCornersSelf (EuclideanSpace (Fin 4))) M] [CompactSpace M] [htop : Mfd4Topology M] (_hb₂ : (Mfd4Topology.Q M).b₂ = 2) ( : (Mfd4Topology.Q M).signature = 2) ( : Mfd4Topology.euler M = 4) (hcp : HasChernPontrjaginData M) (a b : ) (hc₁_decomp : hcp.c₁_sq = a ^ 2 + b ^ 2) :

                                    Obstruction example: $\mathbb{CP}^2 \# \mathbb{CP}^2$ (with $b_2 = 2$, $\sigma = 2$, $\chi = 4$) admits no almost-complex structure, since the Chern number formula forces $c_1^2 = 14$, which cannot be written as a sum of two squares.