NYLL
Module

Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension.lean

Nyll.AlgebraicCurves.Places.Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension
16 declarations indexed from sourceView source ↗

Module documentation

Place eq of forall valuation sub lt one of constant Field Extension

Imports12
Imported by2

Declarations

theorem

mem_of_valuation_lt_one

L52 ↗
AlgebraicCurves.Places.Proofs.Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension.AlgebraicCurve.CentredPlaceRigidity.mem_of_valuation_lt_one
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open _root_.AlgebraicCurve
open scoped TensorProduct IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CentredPlaceRigidity
open _root_.AlgebraicCurve
section General
variable {E FE : Type*} [Field E] [Field FE] [Algebra E FE]
Lean source · statement
theorem mem_of_valuation_lt_one (P : Place E FE) {y : FE}
    (hy : P.toValuationSubring.valuation y < 1) : y ∈ P.toValuationSubring
theorem

adicValuation_lt_one_of_valuation_lt_one

L56 ↗
AlgebraicCurves.Places.Proofs.Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension.AlgebraicCurve.CentredPlaceRigidity.adicValuation_lt_one_of_valuation_lt_one
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open _root_.AlgebraicCurve
open scoped TensorProduct IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CentredPlaceRigidity
open _root_.AlgebraicCurve
section General
variable {E FE : Type*} [Field E] [Field FE] [Algebra E FE]
Lean source · statement
theorem adicValuation_lt_one_of_valuation_lt_one (P : Place E FE) {y : FE}
    (hy : P.toValuationSubring.valuation y < 1) : P.adicValuation y < 1
theorem

ord_ne_zero_of_valuation_lt_one

L62 ↗
AlgebraicCurves.Places.Proofs.Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension.AlgebraicCurve.CentredPlaceRigidity.ord_ne_zero_of_valuation_lt_one
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open _root_.AlgebraicCurve
open scoped TensorProduct IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CentredPlaceRigidity
open _root_.AlgebraicCurve
section General
variable {E FE : Type*} [Field E] [Field FE] [Algebra E FE]
Lean source · statement
theorem ord_ne_zero_of_valuation_lt_one (P : Place E FE) {y : FE} (hy0 : y ≠ 0)
    (hy : P.toValuationSubring.valuation y < 1) : P.ord y ≠ 0
theorem

eq_zero_of_valuation_algebraMap_lt_one

L67 ↗
AlgebraicCurves.Places.Proofs.Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension.AlgebraicCurve.CentredPlaceRigidity.eq_zero_of_valuation_algebraMap_lt_one
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open _root_.AlgebraicCurve
open scoped TensorProduct IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CentredPlaceRigidity
open _root_.AlgebraicCurve
section General
variable {E FE : Type*} [Field E] [Field FE] [Algebra E FE]
Lean source · statement
theorem eq_zero_of_valuation_algebraMap_lt_one (P : Place E FE) {c : E}
    (hc : P.toValuationSubring.valuation (algebraMap E FE c) < 1) : c = 0
theorem

centre_unique

L77 ↗
AlgebraicCurves.Places.Proofs.Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension.AlgebraicCurve.CentredPlaceRigidity.centre_unique
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open _root_.AlgebraicCurve
open scoped TensorProduct IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CentredPlaceRigidity
open _root_.AlgebraicCurve
section General
variable {E FE : Type*} [Field E] [Field FE] [Algebra E FE]
variable {K F : Type*} [Field K] [Field F] [Algebra K F] [Algebra K E] [Algebra F FE]
Lean source · statement
theorem centre_unique (P : Place E FE) {σ τ : F →ₐ[K] E}
    (hσ : ∀ f : F, P.toValuationSubring.valuation (algebraMap F FE f - algebraMap E FE (σ f)) < 1)
    (hτ : ∀ f : F, P.toValuationSubring.valuation (algebraMap F FE f - algebraMap E FE (τ f)) < 1) :
    σ = τ
theorem

algebraMap_mem_of_centred

L89 ↗
AlgebraicCurves.Places.Proofs.Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension.AlgebraicCurve.CentredPlaceRigidity.algebraMap_mem_of_centred
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open _root_.AlgebraicCurve
open scoped TensorProduct IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CentredPlaceRigidity
open _root_.AlgebraicCurve
section General
variable {E FE : Type*} [Field E] [Field FE] [Algebra E FE]
variable {K F : Type*} [Field K] [Field F] [Algebra K F] [Algebra K E] [Algebra F FE]
Lean source · statement
theorem algebraMap_mem_of_centred (P : Place E FE) {σ : F →ₐ[K] E}
    (hσ : ∀ f : F, P.toValuationSubring.valuation (algebraMap F FE f - algebraMap E FE (σ f)) < 1)
    (f : F) : algebraMap F FE f ∈ P.toValuationSubring
theorem

linearIndependent_pow_iff_transcendental

