NYLL
Module

Place_module_finite_residueField_restrict.lean

Nyll.AlgebraicCurves.Places.Place_module_finite_residueField_restrict
7 declarations indexed from sourceView source ↗

Module documentation

Place module finite residue Field restrict

Imports1
Imported by3

Declarations

theorem

mem_of_ord_nonneg'

L39 ↗
AlgebraicCurve.Place.mem_of_ord_nonneg'
Source context 12 commands

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

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

restrictSubringHom

L57 ↗
AlgebraicCurve.Place.restrictSubringHom
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_module_finite_residueField_restrict
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F'] [Algebra K F] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] (w : Place K F')
Lean source · statement
abbrev _root_.AlgebraicCurve.Place.restrictSubringHom : (w.restrict F).toValuationSubring
  →+* w.toValuationSubring
theorem

coe_restrictSubringHom

L62 ↗
AlgebraicCurves.Places.Proofs.Place_module_finite_residueField_restrict.AlgebraicCurve.Place.coe_restrictSubringHom
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_module_finite_residueField_restrict
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F'] [Algebra K F] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] (w : Place K F')
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem coe_restrictSubringHom (x : (w.restrict F).toValuationSubring) :
    (w.restrictSubringHom x : F') = algebraMap F F' (x : F)
theorem

algebraMap_residueField_residue

L65 ↗
AlgebraicCurves.Places.Proofs.Place_module_finite_residueField_restrict.AlgebraicCurve.Place.algebraMap_residueField_residue
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_module_finite_residueField_restrict
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F'] [Algebra K F] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] (w : Place K F')
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem algebraMap_residueField_residue (x : (w.restrict F).toValuationSubring) :
    algebraMap (w.restrict F).ResidueField w.ResidueField
        (IsLocalRing.residue _ x)
      = IsLocalRing.residue _ (w.restrictSubringHom x)
theorem

linearIndependent_of_residue

L71 ↗
AlgebraicCurve.Place.linearIndependent_of_residue
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_module_finite_residueField_restrict
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F'] [Algebra K F] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] (w : Place K F')
open _root_.AlgebraicCurve.Place
Lean source · full declaration
theorem _root_.AlgebraicCurve.Place.linearIndependent_of_residue {n : ℕ} {b : Fin n →
  w.ResidueField}
    (hb : LinearIndependent (w.restrict F).ResidueField b)
    (b' : Fin n → w.toValuationSubring)
    (hb' : ∀ i, IsLocalRing.residue _ (b' i) = b i) :
    LinearIndependent F (fun i => (b' i : F')) := by
  classical
  rw [Fintype.linearIndependent_iff]
  intro g hg
  by_contra hne
  push Not at hne
  obtain ⟨i₀, hi₀⟩ := hne
  set v : Place K F := w.restrict F with hv
  set T : Finset (Fin n) := Finset.univ.filter fun i => g i ≠ 0 with hT
  have hT₀ : T.Nonempty := ⟨i₀, by simp [hT, hi₀]⟩
  obtain ⟨j, hjT, hjmin⟩ := T.exists_min_image (fun i => v.ord (g i)) hT₀
  have hgj : g j ≠ 0 := by simpa [hT] using hjT
  have hcmem : ∀ i, g i / g j ∈ v.toValuationSubring := by
    intro i
    rcases eq_or_ne (g i) 0 with h0 | h0
    · simp [h0, zero_div]
    · refine v.mem_of_ord_nonneg' (div_ne_zero h0 hgj) ?_
      have hle := hjmin i (by simp [hT, h0])
      rw [div_eq_mul_inv, v.ord_mul h0 (inv_ne_zero hgj), v.ord_inv]
      omega
  set c : (i : Fin n) → v.toValuationSubring := fun i => ⟨g i / g j, hcmem i⟩ with hc
  have hsum : (∑ i, w.restrictSubringHom (c i) * b' i) = 0 := by
    have hinj : Function.Injective
        (Subtype.val : w.toValuationSubring → F') := Subtype.val_injective
    apply hinj
    push_cast
    simp only [coe_restrictSubringHom]
    change (∑ i, algebraMap F F' (g i / g j) * (b' i : F')) = (0 : F')
    have hrescale : ∀ i, algebraMap F F' (g i / g j) * (b' i : F')
        = (g j)⁻¹ • (g i • (b' i : F')) := by
      intro i
      rw [smul_smul, Algebra.smul_def, div_eq_inv_mul, map_mul]
    simp only [hrescale]
    rw [← Finset.smul_sum, hg, smul_zero]
  have hres : (∑ i, (IsLocalRing.residue _ (c i)) • b i) = 0 := by
    have := congrArg (IsLocalRing.residue w.toValuationSubring) hsum
    rw [map_sum, map_zero] at this
    convert this using 2 with i
    rw [Algebra.smul_def, algebraMap_residueField_residue, ← hb' i, ← map_mul]
  have hzero := Fintype.linearIndependent_iff.mp hb _ hres j
  have hcj : c j = 1 := by
    ext
    change g j / g j = 1
    exact div_self hgj
  rw [hcj, map_one] at hzero
  exact one_ne_zero hzero
theorem

module_finite_residueField_restrict'

L125 ↗
AlgebraicCurve.Place.module_finite_residueField_restrict'
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_module_finite_residueField_restrict
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F'] [Algebra K F] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] (w : Place K F')
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.module_finite_residueField_restrict' [Module.Finite F
  F'] :
    Module.Finite (w.restrict F).ResidueField w.ResidueField
theorem

module_finite_residueField_restrict

L151 ↗
AlgebraicCurve.Place.module_finite_residueField_restrict
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_module_finite_residueField_restrict
open _root_.AlgebraicCurve
  _root_.AlgebraicCurves.Places.Proofs.Place_module_finite_residueField_restrict.AlgebraicCurve in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.module_finite_residueField_restrict (K F F' : Type*)
    [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F
      F']
    [FiniteDimensional F F'] (w : Place K F') :
    Module.Finite (w.restrict F).ResidueField w.ResidueField

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