Module

Place_exists_comap_algebraMap_eq_of_constantFieldExtension_of_isAlgClosed.lean

Nyll.AlgebraicCurves.Places.Place_exists_comap_algebraMap_eq_of_constantFieldExtension_of_isAlgClosed

26 declarations indexed from sourceView source ↗

Module documentation

Place exists comap algebra Map eq of constant Field Extension of is Alg Closed

Imports7

Imported by8

theorem

ord_nonneg_of_mem

L37 ↗

AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed.W7XUnram.ord_nonneg_of_mem

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
namespace W7XUnram
section Basic
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem ord_nonneg_of_mem {f : F} (hf : f ∈ v.toValuationSubring) : 0 ≤ v.ord f

theorem

ord_eq_zero_of_mem_of_inv_mem

L52 ↗

AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed.W7XUnram.ord_eq_zero_of_mem_of_inv_mem

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
namespace W7XUnram
section Basic
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem ord_eq_zero_of_mem_of_inv_mem {f : F} (h1 : f ∈ v.toValuationSubring)
    (h2 : f⁻¹ ∈ v.toValuationSubring) : v.ord f = 0

theorem

one_le_ord_of_mem_of_inv_not_mem

L59 ↗

AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed.W7XUnram.one_le_ord_of_mem_of_inv_not_mem

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
namespace W7XUnram
section Basic
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem one_le_ord_of_mem_of_inv_not_mem {f : F} (h1 : f ∈ v.toValuationSubring)
    (h2 : f⁻¹ ∉ v.toValuationSubring) : 1 ≤ v.ord f

theorem

mem_iff_ord_nonneg

L76 ↗

AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed.W7XUnram.mem_iff_ord_nonneg

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
namespace W7XUnram
section Basic
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem mem_iff_ord_nonneg (f : F) : f ∈ v.toValuationSubring ↔ 0 ≤ v.ord f

theorem

ord_algebraMap_eq_zero

L85 ↗

AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed.W7XUnram.ord_algebraMap_eq_zero

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
namespace W7XUnram
section Basic
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem ord_algebraMap_eq_zero {L : Type*} [Field L] [Algebra F L] {K' : Type*} [Field K']
    [Algebra K' L] (w : Place K' L) {f : F}
    (h1 : algebraMap F L f ∈ w.toValuationSubring)
    (h2 : algebraMap F L f⁻¹ ∈ w.toValuationSubring) : w.ord (algebraMap F L f) = 0

def

Psi

L102 ↗

AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed.W7XUnram.Psi

Documentation

