PoleData.lean

structure PoleDivisorPackage (K F : Type*) [Field K] [Field F] [Algebra K F] where
  /-- The function whose nonnegative powers are used in the independent family. -/
  x : F
  /-- The effective divisor bounding the poles of the chosen function. -/
  B : Divisor K F
  /-- The pole bound is an effective divisor. -/
  hB_eff : 0 ≤ B
  /-- The chosen function belongs to the Riemann space of the pole bound. -/
  hx_mem : x ∈ LSpace B
  /-- The positive degree of the pole bound and the size of the bounded function family. -/
  n : ℕ
  /-- The degree parameter is positive. -/
  hn_pos : 0 < n
  /-- The degree of the pole bound equals the chosen parameter. -/
  degB_eq : Divisor.degree B = n
  /-- The multiple of the pole bound containing the bounded function family. -/
  c : ℕ
  /-- The finite family of functions used with powers of the chosen function. -/
  u : Fin n → F
  /-- Every member of the finite family lies in the specified Riemann space. -/
  hu_mem : ∀ i, u i ∈ LSpace (c • B)
  /-- Products of powers of the chosen function with the finite family are linearly
  independent. -/
  lin_indep : LinearIndependent K (fun p : ℕ × Fin n => x ^ p.1 * u p.2)

def HasPoleDivisorPackage (K F : Type*) [Field K] [Field F] [Algebra K F] : Prop

structure TranscendenceTower (K E F : Type*) [Field K] [Field E] [Field F]
    [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F] where
  /-- The coordinate function in the intermediate field. -/
  x : E
  /-- The nonnegative coordinate powers are linearly independent over the base field. -/
  hx_indep : LinearIndependent K (fun j : ℕ => x ^ j)
  /-- The intermediate-field place carrying the coordinate pole. -/
  v : Place K E
  /-- The coordinate pole lies at a place of degree one. -/
  hvdeg : v.deg = 1
  /-- The coordinate has a simple pole at the selected place. -/
  hxv : v.ord x = -1
  /-- The coordinate has nonnegative order at every other place. -/
  hxreg : ∀ u : Place K E, u ≠ v → 0 ≤ u.ord x

abbrev xF : F

def poleDivisor [Algebra.IsSeparable E F] [HasPrincipalDivisors K F] : Divisor K F

def RegularOutside (A : Type*) [CommRing A] [Algebra A E] (T : TranscendenceTower K E F) : Prop

structure IntegralBasisInLSpace [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
    (T : TranscendenceTower K E F) where
  /-- The multiple of the tower pole divisor bounding the family. -/
  c : ℕ
  /-- The family indexed by the extension finrank. -/
  u : Fin (Module.finrank E F) → F
  /-- The family is linearly independent over the intermediate field. -/
  hu_indep : LinearIndependent E u
  /-- Every family member belongs to the chosen bounded Riemann space. -/
  hu_mem : ∀ i, u i ∈ LSpace (c • T.poleDivisor)

def HasIntegralBasisInLSpace [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
    (T : TranscendenceTower K E F) : Prop

def HasIntegralBasisRegularOutside [Algebra.IsSeparable E F] (T : TranscendenceTower K E F) :
  Prop

def HasRegularFractionSubring (T : TranscendenceTower K E F) : Prop