Module

Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.lean

Nyll.AlgebraicCurves.Places.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint

77 declarations indexed from sourceView source ↗

Module documentation

Place nat Card set Of comap eq eq deg of linear Disjoint

Imports6

Imported by3

theorem

inv_notMem_of_mem_nonunits

L41 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.inv_notMem_of_mem_nonunits

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section ValSub
variable {L : Type*} [Field L]

Lean source · statement

theorem inv_notMem_of_mem_nonunits (B : ValuationSubring L) {x : L} (hx0 : x ≠ 0)
    (hx : x ∈ B.nonunits) : x⁻¹ ∉ B

theorem

mem_nonunits_of_inv_notMem

L49 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.mem_nonunits_of_inv_notMem

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section ValSub
variable {L : Type*} [Field L]

Lean source · statement

theorem mem_nonunits_of_inv_notMem (B : ValuationSubring L) {x : L} (hx : x⁻¹ ∉ B) :
    x ∈ B.nonunits

theorem

mem_nonunits_iff_inv_notMem

L60 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.mem_nonunits_iff_inv_notMem

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section ValSub
variable {L : Type*} [Field L]

Lean source · statement

theorem mem_nonunits_iff_inv_notMem (B : ValuationSubring L) {x : L} (hx0 : x ≠ 0) :
    x ∈ B.nonunits ↔ x⁻¹ ∉ B

theorem

zero_mem_nonunits

L64 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.zero_mem_nonunits

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section ValSub
variable {L : Type*} [Field L]

Lean source · statement

theorem zero_mem_nonunits (B : ValuationSubring L) : (0 : L) ∈ B.nonunits

theorem

sub_mem_nonunits

L68 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.sub_mem_nonunits

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section ValSub
variable {L : Type*} [Field L]

Lean source · statement

theorem sub_mem_nonunits (B : ValuationSubring L) {x y : L} (hx : x ∈ B.nonunits)
    (hy : y ∈ B.nonunits) : x - y ∈ B.nonunits

theorem

add_mem_nonunits

L73 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.add_mem_nonunits

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section ValSub
variable {L : Type*} [Field L]

Lean source · statement

theorem add_mem_nonunits (B : ValuationSubring L) {x y : L} (hx : x ∈ B.nonunits)
    (hy : y ∈ B.nonunits) : x + y ∈ B.nonunits

theorem

mul_mem_nonunits

L78 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.mul_mem_nonunits

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section ValSub
variable {L : Type*} [Field L]

Lean source · statement

theorem mul_mem_nonunits (B : ValuationSubring L) {b x : L} (hb : b ∈ B)
    (hx : x ∈ B.nonunits) : b * x ∈ B.nonunits

theorem

valuation_eq_one_of_notMem_nonunits

L87 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.valuation_eq_one_of_notMem_nonunits

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section ValSub
variable {L : Type*} [Field L]

Lean source · statement

theorem valuation_eq_one_of_notMem_nonunits (B : ValuationSubring L) {x : L} (hxB : x ∈ B)
    (hx : x ∉ B.nonunits) : B.valuation x = 1

theorem

mul_notMem_nonunits

L93 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.mul_notMem_nonunits

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section ValSub
variable {L : Type*} [Field L]

Lean source · statement

theorem mul_notMem_nonunits (B : ValuationSubring L) {x y : L} (hxB : x ∈ B) (hyB : y ∈ B)
    (hx : x ∉ B.nonunits) (hy : y ∉ B.nonunits) : x * y ∉ B.nonunits

theorem

ne_zero_of_notMem_nonunits

L99 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.ne_zero_of_notMem_nonunits

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section ValSub
variable {L : Type*} [Field L]

Lean source · statement

theorem ne_zero_of_notMem_nonunits (B : ValuationSubring L) {x : L} (hx : x ∉ B.nonunits) :
    x ≠ 0

theorem

nonunits_le

L104 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.nonunits_le

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section ValSub
variable {L : Type*} [Field L]

Lean source · statement

theorem nonunits_le (B : ValuationSubring L) {x : L} (hx : x ∈ B.nonunits) : x ∈ B

theorem

mk_mem_maximalIdeal_iff_mem_nonunits

L107 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.mk_mem_maximalIdeal_iff_mem_nonunits

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section ValSub
variable {L : Type*} [Field L]

Lean source · statement

theorem mk_mem_maximalIdeal_iff_mem_nonunits (B : ValuationSubring L) {x : L} (hx : x ∈ B) :
    (⟨x, hx⟩ : B) ∈ maximalIdeal B ↔ x ∈ B.nonunits

theorem

isUnit_mk_of_notMem_nonunits

