The period group of spherical classes

Let (X, ω) be a closed symplectic manifold and let S be its group of spherical classes, the image of the Hurewicz map π₂(X) → H₂(X; ℤ). Integrating ω and evaluating the first Chern class give homomorphisms ω : S →+ ℝ and c : S →+ ℤ. Two caps of a contractible loop differ by a spherical class B, and replacing one cap by the other shifts the action by ω B and the Conley–Zehnder grading by 2 * c B. Capped Hamiltonian Floer theory therefore takes its coefficients over the period group Γ = S ⧸ (ker ω ⊓ ker c), on which area and first Chern number descend. Quotienting by the joint kernel, rather than by ker ω alone, keeps apart classes of equal area and different Chern number, hence different degree.

This file develops Γ for an arbitrary additive group S with two such homomorphisms. We write Γ as the quotient by the kernel of s ↦ (ω s, c s), which is ker ω ⊓ ker c by AddMonoidHom.ker_prod.

Main definitions

• TauCeti.Floer.PeriodGroup ω c: the period group Γ.
• TauCeti.Floer.PeriodGroup.periods: the injective homomorphism Γ →+ ℝ × ℤ recording area and first Chern number, with components PeriodGroup.area and PeriodGroup.chern.
• TauCeti.Floer.PeriodGroup.degree: the degree γ ↦ 2 c(γ), the grading shift of a recapping by γ.
• TauCeti.Floer.PeriodGroup.chernEquivInt: integer coordinates with positive Chern generator when the Chern map is injective and nonzero; laurentExponent reverses these coordinates to make the Floer Laurent variable have positive valuation in the positive monotone case.
• TauCeti.Floer.PeriodGroup.map: the homomorphism of period groups induced by a homomorphism of class groups preserving area and Chern number.

Main results

• PeriodGroup.ext_iff: a class in Γ is determined by its area and first Chern number; equivalently the kernels of area and Chern number are disjoint (PeriodGroup.disjoint_ker_area_ker_chern).
• PeriodGroup.subsingleton_iff: Γ is trivial exactly when area and Chern number vanish on S, as for symplectically aspherical manifolds.
• PeriodGroup.chern_injective_iff, PeriodGroup.area_injective_iff: the Chern number (resp. the area) embeds Γ into ℤ (resp. ℝ) exactly when its kernel on S lies in the kernel of the area (resp. the Chern number).
• PeriodGroup.chern_injective_of_area_eq_mul_chern, PeriodGroup.isAddCyclic_of_area_eq_mul_chern: if the area is a fixed multiple of the Chern number (spherical monotonicity), then the Chern number embeds Γ into ℤ, so Γ is cyclic.
• PeriodGroup.area_injective_of_chern_eq_zero: if the Chern number vanishes, then the area embeds Γ into ℝ.
• PeriodGroup.negOnePow_eq_negOnePow_of_quotientMk_eq: degrees are even, so the residue of an integer modulo the degrees of Γ determines its parity.
• PeriodGroup.map_injective: induced maps of period groups are injective, and they are bijective when the map of class groups is surjective. They are functorial (PeriodGroup.map_id, PeriodGroup.map_comp).

References

• H. Hofer and D. A. Salamon, Floer homology and Novikov rings, in The Floer memorial volume, Progr. Math. 133 (1995), 483–524.
• D. McDuff and D. Salamon, J-holomorphic curves and symplectic topology, the construction of the Novikov ring in the chapter on quantum cohomology.

@[reducible, inline]

abbrev TauCeti.Floer.PeriodGroup {S : Type u_1} [AddGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) : Type u_1

The period group Γ = S ⧸ (ker ω ⊓ ker c) of a group of spherical classes S with symplectic area ω and first Chern number c, written as the quotient by the kernel of s ↦ (ω s, c s).

It is an abbreviation so that the quotient group API of Mathlib applies to it directly.

def TauCeti.Floer.PeriodGroup.periods {S : Type u_1} [AddGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) : PeriodGroup ω c →+ ℝ × ℤ

The joint period map Γ →+ ℝ × ℤ, recording the area and the first Chern number of a class. It is injective (PeriodGroup.periods_injective).

def TauCeti.Floer.PeriodGroup.area {S : Type u_1} [AddGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) : PeriodGroup ω c →+ ℝ

The symplectic area on the period group.

def TauCeti.Floer.PeriodGroup.chern {S : Type u_1} [AddGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) : PeriodGroup ω c →+ ℤ

