def SymmetricBilinearForms.MatrixCongruent {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] (M N : Matrix n n R) : Prop

Two square matrices M, N over a commutative ring are congruent if there exists an invertible matrix A such that A * M * Aᵀ = N. This is the matrix-level equivalence relation underlying isometry of bilinear forms.

def SymmetricBilinearForms.hyperbolicPlusIdentity : Matrix (Fin 3) (Fin 3) (ZMod 2)

The matrix H ⊕ ⟨1⟩ over F₂, formed by the hyperbolic plane and a rank-one form with diagonal entry 1. This is the model form used in Claim 30.7.

theorem SymmetricBilinearForms.hyperbolicPlusIdentity_matrixCongruent_one : MatrixCongruent hyperbolicPlusIdentity 1

Claim 30.7: the form H ⊕ ⟨1⟩ is congruent over F₂ to the identity form ⟨1⟩ ⊕ ⟨1⟩ ⊕ ⟨1⟩.

class AlgebraicTopologyI.IsTopologicalManifold (M : Type u_1) [TopologicalSpace M] : Prop

Definition 30.1: a topological manifold is a Hausdorff space that is locally homeomorphic to some Euclidean space at every point (the dimension may a priori depend on the point).

• hausdorff : T2Space M
• locally_euclidean (x : M) : ∃ (n : ℕ) (U : Set M), IsOpen U ∧ x ∈ U ∧ Nonempty (↑U ≃ₜ EuclideanSpace ℝ (Fin n))

class AlgebraicTopologyI.TopologicalManifold (n : ℕ) (M : Type u_1) [TopologicalSpace M] extends ChartedSpace (EuclideanSpace ℝ (Fin n)) M : Type u_1

A topological n-manifold: a Hausdorff space equipped with a charted space structure modelled on ℝⁿ. This is the dimension-fixed variant of IsTopologicalManifold.

• atlas : Set (OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n)))
• chartAt : M → OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))
• mem_chart_source (x : M) : x ∈ (ChartedSpace.chartAt x).source
• chart_mem_atlas (x : M) : ChartedSpace.chartAt x ∈ ChartedSpace.atlas
• hausdorff : T2Space M

@[implicit_reducible, instance 100]

instance AlgebraicTopologyI.instTopologicalManifold (n : ℕ) (M : Type u_1) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [T2Space M] : TopologicalManifold n M

A Hausdorff charted space modelled on ℝⁿ automatically gets the TopologicalManifold n instance.

@[reducible, inline]

abbrev SingularCohomology.CohomZMod2 (X : TopCat) (n : ℕ) : Type

Singular cohomology with coefficients in F₂ = ZMod 2, as a type.

@[reducible, inline]

abbrev HomolZMod2 (X : TopCat) (n : ℕ) : Type

Singular homology with coefficients in F₂ = ZMod 2, as a type.

noncomputable def cupProductPairing (X : TopCat) (dim : ℕ) (μ : HomolZMod2 X dim) (p q : ℕ) (hpq : p + q = dim) : SingularCohomology.CohomZMod2 X p →ₗ[ZMod 2] SingularCohomology.CohomZMod2 X q →ₗ[ZMod 2] ZMod 2

The pairing H^p(X; F₂) × H^q(X; F₂) → F₂ induced by cup product with a fixed homology class μ ∈ H_dim(X; F₂), given by (α, β) ↦ ⟨α ⌣ β, μ⟩. Used to formulate Poincaré duality.

theorem poincareDuality_F2 (dim : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin dim)) M] [T2Space M] [CompactSpace M] : ∃! μ : HomolZMod2 (TopCat.of M) dim, ∀ (p q : ℕ) (hpq : p + q = dim), (cupProductPairing (TopCat.of M) dim μ p q hpq).IsPerfPair

Theorem 30.2 (F₂-Poincaré duality). On a closed (compact, Hausdorff) topological dim-manifold there exists a unique fundamental class μ ∈ H_dim(M; F₂) such that, for every p + q = dim, the cup-product pairing H^p(M; F₂) × H^q(M; F₂) → F₂ is a perfect pairing.

structure SurfacesAndBilinearForms.CompactSurface : Type 1