L112 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.isUnit_mk_of_notMem_nonunits

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section ValSub
variable {L : Type*} [Field L]

Lean source · statement

theorem isUnit_mk_of_notMem_nonunits (B : ValuationSubring L) {x : L} (hxB : x ∈ B)
    (hx : x ∉ B.nonunits) : IsUnit (⟨x, hxB⟩ : B)

theorem

eq_zero_of_algebraMap_mem_nonunits

L124 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.eq_zero_of_algebraMap_mem_nonunits

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Residue
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem eq_zero_of_algebraMap_mem_nonunits (W : Place K F) {a : K}
    (ha : algebraMap K F a ∈ W.toValuationSubring.nonunits) : a = 0

def

ResBij

L133 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.ResBij

Documentation

The condition that the base field maps bijectively onto the residue field of the place.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Residue
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

def ResBij (W : Place K F) : Prop

theorem

resBij_of_isAlgClosed

L135 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.resBij_of_isAlgClosed

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Residue
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem resBij_of_isAlgClosed [IsAlgClosed K] [IsCurveOver K F] (W : Place K F) : ResBij W

def

resHom

L141 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.resHom

Documentation

The residue map to K obtained from the bijectivity of the map to the residue field.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Residue
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

def resHom (W : Place K F) (hW : ResBij W) : W.toValuationSubring →ₐ[K] K

theorem

resHom_apply

L152 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.resHom_apply

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Residue
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem resHom_apply (W : Place K F) (hW : ResBij W) (g : W.toValuationSubring) :
    resHom W hW g = (RingEquiv.ofBijective (algebraMap K W.ResidueField) hW).symm
      (IsLocalRing.residue _ g)

theorem

algebraMap_resHom

L156 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.algebraMap_resHom

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Residue
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem algebraMap_resHom (W : Place K F) (hW : ResBij W) (g : W.toValuationSubring) :
    algebraMap K W.ResidueField (resHom W hW g) = IsLocalRing.residue _ g

theorem

resHom_spec

L161 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.resHom_spec

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Residue
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem resHom_spec (W : Place K F) (hW : ResBij W) (g : W.toValuationSubring) :
    (g : F) - algebraMap K F (resHom W hW g) ∈ W.toValuationSubring.nonunits

theorem

resHom_eq_iff

L172 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.resHom_eq_iff

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Residue
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem resHom_eq_iff (W : Place K F) (hW : ResBij W) (g : W.toValuationSubring) (a : K) :
    resHom W hW g = a ↔ (g : F) - algebraMap K F a ∈ W.toValuationSubring.nonunits

theorem

mem_nonunits_iff_resHom_eq_zero

L187 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.mem_nonunits_iff_resHom_eq_zero

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Residue
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mem_nonunits_iff_resHom_eq_zero (W : Place K F) (hW : ResBij W)
    (g : W.toValuationSubring) :
    (g : F) ∈ W.toValuationSubring.nonunits ↔ resHom W hW g = 0

theorem

coe_aeval_mk

L192 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.coe_aeval_mk

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Residue
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem coe_aeval_mk (W : Place K F) {x : F} (hx : x ∈ W.toValuationSubring) (P : K[X]) :
    ((aeval (⟨x, hx⟩ : W.toValuationSubring) P : W.toValuationSubring) : F) = aeval x P

theorem

aeval_mem

L197 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.aeval_mem

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Residue
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem aeval_mem (W : Place K F) {x : F} (hx : x ∈ W.toValuationSubring) (P : K[X]) :
    aeval x P ∈ W.toValuationSubring

theorem

resHom_aeval

L202 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.resHom_aeval

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Residue
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem resHom_aeval (W : Place K F) (hW : ResBij W) {x : F} (hx : x ∈ W.toValuationSubring)
    (P : K[X]) :
    resHom W hW ⟨aeval x P, aeval_mem W hx P⟩ = P.eval (resHom W hW ⟨x, hx⟩)

def

Over

L220 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.Over

Documentation

The condition that the extended place restricts to the given place of the original function field.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Over
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]

Lean source · statement

def Over (v : Place k F₀) (W : Place K F) : Prop

theorem

mem_iff_of_over

L223 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.mem_iff_of_over

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Over
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]

Lean source · statement

theorem mem_iff_of_over {v : Place k F₀} {W : Place K F} (hW : Over v W) (f : F₀) :
    f ∈ v.toValuationSubring ↔ algebraMap F₀ F f ∈ W.toValuationSubring

theorem

nonunits_iff_of_over

L228 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.nonunits_iff_of_over

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Over
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F]

Lean source · statement

