MultiplierBundles.lean`

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Multiplier quotient actions, projections, topology, and local charts; The multiplicative complex torus as a period quotient

abbrev OAI.Nagata.W21.MultiplicativeLineCover line 24
Source documentation
The total space before taking the multiplicative-period quotient.
```
abbrev MultiplicativeLineCover (R : Type*) [CommMonoid R] := Rˣ × R
```
def OAI.Nagata.W21.multiplierStep line 28
Source documentation
The manuscript's generator (z,t) ↦ (τz, γz⁻ⁿt) as an actual equivalence. Units supply the inverse multiplier; invertibility is not assumed as a field.
```
def multiplierStep {R : Type*} [CommMonoid R] (τ γ : Rˣ) (n : ℤ) :
    Equiv.Perm (MultiplicativeLineCover R) where
…
```
Mentions: OAI.Nagata.W21.MultiplicativeLineCover
theorem OAI.Nagata.W21.multiplierStep_base line 43
theorem OAI.Nagata.W21.multiplierStep_fibre line 47
def OAI.Nagata.W21.multiplierIterate line 52
Source documentation
Every integer iterate exists because the generator has a proved inverse.
```
def multiplierIterate {R : Type*} [CommMonoid R] (τ γ : Rˣ) (n k : ℤ) :
    Equiv.Perm (MultiplicativeLineCover R) := multiplierStep τ γ n ^ k
```
Mentions: OAI.Nagata.W21.MultiplicativeLineCover, OAI.Nagata.W21.multiplierStep
theorem OAI.Nagata.W21.multiplierIterate_zero line 55
theorem OAI.Nagata.W21.multiplierIterate_add line 59
def OAI.Nagata.W21.multiplierOrbitSetoid line 66
Source documentation
Orbit relation of the explicit integer iterates.
```
def multiplierOrbitSetoid {R : Type*} [CommMonoid R] (τ γ : Rˣ) (n : ℤ) :
    Setoid (MultiplicativeLineCover R) where
…
```
Mentions: OAI.Nagata.W21.MultiplicativeLineCover
def OAI.Nagata.W21.MultiplierQuotient line 88
instance OAI.Nagata.W21.(instance at line 91) line 91
def OAI.Nagata.W21.torusOrbitSetoid line 105
Source documentation
Two covering-space points represent the same point exactly when they differ by an integer power of the period.
```
def torusOrbitSetoid {G : Type*} [CommGroup G] (τ : G) : Setoid G where
…
```
def OAI.Nagata.W21.TorusPoint line 121
Source documentation
The multiplicative quotient; for the source torus use G = ℂˣ.
```
def TorusPoint {G : Type*} [CommGroup G] (τ : G) : Type _ :=
…
```
def OAI.Nagata.W21.torusPointMk line 124
instance OAI.Nagata.W21.(instance at line 127) line 127
theorem OAI.Nagata.W21.torusPointMk_eq_iff line 130
theorem OAI.Nagata.W21.torusOrbitSetoid_iff_coe line 139
Source documentation
Bridge to the literal scalar equation used in the common logarithmic chart. The source's nonzero complex coordinates are represented by actual units.
```
theorem torusOrbitSetoid_iff_coe {R : Type*} [CommGroupWithZero R] (τ z z' : Rˣ) :
    torusOrbitSetoid τ z z' ↔ ∃ k : ℤ, (z' : R) = (τ : R) ^ k * (z : R) := by
…
```
Mentions: OAI.Nagata.W21.torusOrbitSetoid
theorem OAI.Nagata.W21.multiplierStep_inv_base line 159
theorem OAI.Nagata.W21.multiplierIterate_base line 164
Source documentation
Every iterate covers multiplication by the same power of the period.
```
theorem multiplierIterate_base {R : Type*} [CommMonoid R]
    (τ γ : Rˣ) (n k : ℤ) (p : MultiplicativeLineCover R) :
    (multiplierIterate τ γ n k p).1 = τ ^ k * p.1 := by
…
```
Mentions: OAI.Nagata.W21.MultiplicativeLineCover, OAI.Nagata.W21.multiplierIterate
def OAI.Nagata.W21.multiplierQuotientProjection line 191
Source documentation
Quotienting the scalar multiplier action preserves its projection to the base period quotient; this is not an asserted bundle structure.
```
def multiplierQuotientProjection {R : Type*} [CommMonoid R] (τ γ : Rˣ) (n : ℤ) :
    MultiplierQuotient τ γ n → TorusPoint τ :=