A compact surface: a compact, connected, Hausdorff topological space with a charted-space structure on ℝ² that makes it a C⁰ manifold. This is the geometric setting for the classification of surfaces.

• toTopCat : TopCat
• compact : CompactSpace ↑self.toTopCat
• connected : ConnectedSpace ↑self.toTopCat
• t2 : T2Space ↑self.toTopCat
• charted : ChartedSpace (EuclideanSpace ℝ (Fin 2)) ↑self.toTopCat
• isManifold : IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 2))) 0 ↑self.toTopCat

@[implicit_reducible]

instance SurfacesAndBilinearForms.instCoeSortCompactSurfaceTopCat : CoeSort CompactSurface TopCat

Coerce a CompactSurface to its underlying TopCat object.

instance SurfacesAndBilinearForms.instIsManifoldRealEuclideanSpaceFinOfNatNatModelWithCornersSelfWithTopENatCarrierToTopCat (S : CompactSurface) : IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 2))) 0 ↑S.toTopCat

Make the C⁰-manifold structure of a CompactSurface available automatically through typeclass inference.

noncomputable def SurfacesAndBilinearForms.connectedSumTopCat (S₁ S₂ : CompactSurface) : TopCat

The underlying topological space of the connected sum S₁ ♯ S₂ of two compact surfaces: remove an open disk from each surface and glue along the resulting boundary circles.

theorem SurfacesAndBilinearForms.connectedSum_compact (S₁ S₂ : CompactSurface) : CompactSpace ↑(connectedSumTopCat S₁ S₂)

The connected sum of two compact surfaces is compact.

theorem SurfacesAndBilinearForms.connectedSum_connected (S₁ S₂ : CompactSurface) : ConnectedSpace ↑(connectedSumTopCat S₁ S₂)

The connected sum of two compact surfaces is connected.

theorem SurfacesAndBilinearForms.connectedSum_t2 (S₁ S₂ : CompactSurface) : T2Space ↑(connectedSumTopCat S₁ S₂)

The connected sum of two compact surfaces is Hausdorff.

noncomputable def SurfacesAndBilinearForms.connectedSum_charted (S₁ S₂ : CompactSurface) : ChartedSpace (EuclideanSpace ℝ (Fin 2)) ↑(connectedSumTopCat S₁ S₂)

A charted space structure on the connected sum modelled on ℝ².

noncomputable def SurfacesAndBilinearForms.connectedSum (S₁ S₂ : CompactSurface) : CompactSurface

The connected sum S₁ ♯ S₂ of two compact surfaces, packaged as a CompactSurface.

def SurfacesAndBilinearForms.«term_♯_» : Lean.TrailingParserDescr

noncomputable def SurfacesAndBilinearForms.CompactSurface.fundamentalClass (S : CompactSurface) : HomolZMod2 S.toTopCat 2

The fundamental class [S] ∈ H_2(S; F₂) of a compact surface, provided by F₂-Poincaré duality.

noncomputable def SurfacesAndBilinearForms.intersectionForm (S : CompactSurface) : LinearMap.BilinForm (ZMod 2) (SingularCohomology.CohomZMod2 S.toTopCat 1)

The intersection form on H¹(S; F₂) of a compact surface S: the symmetric bilinear form (α, β) ↦ ⟨α ⌣ β, [S]⟩.

def SurfacesAndBilinearForms.orthogonalDirectSumForm {V₁ V₂ : Type} [AddCommGroup V₁] [Module (ZMod 2) V₁] [AddCommGroup V₂] [Module (ZMod 2) V₂] (B₁ : LinearMap.BilinForm (ZMod 2) V₁) (B₂ : LinearMap.BilinForm (ZMod 2) V₂) : LinearMap.BilinForm (ZMod 2) (V₁ × V₂)

The orthogonal direct sum B₁ ⊥ B₂ of two F₂-bilinear forms on the product space V₁ × V₂, defined by ((x₁, x₂), (y₁, y₂)) ↦ B₁(x₁, y₁) + B₂(x₂, y₂).

noncomputable def SurfacesAndBilinearForms.puncturedSurface (S : CompactSurface) : TopCat

The punctured surface S ∖ B: remove a small open disk from S using a chart centred at an arbitrary point.

def SurfacesAndBilinearForms.puncturedSurfaceInclusion (S : CompactSurface) : puncturedSurface S ⟶ S.toTopCat

