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
LeanTauCeti.SymplecticForm.integral_floerEnergyDensity
Uses 1
Proof usesGreen's theorem on a rectangle

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
LeanTauCeti.Floer.CapClass.mk_eq_mk_iff_action_eq_and_index_eq
Uses 1
Proof usesTauCeti.Floer.PeriodGroup

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
LeanTauCeti.Floer.add_sub_add_two_mul_chern_productClass_eq
Uses 1
Statement usesTauCeti.Floer.PeriodGroup

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
LeanTauCeti.Floer.NovikovRing.forall_finite_lt_iff_bddAbove_degree
Uses 1
Statement usesTauCeti.Floer.PeriodGroup

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
LeanTauCeti.Floer.periodGroupComparison_single_eq_iff
Uses 3
Statement usesTauCeti.Floer.coefficientComparison · TauCeti.Floer.PeriodGroup
Proof usesTauCeti.NovikovSeries.mapRingHom

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)
Lean

Formalized in Tau Ceti as TauCeti.Floer.NovikovRing.

Sources
LeanTauCeti.Floer.NovikovRing
Uses 1
Statement usesTauCeti.Floer.PeriodGroup

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
Lean

Formalized in Tau Ceti as TauCeti.Floer.PeriodGroup.

Sources
LeanTauCeti.Floer.PeriodGroup
Used by 5
Used byTauCeti.Floer.add_sub_add_two_mul_chern_productClass_eq · TauCeti.Floer.CapClass.mk_eq_mk_iff_action_eq_and_index_eq · TauCeti.Floer.NovikovRing · TauCeti.Floer.NovikovRing.forall_finite_lt_iff_bddAbove_degree · TauCeti.Floer.periodGroupComparison_single_eq_iff

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 Γ (-Ω)
Lean

Formalized in Tau Ceti as TauCeti.Floer.coefficientComparison.

Sources
LeanTauCeti.Floer.coefficientComparison
Uses 1 · Used by 1
Statement usesTauCeti.NovikovSeries.mapRingHom
Used byTauCeti.Floer.periodGroupComparison_single_eq_iff

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₀)
Lean

Formalized in Tau Ceti as TauCeti.NovikovModule.kernelProduct.

Sources
LeanTauCeti.NovikovModule.kernelProduct
Used by 1
Used byTauCeti.NovikovModule.novikovKernelProduct

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
LeanTauCeti.NovikovModule.kernelMatrix_mem_periodFiltration

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₀)
Lean

Formalized in Tau Ceti as TauCeti.NovikovModule.novikovKernelProduct.

Sources
LeanTauCeti.NovikovModule.novikovKernelProduct
Uses 1
Statement usesTauCeti.NovikovModule.kernelProduct

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.