…
```
Mentions: OAI.Nagata.W21.MultiplierQuotient, OAI.Nagata.W21.TorusPoint
theorem OAI.Nagata.W21.multiplierQuotientProjection_mk line 200
theorem OAI.Nagata.W21.multiplierQuotientProjection_surjective line 205
Source documentation
Every base point has an actual point above it in the multiplier quotient.
```
theorem multiplierQuotientProjection_surjective {R : Type*} [CommMonoid R]
    (τ γ : Rˣ) (n : ℤ) : Function.Surjective (multiplierQuotientProjection τ γ n) := by
…
```
Mentions: OAI.Nagata.W21.multiplierQuotientProjection
instance OAI.Nagata.W21.torusPointTopologicalSpace line 220
instance OAI.Nagata.W21.multiplierQuotientTopologicalSpace line 224
theorem OAI.Nagata.W21.isQuotientMap_torusPointMk line 230
Source documentation
The base uses the actual quotient topology of its period relation.
```
theorem isQuotientMap_torusPointMk {G : Type*} [CommGroup G] [TopologicalSpace G]
    (τ : G) : Topology.IsQuotientMap (torusPointMk τ) :=
…
```
Mentions: OAI.Nagata.W21.torusPointMk
theorem OAI.Nagata.W21.continuous_torusPointMk line 234
theorem OAI.Nagata.W21.continuous_multiplierQuotientProjection line 239
Source documentation
The fibre projection is continuous for the two actual quotient topologies.
```
theorem continuous_multiplierQuotientProjection {R : Type*} [CommMonoid R]
    [TopologicalSpace R] [TopologicalSpace Rˣ] (τ γ : Rˣ) (n : ℤ) :
    Continuous (multiplierQuotientProjection τ γ n) := by
…
```
Mentions: OAI.Nagata.W21.multiplierQuotientProjection
theorem OAI.Nagata.W21.continuous_multiplierStep line 257
theorem OAI.Nagata.W21.continuous_multiplierStep_inv line 264
theorem OAI.Nagata.W21.continuous_multiplierIterate line 273
Source documentation
All deck transformations are continuous, including negative iterates.
```
theorem continuous_multiplierIterate (τ γ : Rˣ) (n k : ℤ) :
    Continuous (multiplierIterate τ γ n k) := by
…
```
Mentions: OAI.Nagata.W21.multiplierIterate
def OAI.Nagata.W21.multiplierQuotientMk line 299
Source documentation
Canonical projection from the covering surface to its multiplier orbit quotient.
```
def multiplierQuotientMk {R : Type*} [CommMonoid R] (τ γ : Rˣ) (n : ℤ)
    (p : MultiplicativeLineCover R) : MultiplierQuotient τ γ n := Quotient.mk _ p
```
Mentions: OAI.Nagata.W21.MultiplicativeLineCover, OAI.Nagata.W21.MultiplierQuotient
theorem OAI.Nagata.W21.multiplierQuotientMk_eq_iff line 302
theorem OAI.Nagata.W21.multiplierQuotientMk_preimage_image line 310
theorem OAI.Nagata.W21.isQuotientMap_multiplierQuotientMk line 327
theorem OAI.Nagata.W21.continuous_multiplierQuotientMk line 330
theorem OAI.Nagata.W21.isOpenMap_multiplierQuotientMk line 335
def OAI.Nagata.W21.multiplierLocalChart line 344
Source documentation
An injective open subset of the covering surface yields an actual local homeomorphism of the total multiplier quotient.
```
noncomputable def multiplierLocalChart (τ γ : Rˣ) (n : ℤ)
    (U : Set (MultiplicativeLineCover R)) (hU : IsOpen U)
    (hinj : Set.InjOn (multiplierQuotientMk τ γ n) U) :
    OpenPartialHomeomorph (MultiplicativeLineCover R) (MultiplierQuotient τ γ n) :=
…
```
Mentions: OAI.Nagata.W21.MultiplicativeLineCover, OAI.Nagata.W21.multiplierQuotientMk, OAI.Nagata.W21.MultiplierQuotient