Module

LaurentBaseChange.lean

Nyll.AlgebraicCurves.FunctionFields.LaurentBaseChange

15 declarations indexed from sourceView source ↗

Module documentation

Laurent Base Change

Imports2

Mathlib.RingTheory.LaurentSeries
Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Imported by6

def

coeffMap

L32 ↗

ModularCurve.coeffMap

Documentation

The homomorphism of Laurent series induced by a homomorphism of coefficient rings.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open HahnSeries IntermediateField
namespace ModularCurve
section CoeffMap
variable {R S T : Type*} [CommRing R] [CommRing S] [CommRing T]

Lean source · full declaration

def coeffMap (f : R →+* S) : LaurentSeries R →+* LaurentSeries S where
  toFun x := x.map f
  map_zero' := by
    ext k
    simp
  map_one' := by
    ext k
    simp [HahnSeries.coeff_one, apply_ite f]
  map_add' x y := by
    ext k
    simp
  map_mul' x y := by
    have h := HahnSeries.map_mul (f := (f : R →ₙ+* S)) (x := x) (y := y)
    have hx : ∀ z : LaurentSeries R, z.map (f : R →ₙ+* S) = z.map f := fun z =>
      HahnSeries.ext rfl
    rwa [hx, hx, hx] at h

theorem

coeffMap_coeff

L49 ↗

ModularCurve.coeffMap_coeff

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open HahnSeries IntermediateField
namespace ModularCurve
section CoeffMap
variable {R S T : Type*} [CommRing R] [CommRing S] [CommRing T]

Lean source · statement

theorem coeffMap_coeff (f : R →+* S) (x : LaurentSeries R) (k : ℤ) :
    (coeffMap f x).coeff k = f (x.coeff k)

theorem

coeffMap_single

L53 ↗

ModularCurve.coeffMap_single

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open HahnSeries IntermediateField
namespace ModularCurve
section CoeffMap
variable {R S T : Type*} [CommRing R] [CommRing S] [CommRing T]

Lean source · statement

theorem coeffMap_single (f : R →+* S) (k : ℤ) (r : R) :
    coeffMap f (HahnSeries.single k r) = HahnSeries.single k (f r)

theorem

coeffMap_coeffMap

L60 ↗

ModularCurve.coeffMap_coeffMap

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open HahnSeries IntermediateField
namespace ModularCurve
section CoeffMap
variable {R S T : Type*} [CommRing R] [CommRing S] [CommRing T]

Lean source · statement

theorem coeffMap_coeffMap (g : S →+* T) (f : R →+* S) (x : LaurentSeries R) :
    coeffMap g (coeffMap f x) = coeffMap (g.comp f) x

theorem

coeffMap_id

L65 ↗

ModularCurve.coeffMap_id

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open HahnSeries IntermediateField
namespace ModularCurve
section CoeffMap
variable {R S T : Type*} [CommRing R] [CommRing S] [CommRing T]

Lean source · statement

theorem coeffMap_id (x : LaurentSeries R) : coeffMap (RingHom.id R) x = x

theorem

coeffMap_congr

L69 ↗

ModularCurve.coeffMap_congr

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open HahnSeries IntermediateField
namespace ModularCurve
section CoeffMap
variable {R S T : Type*} [CommRing R] [CommRing S] [CommRing T]

Lean source · statement

theorem coeffMap_congr {f g : R →+* S} (h : f = g) (x : LaurentSeries R) :
    coeffMap f x = coeffMap g x

theorem

algebraMap_laurentSeries_eq_single

L79 ↗

ModularCurve.algebraMap_laurentSeries_eq_single

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open HahnSeries IntermediateField
namespace ModularCurve
section Constants
variable (L : Type*) [Field L]

Lean source · statement

theorem algebraMap_laurentSeries_eq_single (c : L) :
    algebraMap L (LaurentSeries L) c = HahnSeries.single 0 c

theorem

coeffMap_algebraMap

L87 ↗

ModularCurve.coeffMap_algebraMap

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open HahnSeries IntermediateField
namespace ModularCurve
section Constants
variable (L : Type*) [Field L]
variable {L} in

Lean source · statement