The first Chern number on the period group.

def TauCeti.Floer.PeriodGroup.degree {S : Type u_1} [AddGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) : PeriodGroup ω c →+ ℤ

The degree 2 c(γ) of a class γ: recapping an orbit by γ shifts its Conley–Zehnder grading by 2 c(γ). It is the degree of the monomial e^γ of the Floer Novikov ring.

@[simp]

theorem TauCeti.Floer.PeriodGroup.degree_apply {S : Type u_1} [AddGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) (γ : PeriodGroup ω c) : (degree ω c) γ = 2 * (chern ω c) γ

The degree of a class is twice its first Chern number.

theorem TauCeti.Floer.PeriodGroup.even_degree {S : Type u_1} [AddGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) (γ : PeriodGroup ω c) : Even ((degree ω c) γ)

Degrees in the period group are even.

theorem TauCeti.Floer.PeriodGroup.negOnePow_eq_negOnePow_of_quotientMk_eq {S : Type u_1} [AddGroup S] {ω : S →+ ℝ} {c : S →+ ℤ} {k l : ℤ} (h : ↑k = ↑l) : k.negOnePow = l.negOnePow

Two integers with the same residue modulo the degrees of the period group have the same parity, since all these degrees are even. Hence the sign (-1)^k is a function of the residue of k.

theorem TauCeti.Floer.PeriodGroup.periods_mk {S : Type u_1} [AddGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) (s : S) : (periods ω c) ↑s = (ω s, c s)

The joint period map sends the class of s to its area and first Chern number.

@[simp]

theorem TauCeti.Floer.PeriodGroup.area_mk {S : Type u_1} [AddGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) (s : S) : (area ω c) ↑s = ω s

The area of the class of a spherical class s is ω s.

@[simp]

theorem TauCeti.Floer.PeriodGroup.chern_mk {S : Type u_1} [AddGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) (s : S) : (chern ω c) ↑s = c s

The first Chern number of the class of a spherical class s is c s.

@[simp]

theorem TauCeti.Floer.PeriodGroup.periods_apply {S : Type u_1} [AddGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) (γ : PeriodGroup ω c) : (periods ω c) γ = ((area ω c) γ, (chern ω c) γ)

The joint period map has components PeriodGroup.area and PeriodGroup.chern.

theorem TauCeti.Floer.PeriodGroup.periods_injective {S : Type u_1} [AddGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) : Function.Injective ⇑(periods ω c)

The joint period map is injective.

