Module

Basic.lean

Nyll.AlgebraicCurves.Places.Rational.Basic

41 declarations indexed from sourceView source ↗

Module documentation

Basic

Polynomial primes and points define finite places of a rational function field, with residue-field comparisons and transport along field equivalences.

Imports6

Mathlib.Data.Int.ConditionallyCompleteOrder
Mathlib.FieldTheory.RatFunc.Basic
Mathlib.RingTheory.Henselian
Mathlib.RingTheory.RegularLocalRing.Defs
Mathlib.RingTheory.SimpleRing.Principal
Nyll.AlgebraicCurves.Divisors.ClassGroup

Imported by118

theorem

adicValuation_valuationSubring

L39 ↗

AlgebraicCurve.Place.adicValuation_valuationSubring

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem adicValuation_valuationSubring :
    v.adicValuation.valuationSubring = v.toValuationSubring

theorem

mem_iff_adicValuation_le_one

L50 ↗

AlgebraicCurve.Place.mem_iff_adicValuation_le_one

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem mem_iff_adicValuation_le_one {f : F} :
    f ∈ v.toValuationSubring ↔ v.adicValuation f ≤ 1

instance

(anonymous instance)

L55 ↗

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

instance : v.adicValuation.IsRankOneDiscrete

instance

(anonymous instance)

L58 ↗

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

instance : v.adicValuation.IsTrivialOn K

theorem

isEquiv_adicValuation_of_valuationSubring_eq

L62 ↗

AlgebraicCurve.Place.isEquiv_adicValuation_of_valuationSubring_eq

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem isEquiv_adicValuation_of_valuationSubring_eq {Γ : Type*}
    [LinearOrderedCommGroupWithZero Γ] {w : Valuation F Γ}
    (h : w.valuationSubring = v.toValuationSubring) : w.IsEquiv v.adicValuation

theorem

mem_maximalIdeal_iff_adicValuation_lt_one

L68 ↗

AlgebraicCurve.Place.mem_maximalIdeal_iff_adicValuation_lt_one

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem mem_maximalIdeal_iff_adicValuation_lt_one (a : v.toValuationSubring) :
    a ∈ IsLocalRing.maximalIdeal v.toValuationSubring ↔ v.adicValuation (a : F) < 1

theorem

ord_eq_zero_iff_adicValuation_eq_one

L75 ↗

AlgebraicCurve.Place.ord_eq_zero_iff_adicValuation_eq_one

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem ord_eq_zero_iff_adicValuation_eq_one {f : F} (hf : f ≠ 0) :
    v.ord f = 0 ↔ v.adicValuation f = 1

theorem

isEquiv_adicValuation_ofHeightOneSpectrum

L91 ↗

AlgebraicCurve.Place.isEquiv_adicValuation_ofHeightOneSpectrum

Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
section OfHeightOneSpectrum
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
  [Algebra K R] [IsScalarTower K R F]

Lean source · statement

theorem isEquiv_adicValuation_ofHeightOneSpectrum (w : HeightOneSpectrum R) :
    (w.valuation F).IsEquiv (ofHeightOneSpectrum (K := K) w).adicValuation

theorem

ofHeightOneSpectrum_injective

L95 ↗

AlgebraicCurve.Place.ofHeightOneSpectrum_injective

Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
section OfHeightOneSpectrum
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
  [Algebra K R] [IsScalarTower K R F]

Lean source · statement

theorem ofHeightOneSpectrum_injective :
    Function.Injective (ofHeightOneSpectrum (K := K) (F := F) (R := R))

theorem

ord_ofHeightOneSpectrum_ne_zero_iff

L103 ↗

AlgebraicCurve.Place.ord_ofHeightOneSpectrum_ne_zero_iff

Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
section OfHeightOneSpectrum
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
  [Algebra K R] [IsScalarTower K R F]

Lean source · statement