theorem nonunits_iff_of_over {v : Place k F₀} {W : Place K F} (hW : Over v W) (f : F₀) :
    algebraMap F₀ F f ∈ W.toValuationSubring.nonunits ↔ f ∈ v.toValuationSubring.nonunits

def

residueₐ

L244 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.residueₐ

Documentation

The residue map of a place as a homomorphism of base-field algebras.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section ResidueData
variable {k F₀ : Type*} [Field k] [Field F₀] [Algebra k F₀]

Lean source · statement

def residueₐ (v : Place k F₀) : v.toValuationSubring →ₐ[k] v.ResidueField

theorem

residueₐ_apply

L247 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.residueₐ_apply

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section ResidueData
variable {k F₀ : Type*} [Field k] [Field F₀] [Algebra k F₀]

Lean source · statement

theorem residueₐ_apply (v : Place k F₀) (x : v.toValuationSubring) :
    residueₐ v x = IsLocalRing.residue _ x

theorem

residue_aeval

L250 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.residue_aeval

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section ResidueData
variable {k F₀ : Type*} [Field k] [Field F₀] [Algebra k F₀]

Lean source · statement

theorem residue_aeval (v : Place k F₀) (θ : v.toValuationSubring) (P : k[X]) :
    IsLocalRing.residue _ (aeval θ P) = aeval (IsLocalRing.residue _ θ) P

theorem

exists_poly_add_mul

L255 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.exists_poly_add_mul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section ResidueData
variable {k F₀ : Type*} [Field k] [Field F₀] [Algebra k F₀]

Lean source · statement

theorem exists_poly_add_mul (v : Place k F₀) [Module.Finite k v.ResidueField]
    {θ π : v.toValuationSubring} (hπ : Irreducible π)
    (hθ : IntermediateField.adjoin k {IsLocalRing.residue _ θ} = ⊤) (f : v.toValuationSubring) :
    ∃ P : k[X], ∃ g : v.toValuationSubring, f = aeval θ P + π * g

theorem

aeval_minpoly_mem

L275 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.aeval_minpoly_mem

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section ResidueData
variable {k F₀ : Type*} [Field k] [Field F₀] [Algebra k F₀]

Lean source · statement

theorem aeval_minpoly_mem (v : Place k F₀) (θ : v.toValuationSubring) :
    aeval θ (minpoly k (IsLocalRing.residue _ θ)) ∈ maximalIdeal v.toValuationSubring

theorem

exists_aeval_minpoly_eq

L279 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.exists_aeval_minpoly_eq

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section ResidueData
variable {k F₀ : Type*} [Field k] [Field F₀] [Algebra k F₀]

Lean source · statement

theorem exists_aeval_minpoly_eq (v : Place k F₀) {θ π : v.toValuationSubring}
    (hπ : Irreducible π) :
    ∃ g : v.toValuationSubring, aeval θ (minpoly k (IsLocalRing.residue _ θ)) = π * g

theorem

natDegree_minpoly_eq_deg

L287 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.natDegree_minpoly_eq_deg

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section ResidueData
variable {k F₀ : Type*} [Field k] [Field F₀] [Algebra k F₀]

Lean source · statement

theorem natDegree_minpoly_eq_deg (v : Place k F₀) [Module.Finite k v.ResidueField]
    {θ : v.toValuationSubring}
    (hθ : IntermediateField.adjoin k {IsLocalRing.residue _ θ} = ⊤) :
    (minpoly k (IsLocalRing.residue _ θ)).natDegree = v.deg

theorem

coe_aeval

L296 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.coe_aeval

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section ResidueData
variable {k F₀ : Type*} [Field k] [Field F₀] [Algebra k F₀]

Lean source · statement

theorem coe_aeval (v : Place k F₀) (θ : v.toValuationSubring) (P : k[X]) :
    ((aeval θ P : v.toValuationSubring) : F₀) = aeval (θ : F₀) P

theorem

coeff_eq_zero_of_sum_smul_pow_mem

L300 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.coeff_eq_zero_of_sum_smul_pow_mem

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section ResidueData
variable {k F₀ : Type*} [Field k] [Field F₀] [Algebra k F₀]

Lean source · statement

theorem coeff_eq_zero_of_sum_smul_pow_mem (v : Place k F₀) (θ : v.toValuationSubring)
    (a : Fin (minpoly k (IsLocalRing.residue _ θ)).natDegree → k)
    (h : v.toValuationSubring.valuation (∑ i, a i • (θ : F₀) ^ (i : ℕ)) < 1) :
    ∀ i, a i = 0

def

Rv

L331 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.Rv

Documentation

The subalgebra generated by the image of the valuation ring after extending constants.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section RingR
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F
variable (K F) in

Lean source · statement

def Rv (v : Place k F₀) : Subalgebra K F

