NYLL
Module

Finrank_le_and_natCard_places_le_of_constantFieldExtension_adjoin.lean

Nyll.AlgebraicCurves.Places.Finrank_le_and_natCard_places_le_of_constantFieldExtension_adjoin
8 declarations indexed from sourceView source ↗

Module documentation

Finrank le and nat Card places le of constant Field Extension adjoin

Imports6
Imported by1

Declarations

theorem

linearIndependent_pow_of_transcendental

L40 ↗
AlgebraicCurves.Places.Proofs.Finrank_le_and_natCard_places_le_of_constantFieldExtension_adjoin.AlgebraicCurve.ConstantFieldAdjoin.linearIndependent_pow_of_transcendental
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Finrank_le_and_natCard_places_le_of_constantFieldExtension_adjoin
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstantFieldAdjoin
open _root_.AlgebraicCurve
section Main
Lean source · full declaration
theorem linearIndependent_pow_of_transcendental {k A : Type*} [Field k] [Ring A] [Algebra k A]
    {Y : A} (hY : Transcendental k Y) (N : ℕ) :
    LinearIndependent k (fun n : Fin N => Y ^ (n : ℕ)) := by
  classical
  rw [Fintype.linearIndependent_iff]
  intro a ha m
  have hinj := transcendental_iff_injective.mp hY
  have hpoly : Polynomial.aeval Y (∑ n : Fin N, Polynomial.monomial (n : ℕ) (a n)) = 0 := by
    rw [map_sum]
    simpa [Polynomial.aeval_monomial, Algebra.smul_def] using ha
  have hzero : (∑ n : Fin N, Polynomial.monomial (n : ℕ) (a n)) = 0 :=
    hinj (by rw [hpoly, map_zero])
  have hcoeff := congrArg (fun p : Polynomial k => p.coeff (m : ℕ)) hzero
  simp only [Polynomial.finsetSum_coeff, Polynomial.coeff_monomial, Polynomial.coeff_zero] at hcoeff
  rw [Finset.sum_eq_single m (fun n _ hn => ite_eq_right (fun h => hn (Fin.ext h)))
    (by simp)] at hcoeff
  simpa using hcoeff
theorem

exists_mul_aeval_eq