theorem ord_ofHeightOneSpectrum_ne_zero_iff (w : HeightOneSpectrum R) {q : R} (hq : q ≠ 0) :
    (ofHeightOneSpectrum (K := K) (F := F) w).ord (algebraMap R F q) ≠ 0 ↔ q ∈ w.asIdeal

def

heightOneSpectrumOfIrreducible

L120 ↗

AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible

Documentation

The height-one polynomial prime generated by the irreducible polynomial.

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K]

Lean source · full declaration

def heightOneSpectrumOfIrreducible {p : K[X]} (hp : Irreducible p) :
    HeightOneSpectrum K[X] where
  asIdeal := Ideal.span {p}
  isPrime := (PrincipalIdealRing.isMaximal_of_irreducible hp).isPrime
  ne_bot := by simpa [Ideal.span_singleton_eq_bot] using hp.ne_zero

theorem

heightOneSpectrumOfIrreducible_asIdeal

L126 ↗

AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K]

Lean source · statement

theorem heightOneSpectrumOfIrreducible_asIdeal {p : K[X]} (hp : Irreducible p) :
    (heightOneSpectrumOfIrreducible K hp).asIdeal = Ideal.span {p}

theorem

exists_irreducible_span

L129 ↗

AlgebraicCurve.RationalFunctionField.exists_irreducible_span

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K]

Lean source · statement

theorem exists_irreducible_span (w : HeightOneSpectrum K[X]) :
    ∃ p : K[X], Irreducible p ∧ w.asIdeal = Ideal.span {p}

def

finitePlace

L142 ↗

AlgebraicCurve.RationalFunctionField.finitePlace

Documentation

The finite rational-function-field place associated to the irreducible polynomial.

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K]

Lean source · statement

def finitePlace {p : K[X]} (hp : Irreducible p) : Place K (RatFunc K)

theorem

finitePlace_def

L145 ↗

AlgebraicCurve.RationalFunctionField.finitePlace_def

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K]

Lean source · statement

theorem finitePlace_def {p : K[X]} (hp : Irreducible p) :
    finitePlace K hp = Place.ofHeightOneSpectrum (heightOneSpectrumOfIrreducible K hp)

theorem

algebraMap_mem_ofHeightOneSpectrum

L150 ↗

AlgebraicCurve.RationalFunctionField.algebraMap_mem_ofHeightOneSpectrum

Source context 7 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K]
section ResidueDegree

Lean source · statement

theorem algebraMap_mem_ofHeightOneSpectrum (w : HeightOneSpectrum K[X]) (q : K[X]) :
    algebraMap K[X] (RatFunc K) q ∈
      (Place.ofHeightOneSpectrum (K := K) (F := RatFunc K) w).toValuationSubring

def

residueOfHeightOneSpectrum

L158 ↗

AlgebraicCurve.RationalFunctionField.residueOfHeightOneSpectrum

Documentation

The polynomial residue map to the residue field at the height-one place.

Source context 7 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K]
section ResidueDegree

Lean source · statement

def residueOfHeightOneSpectrum (w : HeightOneSpectrum K[X]) :
    K[X] →+* (Place.ofHeightOneSpectrum (K := K) (F := RatFunc K) w).ResidueField

theorem

residueOfHeightOneSpectrum_apply

L165 ↗

AlgebraicCurve.RationalFunctionField.residueOfHeightOneSpectrum_apply

Source context 7 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K]
section ResidueDegree

Lean source · statement

theorem residueOfHeightOneSpectrum_apply (w : HeightOneSpectrum K[X]) (q : K[X]) :
    residueOfHeightOneSpectrum K w q = IsLocalRing.residue _
      ⟨algebraMap K[X] (RatFunc K) q, algebraMap_mem_ofHeightOneSpectrum K w q⟩

theorem

ker_residueOfHeightOneSpectrum

L169 ↗

AlgebraicCurve.RationalFunctionField.ker_residueOfHeightOneSpectrum

