Periods of a holomorphic 1-form along a loop (CC6)

Unit: paths-and-integrals (docs/design/paths-and-integrals.md §6). Carrier decision (CC9 alignment): based loops Path x x, with descent to Path.Homotopic.Quotient x x available via pathIntegralQ. This unit does not define the period subgroup (jacobian-construction's job); it exports the loop-algebra lemmas that make AddSubgroup.closure (Set.range (periodVector b)) well-behaved.

Main declarations:

• RS.period γ η — abbreviation for pathIntegral γ η on a based loop.
• RS.period_trans/symm/refl/congr_homotopic/conj.
• RS.periodVector b γ — the period vector w.r.t. a basis b of Form1 X, with periodVector_trans/symm/refl.

@[reducible, inline]

noncomputable abbrev RS.period {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x : X} (γ : Path x x) (η : Form1 X) : ℂ

The period of a 1-form along a loop.

Equations

• RS.period γ η = RS.pathIntegral γ η

theorem RS.period_trans {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x : X} (γ γ' : Path x x) (η : Form1 X) : period (γ.trans γ') η = period γ η + period γ' η

theorem RS.period_symm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x : X} (γ : Path x x) (η : Form1 X) : period γ.symm η = -period γ η

theorem RS.period_refl {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x : X} (η : Form1 X) : period (Path.refl x) η = 0

theorem RS.period_congr_homotopic {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x : X} {γ γ' : Path x x} (h : γ.Homotopic γ') (η : Form1 X) : period γ η = period γ' η

theorem RS.period_conj {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x x' : X} (σ : Path x' x) (γ : Path x x) (η : Form1 X) : period ((σ.trans γ).trans σ.symm) η = period γ η

Conjugation invariance: periods are basepoint-independent along a connecting path.

noncomputable def RS.periodVector {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x : X} {n : ℕ} (b : Module.Basis (Fin n) ℂ (Form1 X)) (γ : Path x x) : Fin n → ℂ

Period vector w.r.t. a basis of Form1 X (CC9 feed).

Equations

• RS.periodVector b γ i = RS.period γ (b i)

theorem RS.periodVector_trans {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x : X} {n : ℕ} (b : Module.Basis (Fin n) ℂ (Form1 X)) (γ γ' : Path x x) : periodVector b (γ.trans γ') = periodVector b γ + periodVector b γ'

theorem RS.periodVector_symm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x : X} {n : ℕ} (b : Module.Basis (Fin n) ℂ (Form1 X)) (γ : Path x x) : periodVector b γ.symm = -periodVector b γ

@[simp]

theorem RS.periodVector_refl {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {x : X} {n : ℕ} (b : Module.Basis (Fin n) ℂ (Form1 X)) : periodVector b (Path.refl x) = 0