The continuous inclusion S ∖ B ↪ S of the punctured surface into the original surface.

theorem SurfacesAndBilinearForms.puncturedSurfaceInclusion_H1_isIso (S : CompactSurface) : CategoryTheory.IsIso (SingularCohomology.singularCohomologyMap (ZMod 2) (puncturedSurfaceInclusion S) 1)

The inclusion of the punctured surface into the surface induces an isomorphism on H¹(–; F₂) (removing an open disk does not change H¹).

noncomputable def SurfacesAndBilinearForms.puncturedSurfaceInclusion_H1_iso (S : CompactSurface) : SingularCohomology.singularCohomology (ZMod 2) S.toTopCat (ModuleCat.of (ZMod 2) (ZMod 2)) 1 ≅ SingularCohomology.singularCohomology (ZMod 2) (puncturedSurface S) (ModuleCat.of (ZMod 2) (ZMod 2)) 1

Package puncturedSurfaceInclusion_H1_isIso as a categorical isomorphism H¹(S; F₂) ≅ H¹(S ∖ B; F₂).

noncomputable def SurfacesAndBilinearForms.puncturedSurface_H1_iso (S : CompactSurface) : SingularCohomology.CohomZMod2 (puncturedSurface S) 1 ≃ₗ[ZMod 2] SingularCohomology.CohomZMod2 S.toTopCat 1

The induced linear isomorphism H¹(S ∖ B; F₂) ≃ₗ H¹(S; F₂).

noncomputable def SurfacesAndBilinearForms.puncturedSurfaceInclusionConnectedSum₁ (S₁ S₂ : CompactSurface) : puncturedSurface S₁ ⟶ (connectedSum S₁ S₂).toTopCat

Inclusion of the first punctured factor S₁ ∖ B₁ into the connected sum S₁ ♯ S₂.

noncomputable def SurfacesAndBilinearForms.puncturedSurfaceInclusionConnectedSum₂ (S₁ S₂ : CompactSurface) : puncturedSurface S₂ ⟶ (connectedSum S₁ S₂).toTopCat

Inclusion of the second punctured factor S₂ ∖ B₂ into the connected sum S₁ ♯ S₂.

noncomputable def SurfacesAndBilinearForms.connectedSum_mv_restrictionMap (S₁ S₂ : CompactSurface) : SingularCohomology.CohomZMod2 (connectedSum S₁ S₂).toTopCat 1 →ₗ[ZMod 2] SingularCohomology.CohomZMod2 (puncturedSurface S₁) 1 × SingularCohomology.CohomZMod2 (puncturedSurface S₂) 1

Mayer–Vietoris restriction map on H¹ for the connected sum: send a cohomology class to its pair of restrictions to the two punctured factors.

noncomputable def SurfacesAndBilinearForms.connectedSum_mv_connectingHomomorphism₀ (S₁ S₂ : CompactSurface) : ZMod 2 →ₗ[ZMod 2] SingularCohomology.CohomZMod2 (connectedSum S₁ S₂).toTopCat 1

The Mayer–Vietoris connecting homomorphism in degree zero, H⁰(S¹; F₂) ≅ F₂ → H¹(S₁ ♯ S₂; F₂).

theorem SurfacesAndBilinearForms.connectedSum_mv_exact_at_H1 (S₁ S₂ : CompactSurface) : Function.Exact ⇑(connectedSum_mv_connectingHomomorphism₀ S₁ S₂) ⇑(connectedSum_mv_restrictionMap S₁ S₂)

Exactness of the Mayer–Vietoris sequence at the H¹(S₁ ♯ S₂) spot: the image of the connecting homomorphism δ⁰ equals the kernel of the restriction map.

def SurfacesAndBilinearForms.connectedSum_mv_restrictionMap₀ (_S₁ _S₂ : CompactSurface) : ZMod 2 × ZMod 2 →ₗ[ZMod 2] ZMod 2

The Mayer–Vietoris restriction map in degree zero, which on F₂ × F₂ → F₂ simply adds the two components.