L64 ↗
AlgebraicCurves.Places.Proofs.Finrank_le_and_natCard_places_le_of_constantFieldExtension_adjoin.AlgebraicCurve.ConstantFieldAdjoin.exists_mul_aeval_eq
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Finrank_le_and_natCard_places_le_of_constantFieldExtension_adjoin
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstantFieldAdjoin
open _root_.AlgebraicCurve
section Main
variable {k : Type*} [Field k] [IsAlgClosed k] [CharZero k]
variable {F : Type*} [Field F] [Algebra k F]
variable {K' : Type*} [Field K'] [Algebra k K']
variable {L : Type*} [Field L] [Algebra K' L] (t : L) (E : IntermediateField K'⟮t⟯ L)
variable [Algebra F E] [Algebra k E] [IsScalarTower k K' E] [IsScalarTower k F E]
Lean source · statement
theorem exists_mul_aeval_eq (l : K'⟮t⟯) :
    ∃ p q : Polynomial K', Polynomial.aeval t q ≠ 0 ∧ (l : L) * Polynomial.aeval t q =
      Polynomial.aeval t p
theorem

finrank_le_finrank

L75 ↗
AlgebraicCurves.Places.Proofs.Finrank_le_and_natCard_places_le_of_constantFieldExtension_adjoin.AlgebraicCurve.ConstantFieldAdjoin.finrank_le_finrank
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Finrank_le_and_natCard_places_le_of_constantFieldExtension_adjoin
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstantFieldAdjoin
open _root_.AlgebraicCurve
section Main
variable {k : Type*} [Field k] [IsAlgClosed k] [CharZero k]
variable {F : Type*} [Field F] [Algebra k F]
variable {K' : Type*} [Field K'] [Algebra k K']
variable {L : Type*} [Field L] [Algebra K' L] (t : L) (E : IntermediateField K'⟮t⟯ L)
variable [Algebra F E] [Algebra k E] [IsScalarTower k K' E] [IsScalarTower k F E]
Lean source · statement
theorem finrank_le_finrank (y : F) (hy : Transcendental k y) [FiniteDimensional k⟮y⟯ F]
    (hyt : (algebraMap F E y : L) = t)
    (hfg' : ∃ x : E, Transcendental K' x ∧ FiniteDimensional K'⟮x⟯ E)
    (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F E)) = ⊤)
    [FiniteDimensional K'⟮t⟯ E] :
    Module.finrank k⟮y⟯ F ≤ Module.finrank K'⟮t⟯ E
theorem

natCard_places_le

L159 ↗
AlgebraicCurves.Places.Proofs.Finrank_le_and_natCard_places_le_of_constantFieldExtension_adjoin.AlgebraicCurve.ConstantFieldAdjoin.natCard_places_le
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Finrank_le_and_natCard_places_le_of_constantFieldExtension_adjoin
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstantFieldAdjoin
open _root_.AlgebraicCurve
section Main
variable {k : Type*} [Field k] [IsAlgClosed k] [CharZero k]
variable {F : Type*} [Field F] [Algebra k F]
variable {K' : Type*} [Field K'] [Algebra k K']
variable {L : Type*} [Field L] [Algebra K' L] (t : L) (E : IntermediateField K'⟮t⟯ L)
variable [Algebra F E] [Algebra k E] [IsScalarTower k K' E] [IsScalarTower k F E]
Lean source · statement
theorem natCard_places_le (y : F) (hy : Transcendental k y) [FiniteDimensional k⟮y⟯ F]
    [AlgebraicCurve.IsCurveOver k F]
    (hfg' : ∃ x : E, Transcendental K' x ∧ FiniteDimensional K'⟮x⟯ E)
    (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F E)) = ⊤)
    (u : F) (hu : u ≠ 0) :
    (Finite {P : AlgebraicCurve.Place K' E // 0 < P.ord (algebraMap F E u)} ∧
      Nat.card {P : AlgebraicCurve.Place K' E // 0 < P.ord (algebraMap F E u)} ≤
        Nat.card {P : AlgebraicCurve.Place k F // 0 < P.ord u}) ∧
      (Finite {P : AlgebraicCurve.Place K' E // P.ord (algebraMap F E u) < 0} ∧
      Nat.card {P : AlgebraicCurve.Place K' E // P.ord (algebraMap F E u) < 0} ≤
        Nat.card {P : AlgebraicCurve.Place k F // P.ord u < 0})
theorem

finiteDimensional_adjoin_of_coe_eq

L261 ↗
AlgebraicCurves.Places.Proofs.Finrank_le_and_natCard_places_le_of_constantFieldExtension_adjoin.AlgebraicCurve.ConstantFieldAdjoin.finiteDimensional_adjoin_of_coe_eq
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Finrank_le_and_natCard_places_le_of_constantFieldExtension_adjoin
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstantFieldAdjoin
open _root_.AlgebraicCurve
section Main
variable {k : Type*} [Field k] [IsAlgClosed k] [CharZero k]
variable {F : Type*} [Field F] [Algebra k F]
variable {K' : Type*} [Field K'] [Algebra k K']
variable {L : Type*} [Field L] [Algebra K' L] (t : L) (E : IntermediateField K'⟮t⟯ L)
variable [Algebra F E] [Algebra k E] [IsScalarTower k K' E] [IsScalarTower k F E]
omit [IsAlgClosed k] [CharZero k] in
Lean source · statement
theorem finiteDimensional_adjoin_of_coe_eq [FiniteDimensional K'⟮t⟯ E] (x : E) (hx : (x : L) = t) :
    FiniteDimensional K'⟮x⟯ E
theorem

adjoin_adjoin_subset

L279 ↗
AlgebraicCurves.Places.Proofs.Finrank_le_and_natCard_places_le_of_constantFieldExtension_adjoin.AlgebraicCurve.ConstantFieldAdjoin.adjoin_adjoin_subset
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Finrank_le_and_natCard_places_le_of_constantFieldExtension_adjoin
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstantFieldAdjoin
open _root_.AlgebraicCurve
section Main
variable {k : Type*} [Field k] [IsAlgClosed k] [CharZero k]
variable {F : Type*} [Field F] [Algebra k F]
variable {K' : Type*} [Field K'] [Algebra k K']
variable {L : Type*} [Field L] [Algebra K' L] (t : L) (E : IntermediateField K'⟮t⟯ L)
variable [Algebra F E] [Algebra k E] [IsScalarTower k K' E] [IsScalarTower k F E]
Lean source · statement
theorem adjoin_adjoin_subset {K' : Type*} [Field K'] {L : Type*} [Field L] [Algebra K' L] (S : Set
  L) (t : L)
    (ht : t ∈ IntermediateField.adjoin K' S) :
    ((IntermediateField.adjoin K'⟮t⟯ S : IntermediateField K'⟮t⟯ L) : Set L) ⊆
      ((IntermediateField.adjoin K' S : IntermediateField K' L) : Set L)
theorem

adjoin_range_eq_top

L295 ↗
AlgebraicCurves.Places.Proofs.Finrank_le_and_natCard_places_le_of_constantFieldExtension_adjoin.AlgebraicCurve.ConstantFieldAdjoin.adjoin_range_eq_top
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Finrank_le_and_natCard_places_le_of_constantFieldExtension_adjoin
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstantFieldAdjoin
open _root_.AlgebraicCurve
section Main
variable {k : Type*} [Field k] [IsAlgClosed k] [CharZero k]
variable {F : Type*} [Field F] [Algebra k F]
variable {K' : Type*} [Field K'] [Algebra k K']
variable {L : Type*} [Field L] [Algebra K' L] (t : L) (E : IntermediateField K'⟮t⟯ L)
variable [Algebra F E] [Algebra k E] [IsScalarTower k K' E] [IsScalarTower k F E]
omit [IsAlgClosed k] [CharZero k] in
Lean source · full declaration
theorem adjoin_range_eq_top
    (hEle : (E : Set L) ⊆
      ((IntermediateField.adjoin K' (Set.range fun u : F => (algebraMap F E u : L)) :
        IntermediateField K' L) : Set L)) :
    IntermediateField.adjoin K' (Set.range (algebraMap F E)) = ⊤ := by
  let f : E →ₐ[K'] L := E.val.restrictScalars K'
  set A := IntermediateField.adjoin K' (Set.range (algebraMap F E)) with hA
  have hmapA : A.map f = IntermediateField.adjoin K' (Set.range fun u : F => (algebraMap F E u :
    L)) := by
    rw [hA, IntermediateField.adjoin_map, ← Set.range_comp]
    rfl
  rw [eq_top_iff]
  intro e _
  have he : (e : L) ∈ A.map f := by
    rw [hmapA]; exact hEle e.2
  obtain ⟨a, ha, hae⟩ := (IntermediateField.mem_map A).mp he
  have : a = e := Subtype.ext hae
  rw [← this]; exact ha
theorem

finrank_le_and_natCard_places_le_of_constantFieldExtension_adjoin

L321 ↗
AlgebraicCurve.finrank_le_and_natCard_places_le_of_constantFieldExtension_adjoin
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Finrank_le_and_natCard_places_le_of_constantFieldExtension_adjoin
open scoped IntermediateField
open scoped IntermediateField in
Lean source · statement
theorem _root_.AlgebraicCurve.finrank_le_and_natCard_places_le_of_constantFieldExtension_adjoin
    {k : Type*} [Field k] [IsAlgClosed k] [CharZero k]
    {F : Type*} [Field F] [Algebra k F] [AlgebraicCurve.IsCurveOver k F]
    (y : F) (hy : Transcendental k y)
    [FiniteDimensional (IntermediateField.adjoin k ({y} : Set F)) F]
    {K' : Type*} [Field K'] [Algebra k K']
    {L : Type*} [Field L] [Algebra K' L] (t : L) (ht : Transcendental K' t)
    (E : IntermediateField (IntermediateField.adjoin K' ({t} : Set L)) L)
    [FiniteDimensional (IntermediateField.adjoin K' ({t} : Set L)) E]
    [Algebra F E] [Algebra k E] [IsScalarTower k K' E] [IsScalarTower k F E]
    (hyt : (algebraMap F E y : L) = t)
    (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F E)) = ⊤) :
    Module.finrank (IntermediateField.adjoin k ({y} : Set F)) F ≤
        Module.finrank (IntermediateField.adjoin K' ({t} : Set L)) E ∧
      ∀ u : F, u ≠ 0 →
        (Finite {P : AlgebraicCurve.Place K' E // 0 < P.ord (algebraMap F E u)} ∧
          Nat.card {P : AlgebraicCurve.Place K' E // 0 < P.ord (algebraMap F E u)} ≤
            Nat.card {P : AlgebraicCurve.Place k F // 0 < P.ord u}) ∧
        (Finite {P : AlgebraicCurve.Place K' E // P.ord (algebraMap F E u) < 0} ∧
          Nat.card {P : AlgebraicCurve.Place K' E // P.ord (algebraMap F E u) < 0} ≤
            Nat.card {P : AlgebraicCurve.Place k F // P.ord u < 0})

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