theorem

algebraMap_mem_Rv

L334 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.algebraMap_mem_Rv

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section RingR
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F
variable (K F) in
omit [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F] in

Lean source · statement

theorem algebraMap_mem_Rv (v : Place k F₀) {f : F₀} (hf : f ∈ v.toValuationSubring) :
    ι f ∈ Rv K F v

theorem

coe_mem_Rv

L338 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.coe_mem_Rv

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section RingR
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F
variable (K F) in
omit [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F] in

Lean source · statement

theorem coe_mem_Rv (v : Place k F₀) (f : v.toValuationSubring) : ι (f : F₀) ∈ Rv K F v

theorem

aeval_mem_Rv

L341 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.aeval_mem_Rv

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section RingR
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F
variable (K F) in
omit [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F] in

Lean source · statement

theorem aeval_mem_Rv (v : Place k F₀) {x : F} (hx : x ∈ Rv K F v) (P : K[X]) :
    aeval x P ∈ Rv K F v

theorem

Rv_le_of_over

L346 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.Rv_le_of_over

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section RingR
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F
variable (K F) in
omit [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F] in

Lean source · statement

theorem Rv_le_of_over {v : Place k F₀} {W : Place K F} (hW : Over v W) {x : F}
    (hx : x ∈ Rv K F v) : x ∈ W.toValuationSubring

theorem

algebraMap_coe_aeval

L356 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.algebraMap_coe_aeval

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section RingR
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F
variable (K F) in

Lean source · statement

theorem algebraMap_coe_aeval (v : Place k F₀) (θ : v.toValuationSubring) (P : k[X]) :
    ι ((aeval θ P : v.toValuationSubring) : F₀) = aeval (ι (θ : F₀)) (P.map (algebraMap k K))

theorem

exists_decomp

L362 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.exists_decomp

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section RingR
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F
variable (K F) in

Lean source · statement

theorem exists_decomp (v : Place k F₀) [Module.Finite k v.ResidueField]
    {θ π : v.toValuationSubring} (hπ : Irreducible π)
    (hθ : IntermediateField.adjoin k {IsLocalRing.residue _ θ} = ⊤) {r : F} (hr : r ∈ Rv K F v) :
    ∃ P : K[X], ∃ r' ∈ Rv K F v, r = aeval (ι (θ : F₀)) P + ι (π : F₀) * r'

theorem

exists_div

L392 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.exists_div

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section RingR
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F
variable (K F) in
omit [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F] in

Lean source · statement

theorem exists_div (v : Place k F₀)
    (hgen : IntermediateField.adjoin K (Set.range (algebraMap F₀ F)) = ⊤) (x : F) :
    ∃ r ∈ Rv K F v, ∃ s ∈ Rv K F v, s ≠ 0 ∧ x = r / s

theorem

exists_sum_of_mem_Rv

L415 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.exists_sum_of_mem_Rv

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section RingR
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F
variable (K F) in
omit [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F] in

Lean source · statement

theorem exists_sum_of_mem_Rv (v : Place k F₀) {r : F} (hr : r ∈ Rv K F v) :
    ∃ n : ℕ, ∃ c : Fin n → K, ∃ f : Fin n → F₀,
      (∀ i, f i ∈ v.toValuationSubring) ∧ r = ∑ i, c i • ι (f i)

theorem

theta_mem

L445 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.theta_mem

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section AlphaW
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F
omit [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F] in

Lean source · statement

theorem theta_mem {v : Place k F₀} {W : Place K F} (hW : Over v W) (θ : v.toValuationSubring) :
    ι (θ : F₀) ∈ W.toValuationSubring

def

αv

L450 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.αv

Documentation

The base-field residue of an integral element at a place above the original place.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section AlphaW
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

def αv {v : Place k F₀} (W : Place K F) (hb : ResBij W) (hW : Over v W)
    (θ : v.toValuationSubring) : K

theorem

theta_sub_alpha_mem

L454 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.theta_sub_alpha_mem

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section AlphaW
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F
omit [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F] in

Lean source · statement

theorem theta_sub_alpha_mem {v : Place k F₀} {W : Place K F} (hb : ResBij W) (hW : Over v W)
    (θ : v.toValuationSubring) :
    ι (θ : F₀) - algebraMap K F (αv W hb hW θ) ∈ W.toValuationSubring.nonunits

theorem

alpha_eq_of_mem_nonunits

L459 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.alpha_eq_of_mem_nonunits

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section AlphaW
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F
omit [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F] in

Lean source · statement

