Multiplication linear equivalence for L(D) (design §6.7, closing the documented gap) #
Unit: meromorphic-and-divisors. linSysMulEquiv: for φ ≠ 0 on a connected surface,
multiplication by φ is a ℂ-linear equivalence L(D) ≃ₗ L(D - divisor φ) (Miranda V.3.11
vocabulary; riemann-roch's lattice tool).
theorem
RS.mul_mem_linSys_sub_divisor
{X : Type u_1}
[TopologicalSpace X]
[ChartedSpace ℂ X]
[T1Space X]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X]
[ConnectedSpace X]
{φ : Mero X}
(hφ : φ ≠ 0)
{D : Divisor X}
{ψ : Mero X}
(hψ : ψ ∈ LinSys D)
:
noncomputable def
RS.linSysMulEquiv
{X : Type u_1}
[TopologicalSpace X]
[ChartedSpace ℂ X]
[T1Space X]
[IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X]
[ConnectedSpace X]
{φ : Mero X}
(hφ : φ ≠ 0)
(D : Divisor X)
:
Multiplication equivalence (linear equivalence of linear systems; Miranda V.3.11 vocab,
riemann-roch's lattice tool): for φ ≠ 0, ψ ↦ φ • ψ maps L(D) isomorphically to
L(D - divisor φ).
Equations
- One or more equations did not get rendered due to their size.