theorem TauCeti.Floer.PeriodGroup.ext {S : Type u_1} [AddGroup S] {ω : S →+ ℝ} {c : S →+ ℤ} {γ γ' : PeriodGroup ω c} (harea : (area ω c) γ = (area ω c) γ') (hchern : (chern ω c) γ = (chern ω c) γ') : γ = γ'

A class in the period group is determined by its area and its first Chern number.

theorem TauCeti.Floer.PeriodGroup.ext_iff {S : Type u_1} [AddGroup S] {ω : S →+ ℝ} {c : S →+ ℤ} {γ γ' : PeriodGroup ω c} : γ = γ' ↔ (area ω c) γ = (area ω c) γ' ∧ (chern ω c) γ = (chern ω c) γ'

Two classes in the period group are equal exactly when they have the same area and the same first Chern number.

theorem TauCeti.Floer.PeriodGroup.mk_eq_mk_iff {S : Type u_1} [AddGroup S] {ω : S →+ ℝ} {c : S →+ ℤ} {s t : S} : ↑s = ↑t ↔ ω s = ω t ∧ c s = c t

Two spherical classes have the same image in the period group exactly when they have the same area and the same first Chern number.

@[simp]

theorem TauCeti.Floer.PeriodGroup.range_area {S : Type u_1} [AddGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) : (area ω c).range = ω.range

The areas of classes in the period group are the areas of spherical classes.

@[simp]

theorem TauCeti.Floer.PeriodGroup.range_chern {S : Type u_1} [AddGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) : (chern ω c).range = c.range

The first Chern numbers of classes in the period group are those of spherical classes.

instance TauCeti.Floer.PeriodGroup.instHasUniqueDiv {S : Type u_1} [AddGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) : HasUniqueDiv (PeriodGroup ω c)

The period group is torsion-free: it embeds into ℝ × ℤ.

theorem TauCeti.Floer.PeriodGroup.subsingleton_iff {S : Type u_1} [AddGroup S] {ω : S →+ ℝ} {c : S →+ ℤ} : Subsingleton (PeriodGroup ω c) ↔ ∀ (s : S), ω s = 0 ∧ c s = 0

The period group is trivial exactly when area and first Chern number vanish on every spherical class, as they do on a symplectically aspherical manifold.

theorem TauCeti.Floer.PeriodGroup.chern_injective_iff {S : Type u_1} [AddGroup S] {ω : S →+ ℝ} {c : S →+ ℤ} : Function.Injective ⇑(chern ω c) ↔ c.ker ≤ ω.ker

The first Chern number embeds the period group into ℤ exactly when every spherical class with vanishing first Chern number has vanishing area.

theorem TauCeti.Floer.PeriodGroup.area_injective_iff {S : Type u_1} [AddGroup S] {ω : S →+ ℝ} {c : S →+ ℤ} : Function.Injective ⇑(area ω c) ↔ ω.ker ≤ c.ker

The area embeds the period group into ℝ exactly when every spherical class with vanishing area has vanishing first Chern number.

theorem TauCeti.Floer.PeriodGroup.degree_injective_iff {S : Type u_1} [AddGroup S] {ω : S →+ ℝ} {c : S →+ ℤ} : Function.Injective ⇑(degree ω c) ↔ Function.Injective ⇑(chern ω c)

The degree is injective exactly when the first Chern number is.

@[simp]

theorem TauCeti.Floer.PeriodGroup.ker_degree {S : Type u_1} [AddGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) : (degree ω c).ker = (chern ω c).ker

A class has degree zero exactly when its first Chern number vanishes.

theorem TauCeti.Floer.PeriodGroup.disjoint_ker_area_ker_chern {S : Type u_1} [AddGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) : Disjoint (area ω c).ker (chern ω c).ker

Area and first Chern number are jointly injective on the period group: the only class with vanishing area and vanishing first Chern number is zero.

theorem TauCeti.Floer.PeriodGroup.isAddCyclic_of_ker_le {S : Type u_1} [AddGroup S] {ω : S →+ ℝ} {c : S →+ ℤ} (h : c.ker ≤ ω.ker) : IsAddCyclic (PeriodGroup ω c)

If every spherical class with vanishing first Chern number has vanishing area, the period group is cyclic.

theorem TauCeti.Floer.PeriodGroup.area_eq_mul_chern {S : Type u_1} [AddGroup S] {ω : S →+ ℝ} {c : S →+ ℤ} {τ : ℝ} (h : ∀ (s : S), ω s = τ * ↑(c s)) (γ : PeriodGroup ω c) : (area ω c) γ = τ * ↑((chern ω c) γ)

If the area of every spherical class is τ times its first Chern number, the same holds on the period group.

theorem TauCeti.Floer.PeriodGroup.ker_le_ker_of_area_eq_mul_chern {S : Type u_1} [AddGroup S] {ω : S →+ ℝ} {c : S →+ ℤ} {τ : ℝ} (h : ∀ (s : S), ω s = τ * ↑(c s)) : c.ker ≤ ω.ker

For a spherically monotone pair, where the area is a fixed multiple of the first Chern number, every spherical class with vanishing first Chern number has vanishing area.

theorem TauCeti.Floer.PeriodGroup.chern_injective_of_area_eq_mul_chern {S : Type u_1} [AddGroup S] {ω : S →+ ℝ} {c : S →+ ℤ} {τ : ℝ} (h : ∀ (s : S), ω s = τ * ↑(c s)) : Function.Injective ⇑(chern ω c)

For a spherically monotone pair, where the area is a fixed multiple of the first Chern number, the first Chern number embeds the period group into ℤ.

theorem TauCeti.Floer.PeriodGroup.degree_injective_of_area_eq_mul_chern {S : Type u_1} [AddGroup S] {ω : S →+ ℝ} {c : S →+ ℤ} {τ : ℝ} (h : ∀ (s : S), ω s = τ * ↑(c s)) : Function.Injective ⇑(degree ω c)

For a spherically monotone pair, the degree embeds the period group into ℤ.

theorem TauCeti.Floer.PeriodGroup.isAddCyclic_of_area_eq_mul_chern {S : Type u_1} [AddGroup S] {ω : S →+ ℝ} {c : S →+ ℤ} {τ : ℝ} (h : ∀ (s : S), ω s = τ * ↑(c s)) : IsAddCyclic (PeriodGroup ω c)

For a spherically monotone pair the period group is cyclic.

theorem TauCeti.Floer.PeriodGroup.chern_eq_zero {S : Type u_1} [AddGroup S] {ω : S →+ ℝ} {c : S →+ ℤ} (h : ∀ (s : S), c s = 0) (γ : PeriodGroup ω c) : (chern ω c) γ = 0

If the first Chern number vanishes on spherical classes, it vanishes on the period group.

theorem TauCeti.Floer.PeriodGroup.area_injective_of_chern_eq_zero {S : Type u_1} [AddGroup S] {ω : S →+ ℝ} {c : S →+ ℤ} (h : ∀ (s : S), c s = 0) : Function.Injective ⇑(area ω c)

If the first Chern number vanishes on spherical classes, the area embeds the period group into ℝ.

noncomputable def TauCeti.Floer.PeriodGroup.chernEquivInt {S : Type u_1} [AddGroup S] {ω : S →+ ℝ} {c : S →+ ℤ} (hker : c.ker ≤ ω.ker) (hc : c ≠ 0) : PeriodGroup ω c ≃+ ℤ

Integer coordinates on a period group whose Chern map is injective and nonzero. The inverse image of one is the generator with positive Chern number.

theorem TauCeti.Floer.PeriodGroup.chern_chernEquivInt_symm_pos {S : Type u_1} [AddGroup S] {ω : S →+ ℝ} {c : S →+ ℤ} (hker : c.ker ≤ ω.ker) (hc : c ≠ 0) : 0 < (chern ω c) ((chernEquivInt hker hc).symm 1)

The positive generator has strictly positive Chern number, the minimal Chern number.

theorem TauCeti.Floer.PeriodGroup.chern_chernEquivInt_symm {S : Type u_1} [AddGroup S] {ω : S →+ ℝ} {c : S →+ ℤ} (hker : c.ker ≤ ω.ker) (hc : c ≠ 0) (k : ℤ) : (chern ω c) ((chernEquivInt hker hc).symm k) = k * (chern ω c) ((chernEquivInt hker hc).symm 1)

The Chern number in integer coordinates is the exponent times the minimal Chern number.

theorem TauCeti.Floer.PeriodGroup.chern_eq_mul_chernEquivInt {S : Type u_1} [AddGroup S] {ω : S →+ ℝ} {c : S →+ ℤ} (hker : c.ker ≤ ω.ker) (hc : c ≠ 0) (γ : PeriodGroup ω c) : (chern ω c) γ = (chernEquivInt hker hc) γ * (chern ω c) ((chernEquivInt hker hc).symm 1)

The Chern number of a period class determines its integer exponent by multiplication by the minimal Chern number.

noncomputable def TauCeti.Floer.PeriodGroup.laurentExponent {S : Type u_1} [AddGroup S] {ω : S →+ ℝ} {c : S →+ ℤ} (hker : c.ker ≤ ω.ker) (hc : c ≠ 0) : PeriodGroup ω c ≃+ ℤ

Laurent exponents for Floer coefficients. The variable corresponds to the negative of the positive Chern generator, so its valuation is positive on positively monotone targets.

@[simp]

theorem TauCeti.Floer.PeriodGroup.laurentExponent_apply {S : Type u_1} [AddGroup S] {ω : S →+ ℝ} {c : S →+ ℤ} (hker : c.ker ≤ ω.ker) (hc : c ≠ 0) (γ : PeriodGroup ω c) : (laurentExponent hker hc) γ = -(chernEquivInt hker hc) γ

A Floer Laurent exponent is the negative of the positive-Chern integer coordinate.

@[simp]

theorem TauCeti.Floer.PeriodGroup.chern_laurentExponent_symm {S : Type u_1} [AddGroup S] {ω : S →+ ℝ} {c : S →+ ℤ} (hker : c.ker ≤ ω.ker) (hc : c ≠ 0) (k : ℤ) : (chern ω c) ((laurentExponent hker hc).symm k) = -k * (chern ω c) ((chernEquivInt hker hc).symm 1)

The class of the Laurent monomial of exponent k has Chern number -k N, where N is the positive minimal Chern number.

theorem TauCeti.Floer.PeriodGroup.area_laurentExponent_symm {S : Type u_1} [AddGroup S] {ω : S →+ ℝ} {c : S →+ ℤ} {τ : ℝ} (h : ∀ (s : S), ω s = τ * ↑(c s)) (hc : c ≠ 0) (k : ℤ) : (area ω c) ((laurentExponent ⋯ hc).symm k) = -(τ * ↑((chern ω c) ((chernEquivInt ⋯ hc).symm 1))) * ↑k

In the monotone case the area of a Laurent monomial is minus its exponent times the area of the positive Chern generator. When 0 < τ, positive exponents have positive Floer valuation.

def TauCeti.Floer.PeriodGroup.map {S : Type u_1} {S' : Type u_2} [AddGroup S] [AddGroup S'] {ω : S →+ ℝ} {c : S →+ ℤ} {ω' : S' →+ ℝ} {c' : S' →+ ℤ} (f : S →+ S') (hω : ω'.comp f = ω) (hc : c'.comp f = c) : PeriodGroup ω c →+ PeriodGroup ω' c'

A homomorphism of class groups preserving area and first Chern number induces a homomorphism of period groups.

@[simp]

theorem TauCeti.Floer.PeriodGroup.map_mk {S : Type u_1} {S' : Type u_2} [AddGroup S] [AddGroup S'] {ω : S →+ ℝ} {c : S →+ ℤ} {ω' : S' →+ ℝ} {c' : S' →+ ℤ} (f : S →+ S') (hω : ω'.comp f = ω) (hc : c'.comp f = c) (s : S) : (map f hω hc) ↑s = ↑(f s)

The induced map sends the class of s to the class of f s.

@[simp]

theorem TauCeti.Floer.PeriodGroup.area_map {S : Type u_1} {S' : Type u_2} [AddGroup S] [AddGroup S'] {ω : S →+ ℝ} {c : S →+ ℤ} {ω' : S' →+ ℝ} {c' : S' →+ ℤ} (f : S →+ S') (hω : ω'.comp f = ω) (hc : c'.comp f = c) (γ : PeriodGroup ω c) : (area ω' c') ((map f hω hc) γ) = (area ω c) γ

The induced map of period groups preserves area.

@[simp]

theorem TauCeti.Floer.PeriodGroup.chern_map {S : Type u_1} {S' : Type u_2} [AddGroup S] [AddGroup S'] {ω : S →+ ℝ} {c : S →+ ℤ} {ω' : S' →+ ℝ} {c' : S' →+ ℤ} (f : S →+ S') (hω : ω'.comp f = ω) (hc : c'.comp f = c) (γ : PeriodGroup ω c) : (chern ω' c') ((map f hω hc) γ) = (chern ω c) γ

The induced map of period groups preserves the first Chern number.

theorem TauCeti.Floer.PeriodGroup.map_injective {S : Type u_1} {S' : Type u_2} [AddGroup S] [AddGroup S'] {ω : S →+ ℝ} {c : S →+ ℤ} {ω' : S' →+ ℝ} {c' : S' →+ ℤ} (f : S →+ S') (hω : ω'.comp f = ω) (hc : c'.comp f = c) : Function.Injective ⇑(map f hω hc)

Induced maps of period groups are injective: classes are separated by area and first Chern number, which the map preserves.

theorem TauCeti.Floer.PeriodGroup.map_surjective {S : Type u_1} {S' : Type u_2} [AddGroup S] [AddGroup S'] {ω : S →+ ℝ} {c : S →+ ℤ} {ω' : S' →+ ℝ} {c' : S' →+ ℤ} (f : S →+ S') (hω : ω'.comp f = ω) (hc : c'.comp f = c) (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(map f hω hc)

The map of period groups induced by a surjective map of class groups is surjective.

@[simp]

theorem TauCeti.Floer.PeriodGroup.map_id {S : Type u_1} [AddGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) : map (AddMonoidHom.id S) ⋯ ⋯ = AddMonoidHom.id (PeriodGroup ω c)

The map of period groups induced by the identity is the identity.

@[simp]

theorem TauCeti.Floer.PeriodGroup.map_comp {S : Type u_1} {S' : Type u_2} [AddGroup S] [AddGroup S'] {ω : S →+ ℝ} {c : S →+ ℤ} {ω' : S' →+ ℝ} {c' : S' →+ ℤ} (f : S →+ S') (hω : ω'.comp f = ω) (hc : c'.comp f = c) {S'' : Type u_3} [AddGroup S''] {ω'' : S'' →+ ℝ} {c'' : S'' →+ ℤ} (g : S' →+ S'') (hω' : ω''.comp g = ω') (hc' : c''.comp g = c') : (map g hω' hc').comp (map f hω hc) = map (g.comp f) ⋯ ⋯

Maps of period groups induced by composable maps of class groups compose.