theorem SurfacesAndBilinearForms.connectedSum_mv_exact_at_H0 (S₁ S₂ : CompactSurface) : Function.Exact ⇑(connectedSum_mv_restrictionMap₀ S₁ S₂) ⇑(connectedSum_mv_connectingHomomorphism₀ S₁ S₂)

Exactness at the H⁰(S¹; F₂) spot of the Mayer–Vietoris sequence: the image of H⁰(S₁∖B) ⊕ H⁰(S₂∖B) → H⁰(S¹) equals the kernel of δ⁰.

theorem SurfacesAndBilinearForms.connectedSum_mv_restrictionMap₀_surjective (S₁ S₂ : CompactSurface) : Function.Surjective ⇑(connectedSum_mv_restrictionMap₀ S₁ S₂)

The degree-zero restriction map F₂ × F₂ → F₂ (addition) is surjective.

theorem SurfacesAndBilinearForms.connectedSum_mv_connectingHomomorphism₀_eq_zero (S₁ S₂ : CompactSurface) : connectedSum_mv_connectingHomomorphism₀ S₁ S₂ = 0

Since the preceding restriction map is surjective, the connecting homomorphism δ⁰ : H⁰(S¹) → H¹(S₁ ♯ S₂) is the zero map.

theorem SurfacesAndBilinearForms.connectedSum_mv_restrictionMap_injective (S₁ S₂ : CompactSurface) : Function.Injective ⇑(connectedSum_mv_restrictionMap S₁ S₂)

Because δ⁰ = 0, exactness at H¹(S₁ ♯ S₂) forces the restriction map to be injective.

noncomputable def SurfacesAndBilinearForms.connectedSum_mv_gammaMap (S₁ S₂ : CompactSurface) : SingularCohomology.CohomZMod2 (puncturedSurface S₁) 1 × SingularCohomology.CohomZMod2 (puncturedSurface S₂) 1 →ₗ[ZMod 2] SingularCohomology.CohomZMod2 (TopCat.of ↑(Metric.sphere 0 1)) 1

The Mayer–Vietoris map H¹(S₁∖B) × H¹(S₂∖B) → H¹(S¹) given by restricting to the boundary circle S¹.

theorem SurfacesAndBilinearForms.connectedSum_mv_exact_at_prod (S₁ S₂ : CompactSurface) (b : SingularCohomology.CohomZMod2 (puncturedSurface S₁) 1 × SingularCohomology.CohomZMod2 (puncturedSurface S₂) 1) : (connectedSum_mv_gammaMap S₁ S₂) b = 0 ↔ b ∈ (connectedSum_mv_restrictionMap S₁ S₂).range

Exactness at the H¹(S₁∖B) × H¹(S₂∖B) spot of the Mayer–Vietoris sequence: an element of the product is in the image of the restriction map iff it is annihilated by the boundary-restriction map.

noncomputable def SurfacesAndBilinearForms.connectedSum_mv_connectingHomomorphism₁ (S₁ S₂ : CompactSurface) : SingularCohomology.CohomZMod2 (TopCat.of ↑(Metric.sphere 0 1)) 1 →ₗ[ZMod 2] SingularCohomology.CohomZMod2 (connectedSum S₁ S₂).toTopCat 2

The Mayer–Vietoris connecting homomorphism in degree one, H¹(S¹; F₂) → H²(S₁ ♯ S₂; F₂).

theorem SurfacesAndBilinearForms.connectedSum_mv_exact_at_circle (S₁ S₂ : CompactSurface) : Function.Exact ⇑(connectedSum_mv_gammaMap S₁ S₂) ⇑(connectedSum_mv_connectingHomomorphism₁ S₁ S₂)

Exactness of the Mayer–Vietoris sequence at the H¹(S¹; F₂) spot: the image of γ equals the kernel of δ¹.

theorem SurfacesAndBilinearForms.connectedSum_mv_connectingHomomorphism₁_injective (S₁ S₂ : CompactSurface) : Function.Injective ⇑(connectedSum_mv_connectingHomomorphism₁ S₁ S₂)

The degree-one connecting homomorphism δ¹ : H¹(S¹) → H²(S₁ ♯ S₂) is injective (it is the dual to the inclusion of the fundamental class).

theorem SurfacesAndBilinearForms.connectedSum_mv_gammaMap_eq_zero (S₁ S₂ : CompactSurface) : connectedSum_mv_gammaMap S₁ S₂ = 0