L99 ↗
AlgebraicCurves.Places.Proofs.Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension.AlgebraicCurve.CentredPlaceRigidity.linearIndependent_pow_iff_transcendental
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open _root_.AlgebraicCurve
open scoped TensorProduct IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CentredPlaceRigidity
open _root_.AlgebraicCurve
section Transcendental
Lean source · full declaration
theorem linearIndependent_pow_iff_transcendental {R A : Type*} [CommRing R] [Ring A]
    [Algebra R A] (x : A) :
    LinearIndependent R (fun n : ℕ => x ^ n) ↔ Transcendental R x := by
  have h := Polynomial.linearIndependent_powers_iff_aeval (Algebra.lmul R A x : A →ₗ[R] A) (1 : A)
  have h1 : (fun n : ℕ => ((Algebra.lmul R A x : A →ₗ[R] A) ^ n) (1 : A)) = fun n => x ^ n := by
    funext n
    rw [← map_pow, Algebra.coe_lmul_eq_mul, LinearMap.mul_apply', mul_one]
  rw [h1] at h
  rw [h, Transcendental, isAlgebraic_iff_not_injective, not_not, injective_iff_map_eq_zero]
  refine forall_congr' fun p => ?_
  rw [Polynomial.aeval_algHom_apply, Algebra.coe_lmul_eq_mul, LinearMap.mul_apply', mul_one]
theorem

span_eq_top_of_adjoin_eq_top

L115 ↗
AlgebraicCurves.Places.Proofs.Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension.AlgebraicCurve.CentredPlaceRigidity.span_eq_top_of_adjoin_eq_top
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open _root_.AlgebraicCurve
open scoped TensorProduct IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CentredPlaceRigidity
open _root_.AlgebraicCurve
section Span
Lean source · statement
theorem span_eq_top_of_adjoin_eq_top {E L M : Type*} [Field E] [Field L] [Field M] [Algebra E L]
    [Algebra L M] [Algebra E M] [IsScalarTower E L M] {ι : Type*} [Finite ι] (b : ι → M)
    (hmul : ∀ i j, b i * b j ∈ Submodule.span L (Set.range b))
    (h1 : (1 : M) ∈ Submodule.span L (Set.range b))
    {T : Set M} (hT : T ⊆ Submodule.span L (Set.range b))
    (hgen : IntermediateField.adjoin E T = ⊤) :
    Submodule.span L (Set.range b) = ⊤
theorem

transcendental_algebraMap

L167 ↗
AlgebraicCurves.Places.Proofs.Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension.AlgebraicCurve.CentredPlaceRigidity.transcendental_algebraMap
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open _root_.AlgebraicCurve
open scoped TensorProduct IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CentredPlaceRigidity
open _root_.AlgebraicCurve
section Setup
variable {K F E FE : Type*} [Field K] [Field F] [Algebra K F] [Field E] [Field FE]
  [Algebra K E] [Algebra E FE] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE]
  [IsScalarTower K F FE]
Lean source · statement
theorem transcendental_algebraMap [IsAlgClosed K] [CharZero K]
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    (hfgE : ∃ x : FE, Transcendental E x ∧
      FiniteDimensional (IntermediateField.adjoin E ({x} : Set FE)) FE)
    (hgen : IntermediateField.adjoin E (Set.range (algebraMap F FE)) = ⊤)
    {x : F} (hx : Transcendental K x) : Transcendental E (algebraMap F FE x)
def

mulMap

L185 ↗
AlgebraicCurves.Places.Proofs.Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension.AlgebraicCurve.CentredPlaceRigidity.mulMap
Documentation

The tensor-product map multiplying the images of the two fields in their common extension.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open _root_.AlgebraicCurve
open scoped TensorProduct IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CentredPlaceRigidity
open _root_.AlgebraicCurve
section Setup
variable {K F E FE : Type*} [Field K] [Field F] [Algebra K F] [Field E] [Field FE]
  [Algebra K E] [Algebra E FE] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE]
  [IsScalarTower K F FE]
variable (K F E FE) in
Lean source · statement
def mulMap : E ⊗[K] F →ₐ[E] FE
theorem

mulMap_tmul

L189 ↗
AlgebraicCurves.Places.Proofs.Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension.AlgebraicCurve.CentredPlaceRigidity.mulMap_tmul
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open _root_.AlgebraicCurve
open scoped TensorProduct IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CentredPlaceRigidity
open _root_.AlgebraicCurve
section Setup
variable {K F E FE : Type*} [Field K] [Field F] [Algebra K F] [Field E] [Field FE]
  [Algebra K E] [Algebra E FE] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE]
  [IsScalarTower K F FE]
variable (K F E FE) in
Lean source · statement
theorem mulMap_tmul (c : E) (f : F) :
    mulMap K F E FE (c ⊗ₜ f) = algebraMap E FE c * algebraMap F FE f
def

evalMap

L193 ↗
AlgebraicCurves.Places.Proofs.Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension.AlgebraicCurve.CentredPlaceRigidity.evalMap
Documentation

The tensor-product evaluation map induced by the given base-field embedding.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open _root_.AlgebraicCurve
open scoped TensorProduct IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CentredPlaceRigidity
open _root_.AlgebraicCurve
section Setup
variable {K F E FE : Type*} [Field K] [Field F] [Algebra K F] [Field E] [Field FE]
  [Algebra K E] [Algebra E FE] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE]
  [IsScalarTower K F FE]
