Module

CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.lean

Nyll.AlgebraicCurves.Models.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl

27 declarations indexed from sourceView source ↗

Module documentation

Curve Model range sections eq map eval2 poly Part inv Poly Part of coe eq compl

Imports6

Imported by4

abbrev

ι

L46 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.ι

Documentation

The homomorphism evaluating Laurent polynomials at the rational function variable.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K]

Lean source · statement

abbrev ι : LaurentPolynomial K →+* RatFunc K

theorem

ι_T

L50 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.ι_T

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K]

Lean source · statement

theorem ι_T (n : ℤ) : ι K (LaurentPolynomial.T n) = (RatFunc.X : RatFunc K) ^ n

theorem

ι_C

L53 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.ι_C

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K]

Lean source · statement

theorem ι_C (a : K) : ι K (LaurentPolynomial.C a) = algebraMap K (RatFunc K) a

theorem

ι_comp_toLaurent

L56 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.ι_comp_toLaurent

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K]

Lean source · statement

theorem ι_comp_toLaurent : (ι K).comp Polynomial.toLaurent = algebraMap K[X] (RatFunc K)

theorem

ι_toLaurent

L62 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.ι_toLaurent

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K]

Lean source · statement

theorem ι_toLaurent (p : K[X]) : ι K (Polynomial.toLaurent p) = algebraMap K[X] (RatFunc K) p

theorem

ι_injective

L65 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.ι_injective

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K]

Lean source · statement

theorem ι_injective : Function.Injective (ι K)

theorem

mem_polyPart_iff

L74 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.mem_polyPart_iff

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K]

Lean source · statement

theorem mem_polyPart_iff (f : LaurentPolynomial K) :
    f ∈ TwoChartCech.polyPart K ↔ ∃ p : K[X], Polynomial.toLaurent p = f

theorem

map_polyPart_eq_range_algebraMap

L99 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.map_polyPart_eq_range_algebraMap

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K]

Lean source · statement

theorem map_polyPart_eq_range_algebraMap :
    (TwoChartCech.polyPart K).toSubring.map (ι K) = (algebraMap K[X] (RatFunc K)).range

theorem

forall_valuation_le_one_iff

L109 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.forall_valuation_le_one_iff

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K]

Lean source · statement

theorem forall_valuation_le_one_iff (g : RatFunc K) :
    (∀ w : HeightOneSpectrum K[X], w.valuation (RatFunc K) g ≤ 1) ↔ g ∈ (algebraMap K[X] (RatFunc
      K)).range

theorem

valuation_X_eq_one_of_ne

L117 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.valuation_X_eq_one_of_ne

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K]

Lean source · statement

theorem valuation_X_eq_one_of_ne {w : HeightOneSpectrum K[X]} (hw : w ≠ Polynomial.idealX K) :
    w.valuation (RatFunc K) RatFunc.X = 1

theorem

forall_ne_valuation_le_one_iff

L129 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.forall_ne_valuation_le_one_iff

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K]

Lean source · statement

theorem forall_ne_valuation_le_one_iff (g : RatFunc K) :
    (∀ w : HeightOneSpectrum K[X], w ≠ Polynomial.idealX K → w.valuation (RatFunc K) g ≤ 1) ↔
      g ∈ (ι K).range

theorem

mul_T_apply

L175 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.mul_T_apply

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K]

Lean source · statement

theorem mul_T_apply (f : LaurentPolynomial K) (n m : ℤ) :
    (f * LaurentPolynomial.T n : LaurentPolynomial K).coeff m = f.coeff (m - n)

theorem

toLaurent_apply_natCast

L180 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.toLaurent_apply_natCast

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K]

Lean source · statement

theorem toLaurent_apply_natCast (p : K[X]) (k : ℕ) :
    (Polynomial.toLaurent p : LaurentPolynomial K).coeff (k : ℤ) = p.coeff k

theorem

toLaurent_apply_of_neg

L185 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.toLaurent_apply_of_neg

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K]

Lean source · statement

theorem toLaurent_apply_of_neg (p : K[X]) (m : ℤ) (hm : m < 0) :
    (Polynomial.toLaurent p : LaurentPolynomial K).coeff m = 0

theorem

mem_invPolyPart_iff_natDegree_le

L191 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.mem_invPolyPart_iff_natDegree_le

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K]

Lean source · statement

