Analytic families and moduli of complex curves
The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.
TheoremWiener's lemma for H^s(A), s > 1/2#
An element of H^s(A) is a unit if and only if
its continuous representative takes invertible values at every point of the circle.
TauCeti.CircleSobolev.isUnit_iff_forall_isUnit.{u_1} {s : ℝ} {A : Type u_1} [NormedCommRing A]
[NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] (T : ℝ) [Fact (0 < T)]
{a : TauCeti.CircleSobolev s A} :
IsUnit a ↔ ∀ (x : AddCircle T), IsUnit (((TauCeti.CircleSobolev.toContinuousMap T ⋯) a) x)
Lean
Formalized in Tau Ceti as TauCeti.CircleSobolev.isUnit_iff_forall_isUnit.
Other forms
Wiener's lemma for H^s, s > 1/2. Formalized in Tau Ceti as TauCeti.CircleSobolev.isUnit_iff_forall_ne_zero.
TauCeti.CircleSobolev.isUnit_iff_forall_ne_zero {s : ℝ} [hs : Fact (1 / 2 < s)] (T : ℝ)
[Fact (0 < T)] {a : TauCeti.CircleSobolev s ℂ} :
IsUnit a ↔ ∀ (x : AddCircle T), ((TauCeti.CircleSobolev.toContinuousMap T ⋯) a) x ≠ 0
Sources
Uses 2
TheoremThe product estimate in H^s(A), s > 1/2#
TauCeti.CircleSobolev.norm_mul_le.{u_4} {s : ℝ} {A : Type u_4} [NormedRing A] [NormedAlgebra ℂ A]
[CompleteSpace A] [hs : Fact (1 / 2 < s)] (a b : TauCeti.CircleSobolev s A) :
‖a * b‖ ≤ 2 ^ (s + 1) * √(∑' (n : ℤ), TauCeti.CircleSobolev.weight (-(2 * s)) n) * ‖a‖ * ‖b‖
Uses 2 · Used by 2
TheoremThe holomorphic Nemytskii map is holomorphic#
If F is holomorphic on an open set U,
then u ↦ nemytskii F u is analytic on the open subset of H^s, s > 1/2, of elements with
values in U (isOpen_setOf_forall_toContinuousMap_mem).
TauCeti.CircleSobolev.analyticOnNhd_nemytskii {s : ℝ} (T : ℝ) [hT : Fact (0 < T)]
[hs : Fact (1 / 2 < s)] {F : ℂ → ℂ} {U : Set ℂ} (hU : IsOpen U) (hF : DifferentiableOn ℂ F U) :
AnalyticOnNhd ℂ (TauCeti.CircleSobolev.nemytskii F)
{u | ∀ (x : AddCircle T), ((TauCeti.CircleSobolev.toContinuousMap T ⋯) u) x ∈ U}
Uses 3 · Used by 1
TheoremStalks at the nodes of a glued nodal curve#
At the node of a flag pair, the restrictions to the two branches identify the stalk of the glued curve with the branch-pair node ring.
TauCeti.NodalGluing.quotientStalkToNode_bijective.{u_1, u_2, u_3} {E : Type u_1}
[NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H]
(I : ModelWithCorners ℂ E H) {ι : Type} {Flag : Type u_3} {X : ι → Type}
[(i : ι) → TopologicalSpace (X i)] [(i : ι) → ChartedSpace H (X i)]
(d : TauCeti.NodalGluing.FlagPairData ι Flag X) [Finite Flag] [∀ (i : ι), T2Space (X i)]
(f : Flag) :
Function.Bijective
⇑(TauCeti.holomorphicStructureSheaf.quotientStalkToNode I (TauCeti.NodalGluing.gluedRelSetoid d)
(TauCeti.NodalGluing.fstPoint d f) (TauCeti.NodalGluing.sndPoint d f) ⋯)
Lean
Formalized in Tau Ceti as TauCeti.NodalGluing.quotientStalkToNode_bijective.
Sources
Uses 1
TheoremStalks at smooth points of a glued nodal curve#
Away from the flag points, restriction to the normalization identifies the stalks of the glued curve with the holomorphic stalks of the normalization.
TauCeti.NodalGluing.quotientStalkBranch_bijective.{u_1, u_2, u_3} {E : Type u_1}
[NormedAddCommGroup E] [NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H]
(I : ModelWithCorners ℂ E H) {ι : Type} {Flag : Type u_3} {X : ι → Type}
[(i : ι) → TopologicalSpace (X i)] [(i : ι) → ChartedSpace H (X i)]
(d : TauCeti.NodalGluing.FlagPairData ι Flag X) [Finite Flag] [∀ (i : ι), T1Space (X i)]
{x : (i : ι) × X i} (hx : x ∉ TauCeti.NodalGluing.flagPointSet d) :
Function.Bijective
⇑(TauCeti.holomorphicStructureSheaf.quotientStalkBranch I (TauCeti.NodalGluing.gluedRelSetoid d)
⟦x⟧ x ⋯)
Lean
Formalized in Tau Ceti as TauCeti.NodalGluing.quotientStalkBranch_bijective.
Sources
Uses 1
TheoremSmoothing preserves the arithmetic genus#
The first Betti number lost by smoothing the
nodes in S reappears in the genera of the smoothed components.
TauCeti.DualGraph.arithmeticGenus_smoothing.{u, v} {ι : Type v} (G : TauCeti.DualGraph ι)
(S : Finset G.Edge) : (G.smoothing S).arithmeticGenus = G.arithmeticGenus
Used by 1
TheoremGenus of a partial normalization#
The sum of the arithmetic genera of its connected pieces, plus the number of cut nodes plus one, equals the original genus plus the number of pieces. This includes separating, nonseparating and simultaneous cuts, without subtraction.
TauCeti.DualGraph.sum_arithmeticGenus_cutComponent_add_card.{u, v} {ι : Type v}
(G : TauCeti.DualGraph ι) (S : Finset G.Edge) :
∑ x, (G.cutComponent S x).arithmeticGenus + S.card + 1 =
G.arithmeticGenus + Fintype.card (G.smoothing Sᶜ).Vertex
Lean
Formalized in Tau Ceti as TauCeti.DualGraph.sum_arithmeticGenus_cutComponent_add_card.
Sources
Uses 1
AbbreviationThe glued space#
The quotient of the disjoint union of the normalization components by the generated relation: the underlying topological space of the nodal curve. The topology is the quotient topology, i.e. the finest topology making the quotient map continuous.
TauCeti.NodalGluing.GluedCurve.{u_1, u_2, u_3} {ι : Type u_1} {Flag : Type u_2} {X : ι → Type u_3}
(d : TauCeti.NodalGluing.FlagPairData ι Flag X) : Type (max u_3 u_1)
DefinitionTauCeti.holomorphicStructureSheaf.quotientSheaf#
The sheaf of holomorphic functions on the normalization which have matching values on each fibre of the quotient map. For paired node flags this is the normalization construction of the structure sheaf of a nodal curve.
TauCeti.holomorphicStructureSheaf.quotientSheaf.{u_1, u_2} {E : Type u_1} [NormedAddCommGroup E]
[NormedSpace ℂ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℂ E H) {X : Type}
[TopologicalSpace X] [ChartedSpace H X] (s : Setoid X) : TopCat.Sheaf CommRingCat ↧(Quotient s)
Lean
Formalized in Tau Ceti as TauCeti.holomorphicStructureSheaf.quotientSheaf.
Sources
StructureAn isomorphism of nodal curves presented by flag-pair data#
A C^n diffeomorphism of the
disjoint unions of the normalization components which carries the two points of a flag pair of
d exactly to the two points of a flag pair of d'. Over ℂ with n = ∞ this is a
biholomorphism of the normalizations matching the nodes.
TauCeti.NodalGluing.Iso.{u_1, u_2, u_3, u_4, u_5, u_6, u_7, u_8, u_9} {𝕜 : Type u_1}
[NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3}
[TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) {ι : Type u_4}
{Flag : Type u_5} {X : ι → Type u_6} [(i : ι) → TopologicalSpace (X i)]
[(i : ι) → ChartedSpace H (X i)] {ι' : Type u_7} {Flag' : Type u_8} {X' : ι' → Type u_9}
[(i : ι') → TopologicalSpace (X' i)] [(i : ι') → ChartedSpace H (X' i)]
(d : TauCeti.NodalGluing.FlagPairData ι Flag X)
(d' : TauCeti.NodalGluing.FlagPairData ι' Flag' X') : Type (max (max (max u_4 u_6) u_7) u_9)
AbbreviationThe automorphism group of a nodal curve presented by flag-pair data#
its isomorphisms with itself, with composition as multiplication.
TauCeti.NodalGluing.Aut.{u_1, u_2, u_3, u_4, u_5, u_6} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
{E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) {ι : Type u_4} {Flag : Type u_5} {X : ι → Type u_6}
[(i : ι) → TopologicalSpace (X i)] [(i : ι) → ChartedSpace H (X i)]
(d : TauCeti.NodalGluing.FlagPairData ι Flag X) : Type (max u_6 u_4)
Uses 1
InstanceThe groupoid of curves with unordered auxiliary marks#
Its arrows are the pairs (π, f)
of AuxiliaryIso, composed by (ρ, h) ∘ (π, f) = (ρ ∘ π, h ∘ f). Its objects are the same as
those of the groupoid of isomorphisms preserving every label, of which it is the
label-permutation extension, a finite extension when R is finite.
TauCeti.NodalGluing.AuxiliaryMarkedCurve.unorderedAuxiliaryIsomorphismGroupoid.{u, v, w, u_1, u_2,
u_3, u_13, u_14}
{𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
{H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {N : Type u_13}
{R : Type u_14} : CategoryTheory.Groupoid (TauCeti.NodalGluing.AuxiliaryMarkedCurve I n N R)
Lean
Formalized in Tau Ceti as TauCeti.NodalGluing.AuxiliaryMarkedCurve.unorderedAuxiliaryIsomorphismGroupoid.
Sources
- Tau Ceti documentation:
TauCeti.NodalGluing.AuxiliaryMarkedCurve.unorderedAuxiliaryIsomorphismGroupoid - Source of
TauCeti.NodalGluing.AuxiliaryMarkedCurve.unorderedAuxiliaryIsomorphismGroupoidin TauCeti/AlgebraicGeometry/Curves/NodalGluing/AuxiliaryMarks.lean - Tau Ceti roadmap status: Analytic families and moduli of complex curves
Uses 1 · Used by 1
DefinitionThe groupoid of curves with partitioned auxiliary marks#
For a colouring κ : R → Cl of
the auxiliary labels, this is the subgroupoid of the groupoid of curves with unordered auxiliary
marks consisting of the colour-preserving arrows (π, f), those whose permutation π lies in
∏_c S(κ ⁻¹' {c}). It is wide (isWide_partitionedAuxiliaryIsomorphismGroupoid): it has the
same objects, but in general fewer arrows between them.
TauCeti.NodalGluing.AuxiliaryMarkedCurve.partitionedAuxiliaryIsomorphismGroupoid.{u, v, w, u_1, u_2,
u_3, u_13, u_14, u_15}
{𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
{H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (N : Type u_13)
{R : Type u_14} {Cl : Type u_15} (κ : R → Cl) :
CategoryTheory.Subgroupoid (TauCeti.NodalGluing.AuxiliaryMarkedCurve I n N R)
Lean
Formalized in Tau Ceti as TauCeti.NodalGluing.AuxiliaryMarkedCurve.partitionedAuxiliaryIsomorphismGroupoid.
Sources
- Tau Ceti documentation:
TauCeti.NodalGluing.AuxiliaryMarkedCurve.partitionedAuxiliaryIsomorphismGroupoid - Source of
TauCeti.NodalGluing.AuxiliaryMarkedCurve.partitionedAuxiliaryIsomorphismGroupoidin TauCeti/AlgebraicGeometry/Curves/NodalGluing/PartitionedAuxiliaryMarks.lean - Tau Ceti roadmap status: Analytic families and moduli of complex curves
DefinitionTauCeti.CircleSobolev.mulFourierSeriesEquiv#
For a smooth function f on the circle that vanishes nowhere, multiplication by f as a
continuous linear automorphism of H^s, for every real s; its inverse is multiplication by
f⁻¹.
TauCeti.CircleSobolev.mulFourierSeriesEquiv.{u_1} {s : ℝ} {E : Type u_1} [NormedAddCommGroup E]
[NormedSpace ℂ E] [CompleteSpace E] {T : ℝ} [Fact (0 < T)] (f : AddCircle T → ℂ)
(hf : ContDiff ℝ ↑⊤ fun x => f ↑x) (hf₀ : ∀ (x : AddCircle T), f x ≠ 0) :
TauCeti.CircleSobolev s E ≃L[ℂ] TauCeti.CircleSobolev s E
Uses 1
TheoremEhrling's inequality on the circle#
for r ≤ t < s, the H^t norm is bounded by an
arbitrarily small multiple of the H^s norm plus a multiple of the weaker H^r norm.
TauCeti.CircleSobolev.exists_norm_inclusion_le.{u_1} {s t : ℝ} {E : Type u_1} [NormedAddCommGroup E]
[NormedSpace ℂ E] {r : ℝ} (hrt : r ≤ t) (hts : t < s) {ε : ℝ} (hε : 0 < ε) :
∃ C,
0 ≤ C ∧
∀ (a : TauCeti.CircleSobolev s E),
‖(TauCeti.CircleSobolev.inclusion ⋯) a‖ ≤
ε * ‖a‖ + C * ‖(TauCeti.CircleSobolev.inclusion ⋯) a‖
TheoremThe nonlinear Hardy graph theorem at a plumbing node#
For s > 1/2 there are a
neighbourhood W of 0 in H^s × H^s and a map ψ, analytic at the origin with ψ 0 = 0, such
that for all data y = (a, p, q) near 0, with p and q of nonnegative frequencies, ψ y is
the unique (F, G) ∈ W with
(F, G)in the neck graph of the plumbingxy = a, and- nonnegative parts of
e^Fande^Gequal to1 + pand1 + q.
In terms of the boundary maps ξ = x e^F and η = y e^G, the conditions say that (ξ, η) solves
the node equation ξ(x) η(a / x) = b with b = a e^{F₀ + G₀}
(CircleSobolev.mul_exp_mul_mul_exp_eq_of_mem_neckGraph), and that the positive Fourier
coefficients of ξ and η are those of x (1 + p) and y (1 + q). So the solution, its
nonpositive coefficients and b depend holomorphically on a and on these positive coefficients,
also at the node a = 0.
TauCeti.CircleSobolev.exists_analyticAt_hardyGraph {s : ℝ} [hs : Fact (1 / 2 < s)] :
∃ ψ,
ψ 0 = 0 ∧
AnalyticAt ℂ ψ 0 ∧
∃ W ∈ nhds 0,
∀ᶠ (y :
ℂ ×
↥(TauCeti.CircleSobolev.supported s ℂ (Set.Ici 0)) ×
↥(TauCeti.CircleSobolev.supported s ℂ (Set.Ici 0))) in
nhds 0,
ψ y ∈ W ∧
∀ p ∈ W,
p ∈ TauCeti.CircleSobolev.neckGraph s ℂ y.1 ∧
(TauCeti.CircleSobolev.indicator (Set.Ici 0))
(TauCeti.CircleSobolev.nemytskii Complex.exp p.1) =
1 + ↑y.2.1 ∧
(TauCeti.CircleSobolev.indicator (Set.Ici 0))
(TauCeti.CircleSobolev.nemytskii Complex.exp p.2) =
1 + ↑y.2.2 ↔
p = ψ y
Lean
Formalized in Tau Ceti as TauCeti.CircleSobolev.exists_analyticAt_hardyGraph.
Sources
TheoremPeetre's inequality (TauCeti.CircleSobolev.weight_add_le)#
(1 + |m + n|) ^ s ≤ (1 + |m|) ^ |s| (1 + |n|) ^ s for every real
s. Shifting frequencies by m therefore changes the weights of every order s by at most the
factor (1 + |m|) ^ |s|.
TauCeti.CircleSobolev.weight_add_le (s : ℝ) (m n : ℤ) :
TauCeti.CircleSobolev.weight s (m + n) ≤
TauCeti.CircleSobolev.weight |s| m * TauCeti.CircleSobolev.weight s n
Used by 1
TheoremRellich's theorem on the circle#
the inclusion H^s → H^t is a compact operator for
t < s when E is finite-dimensional.
TauCeti.CircleSobolev.isCompactOperator_inclusion.{u_1} {s t : ℝ} {E : Type u_1}
[NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] (h : t < s) :
IsCompactOperator ⇑(TauCeti.CircleSobolev.inclusion ⋯)
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.