The additive map summing the chosen basis elements with coefficients from the valuation subring.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
namespace W7XUnram
section Psi
variable {K F K' : Type*} (F' : Type*) [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  {ι : Type*} (B : Module.Basis ι K K') (P : Place K F)

Lean source · statement

def Psi : (ι →₀ P.toValuationSubring) →+ F'

theorem

Psi_single

L109 ↗

AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed.W7XUnram.Psi_single

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
namespace W7XUnram
section Psi
variable {K F K' : Type*} (F' : Type*) [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  {ι : Type*} (B : Module.Basis ι K K') (P : Place K F)
omit [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F'] in

Lean source · statement

theorem Psi_single (j : ι) (o : P.toValuationSubring) :
    Psi F' B P (Finsupp.single j o) = algebraMap K' F' (B j) * algebraMap F F' (o : F)

theorem

Psi_apply

L114 ↗

AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed.W7XUnram.Psi_apply

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
namespace W7XUnram
section Psi
variable {K F K' : Type*} (F' : Type*) [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  {ι : Type*} (B : Module.Basis ι K K') (P : Place K F)
omit [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F'] in

Lean source · full declaration

theorem Psi_apply (w : ι →₀ P.toValuationSubring) :
    Psi F' B P w = w.sum fun j o => algebraMap K' F' (B j) * algebraMap F F' (o : F) := by
  rw [Psi, Finsupp.liftAddHom_apply]
  rfl

theorem

Psi_smul

L120 ↗

AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed.W7XUnram.Psi_smul

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
namespace W7XUnram
section Psi
variable {K F K' : Type*} (F' : Type*) [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  {ι : Type*} (B : Module.Basis ι K K') (P : Place K F)
omit [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F'] in

Lean source · statement

theorem Psi_smul (s : P.toValuationSubring) (w : ι →₀ P.toValuationSubring) :
    Psi F' B P (s • w) = algebraMap F F' (s : F) * Psi F' B P w

def

pureW

L133 ↗

AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed.W7XUnram.pureW

Documentation

The valuation-ring coefficient vector associated to a constant-field element and an integral factor.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
namespace W7XUnram
section Psi
variable {K F K' : Type*} (F' : Type*) [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  {ι : Type*} (B : Module.Basis ι K K') (P : Place K F)

Lean source · statement

def pureW (d : K') (o : P.toValuationSubring) : ι →₀ P.toValuationSubring

theorem

Psi_pureW

L136 ↗

AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed.W7XUnram.Psi_pureW

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
namespace W7XUnram
section Psi
variable {K F K' : Type*} (F' : Type*) [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  {ι : Type*} (B : Module.Basis ι K K') (P : Place K F)

Lean source · statement

theorem Psi_pureW (d : K') (o : P.toValuationSubring) :
    Psi F' B P (pureW B P d o) = algebraMap K' F' d * algebraMap F F' (o : F)

theorem

Psi_mul_mem_range

L146 ↗

AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed.W7XUnram.Psi_mul_mem_range

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
namespace W7XUnram
section Psi
variable {K F K' : Type*} (F' : Type*) [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  {ι : Type*} (B : Module.Basis ι K K') (P : Place K F)

Lean source · statement

theorem Psi_mul_mem_range (w₁ w₂ : ι →₀ P.toValuationSubring) :
    ∃ w, Psi F' B P w = Psi F' B P w₁ * Psi F' B P w₂

def

rangePsi

L158 ↗

AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed.W7XUnram.rangePsi

Documentation

The subring formed by the values of the coefficient evaluation map.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
namespace W7XUnram
section Psi
variable {K F K' : Type*} (F' : Type*) [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  {ι : Type*} (B : Module.Basis ι K K') (P : Place K F)

Lean source · full declaration

def rangePsi : Subring F' where
  carrier := Set.range (Psi F' B P)
  mul_mem' := by
    rintro _ _ ⟨w₁, rfl⟩ ⟨w₂, rfl⟩
    exact Psi_mul_mem_range F' B P w₁ w₂
  one_mem' := ⟨pureW B P 1 1, by simp [Psi_pureW]⟩
  add_mem' := by
    rintro _ _ ⟨w₁, rfl⟩ ⟨w₂, rfl⟩
    exact ⟨w₁ + w₂, map_add _ _ _⟩
  zero_mem' := ⟨0, map_zero _⟩
  neg_mem' := by
    rintro _ ⟨w, rfl⟩
    exact ⟨-w, map_neg _ _⟩

theorem

mem_rangePsi_iff

L172 ↗

AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed.W7XUnram.mem_rangePsi_iff

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
namespace W7XUnram
section Psi
variable {K F K' : Type*} (F' : Type*) [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  {ι : Type*} (B : Module.Basis ι K K') (P : Place K F)

Lean source · statement

theorem mem_rangePsi_iff {y : F'} : y ∈ rangePsi F' B P ↔ ∃ w, Psi F' B P w = y

theorem

algebraMap_mem_rangePsi

L174 ↗

AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed.W7XUnram.algebraMap_mem_rangePsi

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
namespace W7XUnram
section Psi
variable {K F K' : Type*} (F' : Type*) [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  {ι : Type*} (B : Module.Basis ι K K') (P : Place K F)

Lean source · statement

theorem algebraMap_mem_rangePsi (d : K') : algebraMap K' F' d ∈ rangePsi F' B P

theorem

algebraMap_coe_mem_rangePsi

L177 ↗

AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed.W7XUnram.algebraMap_coe_mem_rangePsi

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
namespace W7XUnram
section Psi
variable {K F K' : Type*} (F' : Type*) [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  {ι : Type*} (B : Module.Basis ι K K') (P : Place K F)

Lean source · statement

theorem algebraMap_coe_mem_rangePsi (o : P.toValuationSubring) :
    algebraMap F F' (o : F) ∈ rangePsi F' B P

theorem

Psi_mem

L182 ↗

AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed.W7XUnram.Psi_mem

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
namespace W7XUnram
section Psi
variable {K F K' : Type*} (F' : Type*) [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  {ι : Type*} (B : Module.Basis ι K K') (P : Place K F)
omit [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F'] in

Lean source · statement

theorem Psi_mem {S : Type*} [SetLike S F'] [SubringClass S F'] (V : S)
    (hK : ∀ d : K', algebraMap K' F' d ∈ V)
    (hO : ∀ o : P.toValuationSubring, algebraMap F F' (o : F) ∈ V)
    (w : ι →₀ P.toValuationSubring) : Psi F' B P w ∈ V

def

fracPsi

L193 ↗

AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed.W7XUnram.fracPsi

Documentation

Elements expressible by the coefficient evaluation map after clearing a nonzero integral denominator.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
namespace W7XUnram
section Psi
variable {K F K' : Type*} (F' : Type*) [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  {ι : Type*} (B : Module.Basis ι K K') (P : Place K F)

Lean source · full declaration

def fracPsi : Subalgebra K' F' where
  carrier := {y | ∃ w, ∃ s : P.toValuationSubring, (s : F) ≠ 0 ∧
    y * algebraMap F F' (s : F) = Psi F' B P w}
  mul_mem' := by
    rintro y₁ y₂ ⟨w₁, s₁, hs₁, h₁⟩ ⟨w₂, s₂, hs₂, h₂⟩
    obtain ⟨w, hw⟩ := Psi_mul_mem_range F' B P w₁ w₂
    refine ⟨w, s₁ * s₂, by rw [MulMemClass.coe_mul]; exact mul_ne_zero hs₁ hs₂, ?_⟩
    rw [hw, ← h₁, ← h₂, MulMemClass.coe_mul, map_mul]
    ring
  one_mem' := ⟨pureW B P 1 1, 1, by simp, by simp [Psi_pureW]⟩
  add_mem' := by
    rintro y₁ y₂ ⟨w₁, s₁, hs₁, h₁⟩ ⟨w₂, s₂, hs₂, h₂⟩
    refine ⟨s₂ • w₁ + s₁ • w₂, s₁ * s₂, by rw [MulMemClass.coe_mul]; exact mul_ne_zero hs₁ hs₂, ?_⟩
    rw [map_add, Psi_smul, Psi_smul, ← h₁, ← h₂, MulMemClass.coe_mul, map_mul]
    ring
  zero_mem' := ⟨0, 1, by simp, by simp⟩
  algebraMap_mem' d := ⟨pureW B P d 1, 1, by simp, by simp [Psi_pureW]⟩

theorem

mem_fracPsi_iff

L211 ↗

AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed.W7XUnram.mem_fracPsi_iff

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
namespace W7XUnram
section Psi
variable {K F K' : Type*} (F' : Type*) [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  {ι : Type*} (B : Module.Basis ι K K') (P : Place K F)

Lean source · statement

theorem mem_fracPsi_iff {y : F'} : y ∈ fracPsi F' B P ↔ ∃ w, ∃ s : P.toValuationSubring,
    (s : F) ≠ 0 ∧ y * algebraMap F F' (s : F) = Psi F' B P w

theorem

algebraMap_mem_fracPsi

L214 ↗

AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed.W7XUnram.algebraMap_mem_fracPsi

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
namespace W7XUnram
section Psi
variable {K F K' : Type*} (F' : Type*) [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  {ι : Type*} (B : Module.Basis ι K K') (P : Place K F)

Lean source · statement

theorem algebraMap_mem_fracPsi (f : F) : algebraMap F F' f ∈ fracPsi F' B P

theorem

exists_mul_Psi_eq

L222 ↗

AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed.W7XUnram.exists_mul_Psi_eq

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
namespace W7XUnram
section Psi
variable {K F K' : Type*} (F' : Type*) [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  {ι : Type*} (B : Module.Basis ι K K') (P : Place K F)

Lean source · statement

theorem exists_mul_Psi_eq (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
    {z : F'} (hz : z ≠ 0) :
    ∃ w₁ w₂, Psi F' B P w₂ ≠ 0 ∧ z * Psi F' B P w₂ = Psi F' B P w₁

theorem

ne_zero_and_inv_mem_of_add

L243 ↗

AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed.W7XUnram.ne_zero_and_inv_mem_of_add

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
namespace W7XUnram

Lean source · statement

theorem ne_zero_and_inv_mem_of_add {L : Type*} [Field L] (V : ValuationSubring L) {a m p : L}
    (ha : a ∈ V) (hai : a⁻¹ ∈ V) (ha0 : a ≠ 0) (hm : m ∈ V) (hp : p ∈ V) (hpi : p⁻¹ ∉ V) :
    a + p * m ≠ 0 ∧ (a + p * m)⁻¹ ∈ V

theorem

exists_digit

L272 ↗

AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed.W7XUnram.exists_digit

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
namespace W7XUnram
section Decomp
variable {K F K' : Type*} (F' : Type*) [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  {ι : Type*} (B : Module.Basis ι K K') (P : Place K F)

Lean source · statement

theorem exists_digit [IsAlgClosed K] [IsCurveOver K F] {π : P.toValuationSubring}
    (hπ : Irreducible π) (o : P.toValuationSubring) :
    ∃ a : K, ∃ o' : P.toValuationSubring,
      o = algebraMap K P.toValuationSubring a + π * o' ∧ (o = 0 → o' = 0)

theorem

decomp

L292 ↗

AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed.W7XUnram.decomp

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
namespace W7XUnram
section Decomp
variable {K F K' : Type*} (F' : Type*) [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F']
  {ι : Type*} (B : Module.Basis ι K K') (P : Place K F)

Lean source · statement

theorem decomp [IsAlgClosed K] [IsCurveOver K F] {π : P.toValuationSubring} (hπ : Irreducible π)
    (w : ι →₀ P.toValuationSubring) (hw : w ≠ 0) :
    ∃ (k : ℕ) (d : K') (w' : ι →₀ P.toValuationSubring), d ≠ 0 ∧
      Psi F' B P w = algebraMap F F' (π : F) ^ k *
        (algebraMap K' F' d + algebraMap F F' (π : F) * Psi F' B P w')

theorem

sum_ne_of_not_mem_span

L378 ↗

AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed.W7XUnram.sum_ne_of_not_mem_span

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
namespace W7XUnram
section LinDisj
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F']
  [IsScalarTower K K' F'] [IsScalarTower K F F'] [IsAlgClosed K]

Lean source · statement

theorem sum_ne_of_not_mem_span
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    (hfg' : ∃ x : F', Transcendental K' x ∧
      FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
    (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
    {ι : Type*} (c : ι → K') (s : Finset ι) (o : ι → F) (y : F)
    (hy : y ∉ Submodule.span K (Set.range o)) :
    ∑ j ∈ s, algebraMap K' F' (c j) * algebraMap F F' (o j) ≠ algebraMap F F' y

theorem

exists_comap_algebraMap_eq_of_constantFieldExtension_of_isAlgClosed

L445 ↗

AlgebraicCurve.Place.exists_comap_algebraMap_eq_of_constantFieldExtension_of_isAlgClosed

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceComapConstantsAlgClosed
open AlgebraicCurve
open W7XUnram in

Lean source · statement

theorem
  _root_.AlgebraicCurve.Place.exists_comap_algebraMap_eq_of_constantFieldExtension_of_isAlgClosed
  (K F K' F' : Type*)
    [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
    [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
    [IsAlgClosed K]
    (hfg : ∃ x : F, Transcendental K x ∧ FiniteDimensional (IntermediateField.adjoin K ({x} : Set
      F)) F)
    (hfg' : ∃ x : F', Transcendental K' x ∧
      FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
    [IsCurveOver K F]
    (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
    (P : Place K F) :
    ∃ P' : Place K' F',
      P'.toValuationSubring.comap (algebraMap F F') = P.toValuationSubring ∧
      (∀ f : F, P'.ord (algebraMap F F' f) = P.ord f) ∧
      ∀ Q' : Place K' F',
        Q'.toValuationSubring.comap (algebraMap F F') = P.toValuationSubring → Q' = P'

Module documentation

Place exists comap algebra Map eq of constant Field Extension of is Alg Closed

Declarations