Since δ¹ is injective, exactness at H¹(S¹) forces the boundary-restriction map γ to vanish identically.

theorem SurfacesAndBilinearForms.connectedSum_mv_restrictionMap_surjective (S₁ S₂ : CompactSurface) : Function.Surjective ⇑(connectedSum_mv_restrictionMap S₁ S₂)

Since γ = 0, exactness at the product term implies the restriction map H¹(S₁ ♯ S₂) → H¹(S₁∖B) × H¹(S₂∖B) is surjective.

theorem SurfacesAndBilinearForms.connectedSum_mv_restrictionMap_bijective (S₁ S₂ : CompactSurface) : Function.Bijective ⇑(connectedSum_mv_restrictionMap S₁ S₂)

Combine injectivity and surjectivity: the restriction map is bijective.

noncomputable def SurfacesAndBilinearForms.mayerVietoris_connectedSum_punctured_iso (S₁ S₂ : CompactSurface) : SingularCohomology.CohomZMod2 (connectedSum S₁ S₂).toTopCat 1 ≃ₗ[ZMod 2] SingularCohomology.CohomZMod2 (puncturedSurface S₁) 1 × SingularCohomology.CohomZMod2 (puncturedSurface S₂) 1

Mayer–Vietoris isomorphism (punctured version): H¹(S₁ ♯ S₂; F₂) ≃ H¹(S₁∖B; F₂) × H¹(S₂∖B; F₂).

noncomputable def SurfacesAndBilinearForms.mayerVietoris_connectedSum_H1_iso (S₁ S₂ : CompactSurface) : SingularCohomology.CohomZMod2 (connectedSum S₁ S₂).toTopCat 1 ≃ₗ[ZMod 2] SingularCohomology.CohomZMod2 S₁.toTopCat 1 × SingularCohomology.CohomZMod2 S₂.toTopCat 1

Proposition 30.8: the Mayer–Vietoris isomorphism H¹(S₁ ♯ S₂; F₂) ≃ H¹(S₁; F₂) × H¹(S₂; F₂), obtained by combining the punctured-surface isomorphism with the isomorphisms H¹(Sᵢ∖B; F₂) ≃ H¹(Sᵢ; F₂).

theorem SurfacesAndBilinearForms.mayerVietoris_connectedSum_H1_intersectionForm_compat (S₁ S₂ : CompactSurface) (x y : SingularCohomology.CohomZMod2 (connectedSum S₁ S₂).toTopCat 1) : ((intersectionForm (connectedSum S₁ S₂)) x) y = ((intersectionForm S₁) ((puncturedSurface_H1_iso S₁) ((mayerVietoris_connectedSum_punctured_iso S₁ S₂) x).1)) ((puncturedSurface_H1_iso S₁) ((mayerVietoris_connectedSum_punctured_iso S₁ S₂) y).1) + ((intersectionForm S₂) ((puncturedSurface_H1_iso S₂) ((mayerVietoris_connectedSum_punctured_iso S₁ S₂) x).2)) ((puncturedSurface_H1_iso S₂) ((mayerVietoris_connectedSum_punctured_iso S₁ S₂) y).2)

Compatibility of the intersection form with the Mayer–Vietoris decomposition: the intersection form on S₁ ♯ S₂ decomposes as the sum of the pulled-back intersection forms on S₁ and S₂.

theorem SurfacesAndBilinearForms.mayerVietoris_connectedSum_H1_orthogonal (S₁ S₂ : CompactSurface) (x y : SingularCohomology.CohomZMod2 (connectedSum S₁ S₂).toTopCat 1) : ((intersectionForm (connectedSum S₁ S₂)) x) y = ((orthogonalDirectSumForm (intersectionForm S₁) (intersectionForm S₂)) ((mayerVietoris_connectedSum_H1_iso S₁ S₂) x)) ((mayerVietoris_connectedSum_H1_iso S₁ S₂) y)

Under the Mayer–Vietoris isomorphism, the intersection form of S₁ ♯ S₂ is the orthogonal direct sum of the intersection forms of S₁ and S₂.

