Module

Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.lean

Nyll.AlgebraicCurves.Divisors.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension

37 declarations indexed from sourceView source ↗

Module documentation

Card places deg one eq sum divisors of constant Field Extension

Imports6

Nyll.AlgebraicCurves.FunctionFields.CurveOver
Nyll.AlgebraicCurves.Cohomology.Adelic.Index
Nyll.AlgebraicCurves.Places.OverDVR
Nyll.AlgebraicCurves.Divisors.ConstantExtension
Mathlib.FieldTheory.Finite.GaloisField
Mathlib.RingTheory.Discriminant

Imported by2

theorem

ker_eq_maximalIdeal

L41 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.ker_eq_maximalIdeal

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve

Lean source · statement

theorem ker_eq_maximalIdeal {R L : Type*} [CommRing R] [IsLocalRing R] [Field L] [Finite L]
    (ψ : R →+* L) : RingHom.ker ψ = maximalIdeal R

instance

isScalarTower_valuationSubring

L55 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.isScalarTower_valuationSubring

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Local
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F']
  {k' : Type*} [Field k'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F']

Lean source · statement

instance isScalarTower_valuationSubring (v : Place k F) :
    IsScalarTower k v.toValuationSubring F'

def

constHom

L65 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.constHom

Documentation

The homomorphism mapping extended constants into the integral closure at the place.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Local
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F']
  {k' : Type*} [Field k'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F']
variable [Algebra.IsIntegral k k']

Lean source · statement

def constHom (v : Place k F) : k' →+* integralClosureAt F' v

theorem

coe_constHom

L71 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.coe_constHom

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Local
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F']
  {k' : Type*} [Field k'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F']
variable [Algebra.IsIntegral k k']

Lean source · statement

theorem coe_constHom (v : Place k F) (a : k') :
    ((constHom (F' := F') v a : integralClosureAt F' v) : F') = algebraMap k' F' a

theorem

algebraMap_constHom

L74 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.algebraMap_constHom

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Local
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F']
  {k' : Type*} [Field k'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F']
variable [Algebra.IsIntegral k k']

Lean source · statement

theorem algebraMap_constHom (v : Place k F) (a : k') :
    algebraMap (integralClosureAt F' v) F' (constHom v a) = algebraMap k' F' a

theorem

algebraMap_algebraMap_eq_constHom

L77 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.algebraMap_algebraMap_eq_constHom

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Local
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F']
  {k' : Type*} [Field k'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F']
variable [Algebra.IsIntegral k k']

Lean source · statement

theorem algebraMap_algebraMap_eq_constHom (v : Place k F) (a : k) :
    algebraMap v.toValuationSubring (integralClosureAt F' v) (algebraMap k v.toValuationSubring a)
      = constHom v (algebraMap k k' a)

theorem

constHom_comp_algebraMap

L84 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.constHom_comp_algebraMap

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Local
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F']
  {k' : Type*} [Field k'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F']
variable [Algebra.IsIntegral k k']

Lean source · statement

theorem constHom_comp_algebraMap (v : Place k F) :
    (constHom (F' := F') v).comp (algebraMap k k')
      = (algebraMap v.toValuationSubring (integralClosureAt F' v)).comp
          (algebraMap k v.toValuationSubring)

def

HomO

L94 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.HomO

Documentation

The valuation-ring homomorphisms to the extended constants compatible with the original constants.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Local
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F']
  {k' : Type*} [Field k'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F']
variable [Algebra.IsIntegral k k']
variable (k') in

Lean source · statement

def HomO (v : Place k F) : Type _

def

homOEquivAlgHom

L100 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.homOEquivAlgHom

Documentation

The equivalence between compatible valuation-ring maps and residue-field algebra homomorphisms.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Local
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F']
  {k' : Type*} [Field k'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F']
variable [Algebra.IsIntegral k k']
variable (k') in

Lean source · full declaration

def homOEquivAlgHom [Finite k'] (v : Place k F) :
    HomO k' v ≃ (v.ResidueField →ₐ[k] k') where
  toFun ψ :=
    { Ideal.Quotient.lift (maximalIdeal v.toValuationSubring) ψ.1
        (fun a ha => by rwa [← ker_eq_maximalIdeal ψ.1, RingHom.mem_ker] at ha) with
      commutes' := fun r => by
        change Ideal.Quotient.lift _ _ _
          (Ideal.Quotient.mk _ (algebraMap k v.toValuationSubring r)) = _
        rw [Ideal.Quotient.lift_mk]
        exact ψ.2 r }
  invFun χ :=
    ⟨χ.toRingHom.comp (residue v.toValuationSubring), fun a => by
      change χ (algebraMap k v.ResidueField a) = _
      exact χ.commutes a⟩
  left_inv ψ := by
    apply Subtype.ext
    ext x
    rfl
  right_inv χ := by
    apply AlgHom.ext
    intro x
    obtain ⟨y, rfl⟩ := residue_surjective x
    rfl

def

HomC

L127 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.HomC

Documentation

The homomorphisms from the integral closure to the extended constants that fix those constants.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Local
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F']
  {k' : Type*} [Field k'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F']
variable [Algebra.IsIntegral k k']
variable (k') in
variable (k') in

Lean source · statement

def HomC (v : Place k F) : Type _

def

restrictHomC

L132 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.restrictHomC

Documentation

Restriction of a constant-preserving map from the integral closure to the original valuation ring.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Local
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F']
  {k' : Type*} [Field k'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F']
variable [Algebra.IsIntegral k k']
variable (k') in
variable (k') in

Lean source · statement

def restrictHomC (v : Place k F) (φ : HomC k' (F' := F') v) : HomO k' v

theorem

eq_aeval_constHom

L136 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.eq_aeval_constHom

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Local
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F']
  {k' : Type*} [Field k'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F']
variable [Algebra.IsIntegral k k']
variable (k') in
variable (k') in

Lean source · statement

theorem eq_aeval_constHom (v : Place k F) (α : k') (c : integralClosureAt F' v)
    (p : (v.toValuationSubring)[X]) (hp : aeval (algebraMap k' F' α) p = (c : F')) :
    c = aeval (constHom v α) p

theorem

restrictHomC_bijective

L144 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.restrictHomC_bijective

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Local
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F']
  {k' : Type*} [Field k'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F']
variable [Algebra.IsIntegral k k']
variable (k') in
variable (k') in

Lean source · statement

theorem restrictHomC_bijective (v : Place k F) (α : k')
    (htop : Algebra.adjoin k {α} = ⊤)
    (hgen : ∀ c : integralClosureAt F' v, ∃ p : (v.toValuationSubring)[X],
      aeval (algebraMap k' F' α) p = (c : F'))
    (hdvd : ∀ p : (v.toValuationSubring)[X], aeval (algebraMap k' F' α) p = 0 →
      (minpoly k α).map (algebraMap k v.toValuationSubring) ∣ p) :
    Function.Bijective (restrictHomC (k' := k') (F' := F') v)

def

homCEquivHomO

L213 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.homCEquivHomO

Documentation

The equivalence between maps on the integral closure and maps on the original valuation ring.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Local
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F']
  {k' : Type*} [Field k'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F']
variable [Algebra.IsIntegral k k']
variable (k') in
variable (k') in
variable (k') in

Lean source · statement

def homCEquivHomO (v : Place k F) (α : k')
    (htop : Algebra.adjoin k {α} = ⊤)
    (hgen : ∀ c : integralClosureAt F' v, ∃ p : (v.toValuationSubring)[X],
      aeval (algebraMap k' F' α) p = (c : F'))
    (hdvd : ∀ p : (v.toValuationSubring)[X], aeval (algebraMap k' F' α) p = 0 →
      (minpoly k α).map (algebraMap k v.toValuationSubring) ∣ p) :
    HomC k' (F' := F') v ≃ HomO k' v

def

GoodPrime

L226 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.GoodPrime

Documentation

The height-one primes modulo which every element of the integral closure is a constant.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Local
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F']
  {k' : Type*} [Field k'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F']
variable [Algebra.IsIntegral k k']
variable (k') in
variable (k') in
variable (k') in
variable [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (k') in

Lean source · statement

def GoodPrime (v : Place k F) : Type _

def

goodPrimeOfHomC

L231 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.goodPrimeOfHomC

Documentation

The constant-residue height-one prime defined as the kernel of a constant-preserving map.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Local
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F']
  {k' : Type*} [Field k'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F']
variable [Algebra.IsIntegral k k']
variable (k') in
variable (k') in
variable (k') in
variable [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (k') in

Lean source · statement

def goodPrimeOfHomC [Finite k'] (v : Place k F) (φ : HomC k' (F' := F') v) : GoodPrime k' (F' :=
  F') v

theorem

goodPrimeOfHomC_asIdeal

L245 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.goodPrimeOfHomC_asIdeal

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Local
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F']
  {k' : Type*} [Field k'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F']
variable [Algebra.IsIntegral k k']
variable (k') in
variable (k') in
variable (k') in
variable [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (k') in
omit [FiniteDimensional F F'] [Algebra.IsSeparable F F'] in

Lean source · statement

theorem goodPrimeOfHomC_asIdeal [Finite k'] (v : Place k F) (φ : HomC k' (F' := F')
  v) :
    (goodPrimeOfHomC v φ).1.asIdeal = RingHom.ker φ.1

theorem

goodPrimeOfHomC_bijective

L249 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.goodPrimeOfHomC_bijective

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Local
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F']
  {k' : Type*} [Field k'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F']
variable [Algebra.IsIntegral k k']
variable (k') in
variable (k') in
variable (k') in
variable [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (k') in
omit [FiniteDimensional F F'] [Algebra.IsSeparable F F'] in

Lean source · statement

theorem goodPrimeOfHomC_bijective [Finite k'] (v : Place k F) :
    Function.Bijective (goodPrimeOfHomC (k' := k') (F' := F') v)

def

homCEquivGoodPrime

L288 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.homCEquivGoodPrime

Documentation

The equivalence between constant-preserving maps and primes with constant residue field.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Local
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F']
  {k' : Type*} [Field k'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F']
variable [Algebra.IsIntegral k k']
variable (k') in
variable (k') in
variable (k') in
variable [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (k') in
variable (k') in

Lean source · statement

def homCEquivGoodPrime [Finite k'] (v : Place k F) :
    HomC k' (F' := F') v ≃ GoodPrime k' (F' := F') v

theorem

mem_fiberCenter_iff

L292 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.mem_fiberCenter_iff

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Local
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F']
  {k' : Type*} [Field k'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F']
variable [Algebra.IsIntegral k k']
variable (k') in
variable (k') in
variable (k') in
variable [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (k') in
variable (k') in

Lean source · statement

theorem mem_fiberCenter_iff {v : Place k F} {w : Place k F'} (hw : w.restrict F = v)
    (c : integralClosureAt F' v) :
    c ∈ (fiberCenter F' v hw).asIdeal ↔
      (⟨algebraMap (integralClosureAt F' v) F' c, forall_mem_of_restrict_eq hw c⟩ :
        w.toValuationSubring) ∈ maximalIdeal w.toValuationSubring

theorem

deg_eq_one_iff_forall

L298 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.deg_eq_one_iff_forall

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Local
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F']
  {k' : Type*} [Field k'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F']
variable [Algebra.IsIntegral k k']
variable (k') in
variable (k') in
variable (k') in
variable [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (k') in
variable (k') in

Lean source · statement

theorem deg_eq_one_iff_forall (w' : Place k' F') [Module.Finite k' w'.ResidueField] :
    w'.deg = 1 ↔ ∀ x : w'.ResidueField, ∃ a : k', algebraMap k' w'.ResidueField a = x

theorem

deg_eq_one_iff_good

L304 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.deg_eq_one_iff_good

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Local
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F']
  {k' : Type*} [Field k'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F']
variable [Algebra.IsIntegral k k']
variable (k') in
variable (k') in
variable (k') in
variable [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (k') in
variable (k') in

Lean source · statement

theorem deg_eq_one_iff_good (v : Place k F) (w' : Place k' F')
    [Module.Finite k' w'.ResidueField]
    (hw : (forgetConstants (K := k) w').restrict F = v) :
    w'.deg = 1 ↔ ∀ c : integralClosureAt F' v, ∃ a : k',
      c - constHom v a ∈ (fiberCenter F' v hw).asIdeal

def

DegOneOver

L362 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.DegOneOver

Documentation

The degree-one places of the constant extension lying over the given place.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Local
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F']
  {k' : Type*} [Field k'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F']
variable [Algebra.IsIntegral k k']
variable (k') in
variable (k') in
variable (k') in
variable [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (k') in
variable (k') in
variable (k') in

Lean source · statement

def DegOneOver (v : Place k F) : Type _

def

degOneOverEquivGoodPrime

L366 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.degOneOverEquivGoodPrime

Documentation

The equivalence between degree-one extending places and primes with constant residue field.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Local
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F']
  {k' : Type*} [Field k'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F']
variable [Algebra.IsIntegral k k']
variable (k') in
variable (k') in
variable (k') in
variable [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (k') in
variable (k') in
variable (k') in

Lean source · statement

def degOneOverEquivGoodPrime [∀ w' : Place k' F', Module.Finite k' w'.ResidueField]
    (v : Place k F) : DegOneOver k' (F' := F') v ≃ GoodPrime k' (F' := F') v

theorem

card_degOneOver

L378 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.card_degOneOver

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Local
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F']
  {k' : Type*} [Field k'] [Algebra k k'] [Algebra k' F'] [IsScalarTower k k' F']
variable [Algebra.IsIntegral k k']
variable (k') in
variable (k') in
variable (k') in
variable [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable (k') in
variable (k') in
variable (k') in

Lean source · full declaration

theorem card_degOneOver [Finite k'] [∀ w' : Place k' F', Module.Finite k' w'.ResidueField]
    (v : Place k F) [Module.Finite k v.ResidueField] (α : k')
    (htop : Algebra.adjoin k {α} = ⊤)
    (hgen : ∀ c : integralClosureAt F' v, ∃ p : (v.toValuationSubring)[X],
      aeval (algebraMap k' F' α) p = (c : F'))
    (hdvd : ∀ p : (v.toValuationSubring)[X], aeval (algebraMap k' F' α) p = 0 →
      (minpoly k α).map (algebraMap k v.toValuationSubring) ∣ p) :
    Nat.card (DegOneOver k' (F' := F') v) =
      if v.deg ∣ Module.finrank k k' then v.deg else 0 := by
  have e : DegOneOver k' (F' := F') v ≃ (v.ResidueField →ₐ[k] k') :=
    (degOneOverEquivGoodPrime v).trans <| (homCEquivGoodPrime k' v).symm.trans <|
      (homCEquivHomO k' v α htop hgen hdvd).trans (homOEquivAlgHom v)
  rw [Nat.card_congr e]
  split_ifs with h
  · exact FiniteField.natCard_algHom_of_finrank_dvd h
  · have : IsEmpty (v.ResidueField →ₐ[k] k') :=
      ⟨fun χ => h (FiniteField.nonempty_algHom_iff_finrank_dvd.mp ⟨χ⟩)⟩
    exact Nat.card_of_isEmpty

theorem

finiteDimensional_of_adjoin_range_eq_top

L405 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.finiteDimensional_of_adjoin_range_eq_top

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section ConstExt
variable {k k' F F' : Type*} [Field k] [Finite k] [Field k'] [Finite k'] [Field F] [Field F']
  [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F']
  [Algebra k F] [Algebra F F'] [IsScalarTower k F F']

Lean source · statement

theorem finiteDimensional_of_adjoin_range_eq_top [Algebra.IsIntegral F F']
    (hgen : Algebra.adjoin F (Set.range (algebraMap k' F')) = ⊤) :
    FiniteDimensional F F'

theorem

adjoin_eq_top_of_primitive

L413 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.adjoin_eq_top_of_primitive

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section ConstExt
variable {k k' F F' : Type*} [Field k] [Finite k] [Field k'] [Finite k'] [Field F] [Field F']
  [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F']
  [Algebra k F] [Algebra F F'] [IsScalarTower k F F']
omit [Finite k] in

Lean source · statement

theorem adjoin_eq_top_of_primitive (α : k') (hα : IntermediateField.adjoin k {α} = ⊤) :
    Algebra.adjoin k {α} = ⊤

theorem

adjoin_algebraMap_eq_top

L418 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.adjoin_algebraMap_eq_top

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section ConstExt
variable {k k' F F' : Type*} [Field k] [Finite k] [Field k'] [Finite k'] [Field F] [Field F']
  [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F']
  [Algebra k F] [Algebra F F'] [IsScalarTower k F F']
omit [Finite k] [Finite k'] in

Lean source · statement

theorem adjoin_algebraMap_eq_top (α : k') (htop : Algebra.adjoin k {α} = ⊤)
    (hgen : Algebra.adjoin F (Set.range (algebraMap k' F')) = ⊤) :
    Algebra.adjoin F {algebraMap k' F' α} = ⊤

theorem

isSeparable_algebraMap

L431 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.isSeparable_algebraMap

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section ConstExt
variable {k k' F F' : Type*} [Field k] [Finite k] [Field k'] [Finite k'] [Field F] [Field F']
  [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F']
  [Algebra k F] [Algebra F F'] [IsScalarTower k F F']
include k in

Lean source · statement

theorem isSeparable_algebraMap (α : k') : IsSeparable F (algebraMap k' F' α)

theorem

isSeparable_of_adjoin_range_eq_top

L438 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.isSeparable_of_adjoin_range_eq_top

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section ConstExt
variable {k k' F F' : Type*} [Field k] [Finite k] [Field k'] [Finite k'] [Field F] [Field F']
  [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F']
  [Algebra k F] [Algebra F F'] [IsScalarTower k F F']
include k in

Lean source · statement

theorem isSeparable_of_adjoin_range_eq_top [Algebra.IsIntegral F F']
    (hgen : Algebra.adjoin F (Set.range (algebraMap k' F')) = ⊤) :
    Algebra.IsSeparable F F'

theorem

minpoly_algebraMap_eq_map

L451 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.minpoly_algebraMap_eq_map

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section ConstExt
variable {k k' F F' : Type*} [Field k] [Finite k] [Field k'] [Finite k'] [Field F] [Field F']
  [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F']
  [Algebra k F] [Algebra F F'] [IsScalarTower k F F']
omit [Finite k] in

Lean source · statement

theorem minpoly_algebraMap_eq_map [Algebra.IsIntegral F F']
    (hconst : ∀ y : F, IsAlgebraic k y → y ∈ (algebraMap k F).range) (α : k') :
    minpoly F (algebraMap k' F' α) = (minpoly k α).map (algebraMap k F)

theorem

map_minpoly_dvd

L508 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.map_minpoly_dvd

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section ConstExt
variable {k k' F F' : Type*} [Field k] [Finite k] [Field k'] [Finite k'] [Field F] [Field F']
  [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F']
  [Algebra k F] [Algebra F F'] [IsScalarTower k F F']
omit [Finite k] in

Lean source · statement

theorem map_minpoly_dvd [Algebra.IsIntegral F F']
    (hconst : ∀ y : F, IsAlgebraic k y → y ∈ (algebraMap k F).range) (v : Place k F) (α : k')
    (p : (v.toValuationSubring)[X]) (hp : aeval (algebraMap k' F' α) p = 0) :
    (minpoly k α).map (algebraMap k v.toValuationSubring) ∣ p

theorem

exists_aeval_eq

L522 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.exists_aeval_eq

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section ConstExt
variable {k k' F F' : Type*} [Field k] [Finite k] [Field k'] [Finite k'] [Field F] [Field F']
  [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F']
  [Algebra k F] [Algebra F F'] [IsScalarTower k F F']

Lean source · statement

theorem exists_aeval_eq [Algebra.IsIntegral F F'] [FiniteDimensional F F']
    [Algebra.IsSeparable F F']
    (hconst : ∀ y : F, IsAlgebraic k y → y ∈ (algebraMap k F).range) (v : Place k F) (α : k')
    (hFtop : IntermediateField.adjoin F {algebraMap k' F' α} = ⊤)
    (c : integralClosureAt F' v) :
    ∃ p : (v.toValuationSubring)[X], aeval (algebraMap k' F' α) p = (c : F')

theorem

ord_ne_zero_of_not_mem

L579 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.ord_ne_zero_of_not_mem

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Finiteness
variable {k F : Type*} [Field k] [Finite k] [Field F] [Algebra k F]
omit [Finite k] in

Lean source · statement

theorem ord_ne_zero_of_not_mem (v : Place k F) {x : F} (hx : x ∉ v.toValuationSubring) :
    v.ord x ≠ 0

theorem

finite_setOf_deg_eq

L600 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.finite_setOf_deg_eq

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Finiteness
variable {k F : Type*} [Field k] [Finite k] [Field F] [Algebra k F]

Lean source · statement

theorem finite_setOf_deg_eq [IsCurveOver k F] {d : ℕ} (hd : 0 < d) :
    {v : Place k F | v.deg = d}.Finite

theorem

card_places_deg_one

L659 ↗

AlgebraicCurves.Divisors.Proofs.Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension.AlgebraicCurve.Place.ConstFieldExtCount.card_places_deg_one

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ConstFieldExtCount
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Global

Lean source · statement

theorem card_places_deg_one
    {k k' F F' : Type*} [Field k] [Finite k] [Field k'] [Finite k'] [Field F] [Field F']
    [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F']
    [Algebra k F] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F']
    [AlgebraicCurve.IsCurveOver k F]
    [AlgebraicCurve.IsCurveOver k' F']
    (hgen : Algebra.adjoin F (Set.range (algebraMap k' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic k y → y ∈ (algebraMap k F).range) :
    Nat.card {w : AlgebraicCurve.Place k' F' | w.deg = 1} =
      ∑ d ∈ Nat.divisors (Module.finrank k k'),
        d * Nat.card {v : AlgebraicCurve.Place k F | v.deg = d}

theorem

card_places_deg_one_eq_sum_divisors_of_constantFieldExtension

L752 ↗

AlgebraicCurve.card_places_deg_one_eq_sum_divisors_of_constantFieldExtension

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
open Polynomial IsDedekindDomain IsLocalRing

Lean source · statement

theorem _root_.AlgebraicCurve.card_places_deg_one_eq_sum_divisors_of_constantFieldExtension
    {k k' F F' : Type*} [Field k] [Finite k] [Field k'] [Finite k'] [Field F] [Field F']
    [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F']
    [Algebra k F] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F']
    [AlgebraicCurve.IsCurveOver k F] [Algebra.EssFiniteType k F]
    [AlgebraicCurve.IsCurveOver k' F']
    (hgen : Algebra.adjoin F (Set.range (algebraMap k' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic k y → y ∈ (algebraMap k F).range) :
    Nat.card {w : AlgebraicCurve.Place k' F' | w.deg = 1} =
      ∑ d ∈ Nat.divisors (Module.finrank k k'),
        d * Nat.card {v : AlgebraicCurve.Place k F | v.deg = d}

Module documentation

Card places deg one eq sum divisors of constant Field Extension

Declarations