Comparing quantum and Floer coefficients

Quantum coefficients use the area period ω, whereas Floer coefficients use the negative area period. The comparison sends a class A to the negative of its image in the chosen Floer class group: q^A ↦ e^(-q A). This preserves periods, so it extends to a continuous unital homomorphism of the completed rings. Its coefficients are finite sums even if the class-group map has infinite kernel or area has dense image.

We allow any class-group homomorphism preserving area. If it also preserves a Chern map, the comparison negates Chern number on homogeneous supports. Thus raw Floer coefficient degree 2 c₁ becomes quantum coefficient degree after cochain regrading. For a quotient by any subgroup of the joint area/Chern kernel, use the descended area and Chern homomorphisms. periodGroupComparison specializes to the quotient by the entire joint kernel. In that case two monomials with the same nonzero coefficient become equal exactly when their areas and Chern numbers agree. No individual quantum invariant is assumed to descend without summation. If the target class group is trivial, the comparison sends a series to the sum of all of its coefficients (coeff_zero_coefficientComparison_of_subsingleton).

The construction reuses NovikovSeries.mapRingHom; no augmentation at q = 1 is involved.

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 Novikov coefficient conventions in the chapter on quantum cohomology.

noncomputable def TauCeti.Floer.coefficientComparison {R : Type u_1} {S : Type u_2} {Γ : Type u_3} [AddMonoid S] [AddCommGroup Γ] {ω : S →+ ℝ} {Ω : Γ →+ ℝ} [Semiring R] (q : S →+ Γ) (hω : ∀ (A : S), Ω (q A) = ω A) : NovikovSeries R S ω →+* NovikovSeries R Γ (-Ω)

The completed coefficient comparison q^A ↦ e^(-q A), with source period ω and target period -Ω. Area preservation makes it a unital ring homomorphism.

theorem TauCeti.Floer.coefficientComparison_apply {R : Type u_1} {S : Type u_2} {Γ : Type u_3} [AddMonoid S] [AddCommGroup Γ] {ω : S →+ ℝ} {Ω : Γ →+ ℝ} [Semiring R] (q : S →+ Γ) (hω : ∀ (A : S), Ω (q A) = ω A) (a : NovikovSeries R S ω) : (coefficientComparison q hω) a = (NovikovSeries.map (↑(RingHom.id R)) (-q) ⋯) a

The comparison is the existing finite-fibre Novikov pushforward along negative class projection.

@[simp]

theorem TauCeti.Floer.coefficientComparison_single {R : Type u_1} {S : Type u_2} {Γ : Type u_3} [AddMonoid S] [AddCommGroup Γ] {ω : S →+ ℝ} {Ω : Γ →+ ℝ} [Semiring R] (q : S →+ Γ) (hω : ∀ (A : S), Ω (q A) = ω A) (A : S) (r : R) : (coefficientComparison q hω) (NovikovSeries.single A r) = NovikovSeries.single (-q A) r

The comparison sends a quantum monomial to its negatively indexed Floer monomial.

theorem TauCeti.Floer.coeff_coefficientComparison {R : Type u_1} {S : Type u_2} {Γ : Type u_3} [AddMonoid S] [AddCommGroup Γ] {ω : S →+ ℝ} {Ω : Γ →+ ℝ} [Semiring R] (q : S →+ Γ) (hω : ∀ (A : S), Ω (q A) = ω A) (a : NovikovSeries R S ω) (γ : Γ) : ((coefficientComparison q hω) a).coeff γ = ∑ A ∈ ⋯.toFinset, a.coeff A

A coefficient of the comparison is the finite sum over its supported fibre.

theorem TauCeti.Floer.coeff_zero_coefficientComparison_of_subsingleton {R : Type u_1} {S : Type u_2} {Γ : Type u_3} [AddMonoid S] [AddCommGroup Γ] {ω : S →+ ℝ} {Ω : Γ →+ ℝ} [Semiring R] (q : S →+ Γ) (hω : ∀ (A : S), Ω (q A) = ω A) [Subsingleton Γ] (a : NovikovSeries R S ω) : ((coefficientComparison q hω) a).coeff 0 = ∑ᶠ (A : S), a.coeff A

Over a trivial target class group the comparison is the total count. The comparison sends ∑_A N_A q^A to ∑_A N_A, a finite sum by TauCeti.NovikovSeries.finite_support_of_bddAbove_image, since every class has zero area: ω A = Ω (q A) = 0.

theorem TauCeti.Floer.support_coefficientComparison_subset {R : Type u_1} {S : Type u_2} {Γ : Type u_3} [AddMonoid S] [AddCommGroup Γ] {ω : S →+ ℝ} {Ω : Γ →+ ℝ} [Semiring R] (q : S →+ Γ) (hω : ∀ (A : S), Ω (q A) = ω A) (a : NovikovSeries R S ω) : ((coefficientComparison q hω) a).support ⊆ ⇑(-q) '' a.support