theorem alpha_eq_of_mem_nonunits {v : Place k F₀} {W : Place K F} (hb : ResBij W) (hW : Over v W)
    (θ : v.toValuationSubring) {a : K}
    (h : ι (θ : F₀) - algebraMap K F a ∈ W.toValuationSubring.nonunits) : αv W hb hW θ = a

theorem

coe_mem_nonunits_iff

L464 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.coe_mem_nonunits_iff

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section AlphaW
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

theorem coe_mem_nonunits_iff {v : Place k F₀} (x : v.toValuationSubring) :
    (x : F₀) ∈ v.toValuationSubring.nonunits ↔ x ∈ maximalIdeal v.toValuationSubring

theorem

pi_mem_nonunits

L468 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.pi_mem_nonunits

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section AlphaW
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F
omit [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F] in

Lean source · statement

theorem pi_mem_nonunits {v : Place k F₀} {W : Place K F} (hW : Over v W)
    {π : v.toValuationSubring} (hπ : Irreducible π) :
    ι (π : F₀) ∈ W.toValuationSubring.nonunits

theorem

pi_ne_zero

L474 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.pi_ne_zero

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section AlphaW
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F
omit [Algebra k F] [IsScalarTower k F₀ F] in

Lean source · statement

theorem pi_ne_zero {v : Place k F₀} {π : v.toValuationSubring} (hπ : Irreducible π) :
    ι (π : F₀) ≠ 0

theorem

mem_nonunits_iff_isRoot

L479 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.mem_nonunits_iff_isRoot

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section AlphaW
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F
omit [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F] in

Lean source · statement