variable (K F E FE) in
Lean source · statement
def evalMap (e : F →ₐ[K] E) : E ⊗[K] F →ₐ[E] E
theorem

evalMap_tmul

L196 ↗
AlgebraicCurves.Places.Proofs.Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension.AlgebraicCurve.CentredPlaceRigidity.evalMap_tmul
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open _root_.AlgebraicCurve
open scoped TensorProduct IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CentredPlaceRigidity
open _root_.AlgebraicCurve
section Setup
variable {K F E FE : Type*} [Field K] [Field F] [Algebra K F] [Field E] [Field FE]
  [Algebra K E] [Algebra E FE] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE]
  [IsScalarTower K F FE]
variable (K F E FE) in
Lean source · statement
theorem evalMap_tmul (e : F →ₐ[K] E) (c : E) (f : F) : evalMap e (c ⊗ₜ f) = c * e f
theorem

mulMap_injective

L198 ↗
AlgebraicCurves.Places.Proofs.Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension.AlgebraicCurve.CentredPlaceRigidity.mulMap_injective
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open _root_.AlgebraicCurve
open scoped TensorProduct IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CentredPlaceRigidity
open _root_.AlgebraicCurve
section Setup
variable {K F E FE : Type*} [Field K] [Field F] [Algebra K F] [Field E] [Field FE]
  [Algebra K E] [Algebra E FE] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE]
  [IsScalarTower K F FE]
variable (K F E FE) in
Lean source · full declaration
theorem mulMap_injective
    (hli : LinearIndependent E (fun i => algebraMap F FE (Module.Basis.ofVectorSpace K F i))) :
    Function.Injective (mulMap K F E FE) := by
  classical
  let bE := Algebra.TensorProduct.basis E (Module.Basis.ofVectorSpace K F)
  rw [injective_iff_map_eq_zero]
  intro z hz
  have hrepr : Finsupp.linearCombination E bE (bE.repr z) = z := bE.linearCombination_repr z
  have hcomp : ((mulMap K F E FE).toLinearMap : E ⊗[K] F →ₗ[E] FE) ∘ bE =
      fun i => algebraMap F FE (Module.Basis.ofVectorSpace K F i) := by
    funext i
    simp [bE, Algebra.TensorProduct.basis_apply]
  have h0 : Finsupp.linearCombination E (fun i => algebraMap F FE (Module.Basis.ofVectorSpace K F
    i))
      (bE.repr z) = 0 := by
    rw [← hcomp, ← Finsupp.apply_linearCombination, hrepr]
    exact hz
  have hc : bE.repr z = 0 := hli (by rw [map_zero]; exact h0)
  rw [← hrepr, hc, map_zero]
theorem

exists_centred

L218 ↗
AlgebraicCurves.Places.Proofs.Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension.AlgebraicCurve.CentredPlaceRigidity.exists_centred
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open _root_.AlgebraicCurve
open scoped TensorProduct IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CentredPlaceRigidity
open _root_.AlgebraicCurve
section Setup
variable {K F E FE : Type*} [Field K] [Field F] [Algebra K F] [Field E] [Field FE]
  [Algebra K E] [Algebra E FE] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE]
  [IsScalarTower K F FE]
variable (K F E FE) in
Lean source · statement
theorem exists_centred [IsAlgClosed K] [CharZero K]
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    (hfgE : ∃ x : FE, Transcendental E x ∧
      FiniteDimensional (IntermediateField.adjoin E ({x} : Set FE)) FE)
    (hgen : IntermediateField.adjoin E (Set.range (algebraMap F FE)) = ⊤)
    (e : F →ₐ[K] E) :
    ∃ P : Place E FE, ∀ f : F,
      P.toValuationSubring.valuation (algebraMap F FE f - algebraMap E FE (e f)) < 1
theorem

eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension

L278 ↗
AlgebraicCurve.Place.eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open _root_.AlgebraicCurve
open scoped TensorProduct IntermediateField
open AlgebraicCurve.CentredPlaceRigidity in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.eq_of_forall_valuation_sub_lt_one_of_constantFieldExtension
    (K F : Type*) [Field K] [Field F] [Algebra K F] [IsAlgClosed K] [CharZero K] [IsCurveOver K F]
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    (E FE : Type*) [Field E] [Field FE] [Algebra K E] [Algebra E FE] [Algebra F FE] [Algebra K FE]
    [IsScalarTower K E FE] [IsScalarTower K F FE] [IsAlgClosed E] [IsCurveOver E FE]
    (hfgE : ∃ x : FE, Transcendental E x ∧
      FiniteDimensional (IntermediateField.adjoin E ({x} : Set FE)) FE)
    (hgen : IntermediateField.adjoin E (Set.range (algebraMap F FE)) = ⊤)
    (e : F →ₐ[K] E) (P Q : Place E FE)
    (hP : ∀ f : F, P.toValuationSubring.valuation (algebraMap F FE f - algebraMap E FE (e f)) < 1)
    (hQ : ∀ f : F, Q.toValuationSubring.valuation (algebraMap F FE f - algebraMap E FE (e f)) < 1) :
    P = Q

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.