theorem SurfacesAndBilinearForms.cohomology_connectedSum_iso (S₁ S₂ : CompactSurface) : ∃ (φ : SingularCohomology.CohomZMod2 (connectedSum S₁ S₂).toTopCat 1 ≃ₗ[ZMod 2] SingularCohomology.CohomZMod2 S₁.toTopCat 1 × SingularCohomology.CohomZMod2 S₂.toTopCat 1), ∀ (x y : SingularCohomology.CohomZMod2 (connectedSum S₁ S₂).toTopCat 1), ((intersectionForm (connectedSum S₁ S₂)) x) y = ((orthogonalDirectSumForm (intersectionForm S₁) (intersectionForm S₂)) (φ x)) (φ y)

Existential form of Proposition 30.8: there exists a linear isomorphism H¹(S₁ ♯ S₂; F₂) ≃ H¹(S₁; F₂) × H¹(S₂; F₂) under which the intersection form of S₁ ♯ S₂ equals the orthogonal direct sum of those of S₁, S₂.

def SurfacesAndBilinearForms.CompactSurface.Homeomorphic (S₁ S₂ : CompactSurface) : Prop

Two compact surfaces are homeomorphic if there exists a homeomorphism between their underlying topological spaces.

def SurfacesAndBilinearForms.SurfaceClass : Type 1

The set of homeomorphism classes of compact surfaces, as a quotient of CompactSurface by the homeomorphism relation.

def SurfacesAndBilinearForms.SurfaceClass.mk : CompactSurface → SurfaceClass

The canonical map sending a compact surface to its homeomorphism class.

@[implicit_reducible]

noncomputable instance SurfacesAndBilinearForms.SurfaceClass.instAddCommMonoid : AddCommMonoid SurfaceClass

The connected sum endows the set of homeomorphism classes of compact surfaces with the structure of a commutative monoid.

structure SurfacesAndBilinearForms.NondegenSymmBilinFormF2 : Type 1

A nondegenerate symmetric bilinear form over F₂ packaged with its underlying finite-dimensional F₂-vector space.

• V : Type
• instAddCommGroup : AddCommGroup self.V
• instModule : Module (ZMod 2) self.V
• instFiniteDimensional : FiniteDimensional (ZMod 2) self.V
• form : LinearMap.BilinForm (ZMod 2) self.V
• isSymm : self.form.IsSymm
• isNondeg : self.form.Nondegenerate

def SurfacesAndBilinearForms.NondegenSymmBilinFormF2.Isometric (B₁ B₂ : NondegenSymmBilinFormF2) : Prop

Two nondegenerate symmetric bilinear forms over F₂ are isometric if there is a linear isomorphism of the underlying vector spaces that takes one form to the other.

def SurfacesAndBilinearForms.BilinFormClass : Type 1

The set of isometry classes of nondegenerate symmetric bilinear forms over F₂.

@[implicit_reducible]

noncomputable instance SurfacesAndBilinearForms.BilinFormClass.instAddCommMonoid : AddCommMonoid BilinFormClass

The orthogonal direct sum endows the set of isometry classes of nondegenerate symmetric F₂-bilinear forms with the structure of a commutative monoid.

def SurfacesAndBilinearForms.BilinFormClass.mk : NondegenSymmBilinFormF2 → BilinFormClass

The canonical map sending a nondegenerate symmetric F₂-bilinear form to its isometry class.

theorem SurfacesAndBilinearForms.intersectionForm_isSymm (S : CompactSurface) : (intersectionForm S).IsSymm

The intersection form on H¹(S; F₂) of a compact surface is symmetric (over characteristic 2 the cup product is graded-commutative without sign).

theorem SurfacesAndBilinearForms.intersectionForm_nondegenerate (S : CompactSurface) : (intersectionForm S).Nondegenerate

The intersection form on H¹(S; F₂) of a compact surface is nondegenerate, as a consequence of Poincaré duality.

theorem SurfacesAndBilinearForms.cohomH1_finiteDimensional (S : CompactSurface) : FiniteDimensional (ZMod 2) (SingularCohomology.CohomZMod2 S.toTopCat 1)

The first F₂-cohomology of a compact surface is finite-dimensional.

noncomputable def SurfacesAndBilinearForms.CompactSurface.intersectionFormF2 (S : CompactSurface) : NondegenSymmBilinFormF2