Source context 7 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K]
section ResidueDegree

Lean source · statement

theorem ker_residueOfHeightOneSpectrum (w : HeightOneSpectrum K[X]) :
    RingHom.ker (residueOfHeightOneSpectrum K w) = w.asIdeal

theorem

surjective_residueOfHeightOneSpectrum

L178 ↗

AlgebraicCurve.RationalFunctionField.surjective_residueOfHeightOneSpectrum

Source context 7 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K]
section ResidueDegree

Lean source · statement

theorem surjective_residueOfHeightOneSpectrum (w : HeightOneSpectrum K[X]) :
    Function.Surjective (residueOfHeightOneSpectrum K w)

def

residueFieldEquivOfHeightOneSpectrum

L230 ↗

AlgebraicCurve.RationalFunctionField.residueFieldEquivOfHeightOneSpectrum

Documentation

The polynomial-prime quotient identified with the residue field of its place.

Source context 7 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K]
section ResidueDegree

Lean source · statement

def residueFieldEquivOfHeightOneSpectrum (w : HeightOneSpectrum K[X]) :
    (K[X] ⧸ w.asIdeal) ≃ₐ[K]
      (Place.ofHeightOneSpectrum (K := K) (F := RatFunc K) w).ResidueField

theorem

deg_ofHeightOneSpectrum

L244 ↗

AlgebraicCurve.RationalFunctionField.deg_ofHeightOneSpectrum

Source context 7 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K]
section ResidueDegree

Lean source · statement

theorem deg_ofHeightOneSpectrum {w : HeightOneSpectrum K[X]} {p : K[X]}
    (hw : w.asIdeal = Ideal.span {p}) :
    (Place.ofHeightOneSpectrum (K := K) (F := RatFunc K) w).deg = p.natDegree

theorem

deg_finitePlace

L250 ↗

AlgebraicCurve.RationalFunctionField.deg_finitePlace

Source context 7 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K]
section ResidueDegree

Lean source · statement

theorem deg_finitePlace {p : K[X]} (hp : Irreducible p) :
    (finitePlace K hp).deg = p.natDegree

def

placeOfPoint

L257 ↗

AlgebraicCurve.RationalFunctionField.placeOfPoint

Documentation

The finite place given by the linear polynomial vanishing at the chosen base-field point.

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K]

Lean source · statement

def placeOfPoint (a : K) : Place K (RatFunc K)

theorem

placeOfPoint_def

L260 ↗

AlgebraicCurve.RationalFunctionField.placeOfPoint_def

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K]

Lean source · statement

theorem placeOfPoint_def (a : K) :
    placeOfPoint K a = finitePlace K (irreducible_X_sub_C a)

theorem

placeOfPoint_eq_ofHeightOneSpectrum

L263 ↗

AlgebraicCurve.RationalFunctionField.placeOfPoint_eq_ofHeightOneSpectrum

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K]

Lean source · statement

theorem placeOfPoint_eq_ofHeightOneSpectrum (a : K) :
    placeOfPoint K a
      = Place.ofHeightOneSpectrum (heightOneSpectrumOfIrreducible K (irreducible_X_sub_C a))

theorem

placeOfPoint_injective

L268 ↗

AlgebraicCurve.RationalFunctionField.placeOfPoint_injective

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K]

Lean source · statement

theorem placeOfPoint_injective : Function.Injective (placeOfPoint K)

theorem

deg_placeOfPoint

L282 ↗

AlgebraicCurve.RationalFunctionField.deg_placeOfPoint

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K]

Lean source · statement

theorem deg_placeOfPoint (a : K) : (placeOfPoint K a).deg = 1

def

comapSymmRingEquiv

L295 ↗

AlgebraicCurve.Place.comapSymmRingEquiv

Documentation

The equivalence from a valuation subring to its transport under the field equivalence.

Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace Place
section Congr
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F')