theorem mem_invPolyPart_iff_natDegree_le {f : LaurentPolynomial K} {n : ℕ} {p : K[X]}
    (hp : Polynomial.toLaurent p = f * LaurentPolynomial.T (n : ℤ)) :
    f ∈ TwoChartCech.invPolyPart K ↔ p.natDegree ≤ n

theorem

inftyValuation_ι_le_one_iff

L218 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.inftyValuation_ι_le_one_iff

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K]
variable [DecidableEq (RatFunc K)]

Lean source · statement

theorem inftyValuation_ι_le_one_iff {f : LaurentPolynomial K} {n : ℕ} {p : K[X]}
    (hp : Polynomial.toLaurent p = f * LaurentPolynomial.T (n : ℤ)) (hp0 : p ≠ 0) :
    RatFunc.inftyValuation K (ι K f) ≤ 1 ↔ p.natDegree ≤ n

theorem

map_invPolyPart_eq

L235 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.map_invPolyPart_eq

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K]
variable [DecidableEq (RatFunc K)]

Lean source · statement

theorem map_invPolyPart_eq :
    (TwoChartCech.invPolyPart K).toSubring.map (ι K) =
      (ι K).range ⊓ (RationalFunctionField.placeInfty K).toValuationSubring.toSubring

theorem

place_eq_ofHeightOneSpectrum_or_eq_placeInfty

L275 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.place_eq_ofHeightOneSpectrum_or_eq_placeInfty

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K] [DecidableEq (RatFunc K)]
open _root_.AlgebraicCurve.RationalFunctionField in

Lean source · statement

theorem place_eq_ofHeightOneSpectrum_or_eq_placeInfty (v : Place K (RatFunc K)) :
    (∃ w : HeightOneSpectrum K[X], v = Place.ofHeightOneSpectrum w) ∨ v = placeInfty K

theorem

ofHeightOneSpectrum_ne_placeInfty

L284 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.ofHeightOneSpectrum_ne_placeInfty

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K] [DecidableEq (RatFunc K)]

Lean source · statement

theorem ofHeightOneSpectrum_ne_placeInfty (w : HeightOneSpectrum K[X]) :
    Place.ofHeightOneSpectrum (K := K) (F := RatFunc K) w ≠ RationalFunctionField.placeInfty K

theorem

mem_ofHeightOneSpectrum_iff

L292 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.mem_ofHeightOneSpectrum_iff

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K] [DecidableEq (RatFunc K)]
omit [DecidableEq (RatFunc K)] in

Lean source · statement

theorem mem_ofHeightOneSpectrum_iff (w : HeightOneSpectrum K[X]) (g : RatFunc K) :
    g ∈ (Place.ofHeightOneSpectrum (K := K) (F := RatFunc K) w).toValuationSubring ↔
      w.valuation (RatFunc K) g ≤ 1

theorem

placeOfPoint_zero_eq

L297 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.placeOfPoint_zero_eq

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K] [DecidableEq (RatFunc K)]
omit [DecidableEq (RatFunc K)] in

Lean source · statement

theorem placeOfPoint_zero_eq :
    RationalFunctionField.placeOfPoint K 0 = Place.ofHeightOneSpectrum (Polynomial.idealX K)

theorem

iInf_ne_placeInfty_eq

L305 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.iInf_ne_placeInfty_eq

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K] [DecidableEq (RatFunc K)]

Lean source · statement

theorem iInf_ne_placeInfty_eq :
    (⨅ (v : Place K (RatFunc K)) (_ : v ≠ RationalFunctionField.placeInfty K),
      v.toValuationSubring.toSubring) =
      (TwoChartCech.polyPart K).toSubring.map (ι K)

theorem

iInf_ne_ne_eq

L322 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.iInf_ne_ne_eq

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K] [DecidableEq (RatFunc K)]

Lean source · statement

theorem iInf_ne_ne_eq :
    (⨅ (v : Place K (RatFunc K)) (_ : v ≠ RationalFunctionField.placeInfty K)
        (_ : v ≠ RationalFunctionField.placeOfPoint K 0), v.toValuationSubring.toSubring) = (ι
          K).range

theorem

iInf_ne_placeOfPoint_zero_eq

L343 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.iInf_ne_placeOfPoint_zero_eq

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K] [DecidableEq (RatFunc K)]
omit [DecidableEq (RatFunc K)] in

Lean source · statement