No new support classes appear except images under negative class projection.

theorem TauCeti.Floer.coefficientComparison_surjective {R : Type u_1} {S : Type u_2} {Γ : Type u_3} [AddMonoid S] [AddCommGroup Γ] {ω : S →+ ℝ} {Ω : Γ →+ ℝ} [Semiring R] (q : S →+ Γ) (hω : ∀ (A : S), Ω (q A) = ω A) (hq : Function.Surjective ⇑q) : Function.Surjective ⇑(coefficientComparison q hω)

A quotient of class groups gives a surjective comparison, without a finite-kernel assumption. Each target series can be lifted using one representative of each exponent.

theorem TauCeti.Floer.chern_support_coefficientComparison {R : Type u_1} {S : Type u_2} {Γ : Type u_3} [AddMonoid S] [AddCommGroup Γ] {ω : S →+ ℝ} {Ω : Γ →+ ℝ} [Semiring R] (q : S →+ Γ) (hω : ∀ (A : S), Ω (q A) = ω A) (c : S →+ ℤ) (c' : Γ →+ ℤ) (hc : ∀ (A : S), c' (q A) = c A) {k : ℤ} {a : NovikovSeries R S ω} (ha : ∀ A ∈ a.support, c A = k) (γ : Γ) : γ ∈ ((coefficientComparison q hω) a).support → c' γ = -k

If source and target Chern maps agree under class projection, the comparison negates the Chern number of a homogeneous support.

theorem TauCeti.Floer.continuous_coefficientComparison {R : Type u_1} {S : Type u_2} {Γ : Type u_3} [AddMonoid S] [AddCommGroup Γ] {ω : S →+ ℝ} {Ω : Γ →+ ℝ} [Ring R] (q : S →+ Γ) (hω : ∀ (A : S), Ω (q A) = ω A) : Continuous ⇑(coefficientComparison q hω)

The coefficient comparison is continuous for the period topologies.

theorem TauCeti.Floer.coefficientComparison_mem_periodFiltration {R : Type u_1} {S : Type u_2} {Γ : Type u_3} [AddMonoid S] [AddCommGroup Γ] {ω : S →+ ℝ} {Ω : Γ →+ ℝ} [Ring R] (q : S →+ Γ) (hω : ∀ (A : S), Ω (q A) = ω A) {C : ℝ} {a : NovikovSeries R S ω} (ha : a ∈ NovikovSeries.periodFiltration R ω C) : (coefficientComparison q hω) a ∈ NovikovSeries.periodFiltration R (-Ω) C

The comparison preserves every energy cutoff, including all reference-class constants that have already been incorporated into that cutoff.

noncomputable def TauCeti.Floer.periodGroupComparison {R : Type u_1} {S : Type u_2} [AddCommGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) [Semiring R] : NovikovSeries R S ω →+* NovikovSeries R (PeriodGroup ω c) (-PeriodGroup.area ω c)

Descent from a common class group to the Floer joint-period quotient, with the sign change q^A ↦ e^(-[A]) and finite summation of all coefficients having that image.

theorem TauCeti.Floer.periodGroupComparison_apply {R : Type u_1} {S : Type u_2} [AddCommGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) [Semiring R] (a : NovikovSeries R S ω) : (periodGroupComparison ω c) a = (coefficientComparison (QuotientAddGroup.mk' (ω.prod c).ker) ⋯) a

The joint-period comparison is the signed coefficient comparison for the canonical quotient projection. This gives access to its finite coefficient-sum and support formulas.

@[simp]

theorem TauCeti.Floer.periodGroupComparison_single {R : Type u_1} {S : Type u_2} [AddCommGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) [Semiring R] (A : S) (r : R) : (periodGroupComparison ω c) (NovikovSeries.single A r) = NovikovSeries.single (-↑A) r

The joint-period comparison sends q^A to e^(-[A]).

theorem TauCeti.Floer.periodGroupComparison_surjective {R : Type u_1} {S : Type u_2} [AddCommGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) [Semiring R] : Function.Surjective ⇑(periodGroupComparison ω c)

Descent to the joint-period quotient is surjective even when area alone fails to separate classes.

theorem TauCeti.Floer.continuous_periodGroupComparison {R : Type u_1} {S : Type u_2} [AddCommGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) [Ring R] : Continuous ⇑(periodGroupComparison ω c)

The joint-period comparison is continuous for the energy topologies.

theorem TauCeti.Floer.periodGroupComparison_single_eq_iff {R : Type u_1} {S : Type u_2} [AddCommGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) [Semiring R] {r : R} (hr : r ≠ 0) (A B : S) : (periodGroupComparison ω c) (NovikovSeries.single A r) = (periodGroupComparison ω c) (NovikovSeries.single B r) ↔ ω A = ω B ∧ c A = c B

Monomial descent identifies precisely the joint periods, retaining equal-area classes of different Chern number. The coefficient is assumed nonzero.