NYLL
Module

Place_mk_mem_maximalIdeal_iff.lean

Nyll.AlgebraicCurves.Places.Place_mk_mem_maximalIdeal_iff
15 declarations indexed from sourceView source ↗

Module documentation

Place mk mem maximal Ideal iff

Imports4
Imported by5

Declarations

theorem

ord_nonneg_of_mem

L33 ↗
AlgebraicCurve.Place.ord_nonneg_of_mem
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ord_nonneg_of_mem {f : F} (hf : f ∈
  v.toValuationSubring) : 0 ≤ v.ord f
theorem

mem_of_ord_nonneg

L49 ↗
AlgebraicCurve.Place.mem_of_ord_nonneg
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mem_of_ord_nonneg {f : F} (hf : f ≠ 0) (h : 0 ≤ v.ord
  f) :
    f ∈ v.toValuationSubring
theorem

mem_iff_ord_nonneg

L58 ↗
AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff.AlgebraicCurve.Place.mem_iff_ord_nonneg
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem mem_iff_ord_nonneg {f : F} (hf : f ≠ 0) :
    f ∈ v.toValuationSubring ↔ 0 ≤ v.ord f
theorem

degree_eq_sum_support

L72 ↗
AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff.AlgebraicCurve.Divisor.degree_eq_sum_support
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open scoped _root_.AlgebraicCurve.Divisor in
Lean source · statement
theorem Divisor.degree_eq_sum_support (D : Divisor K F) :
    Divisor.degree D = ∑ v ∈ D.support, D v * (v.deg : ℤ)
theorem

degree_nonneg_of_nonneg

L78 ↗
AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff.AlgebraicCurve.Divisor.degree_nonneg_of_nonneg
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D : Divisor K F}
open scoped _root_.AlgebraicCurve.Divisor in
Lean source · statement
theorem Divisor.degree_nonneg_of_nonneg [IsCurveOver K F]
    {D : Divisor K F} (hD : ∀ v, 0 ≤ D v) : 0 ≤ Divisor.degree D
theorem

lSpace_eq_bot_of_degree_neg

L82 ↗
AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff.AlgebraicCurve.lSpace_eq_bot_of_degree_neg
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D : Divisor K F}
Lean source · statement
theorem lSpace_eq_bot_of_degree_neg [IsCurveOver K F]
    (hD : Divisor.degree D < 0) : LSpace D = ⊥
theorem

ell_eq_zero_of_degree_neg

L98 ↗
AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff.AlgebraicCurve.ell_eq_zero_of_degree_neg
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D : Divisor K F}
Lean source · statement
theorem ell_eq_zero_of_degree_neg [IsCurveOver K F] (hD : Divisor.degree D < 0) :
    ell D = 0
theorem

mk_mem_maximalIdeal_iff_port

L122 ↗
AlgebraicCurve.Place.mk_mem_maximalIdeal_iff_port
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F)
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mk_mem_maximalIdeal_iff_port {f : F} (hf : f ∈
  v.toValuationSubring) :
    (⟨f, hf⟩ : v.toValuationSubring) ∈ IsLocalRing.maximalIdeal v.toValuationSubring
      ↔ f = 0 ∨ 0 < v.ord f
theorem

ell_le_ell_sub_single_add_deg

L152 ↗
AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff.AlgebraicCurve.ell_le_ell_sub_single_add_deg
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ell_le_ell_sub_single_add_deg [IsCurveOver K F] (D : Divisor K F) (P : Place K F) :
    ell D ≤ ell (D - Finsupp.single P 1) + P.deg
theorem

one_le_deg

L244 ↗
AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff.AlgebraicCurve.one_le_deg
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem one_le_deg [IsCurveOver K F] (P : Place K F) : 1 ≤ P.deg
theorem

ell_le_degree_add_ellZero

L248 ↗
AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff.AlgebraicCurve.ell_le_degree_add_ellZero
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ell_le_degree_add_ellZero [IsCurveOver K F] {D : Divisor K F}
    (hD : ∀ v, 0 ≤ D v) :
    (ell D : ℤ) ≤ Divisor.degree D + ell (0 : Divisor K F)
theorem

ell_le_degree_add_one_of_effective

L285 ↗
AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff.AlgebraicCurve.ell_le_degree_add_one_of_effective
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ell_le_degree_add_one_of_effective [IsCurveOver K F]
    (hC : ConstantsAreBase K F) {D : Divisor K F} (hD : ∀ v, 0 ≤ D v) :
    (ell D : ℤ) ≤ Divisor.degree D + 1
def

lSpaceShiftEquiv

L294 ↗
AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff.AlgebraicCurve.lSpaceShiftEquiv
Documentation

Multiplication by the inverse of g identifies the spaces for divisors differing by its divisor.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · full declaration
def lSpaceShiftEquiv (D : Divisor K F) {g : F} (hg : g ≠ 0)
    {Dg : Divisor K F} (hDg : ∀ v, Dg v = v.ord g) :
    LSpace D ≃ₗ[K] LSpace (D + Dg) where
  toFun h := ⟨(h : F) * g⁻¹, by
    rw [mem_lSpace_iff_ord]
    rcases eq_or_ne (h : F) 0 with hh0 | hh0
    · left; rw [hh0, zero_mul]
    · right; intro v
      rw [Finsupp.add_apply, hDg, v.ord_mul hh0 (inv_ne_zero hg), v.ord_inv]
      have := (mem_lSpace_iff_ord.mp h.2).resolve_left hh0 v
      linarith⟩
  invFun k := ⟨(k : F) * g, by
    rw [mem_lSpace_iff_ord]
    rcases eq_or_ne (k : F) 0 with hk0 | hk0
    · left; rw [hk0, zero_mul]
    · right; intro v
      have := (mem_lSpace_iff_ord.mp k.2).resolve_left hk0 v
      rw [Finsupp.add_apply, hDg] at this
      rw [v.ord_mul hk0 hg]
      linarith⟩
  map_add' h₁ h₂ := by apply Subtype.ext; push_cast; ring
  map_smul' c h := by
    apply Subtype.ext
    simp only [RingHom.id_apply, SetLike.val_smul, Algebra.smul_def]
    ring
  left_inv h := by
    apply Subtype.ext
    change (h : F) * g⁻¹ * g = (h : F)
    rw [mul_assoc, inv_mul_cancel₀ hg, mul_one]
  right_inv k := by
    apply Subtype.ext
    change (k : F) * g * g⁻¹ = (k : F)
    rw [mul_assoc, mul_inv_cancel₀ hg, mul_one]
theorem

ell_le_degree_add_one

L328 ↗
AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff.AlgebraicCurve.ell_le_degree_add_one
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ell_le_degree_add_one [IsCurveOver K F] (hC : ConstantsAreBase K F)
    {D : Divisor K F} (hD : 0 ≤ Divisor.degree D) :
    (ell D : ℤ) ≤ Divisor.degree D + 1
theorem

mk_mem_maximalIdeal_iff

L354 ↗
AlgebraicCurve.Place.mk_mem_maximalIdeal_iff
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff
open _root_.AlgebraicCurve
  _root_.AlgebraicCurves.Places.Proofs.Place_mk_mem_maximalIdeal_iff.AlgebraicCurve in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mk_mem_maximalIdeal_iff {K F : Type*} [Field K] [Field F]
  [Algebra K F] (v : Place K F) {f : F} (hf : f ∈ v.toValuationSubring) :
    (⟨f, hf⟩ : v.toValuationSubring) ∈ IsLocalRing.maximalIdeal v.toValuationSubring
      ↔ f = 0 ∨ 0 < v.ord f

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