NYLL
Module

ValuationSubring_exists_le_forall_mem_iff_apply_mem.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_le_forall_mem_iff_apply_mem
8 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring exists le forall mem iff apply mem

Imports5
  • Mathlib.Algebra.Group.Units.Defs
  • Mathlib.Algebra.Group.Units.Hom
  • Mathlib.RingTheory.Ideal.Maps
  • Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
  • Mathlib.RingTheory.Valuation.ValuationSubring
Imported by2

Declarations

theorem

exists_inv_mem

L37 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_le_forall_mem_iff_apply_mem.ValuationSubring.W9OComposite.exists_inv_mem
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_le_forall_mem_iff_apply_mem
namespace ValuationSubring
open _root_.ValuationSubring
namespace W9OComposite
open _root_.ValuationSubring
variable {F : Type*} [Field F] (O : ValuationSubring F)
variable {Kbar : Type*} [Field Kbar] (res : O →+* Kbar)
variable (hker : IsLocalRing.maximalIdeal O ≤ RingHom.ker res)
include hker in
Lean source · statement
theorem exists_inv_mem (x : F) (hx : x ∈ O) (h0 : res ⟨x, hx⟩ ≠ 0) :
    ∃ hx' : x⁻¹ ∈ O, res ⟨x⁻¹, hx'⟩ = (res ⟨x, hx⟩)⁻¹
theorem

apply_eq_zero_of_not_isUnit

L58 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_le_forall_mem_iff_apply_mem.ValuationSubring.W9OComposite.apply_eq_zero_of_not_isUnit
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_le_forall_mem_iff_apply_mem
namespace ValuationSubring
open _root_.ValuationSubring
namespace W9OComposite
open _root_.ValuationSubring
variable {F : Type*} [Field F] (O : ValuationSubring F)
variable {Kbar : Type*} [Field Kbar] (res : O →+* Kbar)
variable (hker : IsLocalRing.maximalIdeal O ≤ RingHom.ker res)
include hker in
Lean source · statement
theorem apply_eq_zero_of_not_isUnit (x : O) (hx : ¬IsUnit x) : res x = 0
def

composite

L62 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_le_forall_mem_iff_apply_mem.ValuationSubring.W9OComposite.composite
Documentation