theorem coeffMap_algebraMap (φ : L →+* L) (c : L) :
    coeffMap φ (algebraMap L (LaurentSeries L) c) = algebraMap L (LaurentSeries L) (φ c)

def

coeffEmb

L95 ↗

ModularCurve.coeffEmb

Documentation

The inclusion of rational-coefficient Laurent series into Laurent series over the extension field.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open HahnSeries IntermediateField
namespace ModularCurve
section Constants
variable (L : Type*) [Field L]
variable {L} in
variable [Algebra ℚ L]

Lean source · statement

def coeffEmb : LaurentSeries ℚ →+* LaurentSeries L

theorem

coeffEmb_coeff

L98 ↗

ModularCurve.coeffEmb_coeff

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open HahnSeries IntermediateField
namespace ModularCurve
section Constants
variable (L : Type*) [Field L]
variable {L} in
variable [Algebra ℚ L]

Lean source · statement

theorem coeffEmb_coeff (x : LaurentSeries ℚ) (k : ℤ) :
    (coeffEmb L x).coeff k = algebraMap ℚ L (x.coeff k)

theorem

coeffMap_coeffEmb

L103 ↗

ModularCurve.coeffMap_coeffEmb

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open HahnSeries IntermediateField
namespace ModularCurve
section Constants
variable (L : Type*) [Field L]
variable {L} in
variable [Algebra ℚ L]
variable {L} in

Lean source · statement

theorem coeffMap_coeffEmb (σ : L ≃ₐ[ℚ] L) (x : LaurentSeries ℚ) :
    coeffMap (σ : L →+* L) (coeffEmb L x) = coeffEmb L x

def

laurentBaseChange

L116 ↗

ModularCurve.laurentBaseChange

Documentation

The intermediate field generated after extending the coefficients of the Laurent series.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open HahnSeries IntermediateField
namespace ModularCurve
section BaseChange
variable (L : Type*) [Field L] [Algebra ℚ L]
variable (F₀ : IntermediateField ℚ (LaurentSeries ℚ))

Lean source · statement

def laurentBaseChange : IntermediateField L (LaurentSeries L)

theorem

coeffEmb_mem_laurentBaseChange

L120 ↗

ModularCurve.coeffEmb_mem_laurentBaseChange

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open HahnSeries IntermediateField
namespace ModularCurve
section BaseChange
variable (L : Type*) [Field L] [Algebra ℚ L]
variable (F₀ : IntermediateField ℚ (LaurentSeries ℚ))
variable {F₀} in

Lean source · statement

theorem coeffEmb_mem_laurentBaseChange {x : LaurentSeries ℚ} (hx : x ∈ F₀) :
    coeffEmb L x ∈ laurentBaseChange L F₀

theorem

mem_laurentBaseChange_iff

L125 ↗

ModularCurve.mem_laurentBaseChange_iff

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open HahnSeries IntermediateField
namespace ModularCurve
section BaseChange
variable (L : Type*) [Field L] [Algebra ℚ L]
variable (F₀ : IntermediateField ℚ (LaurentSeries ℚ))
variable {F₀} in
variable {L F₀} in

Lean source · statement

theorem mem_laurentBaseChange_iff {x : LaurentSeries L} :
    x ∈ laurentBaseChange L F₀ ↔
      x ∈ Subfield.closure
        (Set.range (algebraMap L (LaurentSeries L)) ∪
          (⇑(coeffEmb L) '' (F₀ : Set (LaurentSeries ℚ))))

theorem

coeffMap_mem_laurentBaseChange

L133 ↗

ModularCurve.coeffMap_mem_laurentBaseChange

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open HahnSeries IntermediateField
namespace ModularCurve
section BaseChange
variable (L : Type*) [Field L] [Algebra ℚ L]
variable (F₀ : IntermediateField ℚ (LaurentSeries ℚ))
variable {F₀} in
variable {L F₀} in
variable {L F₀} in

Lean source · statement

theorem coeffMap_mem_laurentBaseChange (σ : L ≃ₐ[ℚ] L) {x : LaurentSeries L}
    (hx : x ∈ laurentBaseChange L F₀) :
    coeffMap (σ : L →+* L) x ∈ laurentBaseChange L F₀

Module documentation

Laurent Base Change

Declarations