The germ space MeroGermOn X U and ℳ X (CC3, D1/D6)

Unit: meromorphic-and-divisors (docs/design/meromorphic-and-divisors.md §4.3, D1, D6).

• Algebra ℂ (Filter.Germ l ℂ) (Compat, upstreamable): built from the existing Module ℂ instance via Algebra.ofModule, no diamond.
• meroGermSubalgebra X U : Subalgebra ℂ (Filter.Germ (codiscreteWithin U) ℂ): germs admitting a meromorphic representative on U. MeroGermOn X U := meroGermSubalgebra X U (as a type, via the Subalgebra coercion to Type); ℳ X := MeroGermOn X Set.univ (CC3's ℳ(X), an abbrev, so all MeroGermOn API applies verbatim).
• MeroGermOn.mk, mk_eq_mk, exists_rep, ind; mk_add/mk_mul/mk_neg/mk_smul/mk_zero/mk_one, algebraMap_mk.
• MeroGermOn.restrict (h : V ⊆ U) : MeroGermOn X U →ₐ[ℂ] MeroGermOn X V (Čech's structure maps), with restrict_mk, restrict_restrict, restrict_id.

Compat: Algebra ℂ (Germ l ℂ)

@[instance_reducible]

noncomputable instance RS.instAlgebraGerm {α : Type u_1} {l : Filter α} : Algebra ℂ (l.Germ ℂ)

Equations

• RS.instAlgebraGerm = Algebra.ofModule ⋯ ⋯

@[simp]

theorem RS.Filter.Germ.algebraMap_apply {α : Type u_1} {l : Filter α} (c : ℂ) : (algebraMap ℂ (l.Germ ℂ)) c = ↑fun (x : α) => c

The subalgebra and the type MeroGermOn

noncomputable def RS.meroGermSubalgebra (X : Type u_1) [TopologicalSpace X] [ChartedSpace ℂ X] (U : Set X) : Subalgebra ℂ ((Filter.codiscreteWithin U).Germ ℂ)

Germs over codiscreteWithin U admitting a meromorphic representative.

Equations

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

def RS.MeroGermOn (X : Type u_1) [TopologicalSpace X] [ChartedSpace ℂ X] (U : Set X) : Type u_1

The space of meromorphic germ classes on U (CC3 relativized; junk-free).

Equations

• RS.MeroGermOn X U = ↥(RS.meroGermSubalgebra X U)

@[reducible, inline]

abbrev RS.Mero (X : Type u_1) [TopologicalSpace X] [ChartedSpace ℂ X] : Type u_1

CC3 (frozen): the field of meromorphic functions, ℳ X.

Equations

• RS.Mero X = RS.MeroGermOn X Set.univ

def RS.termℳ : Lean.ParserDescr

CC3 (frozen): the field of meromorphic functions, ℳ X.

Equations

• RS.termℳ = Lean.ParserDescr.node `RS.termℳ 1024 (Lean.ParserDescr.symbol "ℳ")

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• RS.instAlgebraComplexMeroGermOn = { smul := RS.instAlgebraComplexMeroGermOn._aux_1, algebraMap := RS.instAlgebraComplexMeroGermOn._aux_3, commutes' := ⋯, smul_def' := ⋯ }

@[instance_reducible]

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

Equations

• RS.instModuleComplexMeroGermOn = { toDistribMulAction := Algebra.toModule.toDistribMulAction, add_smul := ⋯, zero_smul := ⋯ }

instance RS.instNontrivialMero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [Nonempty X] : Nontrivial (Mero X)

noncomputable def RS.MeroGermOn.mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} (f : X → ℂ) (hf : MeromorphicOnX f U) : MeroGermOn X U

Constructor: the class of a meromorphic function.

Equations

• RS.MeroGermOn.mk f hf = ⟨↑f, ⋯⟩

theorem RS.MeroGermOn.mk_eq_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {f g : X → ℂ} {hf : MeromorphicOnX f U} {hg : MeromorphicOnX g U} : mk f hf = mk g hg ↔ f =ᶠ[Filter.codiscreteWithin U] g

theorem RS.MeroGermOn.exists_rep {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} (φ : MeroGermOn X U) : ∃ (f : X → ℂ) (hf : MeromorphicOnX f U), mk f hf = φ

theorem RS.MeroGermOn.ind {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {motive : MeroGermOn X U → Prop} (h : ∀ (f : X → ℂ) (hf : MeromorphicOnX f U), motive (mk f hf)) (φ : MeroGermOn X U) : motive φ

@[simp]

theorem RS.MeroGermOn.mk_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {f g : X → ℂ} {hf : MeromorphicOnX f U} {hg : MeromorphicOnX g U} : mk f hf + mk g hg = mk (f + g) ⋯

@[simp]

theorem RS.MeroGermOn.mk_mul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {f g : X → ℂ} {hf : MeromorphicOnX f U} {hg : MeromorphicOnX g U} : mk f hf * mk g hg = mk (f * g) ⋯

@[simp]

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

@[simp]

theorem RS.MeroGermOn.mk_sub {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} {f g : X → ℂ} {hf : MeromorphicOnX f U} {hg : MeromorphicOnX g U} : mk f hf - mk g hg = mk (f - g) ⋯

mk turns subtraction into subtraction. Stated directly (rather than via mk_neg/mk_add) because a rewrite chain through those cannot instantiate the proof-valued arguments.

@[simp]

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

@[simp]

theorem RS.MeroGermOn.mk_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} : mk (fun (x : X) => 0) ⋯ = 0

@[simp]

theorem RS.MeroGermOn.mk_one {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} : mk (fun (x : X) => 1) ⋯ = 1

theorem RS.MeroGermOn.algebraMap_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} (c : ℂ) : (algebraMap ℂ (MeroGermOn X U)) c = mk (fun (x : X) => c) ⋯

Restriction (Čech's structure maps)

noncomputable def RS.restrictGerm {X : Type u_1} [TopologicalSpace X] {U V : Set X} (h : V ⊆ U) (γ : (Filter.codiscreteWithin U).Germ ℂ) : (Filter.codiscreteWithin V).Germ ℂ

The germ-level restriction map: pulling back a codiscreteWithin U-germ to a codiscreteWithin V-germ, for V ⊆ U. Meromorphy-free.

Equations

• RS.restrictGerm h γ = γ.liftOn (fun (f : X → ℂ) => ↑f) ⋯

@[simp]

theorem RS.restrictGerm_coe {X : Type u_1} [TopologicalSpace X] {U V : Set X} (h : V ⊆ U) (f : X → ℂ) : restrictGerm h ↑f = ↑f

theorem RS.restrictGerm_add {X : Type u_1} [TopologicalSpace X] {U V : Set X} (h : V ⊆ U) (γ₁ γ₂ : (Filter.codiscreteWithin U).Germ ℂ) : restrictGerm h (γ₁ + γ₂) = restrictGerm h γ₁ + restrictGerm h γ₂

theorem RS.restrictGerm_mul {X : Type u_1} [TopologicalSpace X] {U V : Set X} (h : V ⊆ U) (γ₁ γ₂ : (Filter.codiscreteWithin U).Germ ℂ) : restrictGerm h (γ₁ * γ₂) = restrictGerm h γ₁ * restrictGerm h γ₂

theorem RS.restrictGerm_one {X : Type u_1} [TopologicalSpace X] {U V : Set X} (h : V ⊆ U) : restrictGerm h 1 = 1

theorem RS.restrictGerm_zero {X : Type u_1} [TopologicalSpace X] {U V : Set X} (h : V ⊆ U) : restrictGerm h 0 = 0

theorem RS.restrictGerm_mem {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U V : Set X} (h : V ⊆ U) {γ : (Filter.codiscreteWithin U).Germ ℂ} (hγ : γ ∈ meroGermSubalgebra X U) : restrictGerm h γ ∈ meroGermSubalgebra X V

noncomputable def RS.MeroGermOn.restrict {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U V : Set X} (h : V ⊆ U) : MeroGermOn X U →ₐ[ℂ] MeroGermOn X V

Restriction to a smaller open set (Čech's structure maps).

Equations

• RS.MeroGermOn.restrict h = { toFun := fun (φ : RS.MeroGermOn X U) => ⟨RS.restrictGerm h ↑φ, ⋯⟩, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem RS.MeroGermOn.restrict_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U V : Set X} (h : V ⊆ U) {f : X → ℂ} {hf : MeromorphicOnX f U} : (restrict h) (mk f hf) = mk f ⋯

theorem RS.MeroGermOn.restrict_restrict {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U V W : Set X} (h₁ : V ⊆ U) (h₂ : W ⊆ V) (φ : MeroGermOn X U) : (restrict h₂) ((restrict h₁) φ) = (restrict ⋯) φ

theorem RS.MeroGermOn.restrict_id {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} (φ : MeroGermOn X U) : (restrict ⋯) φ = φ

theorem RS.algebraMap_injective {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [Nonempty X] : Function.Injective ⇑(algebraMap ℂ (Mero X))