The composite valuation ring consisting of elements of O whose residue lies in W.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_le_forall_mem_iff_apply_mem
namespace ValuationSubring
open _root_.ValuationSubring
namespace W9OComposite
open _root_.ValuationSubring
variable {F : Type*} [Field F] (O : ValuationSubring F)
variable {Kbar : Type*} [Field Kbar] (res : O →+* Kbar)
variable (hker : IsLocalRing.maximalIdeal O ≤ RingHom.ker res)
Lean source · full declaration
def composite (W : ValuationSubring Kbar) : ValuationSubring F where
  carrier := {x | ∃ hx : x ∈ O, res ⟨x, hx⟩ ∈ W}
  mul_mem' := by
    rintro a b ⟨ha, haW⟩ ⟨hb, hbW⟩
    refine ⟨MulMemClass.mul_mem ha hb, ?_⟩
    have : (⟨a * b, MulMemClass.mul_mem ha hb⟩ : O) = ⟨a, ha⟩ * ⟨b, hb⟩ := rfl
    rw [this, map_mul]
    exact MulMemClass.mul_mem haW hbW
  one_mem' := ⟨O.one_mem, by
    have : (⟨(1 : F), O.one_mem⟩ : O) = 1 := rfl
    rw [this, map_one]; exact W.one_mem⟩
  add_mem' := by
    rintro a b ⟨ha, haW⟩ ⟨hb, hbW⟩
    refine ⟨AddMemClass.add_mem ha hb, ?_⟩
    have : (⟨a + b, AddMemClass.add_mem ha hb⟩ : O) = ⟨a, ha⟩ + ⟨b, hb⟩ := rfl
    rw [this, map_add]
    exact AddMemClass.add_mem haW hbW
  zero_mem' := ⟨O.zero_mem, by
    have : (⟨(0 : F), O.zero_mem⟩ : O) = 0 := rfl
    rw [this, map_zero]; exact W.zero_mem⟩
  neg_mem' := by
    rintro a ⟨ha, haW⟩
    refine ⟨NegMemClass.neg_mem ha, ?_⟩
    have : (⟨-a, NegMemClass.neg_mem ha⟩ : O) = -⟨a, ha⟩ := rfl
    rw [this, map_neg]
    exact NegMemClass.neg_mem haW
  mem_or_inv_mem' := by
    intro x
    by_cases hx : x ∈ O
    · by_cases hW : res ⟨x, hx⟩ ∈ W
      · exact Or.inl ⟨hx, hW⟩
      · right
        have h0 : res ⟨x, hx⟩ ≠ 0 := by
          rintro h; exact hW (h ▸ W.zero_mem)
        obtain ⟨hx', hres⟩ := exists_inv_mem O res hker x hx h0
        refine ⟨hx', ?_⟩
        rw [hres]
        rcases W.mem_or_inv_mem (res ⟨x, hx⟩) with h | h
        · exact (hW h).elim
        · exact h
    · right
      have hx' : x⁻¹ ∈ O := (O.mem_or_inv_mem x).resolve_left hx
      refine ⟨hx', ?_⟩
      have hnu : ¬IsUnit (⟨x⁻¹, hx'⟩ : O) := by
        intro hu
        have h0 : res ⟨x⁻¹, hx'⟩ ≠ 0 := (hu.map res).ne_zero
        obtain ⟨hx'', -⟩ := exists_inv_mem O res hker x⁻¹ hx' h0
        exact hx (by simpa using hx'')
      rw [apply_eq_zero_of_not_isUnit O res hker _ hnu]
      exact W.zero_mem
theorem

mem_composite_iff

L115 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_le_forall_mem_iff_apply_mem.ValuationSubring.W9OComposite.mem_composite_iff
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_le_forall_mem_iff_apply_mem
namespace ValuationSubring
open _root_.ValuationSubring
namespace W9OComposite
open _root_.ValuationSubring
variable {F : Type*} [Field F] (O : ValuationSubring F)
variable {Kbar : Type*} [Field Kbar] (res : O →+* Kbar)
variable (hker : IsLocalRing.maximalIdeal O ≤ RingHom.ker res)
variable (W : ValuationSubring Kbar)
Lean source · statement
theorem mem_composite_iff {x : F} :
    x ∈ composite O res hker W ↔ ∃ hx : x ∈ O, res ⟨x, hx⟩ ∈ W
theorem

composite_le

L118 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_le_forall_mem_iff_apply_mem.ValuationSubring.W9OComposite.composite_le
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_le_forall_mem_iff_apply_mem
namespace ValuationSubring
open _root_.ValuationSubring
namespace W9OComposite
open _root_.ValuationSubring
variable {F : Type*} [Field F] (O : ValuationSubring F)
variable {Kbar : Type*} [Field Kbar] (res : O →+* Kbar)
variable (hker : IsLocalRing.maximalIdeal O ≤ RingHom.ker res)
variable (W : ValuationSubring Kbar)
Lean source · statement
theorem composite_le : composite O res hker W ≤ O
theorem

coe_mem_composite_iff

L121 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_le_forall_mem_iff_apply_mem.ValuationSubring.W9OComposite.coe_mem_composite_iff
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_le_forall_mem_iff_apply_mem
namespace ValuationSubring
open _root_.ValuationSubring
namespace W9OComposite
open _root_.ValuationSubring
variable {F : Type*} [Field F] (O : ValuationSubring F)
variable {Kbar : Type*} [Field Kbar] (res : O →+* Kbar)
variable (hker : IsLocalRing.maximalIdeal O ≤ RingHom.ker res)
variable (W : ValuationSubring Kbar)
Lean source · statement
theorem coe_mem_composite_iff (x : O) : (x : F) ∈ composite O res hker W ↔ res x ∈ W
theorem

coe_mem_nonunits_composite_iff

L125 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_le_forall_mem_iff_apply_mem.ValuationSubring.W9OComposite.coe_mem_nonunits_composite_iff
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_le_forall_mem_iff_apply_mem
namespace ValuationSubring
open _root_.ValuationSubring
namespace W9OComposite
open _root_.ValuationSubring
variable {F : Type*} [Field F] (O : ValuationSubring F)
variable {Kbar : Type*} [Field Kbar] (res : O →+* Kbar)
variable (hker : IsLocalRing.maximalIdeal O ≤ RingHom.ker res)
variable (W : ValuationSubring Kbar)
Lean source · statement
theorem coe_mem_nonunits_composite_iff (x : O) :
    (x : F) ∈ (composite O res hker W).nonunits ↔ res x ∈ W.nonunits
theorem

exists_le_forall_mem_iff_apply_mem

L177 ↗
ValuationSubring.exists_le_forall_mem_iff_apply_mem
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_le_forall_mem_iff_apply_mem
open ValuationSubring.W9OComposite in
Lean source · statement
theorem _root_.ValuationSubring.exists_le_forall_mem_iff_apply_mem
    {F : Type*} [Field F] (O : ValuationSubring F)
    {Kbar : Type*} [Field Kbar] (res : O →+* Kbar)
    (hker : IsLocalRing.maximalIdeal O ≤ RingHom.ker res)
    (W : ValuationSubring Kbar) :
    ∃ O' : ValuationSubring F, O' ≤ O ∧
      (∀ x : O, (x : F) ∈ O' ↔ res x ∈ W) ∧
      (∀ x : O, (x : F) ∈ O'.nonunits ↔ res x ∈ W.nonunits)

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