theorem mem_nonunits_iff_isRoot {v : Place k F₀} {W : Place K F} (hb : ResBij W) (hW : Over v W)
    {θ π : v.toValuationSubring} (hπ : Irreducible π) {r r' : F} (hr' : r' ∈ Rv K F v)
    {P : K[X]} (hr : r = aeval (ι (θ : F₀)) P + ι (π : F₀) * r') :
    r ∈ W.toValuationSubring.nonunits ↔ P.IsRoot (αv W hb hW θ)

theorem

isRoot_alpha

L501 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.isRoot_alpha

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section AlphaW
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

theorem isRoot_alpha {v : Place k F₀} {W : Place K F} (hb : ResBij W) (hW : Over v W)
    {θ π : v.toValuationSubring} (hπ : Irreducible π) :
    ((minpoly k (IsLocalRing.residue _ θ)).map (algebraMap k K)).IsRoot (αv W hb hW θ)

theorem

not_isRoot_divByMonic

L514 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.not_isRoot_divByMonic

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section AlphaW
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

theorem not_isRoot_divByMonic {p : K[X]} (hsep : p.Separable) {a : K} (ha : p.IsRoot a) :
    ¬ (p /ₘ (X - C a)).IsRoot a

theorem

e_notMem_nonunits

L523 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.e_notMem_nonunits

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section AlphaW
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

theorem e_notMem_nonunits {v : Place k F₀} {W : Place K F} (hb : ResBij W) (hW : Over v W)
    {θ π : v.toValuationSubring} (hπ : Irreducible π)
    (hsep : ((minpoly k (IsLocalRing.residue _ θ)).map (algebraMap k K)).Separable) :
    aeval (ι (θ : F₀)) (((minpoly k (IsLocalRing.residue _ θ)).map (algebraMap k K))
      /ₘ (X - C (αv W hb hW θ))) ∉ W.toValuationSubring.nonunits

theorem

e_mul_eq

L533 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.e_mul_eq

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section AlphaW
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

theorem e_mul_eq {v : Place k F₀} [Module.Finite k v.ResidueField] {W : Place K F}
    (hb : ResBij W) (hW : Over v W) {θ π : v.toValuationSubring} (hπ : Irreducible π)
    (hθ : IntermediateField.adjoin k {IsLocalRing.residue _ θ} = ⊤)
    {r : F} (hr : r ∈ Rv K F v) (hru : r ∈ W.toValuationSubring.nonunits) :
    ∃ r₂ ∈ Rv K F v,
      aeval (ι (θ : F₀)) (((minpoly k (IsLocalRing.residue _ θ)).map (algebraMap k K))
        /ₘ (X - C (αv W hb hW θ))) * r = ι (π : F₀) * r₂

theorem

one_notMem_nonunits

L571 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.one_notMem_nonunits

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Uniqueness
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

theorem one_notMem_nonunits {L : Type*} [Field L] (B : ValuationSubring L) :
    (1 : L) ∉ B.nonunits

theorem

ord_pos_of_mem_nonunits

L575 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.ord_pos_of_mem_nonunits

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Uniqueness
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

theorem ord_pos_of_mem_nonunits (W : Place K F) {x : F} (hx : x ∈ W.toValuationSubring.nonunits)
    (hx0 : x ≠ 0) : 0 < W.ord x

theorem

ord_eq_zero_of_notMem_nonunits

L581 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.ord_eq_zero_of_notMem_nonunits

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Uniqueness
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

theorem ord_eq_zero_of_notMem_nonunits (W : Place K F) {x : F} (hxW : x ∈ W.toValuationSubring)
    (hx : x ∉ W.toValuationSubring.nonunits) : W.ord x = 0

theorem

exists_factor

L588 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.exists_factor

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Uniqueness
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

theorem exists_factor {v : Place k F₀} [Module.Finite k v.ResidueField] {W : Place K F}
    (hb : ResBij W) (hW : Over v W) {θ π : v.toValuationSubring} (hπ : Irreducible π)
    (hθ : IntermediateField.adjoin k {IsLocalRing.residue _ θ} = ⊤)
    (hsep : ((minpoly k (IsLocalRing.residue _ θ)).map (algebraMap k K)).Separable)
    {r : F} (hr : r ∈ Rv K F v) (hr0 : r ≠ 0) :
    ∃ n : ℕ, ∃ s ∈ Rv K F v, ∃ u ∈ Rv K F v, s ∉ W.toValuationSubring.nonunits ∧
      u ∉ W.toValuationSubring.nonunits ∧ s * r = ι (π : F₀) ^ n * u

theorem

div_mem_iff_of_factor

L637 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.div_mem_iff_of_factor

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Uniqueness
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

theorem div_mem_iff_of_factor {L : Type*} [Field L] (B : ValuationSubring L)
    {ϖ r s sr ur ss us : L} (hϖ : ϖ ∈ B.nonunits) (hϖ0 : ϖ ≠ 0)
    (hsrB : sr ∈ B) (hurB : ur ∈ B) (hssB : ss ∈ B) (husB : us ∈ B)
    (hsr : sr ∉ B.nonunits) (hur : ur ∉ B.nonunits) (hss : ss ∉ B.nonunits)
    (hus : us ∉ B.nonunits) (hs0 : s ≠ 0) {a b : ℕ}
    (hfr : sr * r = ϖ ^ a * ur) (hfs : ss * s = ϖ ^ b * us) :
    r / s ∈ B ↔ b ≤ a

theorem

nonunits_iff_of_alpha_eq

L664 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.nonunits_iff_of_alpha_eq

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Uniqueness
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

theorem nonunits_iff_of_alpha_eq {v : Place k F₀} [Module.Finite k v.ResidueField]
    {W₁ W₂ : Place K F} (hb₁ : ResBij W₁) (hb₂ : ResBij W₂) (hW₁ : Over v W₁) (hW₂ : Over v W₂)
    {θ π : v.toValuationSubring} (hπ : Irreducible π)
    (hθ : IntermediateField.adjoin k {IsLocalRing.residue _ θ} = ⊤)
    (hα : αv W₁ hb₁ hW₁ θ = αv W₂ hb₂ hW₂ θ) {r : F} (hr : r ∈ Rv K F v) :
    r ∈ W₁.toValuationSubring.nonunits ↔ r ∈ W₂.toValuationSubring.nonunits

theorem

eq_of_alpha_eq

L673 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.eq_of_alpha_eq

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Uniqueness
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

theorem eq_of_alpha_eq {v : Place k F₀} [Module.Finite k v.ResidueField]
    (hgen : IntermediateField.adjoin K (Set.range (algebraMap F₀ F)) = ⊤)
    {W₁ W₂ : Place K F} (hb₁ : ResBij W₁) (hb₂ : ResBij W₂) (hW₁ : Over v W₁) (hW₂ : Over v W₂)
    {θ π : v.toValuationSubring} (hπ : Irreducible π)
    (hθ : IntermediateField.adjoin k {IsLocalRing.residue _ θ} = ⊤)
    (hsep : ((minpoly k (IsLocalRing.residue _ θ)).map (algebraMap k K)).Separable)
    (hα : αv W₁ hb₁ hW₁ θ = αv W₂ hb₂ hW₂ θ) : W₁ = W₂

theorem

eq_of_le_of_ne_top

L710 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.eq_of_le_of_ne_top

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Existence
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

theorem eq_of_le_of_ne_top (v : Place k F₀) {O' : ValuationSubring F₀}
    (hle : v.toValuationSubring ≤ O') (hne : O' ≠ ⊤) : O' = v.toValuationSubring

def

Nsub

L761 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.Nsub

Documentation

The base-field submodule of elements with valuation strictly less than one.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Existence
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · full declaration

def Nsub (v : Place k F₀) : Submodule k F₀ where
  carrier := {y | v.toValuationSubring.valuation y < 1}
  zero_mem' := by
    change v.toValuationSubring.valuation 0 < 1
    rw [map_zero]; exact zero_lt_one
  add_mem' := by
    intro x y hx hy
    simp only [Set.mem_ofPred_eq] at hx hy ⊢
    exact lt_of_le_of_lt (Valuation.map_add _ x y) (max_lt hx hy)
  smul_mem' := by
    intro c y hy
    change v.toValuationSubring.valuation (c • y) < 1
    have hc : v.toValuationSubring.valuation (algebraMap k F₀ c) ≤ 1 :=
      (v.toValuationSubring.valuation_le_one_iff _).mpr (v.algebraMap_mem' c)
    rw [Algebra.smul_def, map_mul]
    calc v.toValuationSubring.valuation (algebraMap k F₀ c) * v.toValuationSubring.valuation y
        ≤ 1 * v.toValuationSubring.valuation y := mul_le_mul_left hc _
      _ = v.toValuationSubring.valuation y := one_mul _
      _ < 1 := hy

theorem

mem_Nsub

L781 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.mem_Nsub

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Existence
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

theorem mem_Nsub (v : Place k F₀) (y : F₀) : y ∈ Nsub v ↔ v.toValuationSubring.valuation y < 1

theorem

linearIndependent_pow_theta

L784 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.linearIndependent_pow_theta

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Existence
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · full declaration

theorem linearIndependent_pow_theta (v : Place k F₀) (θ : v.toValuationSubring) :
    LinearIndependent k
      (fun i : Fin (minpoly k (IsLocalRing.residue _ θ)).natDegree => (θ : F₀) ^ (i : ℕ)) := by
  rw [Fintype.linearIndependent_iff]
  intro a ha
  apply coeff_eq_zero_of_sum_smul_pow_mem v θ a
  rw [ha, map_zero]
  exact zero_lt_one

theorem

disjoint_span_pow_Nsub

L793 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.disjoint_span_pow_Nsub

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Existence
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · full declaration

theorem disjoint_span_pow_Nsub (v : Place k F₀) (θ : v.toValuationSubring) :
    Disjoint (Submodule.span k (Set.range
      (fun i : Fin (minpoly k (IsLocalRing.residue _ θ)).natDegree => (θ : F₀) ^ (i : ℕ))))
      (Nsub v) := by
  rw [Submodule.disjoint_def]
  intro x hx hN
  obtain ⟨a, rfl⟩ := (Submodule.mem_span_range_iff_exists_fun k).mp hx
  have := coeff_eq_zero_of_sum_smul_pow_mem v θ a hN
  simp [this]

theorem

algebraMap_mem_span_image

L803 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.algebraMap_mem_span_image

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Existence
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

theorem algebraMap_mem_span_image {t : Set F₀} {z : F₀} (hz : z ∈ Submodule.span k t) :
    ι z ∈ Submodule.span K (algebraMap F₀ F '' t)

theorem

coeff_eq_zero_of_LD

L816 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.coeff_eq_zero_of_LD

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Existence
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

theorem coeff_eq_zero_of_LD
    (hLD : ∀ (n : ℕ) (f : Fin n → F₀) (c : Fin n → K), LinearIndependent k f →
      ∑ i, algebraMap K F (c i) * algebraMap F₀ F (f i) = 0 → ∀ i, c i = 0)
    (v : Place k F₀) (θ : v.toValuationSubring)
    (a : Fin (minpoly k (IsLocalRing.residue _ θ)).natDegree → K) {y : F}
    (hy : y ∈ Submodule.span K (algebraMap F₀ F '' (Nsub v : Set F₀)))
    (h : ∑ i, a i • ι (θ : F₀) ^ (i : ℕ) = y) : ∀ i, a i = 0

theorem

valuation_pi_lt_one

L873 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.valuation_pi_lt_one

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Existence
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

theorem valuation_pi_lt_one (v : Place k F₀) {π : v.toValuationSubring} (hπ : Irreducible π) :
    v.toValuationSubring.valuation (π : F₀) < 1

theorem

aeval_divByMonic_ne

L878 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.aeval_divByMonic_ne

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Existence
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

theorem aeval_divByMonic_ne
    (hLD : ∀ (n : ℕ) (f : Fin n → F₀) (c : Fin n → K), LinearIndependent k f →
      ∑ i, algebraMap K F (c i) * algebraMap F₀ F (f i) = 0 → ∀ i, c i = 0)
    (v : Place k F₀) [Module.Finite k v.ResidueField] {θ π : v.toValuationSubring}
    (hπ : Irreducible π) {α : K}
    (hα : ((minpoly k (IsLocalRing.residue _ θ)).map (algebraMap k K)).IsRoot α)
    {r₀ : F} (hr₀ : r₀ ∈ Rv K F v) :
    aeval (ι (θ : F₀)) (((minpoly k (IsLocalRing.residue _ θ)).map (algebraMap k K))
      /ₘ (X - C α)) ≠ ι (π : F₀) * r₀

theorem

exists_place_of_isRoot

L920 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.exists_place_of_isRoot

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section Existence
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]
local notation "ι" => algebraMap F₀ F

Lean source · statement

theorem exists_place_of_isRoot
    (hLD : ∀ (n : ℕ) (f : Fin n → F₀) (c : Fin n → K), LinearIndependent k f →
      ∑ i, algebraMap K F (c i) * algebraMap F₀ F (f i) = 0 → ∀ i, c i = 0)
    (hsepx : ∃ x : F, FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F ∧
      Algebra.IsSeparable (IntermediateField.adjoin K ({x} : Set F)) F)
    (hb : ∀ W : Place K F, ResBij W)
    (v : Place k F₀) [Module.Finite k v.ResidueField] {θ π : v.toValuationSubring}
    (hπ : Irreducible π) {α : K}
    (hα : ((minpoly k (IsLocalRing.residue _ θ)).map (algebraMap k K)).IsRoot α) :
    ∃ W : Place K F, ∃ hW : Over v W, αv W (hb W) hW θ = α

theorem

essFiniteType_of_gen

L1002 ↗

AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint.AlgebraicCurve.CFEFibre.essFiniteType_of_gen

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace CFEFibre
section EssFinite
variable {k K F₀ F : Type*} [Field k] [Field K] [Field F₀] [Field F]
  [Algebra k F₀] [Algebra K F] [Algebra F₀ F] [Algebra k K] [Algebra k F]
  [IsScalarTower k K F] [IsScalarTower k F₀ F]

Lean source · statement

theorem essFiniteType_of_gen (hfg : ∃ s : Finset F₀, IntermediateField.adjoin k (s : Set F₀) = ⊤)
    (hgen : IntermediateField.adjoin K (Set.range (algebraMap F₀ F)) = ⊤) :
    Algebra.EssFiniteType K F

theorem

natCard_setOf_comap_eq_eq_deg_of_linearDisjoint

L1028 ↗

AlgebraicCurve.Place.natCard_setOf_comap_eq_eq_deg_of_linearDisjoint

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
noncomputable section
open Polynomial IsLocalRing
open _root_.AlgebraicCurve AlgebraicCurve AlgebraicCurve.CFEFibre Polynomial in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.natCard_setOf_comap_eq_eq_deg_of_linearDisjoint
    {k K F₀ F : Type*} [Field k] [PerfectField k] [Field K] [IsAlgClosed K]
    [Field F₀] [Field F] [Algebra k F₀] [Algebra K F] [Algebra F₀ F]
    [Algebra k K] [Algebra k F] [IsScalarTower k K F] [IsScalarTower k F₀ F]
    [AlgebraicCurve.IsCurveOver k F₀] [AlgebraicCurve.IsCurveOver K F]
    (hfg : ∃ s : Finset F₀, IntermediateField.adjoin k (s : Set F₀) = ⊤)
    (hgen : IntermediateField.adjoin K (Set.range (algebraMap F₀ F)) = ⊤)
    (hLD : ∀ (n : ℕ) (f : Fin n → F₀) (c : Fin n → K), LinearIndependent k f →
      ∑ i, algebraMap K F (c i) * algebraMap F₀ F (f i) = 0 → ∀ i, c i = 0)
    (v : AlgebraicCurve.Place k F₀) :
    {W : AlgebraicCurve.Place K F |
        W.toValuationSubring.comap (algebraMap F₀ F) = v.toValuationSubring}.Finite ∧
    Nat.card {W : AlgebraicCurve.Place K F |
        W.toValuationSubring.comap (algebraMap F₀ F) = v.toValuationSubring} = v.deg ∧
    ∀ W₁ W₂ : AlgebraicCurve.Place K F,
      W₁.toValuationSubring.comap (algebraMap F₀ F) = v.toValuationSubring →
      W₂.toValuationSubring.comap (algebraMap F₀ F) = v.toValuationSubring →
      (∀ f : F₀, f ∈ v.toValuationSubring → ∀ a : K,
        algebraMap F₀ F f - algebraMap K F a ∈ W₁.toValuationSubring.nonunits →
        algebraMap F₀ F f - algebraMap K F a ∈ W₂.toValuationSubring.nonunits) →
      W₁ = W₂

Module documentation

Place nat Card set Of comap eq eq deg of linear Disjoint

Declarations