theorem iInf_ne_placeOfPoint_zero_eq :
    (⨅ (v : Place K (RatFunc K)) (_ : v ≠ RationalFunctionField.placeOfPoint K 0),
      v.toValuationSubring.toSubring) =
      (TwoChartCech.invPolyPart K).toSubring.map (ι K)

theorem

range_sections_eq_iInf

L370 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.range_sections_eq_iInf

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K]

Lean source · statement

theorem range_sections_eq_iInf (M : CurveModel K (RatFunc K)) (W : M.C.Opens) (hW : IsAffineOpen W)
  [Nonempty W] :
    ((M.ffEquiv.symm : M.C.functionField ≃+* RatFunc K).toRingHom.comp
        (algebraMap Γ(M.C, W) M.C.functionField)).range =
      ⨅ (w : Place K (RatFunc K)) (_ : (M.placeEquiv.symm w).1 ∈ W), w.toValuationSubring.toSubring

theorem

coe_placeEquiv_symm_mem_iff_ne

L443 ↗

AlgebraicCurves.Models.Proofs.CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl.AlgebraicCurve.S1c.coe_placeEquiv_symm_mem_iff_ne

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace S1c
open _root_.AlgebraicCurve
variable (K : Type u) [Field K] [DecidableEq (RatFunc K)]
omit [DecidableEq (RatFunc K)] in

Lean source · statement

theorem coe_placeEquiv_symm_mem_iff_ne (M : CurveModel K (RatFunc K)) (W : M.C.Opens) (v₀ : Place K
  (RatFunc K))
    (hW : ((W : Set M.C)) = {(M.placeEquiv.symm v₀).1}ᶜ) (w : Place K (RatFunc K)) :
    (M.placeEquiv.symm w).1 ∈ W ↔ w ≠ v₀

theorem

range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl

L453 ↗

AlgebraicCurve.CurveModel.range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs
namespace CurveModel_range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.IsDedekindDomain
open scoped Polynomial
universe u
open AlgebraicCurve.S1c in

Lean source · statement

theorem
  _root_.AlgebraicCurve.CurveModel.range_sections_eq_map_eval2_polyPart_invPolyPart_of_coe_eq_compl
    (K : Type u) [Field K] [DecidableEq (RatFunc K)]
    (M : CurveModel K (RatFunc K)) (U V : M.C.Opens)
    (hU : IsAffineOpen U) (hV : IsAffineOpen V) (hUV : IsAffineOpen (U ⊓ V))
    [Nonempty U] [Nonempty V] [Nonempty (U ⊓ V : M.C.Opens)]
    (hUset : ((U : Set M.C)) = {(M.placeEquiv.symm (RationalFunctionField.placeInfty K)).1}ᶜ)
    (hVset : ((V : Set M.C)) = {(M.placeEquiv.symm (RationalFunctionField.placeOfPoint K 0)).1}ᶜ) :
    Function.Injective
        (LaurentPolynomial.eval₂ (algebraMap K (RatFunc K)) (Units.mk0 (RatFunc.X : RatFunc K)
          RatFunc.X_ne_zero)) ∧
      ((M.ffEquiv.symm : M.C.functionField ≃+* RatFunc K).toRingHom.comp
          (algebraMap Γ(M.C, U) M.C.functionField)).range =
        ((TwoChartCech.polyPart K).toSubring).map
          (LaurentPolynomial.eval₂ (algebraMap K (RatFunc K)) (Units.mk0 (RatFunc.X : RatFunc K)
            RatFunc.X_ne_zero)) ∧
      ((M.ffEquiv.symm : M.C.functionField ≃+* RatFunc K).toRingHom.comp
          (algebraMap Γ(M.C, V) M.C.functionField)).range =
        ((TwoChartCech.invPolyPart K).toSubring).map
          (LaurentPolynomial.eval₂ (algebraMap K (RatFunc K)) (Units.mk0 (RatFunc.X : RatFunc K)
            RatFunc.X_ne_zero)) ∧
      ((M.ffEquiv.symm : M.C.functionField ≃+* RatFunc K).toRingHom.comp
          (algebraMap Γ(M.C, U ⊓ V) M.C.functionField)).range =
        (LaurentPolynomial.eval₂ (algebraMap K (RatFunc K))
          (Units.mk0 (RatFunc.X : RatFunc K) RatFunc.X_ne_zero)).range

Module documentation

Curve Model range sections eq map eval2 poly Part inv Poly Part of coe eq compl

Declarations