structure HopfSurfaceData : Type (max (u_1 + 1) (u_2 + 1))

Data witnessing the Hopf surface: a compact complex manifold with $H^2$ trivial and which admits no symplectic structure.

• Ω : ℕ → Type u_1
• VF : Type u_2
• inst : DifferentialFormSpace self.Ω self.VF
• J : AlmostComplexStr
• nij : NijenhuisTensor self.J
• integrable : IsIntegrable self.J self.nij
• h2_trivial (ω : self.Ω 2) : DifferentialFormSpace.d self.VF ω = 0 → ∃ (β : self.Ω 1), DifferentialFormSpace.d self.VF β = ω
• not_symplectic : ¬Nonempty (SymplecticManifold self.Ω self.VF)

structure S4Data : Type (max (u_1 + 1) (u_2 + 1))

Data witnessing the $4$-sphere $S^4$: a compact manifold which admits no symplectic structure (every closed $2$-form is exact, so $\omega^2$ cannot be a volume form).

• Ω : ℕ → Type u_1
• VF : Type u_2
• inst : DifferentialFormSpace self.Ω self.VF
• compact : IsCompactSymplectic self.Ω self.VF
• h2_trivial (α : self.Ω 2) : DifferentialFormSpace.d self.VF α = 0 → ∃ (β : self.Ω 1), α = DifferentialFormSpace.d self.VF β

structure KTGamma : Type

The fundamental group $\Gamma$ of the Kodaira–Thurston manifold, presented as quadruples $(a,b,c,d) \in \mathbb{Z}^4$ with a twisted multiplication.

• a : ℤ
• b : ℤ
• c : ℤ
• d : ℤ

def instDecidableEqKTGamma.decEq (x✝ x✝¹ : KTGamma) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance instDecidableEqKTGamma : DecidableEq KTGamma

def KTGamma.mul' (g h : KTGamma) : KTGamma

