Field (ℳ X) and pointwise inverse (CC3, proof plan §6.2)

Unit: meromorphic-and-divisors (docs/design/meromorphic-and-divisors.md §4.5).

• Inv (MeroGermOn X U): the honest pointwise inverse on germs (Germ.instInv), unconditional (no if), junk-free — mk_inv, ord_inv (unconditional, matches ordAtX_inv).
• On a connected surface, the meromorphic identity dichotomy (CodiscreteBridge) classifies the zero class (Mero.ord_eq_top_iff) and gives mul_inv_cancel₀, assembling Field (ℳ X).

@[instance_reducible]

noncomputable instance RS.MeroGermOn.instInv {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} : Inv (MeroGermOn X U)

Equations

• RS.MeroGermOn.instInv = { inv := fun (φ : RS.MeroGermOn X U) => ⟨(↑φ)⁻¹, ⋯⟩ }

@[simp]

theorem RS.MeroGermOn.mk_inv {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {f : X → ℂ} {hf : MeromorphicOnX f U} : (mk f hf)⁻¹ = mk f⁻¹ ⋯

theorem RS.MeroGermOn.ord_inv {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {x : X} (hU : IsOpen U) (hx : x ∈ U) (φ : MeroGermOn X U) : φ⁻¹.ord x = -φ.ord x

theorem RS.MeroGermOn.inv_zero_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} : 0⁻¹ = 0

The zero class on a connected surface

theorem RS.Mero.ord_ne_top {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [ConnectedSpace X] {φ : Mero X} (h : φ ≠ 0) (x : X) : MeroGermOn.ord φ x ≠ ⊤

theorem RS.Mero.ord_eq_top_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [ConnectedSpace X] {φ : Mero X} (x : X) : MeroGermOn.ord φ x = ⊤ ↔ φ = 0

Field (ℳ X)

theorem RS.Mero.mul_inv_cancel {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [ConnectedSpace X] {φ : Mero X} (hφ : φ ≠ 0) : φ * φ⁻¹ = 1

@[instance_reducible]

noncomputable instance RS.instFieldMero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T2Space X] [ConnectedSpace X] : Field (Mero X)

Equations

• One or more equations did not get rendered due to their size.