Lean source · full declaration

def comapSymmRingEquiv (V : ValuationSubring F) :
    V ≃+* (V.comap (e.symm : F' →+* F)) where
  toFun x := ⟨e x, by
    rw [ValuationSubring.mem_comap]
    change e.symm (e x) ∈ V
    rw [e.symm_apply_apply]
    exact x.2⟩
  invFun y := ⟨e.symm y, y.2⟩
  left_inv x := by
    ext
    exact e.symm_apply_apply x
  right_inv y := by
    ext
    exact e.apply_symm_apply y
  map_mul' x y := by
    ext
    exact e.map_mul x y
  map_add' x y := by
    ext
    exact e.map_add x y

theorem

coe_comapSymmRingEquiv_apply

L316 ↗

AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply

Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace Place
section Congr
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F')

Lean source · statement

theorem coe_comapSymmRingEquiv_apply (V : ValuationSubring F) (x : V) :
    ((comapSymmRingEquiv e V x : (V.comap (e.symm : F' →+* F))) : F') = e x

theorem

symm_algebraMap_comm

L322 ↗

AlgebraicCurve.Place.symm_algebraMap_comm

Source context 10 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace Place
section Congr
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F')
variable (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include he

Lean source · statement

theorem symm_algebraMap_comm (a : K) : e.symm (algebraMap K F' a) = algebraMap K F a

def

congrRingEquiv

L326 ↗

AlgebraicCurve.Place.congrRingEquiv

Documentation

The place transported along a field equivalence compatible with the constant-field maps.

Source context 10 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace Place
section Congr
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F')
variable (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include he

Lean source · full declaration

def congrRingEquiv (v : Place K F) : Place K F' where
  toValuationSubring := v.toValuationSubring.comap (e.symm : F' →+* F)
  algebraMap_mem' a := by
    rw [ValuationSubring.mem_comap]
    change e.symm (algebraMap K F' a) ∈ v.toValuationSubring
    rw [symm_algebraMap_comm e he a]
    exact v.algebraMap_mem' a
  ne_top' := fun h =>
    v.ne_top' (SetLike.ext fun x =>
      ⟨fun _ => ValuationSubring.mem_top x, fun _ => by
        have hx : e x ∈ v.toValuationSubring.comap (e.symm : F' →+* F) := by
          rw [h]
          exact ValuationSubring.mem_top _
        rw [ValuationSubring.mem_comap] at hx
        have : e.symm (e x) ∈ v.toValuationSubring := hx
        rwa [e.symm_apply_apply] at this⟩)
  isPrincipalIdealRing' :=
    IsPrincipalIdealRing.of_surjective
      (comapSymmRingEquiv e v.toValuationSubring : _ ≃+* _)
      (comapSymmRingEquiv e v.toValuationSubring).surjective

theorem

congrRingEquiv_toValuationSubring

L347 ↗

AlgebraicCurve.Place.congrRingEquiv_toValuationSubring

Source context 10 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace Place
section Congr
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F')
variable (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include he

Lean source · statement

theorem congrRingEquiv_toValuationSubring (v : Place K F) :
    (congrRingEquiv e he v).toValuationSubring
      = v.toValuationSubring.comap (e.symm : F' →+* F)

def

congrValuationSubringEquiv

L352 ↗

AlgebraicCurve.Place.congrValuationSubringEquiv

Documentation

The induced equivalence between the original and transported valuation subrings.

Source context 10 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace Place
section Congr
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F')
variable (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include he

Lean source · full declaration

def congrValuationSubringEquiv (v : Place K F) :
    v.toValuationSubring ≃+* (congrRingEquiv e he v).toValuationSubring where
  toFun x := ⟨e x, by
    rw [congrRingEquiv_toValuationSubring, ValuationSubring.mem_comap]
    exact (comapSymmRingEquiv e v.toValuationSubring x).2⟩
  invFun y := ⟨e.symm y, by
    have hy : (y : F') ∈ v.toValuationSubring.comap (e.symm : F' →+* F) := by
      rw [← congrRingEquiv_toValuationSubring e he v]
      exact y.2
    rw [ValuationSubring.mem_comap] at hy
    exact hy⟩
  left_inv x := by
    ext
    exact e.symm_apply_apply x
  right_inv y := by
    ext
    exact e.apply_symm_apply y
  map_mul' x y := by
    ext
    exact e.map_mul x y
  map_add' x y := by
    ext
    exact e.map_add x y

theorem

coe_congrValuationSubringEquiv_apply

L376 ↗

AlgebraicCurve.Place.coe_congrValuationSubringEquiv_apply

Source context 10 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace Place
section Congr
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F')
variable (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include he

Lean source · statement

theorem coe_congrValuationSubringEquiv_apply (v : Place K F) (x : v.toValuationSubring) :
    ((congrValuationSubringEquiv e he v x :
      (congrRingEquiv e he v).toValuationSubring) : F') = e x

theorem

ord_congrRingEquiv

L380 ↗

AlgebraicCurve.Place.ord_congrRingEquiv

Source context 10 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace Place
section Congr
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F')
variable (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include he

Lean source · statement

theorem ord_congrRingEquiv (v : Place K F) (f : F) :
    (congrRingEquiv e he v).ord (e f) = v.ord f

def

congrResidueAlgEquiv

L400 ↗

AlgebraicCurve.Place.congrResidueAlgEquiv

Documentation

The induced base-field algebra equivalence between the residue fields.

Source context 10 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace Place
section Congr
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F')
variable (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include he

Lean source · statement

def congrResidueAlgEquiv (v : Place K F) :
    v.ResidueField ≃ₐ[K] (congrRingEquiv e he v).ResidueField

theorem

deg_congrRingEquiv

L416 ↗

AlgebraicCurve.Place.deg_congrRingEquiv

Source context 10 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace Place
section Congr
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F')
variable (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include he

Lean source · statement

theorem deg_congrRingEquiv (v : Place K F) : (congrRingEquiv e he v).deg = v.deg

def

congrEquiv

L420 ↗

AlgebraicCurve.Place.congrEquiv

Documentation

The equivalence of place sets induced by the compatible field equivalence.

Source context 10 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace Place
section Congr
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F')
variable (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include he

Lean source · full declaration

def congrEquiv : Place K F ≃ Place K F' where
  toFun := congrRingEquiv e he
  invFun := congrRingEquiv e.symm (symm_algebraMap_comm e he)
  left_inv v := by
    ext1
    refine SetLike.ext fun x => ?_
    change e.symm (e.symm.symm x) ∈ v.toValuationSubring ↔ x ∈ v.toValuationSubring
    rw [RingEquiv.symm_symm, e.symm_apply_apply]
  right_inv v := by
    ext1
    refine SetLike.ext fun x => ?_
    change e.symm.symm (e.symm x) ∈ v.toValuationSubring ↔ x ∈ v.toValuationSubring
    rw [RingEquiv.symm_symm, e.apply_symm_apply]

theorem

congrEquiv_apply

L434 ↗

AlgebraicCurve.Place.congrEquiv_apply

Source context 10 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace Place
section Congr
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F')
variable (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include he

Lean source · statement

theorem congrEquiv_apply (v : Place K F) : congrEquiv e he v = congrRingEquiv e he v

theorem

congrEquiv_symm_apply

L436 ↗

AlgebraicCurve.Place.congrEquiv_symm_apply

Source context 10 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace Place
section Congr
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F')
variable (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include he

Lean source · statement

theorem congrEquiv_symm_apply (v : Place K F') :
    (congrEquiv e he).symm v = congrRingEquiv e.symm (symm_algebraMap_comm e he) v

Module documentation

Basic

Declarations