Twisted group multiplication on KTGamma: $(a,b,c,d)(a',b',c',d') = (a+a',\,b+b',\,c+c'+bd',\,d+d')$.

def KTGamma.one' : KTGamma

Identity element of KTGamma.

def KTGamma.inv' (g : KTGamma) : KTGamma

Group inverse in KTGamma.

theorem KTGamma.ext {g h : KTGamma} (ha : g.a = h.a) (hb : g.b = h.b) (hc : g.c = h.c) (hd : g.d = h.d) : g = h

Extensionality for KTGamma: two elements are equal iff all four components agree.

theorem KTGamma.ext_iff {g h : KTGamma} : g = h ↔ g.a = h.a ∧ g.b = h.b ∧ g.c = h.c ∧ g.d = h.d

@[implicit_reducible]

instance KTGamma.instGroup : Group KTGamma

@[simp]

theorem KTGamma.mul_def (g h : KTGamma) : g * h = g.mul' h

Unfold the Group multiplication on KTGamma to mul'.

@[simp]

theorem KTGamma.one_def : 1 = one'

Unfold the identity of KTGamma to one'.

@[simp]

theorem KTGamma.inv_def (g : KTGamma) : g⁻¹ = g.inv'

Unfold the inverse of KTGamma to inv'.

def KTGamma.generator3 : KTGamma

The "third generator" $(0,0,1,0) \in \Gamma$, which lies in the commutator subgroup.

theorem KTGamma.generator3_eq_commutator : generator3 = { a := 0, b := 1, c := 0, d := 0 } * { a := 0, b := 0, c := 0, d := 1 } * { a := 0, b := 1, c := 0, d := 0 }⁻¹ * { a := 0, b := 0, c := 0, d := 1 }⁻¹

generator3 equals the commutator $[(0,1,0,0), (0,0,0,1)]$ in $\Gamma$.

theorem KTGamma.of_generator3_eq_one : Abelianization.of generator3 = 1

In the abelianization $\Gamma^{\mathrm{ab}}$, the image of generator3 is trivial.

theorem KTGamma.of_c_component_trivial (c : ℤ) : Abelianization.of { a := 0, b := 0, c := c, d := 0 } = 1

The $c$-component of $\Gamma$ is killed in the abelianization for every $c \in \mathbb{Z}$.

theorem KTGamma.of_eq_of_drop_c (a b c d : ℤ) : Abelianization.of { a := a, b := b, c := c, d := d } = Abelianization.of { a := a, b := b, c := 0, d := d }

In $\Gamma^{\mathrm{ab}}$, the class of $(a,b,c,d)$ equals that of $(a,b,0,d)$.

def KTGamma.projHom : KTGamma →* Multiplicative ℤ × Multiplicative ℤ × Multiplicative ℤ

The projection homomorphism $\Gamma \to \mathbb{Z}^3$ sending $(a,b,c,d) \mapsto (a,b,d)$.

def KTGamma.liftedProj : Abelianization KTGamma →* Multiplicative ℤ × Multiplicative ℤ × Multiplicative ℤ

The induced homomorphism $\Gamma^{\mathrm{ab}} \to \mathbb{Z}^3$ from projHom.

def KTGamma.sectionHom : Multiplicative ℤ × Multiplicative ℤ × Multiplicative ℤ →* Abelianization KTGamma

A section $\mathbb{Z}^3 \to \Gamma^{\mathrm{ab}}$ of liftedProj, sending $(x,y,z)$ to the class of $(x,y,0,z)$.

theorem KTGamma.liftedProj_sectionHom : liftedProj.comp sectionHom = MonoidHom.id (Multiplicative ℤ × Multiplicative ℤ × Multiplicative ℤ)

The composite $\mathbb{Z}^3 \xrightarrow{\mathrm{sec}} \Gamma^{\mathrm{ab}} \xrightarrow{\mathrm{proj}} \mathbb{Z}^3$ is the identity.

theorem KTGamma.sectionHom_liftedProj : sectionHom.comp liftedProj = MonoidHom.id (Abelianization KTGamma)

The composite $\Gamma^{\mathrm{ab}} \xrightarrow{\mathrm{proj}} \mathbb{Z}^3 \xrightarrow{\mathrm{sec}} \Gamma^{\mathrm{ab}}$ is the identity.

noncomputable def KTGamma.abelianizationEquiv : Abelianization KTGamma ≃* Multiplicative ℤ × Multiplicative ℤ × Multiplicative ℤ

The abelianization of the Kodaira–Thurston fundamental group is $\Gamma^{\mathrm{ab}} \cong \mathbb{Z}^3$.

class FreeAbelianRank (G : Type u_1) [CommGroup G] : Type

Typeclass recording the rank of a free abelian group $G$.

• rank : ℕ

@[implicit_reducible]

instance freeAbelianRank_Z : FreeAbelianRank (Multiplicative ℤ)

The free abelian group $\mathbb{Z}$ has rank $1$.

@[implicit_reducible]

instance freeAbelianRank_prod {A : Type u_1} {B : Type u_2} [CommGroup A] [CommGroup B] [FreeAbelianRank A] [FreeAbelianRank B] : FreeAbelianRank (A × B)

The rank of a product of free abelian groups is the sum of the ranks.

theorem freeAbelianRank_Z3 : FreeAbelianRank.rank (Multiplicative ℤ × Multiplicative ℤ × Multiplicative ℤ) = 3

The free abelian group $\mathbb{Z}^3$ has rank $3$.

def KTGamma.abelianizationFreeRank : ℕ

The free rank of the abelianization $\Gamma^{\mathrm{ab}}$ of the Kodaira–Thurston group.

theorem KTGamma.abelianizationFreeRank_eq_three : abelianizationFreeRank = 3

Lemma 1: $H_1(M, \mathbb{Z}) \cong \mathbb{Z}^3$ for the Kodaira–Thurston manifold; equivalently $\Gamma^{\mathrm{ab}}$ has free rank $3$.

structure KodairaThurstonManifold : Type (max (u_1 + 1) (u_2 + 1))

Data of the Kodaira–Thurston manifold: a compact symplectic $4$-manifold with $b_1 = 3$ (odd), hence not Kähler.

• Ω : ℕ → Type u_1
• VF : Type u_2
• inst : DifferentialFormSpace self.Ω self.VF
• compact : IsCompactSymplectic self.Ω self.VF
• bracket : HasLieBracket self.Ω self.VF
• symplectic : SymplecticManifold self.Ω self.VF
• J : AlmostComplexStr
• hodge : HasHodgeNumbers
• betti_one_eq_three : HasHodgeNumbers.betti self.Ω self.VF 1 = 3

theorem kodaira_thurston_first_betti (M : KodairaThurstonManifold) : HasHodgeNumbers.betti M.Ω M.VF 1 = 3

The first Betti number of the Kodaira–Thurston manifold is $b_1(M) = 3$.

theorem kodaira_thurston_not_kahler {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hcs : IsCompactSymplectic Ω VF] [hbr : HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) [hH : HasHodgeNumbers] (hb1 : HasHodgeNumbers.betti Ω VF 1 = 3) : ¬IsKahler S J

The Kodaira–Thurston manifold is not Kähler: a compact Kähler manifold has even odd Betti numbers, but $b_1 = 3$ is odd.

structure CP2TripleSumData : Type (max (u_1 + 1) (u_2 + 1))

Data witnessing the connected sum $\mathbb{CP}^2 \# \mathbb{CP}^2 \# \mathbb{CP}^2$: a smooth $4$-manifold which is neither symplectic nor complex (no integrable almost complex structure).

• Ω : ℕ → Type u_1
• VF : Type u_2
• inst : DifferentialFormSpace self.Ω self.VF
• J : AlmostComplexStr
• not_symplectic : ¬Nonempty (SymplecticManifold self.Ω self.VF)
• not_complex (J' : AlmostComplexStr) (nij : NijenhuisTensor J') : ¬IsIntegrable J' nij