Package the intersection form of a compact surface as a nondegenerate symmetric F₂-bilinear form (on the finite-dimensional space H¹(S; F₂)).

noncomputable def SurfacesAndBilinearForms.intersectionFormMap_surface : CompactSurface → BilinFormClass

The map sending a compact surface to the isometry class of its intersection form.

theorem SurfacesAndBilinearForms.intersectionFormMap_respects_homeomorphism (S₁ S₂ : CompactSurface) (h : S₁.Homeomorphic S₂) : intersectionFormMap_surface S₁ = intersectionFormMap_surface S₂

Homeomorphic compact surfaces have isometric intersection forms, so the map descends to a function on surface classes.

noncomputable def SurfacesAndBilinearForms.intersectionFormClassMap : SurfaceClass → BilinFormClass

The induced map on homeomorphism classes of surfaces: send a class [S] to the isometry class of its intersection form on H¹(S; F₂).

noncomputable def SurfacesAndBilinearForms.intersectionForm_isomorphism : SurfaceClass ≃+ BilinFormClass

Theorem 30.9: the intersection form yields a monoid isomorphism between the monoid of homeomorphism classes of compact surfaces (under connected sum) and the monoid of isometry classes of nondegenerate symmetric F₂-bilinear forms (under orthogonal direct sum).

theorem BilinearForm.restrict_nondegenerate_iff_disjoint_orthogonal {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : LinearMap.BilinForm K V) (hB_refl : B.IsRefl) (W : Submodule K V) : (B.restrict W).Nondegenerate ↔ Disjoint W (B.orthogonal W)

For a reflexive bilinear form B, the restriction B|_W is nondegenerate iff W and its orthogonal complement intersect only at zero.

theorem BilinearForm.restrict_orthogonal_nondegenerate {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (hB_refl : B.IsRefl) {W : Submodule K V} (hW : (B.restrict W).Nondegenerate) : (B.restrict (B.orthogonal W)).Nondegenerate

If B is nondegenerate and reflexive and B|_W is nondegenerate, then the restriction of B to the orthogonal complement W^⊥ is also nondegenerate.

noncomputable def BilinearForm.orthogonalProdEquiv {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : LinearMap.BilinForm K V) (hB_refl : B.IsRefl) {W : Submodule K V} (hW : (B.restrict W).Nondegenerate) : (↥W × ↥(B.orthogonal W)) ≃ₗ[K] V

When B|_W is nondegenerate, V decomposes as the internal direct sum W ⊕ W^⊥, giving a linear equivalence W × W^⊥ ≃ₗ V.

theorem BilinearForm.orthogonalProdEquiv_respects_form {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : LinearMap.BilinForm K V) (hB_refl : B.IsRefl) {W : Submodule K V} (hW : (B.restrict W).Nondegenerate) (x y : ↥W × ↥(B.orthogonal W)) : (B ((orthogonalProdEquiv B hB_refl hW) x)) ((orthogonalProdEquiv B hB_refl hW) y) = (B ↑x.1) ↑y.1 + (B ↑x.2) ↑y.2

Under the direct-sum decomposition V ≃ W × W^⊥, the form B becomes the orthogonal direct sum of B|_W and B|_{W^⊥}; the cross terms vanish because they lie in the orthogonal complement.

theorem BilinearForm.restrict_nondegenerate_characterization {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (hB_refl : B.IsRefl) (W : Submodule K V) : ((B.restrict W).Nondegenerate ↔ Disjoint W (B.orthogonal W)) ∧ ((B.restrict W).Nondegenerate → (B.restrict (B.orthogonal W)).Nondegenerate) ∧ ((B.restrict W).Nondegenerate → ∃ (e : (↥W × ↥(B.orthogonal W)) ≃ₗ[K] V), ∀ (x y : ↥W × ↥(B.orthogonal W)), (B (e x)) (e y) = (B ↑x.1) ↑y.1 + (B ↑x.2) ↑y.2)

Lemma 30.5 (packaged form): a triple characterisation of nondegeneracy of the restriction B|_W of a nondegenerate reflexive bilinear form, combining the disjointness criterion, the nondegeneracy of the restriction to the orthogonal complement, and the orthogonal-direct-sum decomposition of V together with the corresponding factorisation of B.