Hamiltonian Floer operations: geometric product and multiplicative PSS
The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.
TheoremThe energy identity on a rectangle#
For a map u and perturbation data that are C¹ over
an open neighbourhood of a rectangle [a₁, b₁] × [a₂, b₂], the integral of the Floer energy
density over the rectangle is the symplectic area, plus the integral of the pulled-back one-form
K(u) = K_s(u) ds + K_t(u) dt over the positively oriented boundary, minus the integral of the
curvature R_K(u).
TauCeti.SymplecticForm.integral_floerEnergyDensity.{u_1} {V : Type u_1} [NormedAddCommGroup V]
[NormedSpace ℝ V] [FiniteDimensional ℝ V] {Ks Kt : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V}
(ω : TauCeti.SymplecticForm V) {U : Set (ℝ × ℝ)} (hU : IsOpen U) (hu : ContDiffOn ℝ 1 u U)
(hKs : ContDiffOn ℝ 1 (Function.uncurry Ks) (U ×ˢ Set.univ))
(hKt : ContDiffOn ℝ 1 (Function.uncurry Kt) (U ×ˢ Set.univ)) {a b : ℝ × ℝ} (hab : a ≤ b)
(habU : Set.Icc a b ⊆ U) :
∫ (z : ℝ × ℝ) in Set.Icc a b, ω.floerEnergyDensity Ks Kt u z =
(∫ (z : ℝ × ℝ) in Set.Icc a b,
(fun v w => (ω.toBilinForm v) w) ((fderiv ℝ u z) TauCeti.stdComplexLineReal)
((fderiv ℝ u z) TauCeti.stdComplexLineImag)) +
((((∫ (s : ℝ) in a.1..b.1, Ks (s, a.2) (u (s, a.2))) +
∫ (t : ℝ) in a.2..b.2, Kt (b.1, t) (u (b.1, t))) -
∫ (s : ℝ) in a.1..b.1, Ks (s, b.2) (u (s, b.2))) -
∫ (t : ℝ) in a.2..b.2, Kt (a.1, t) (u (a.1, t))) -
∫ (z : ℝ × ℝ) in Set.Icc a b, ω.hamiltonianCurvature Ks Kt z (u z)
Lean
Formalized in Tau Ceti as TauCeti.SymplecticForm.integral_floerEnergyDensity.
Sources
Uses 1
TheoremTauCeti.Floer.CapClass.mk_eq_mk_iff_action_eq_and_index_eq#
Two raw caps have the same class exactly when they have the same action and the same grading,
for functions a and m on raw caps obeying the recapping laws for area and twice the first
Chern number.
TauCeti.Floer.CapClass.mk_eq_mk_iff_action_eq_and_index_eq.{u_1, u_2} {S : Type u_1} [AddGroup S]
{ω : S →+ ℝ} {c : S →+ ℤ} {P : Type u_2} [AddTorsor S P] {a : P → ℝ} {m : P → ℤ}
(ha : ∀ (g : S) (p : P), a (g +ᵥ p) = ω g + a p)
(hm : ∀ (g : S) (p : P), m (g +ᵥ p) = 2 * c g + m p) {p q : P} :
Quotient.mk'' p = Quotient.mk'' q ↔ a p = a q ∧ m p = m q
Lean
Formalized in Tau Ceti as TauCeti.Floer.CapClass.mk_eq_mk_iff_action_eq_and_index_eq.
Sources
Uses 1
TheoremTauCeti.Floer.add_sub_add_two_mul_chern_productClass_eq#
Cap independence of the index μ₁(D₁) + μ₂(D₂) − μ₀(D₀) + 2 c₁(A) of a product coefficient,
for gradings mᵢ obeying the recapping law for twice the first Chern number. The Fredholm index
of a pair of pants in class A is this quantity minus half the dimension of the target.
TauCeti.Floer.add_sub_add_two_mul_chern_productClass_eq.{u_1, u_2, u_3, u_4} {S : Type u_1}
[AddGroup S] {ω : S →+ ℝ} {c : S →+ ℤ} {C₁ : Type u_2} {C₂ : Type u_3} {C₀ : Type u_4}
[AddTorsor (TauCeti.Floer.PeriodGroup ω c) C₀] {glue : C₁ → C₂ → C₀}
[AddTorsor (TauCeti.Floer.PeriodGroup ω c) C₁] [AddTorsor (TauCeti.Floer.PeriodGroup ω c) C₂]
{m₁ : C₁ → ℤ} {m₂ : C₂ → ℤ} {m₀ : C₀ → ℤ}
(hglue₁ :
∀ (γ : TauCeti.Floer.PeriodGroup ω c) (D₁ : C₁) (D₂ : C₂), glue (γ +ᵥ D₁) D₂ = γ +ᵥ glue D₁ D₂)
(hglue₂ :
∀ (γ : TauCeti.Floer.PeriodGroup ω c) (D₁ : C₁) (D₂ : C₂), glue D₁ (γ +ᵥ D₂) = γ +ᵥ glue D₁ D₂)
(hm₁ :
∀ (γ : TauCeti.Floer.PeriodGroup ω c) (D : C₁),
m₁ (γ +ᵥ D) = 2 * (TauCeti.Floer.PeriodGroup.chern ω c) γ + m₁ D)
(hm₂ :
∀ (γ : TauCeti.Floer.PeriodGroup ω c) (D : C₂),
m₂ (γ +ᵥ D) = 2 * (TauCeti.Floer.PeriodGroup.chern ω c) γ + m₂ D)
(hm₀ :
∀ (γ : TauCeti.Floer.PeriodGroup ω c) (D : C₀),
m₀ (γ +ᵥ D) = 2 * (TauCeti.Floer.PeriodGroup.chern ω c) γ + m₀ D)
(D₁ D₁' : C₁) (D₂ D₂' : C₂) (D₀ D₀' : C₀) :
m₁ D₁ + m₂ D₂ - m₀ D₀ +
2 * (TauCeti.Floer.PeriodGroup.chern ω c) (TauCeti.Floer.productClass glue D₁ D₂ D₀) =
m₁ D₁' + m₂ D₂' - m₀ D₀' +
2 * (TauCeti.Floer.PeriodGroup.chern ω c) (TauCeti.Floer.productClass glue D₁' D₂' D₀')
Lean
Formalized in Tau Ceti as TauCeti.Floer.add_sub_add_two_mul_chern_productClass_eq.
Sources
Uses 1
TheoremTauCeti.Floer.NovikovRing.forall_finite_lt_iff_bddAbove_degree#
For a positively monotone pair, a coefficient function on the period group satisfies the Novikov condition of the Floer Novikov ring exactly when the degrees of its support are bounded above.
TauCeti.Floer.NovikovRing.forall_finite_lt_iff_bddAbove_degree.{u_1, u_2} {S : Type u_1}
[AddGroup S] {R : Type u_2} {ω : S →+ ℝ} {c : S →+ ℤ} [Zero R] {τ : ℝ}
(h : ∀ (s : S), ω s = τ * ↑(c s)) (hτ : 0 < τ) (g : TauCeti.Floer.PeriodGroup ω c → R) :
(∀ (C : ℝ), {γ | g γ ≠ 0 ∧ (-TauCeti.Floer.PeriodGroup.area ω c) γ < C}.Finite) ↔
BddAbove (⇑(TauCeti.Floer.PeriodGroup.degree ω c) '' Function.support g)
Lean
Formalized in Tau Ceti as TauCeti.Floer.NovikovRing.forall_finite_lt_iff_bddAbove_degree.
Sources
- Tau Ceti documentation:
TauCeti.Floer.NovikovRing.forall_finite_lt_iff_bddAbove_degree - Source of
TauCeti.Floer.NovikovRing.forall_finite_lt_iff_bddAbove_degreein TauCeti/Geometry/Symplectic/Floer/NovikovRing.lean - Tau Ceti roadmap status: Hamiltonian Floer operations: geometric product and multiplicative PSS
Uses 1
TheoremTauCeti.Floer.periodGroupComparison_single_eq_iff#
Monomial descent identifies precisely the joint periods, retaining equal-area classes of different Chern number. The coefficient is assumed nonzero.
TauCeti.Floer.periodGroupComparison_single_eq_iff.{u_1, u_2} {R : Type u_1} {S : Type u_2}
[AddCommGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) [Semiring R] {r : R} (hr : r ≠ 0) (A B : S) :
(TauCeti.Floer.periodGroupComparison ω c) (TauCeti.NovikovSeries.single A r) =
(TauCeti.Floer.periodGroupComparison ω c) (TauCeti.NovikovSeries.single B r) ↔
ω A = ω B ∧ c A = c B
Lean
Formalized in Tau Ceti as TauCeti.Floer.periodGroupComparison_single_eq_iff.
Sources
Uses 3
AbbreviationTauCeti.Floer.NovikovRing#
The Floer Novikov ring over R: Novikov series ∑ a_γ e^γ over the period group, with
valuation ν(γ) = -ω(γ), so that for every bound C only finitely many classes with nonzero
coefficient have area greater than -C. It is graded by PeriodGroup.degree.
TauCeti.Floer.NovikovRing.{u_1, u_2} {S : Type u_1} [AddGroup S] (R : Type u_2) (ω : S →+ ℝ)
(c : S →+ ℤ) [Zero R] : Type (max u_1 u_2)
Uses 1
AbbreviationTauCeti.Floer.PeriodGroup#
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.
TauCeti.Floer.PeriodGroup.{u_1} {S : Type u_1} [AddGroup S] (ω : S →+ ℝ) (c : S →+ ℤ) : Type u_1
DefinitionTauCeti.Floer.coefficientComparison#
The completed coefficient comparison q^A ↦ e^(-q A), with source period ω and
target period -Ω. Area preservation makes it a unital ring homomorphism.
TauCeti.Floer.coefficientComparison.{u_1, u_2, u_3} {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) : TauCeti.NovikovSeries R S ω →+* TauCeti.NovikovSeries R Γ (-Ω)
Uses 1 · Used by 1
DefinitionTauCeti.NovikovModule.kernelProduct#
The bilinear product of completed combinations given by a kernel n with potential bound C
and completed outputs: the coefficient of p₀ in the product of a and b is the finite sum
∑ a(p₁) b(p₂) n(p₁, p₂, p₀) over all pairs of generators.
TauCeti.NovikovModule.kernelProduct.{u_1, u_2, u_3, u_4} {R : Type u_1} {S₁ : Type u_2}
{S₂ : Type u_3} {S₀ : Type u_4} {F₁ : S₁ → ℝ} {F₂ : S₂ → ℝ} {F₀ : S₀ → ℝ} [CommSemiring R] {C : ℝ}
{n : S₁ → S₂ → S₀ → R}
(hn : ∀ (p₁ : S₁) (p₂ : S₂) (p₀ : S₀), n p₁ p₂ p₀ ≠ 0 → F₀ p₀ ≤ F₁ p₁ + F₂ p₂ + C)
(hfin : ∀ (p₁ : S₁) (p₂ : S₂), n p₁ p₂ ∈ TauCeti.NovikovModule R F₀) :
↥(TauCeti.NovikovModule R F₁) →ₗ[R]
↥(TauCeti.NovikovModule R F₂) →ₗ[R] ↥(TauCeti.NovikovModule R F₀)
Used by 1
TheoremTauCeti.NovikovModule.kernelMatrix_mem_periodFiltration#
Under a potential bound with constant C, the (i, j, k) entry of the kernel matrix lies in
the period filtration at level F₀(r₀ k) - F₁(r₁ i) - F₂(r₂ j) - C.
TauCeti.NovikovModule.kernelMatrix_mem_periodFiltration.{u_1, u_2, u_3, u_4, u_5, u_6, u_7, u_8}
{R : Type u_1} {H : Type u_2} {ι₁ : Type u_3} {ι₂ : Type u_4} {ι₀ : Type u_5} [AddGroup H]
{N : H →+ ℝ} {P₁ : ι₁ → Type u_6} {P₂ : ι₂ → Type u_7} {P₀ : ι₀ → Type u_8}
[(k : ι₀) → AddTorsor H (P₀ k)] {F₁ : (i : ι₁) × P₁ i → ℝ} {F₂ : (j : ι₂) × P₂ j → ℝ}
{F₀ : (k : ι₀) × P₀ k → ℝ} {C : ℝ} {n : (i : ι₁) × P₁ i → (j : ι₂) × P₂ j → (k : ι₀) × P₀ k → R}
[Ring R] [Finite ι₀] (hF₀ : ∀ (k : ι₀) (h : H) (p : P₀ k), F₀ ⟨k, h +ᵥ p⟩ = F₀ ⟨k, p⟩ - N h)
(hn :
∀ (p₁ : (i : ι₁) × P₁ i) (p₂ : (j : ι₂) × P₂ j) (p₀ : (k : ι₀) × P₀ k),
n p₁ p₂ p₀ ≠ 0 → F₀ p₀ ≤ F₁ p₁ + F₂ p₂ + C)
(hfin : ∀ (p₁ : (i : ι₁) × P₁ i) (p₂ : (j : ι₂) × P₂ j), n p₁ p₂ ∈ TauCeti.NovikovModule R F₀)
(r₁ : (i : ι₁) → P₁ i) (r₂ : (j : ι₂) → P₂ j) (r₀ : (k : ι₀) → P₀ k) (i : ι₁) (j : ι₂) (k : ι₀) :
TauCeti.NovikovModule.kernelMatrix hF₀ hfin r₁ r₂ r₀ i j k ∈
TauCeti.NovikovSeries.periodFiltration R N (F₀ ⟨k, r₀ k⟩ - F₁ ⟨i, r₁ i⟩ - F₂ ⟨j, r₂ j⟩ - C)
Lean
Formalized in Tau Ceti as TauCeti.NovikovModule.kernelMatrix_mem_periodFiltration.
Sources
DefinitionTauCeti.NovikovModule.novikovKernelProduct#
The product of an invariant kernel, as a bilinear map over the Novikov ring, for the Novikov
module structures of TauCeti.NovikovModule.module.
TauCeti.NovikovModule.novikovKernelProduct.{u_1, u_2, u_3, u_4, u_5, u_6, u_7, u_8} {R : Type u_1}
{H : Type u_2} {ι₁ : Type u_3} {ι₂ : Type u_4} {ι₀ : Type u_5} [CommSemiring R] [AddCommGroup H]
{N : H →+ ℝ} {P₁ : ι₁ → Type u_6} {P₂ : ι₂ → Type u_7} {P₀ : ι₀ → Type u_8}
[(i : ι₁) → AddTorsor H (P₁ i)] [(j : ι₂) → AddTorsor H (P₂ j)] [(k : ι₀) → AddTorsor H (P₀ k)]
[Finite ι₁] [Finite ι₂] [Finite ι₀] {F₁ : (i : ι₁) × P₁ i → ℝ} {F₂ : (j : ι₂) × P₂ j → ℝ}
{F₀ : (k : ι₀) × P₀ k → ℝ} {C : ℝ} {n : (i : ι₁) × P₁ i → (j : ι₂) × P₂ j → (k : ι₀) × P₀ k → R}
(hF₁ : ∀ (i : ι₁) (h : H) (p : P₁ i), F₁ ⟨i, h +ᵥ p⟩ = F₁ ⟨i, p⟩ - N h)
(hF₂ : ∀ (j : ι₂) (h : H) (p : P₂ j), F₂ ⟨j, h +ᵥ p⟩ = F₂ ⟨j, p⟩ - N h)
(hF₀ : ∀ (k : ι₀) (h : H) (p : P₀ k), F₀ ⟨k, h +ᵥ p⟩ = F₀ ⟨k, p⟩ - N h)
(hn :
∀ (p₁ : (i : ι₁) × P₁ i) (p₂ : (j : ι₂) × P₂ j) (p₀ : (k : ι₀) × P₀ k),
n p₁ p₂ p₀ ≠ 0 → F₀ p₀ ≤ F₁ p₁ + F₂ p₂ + C)
(hfin : ∀ (p₁ : (i : ι₁) × P₁ i) (p₂ : (j : ι₂) × P₂ j), n p₁ p₂ ∈ TauCeti.NovikovModule R F₀)
(hn₁ :
∀ (g : H) (i : ι₁) (p₁ : P₁ i) (p₂ : (j : ι₂) × P₂ j) (k : ι₀) (p₀ : P₀ k),
n ⟨i, g +ᵥ p₁⟩ p₂ ⟨k, g +ᵥ p₀⟩ = n ⟨i, p₁⟩ p₂ ⟨k, p₀⟩)
(hn₂ :
∀ (g : H) (p₁ : (i : ι₁) × P₁ i) (j : ι₂) (p₂ : P₂ j) (k : ι₀) (p₀ : P₀ k),
n p₁ ⟨j, g +ᵥ p₂⟩ ⟨k, g +ᵥ p₀⟩ = n p₁ ⟨j, p₂⟩ ⟨k, p₀⟩) :
↥(TauCeti.NovikovModule R F₁) →ₗ[TauCeti.NovikovSeries R H N]
↥(TauCeti.NovikovModule R F₂) →ₗ[TauCeti.NovikovSeries R H N] ↥(TauCeti.NovikovModule R F₀)
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.