NYLL
Module

Place_ramificationIndexAlong_eq_one_of_pow_eq_of_mem_of_inv_mem.lean

Nyll.AlgebraicCurves.Places.Place_ramificationIndexAlong_eq_one_of_pow_eq_of_mem_of_inv_mem
8 declarations indexed from sourceView source ↗

Module documentation

Place ramification Index Along eq one of pow eq of mem of inv mem

Imports3
Imported by1

Declarations

theorem

mem_nonunits_comap_iff

L37 ↗
AlgebraicCurves.Places.Proofs.Place_ramificationIndexAlong_eq_one_of_pow_eq_of_mem_of_inv_mem.AlgebraicCurve.KummerUnram.mem_nonunits_comap_iff
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ramificationIndexAlong_eq_one_of_pow_eq_of_mem_of_inv_mem
open _root_.Polynomial
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace KummerUnram
open _root_.AlgebraicCurve
section Transport
variable {K K' : Type*} [Field K] [Field K']
Lean source · statement
theorem mem_nonunits_comap_iff (A : ValuationSubring K') (φ : K →+* K') (x : K) :
    x ∈ (A.comap φ).nonunits ↔ φ x ∈ A.nonunits
theorem

inv_mem_of_not_mem_nonunits

L43 ↗
AlgebraicCurves.Places.Proofs.Place_ramificationIndexAlong_eq_one_of_pow_eq_of_mem_of_inv_mem.AlgebraicCurve.KummerUnram.inv_mem_of_not_mem_nonunits
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ramificationIndexAlong_eq_one_of_pow_eq_of_mem_of_inv_mem
open _root_.Polynomial
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace KummerUnram
open _root_.AlgebraicCurve
section Transport
variable {K K' : Type*} [Field K] [Field K']
Lean source · statement
theorem inv_mem_of_not_mem_nonunits (A : ValuationSubring K) {x : K} (h : x ∉ A.nonunits) : x⁻¹ ∈ A
theorem

ne_top_of_mem_nonunits

L48 ↗
AlgebraicCurves.Places.Proofs.Place_ramificationIndexAlong_eq_one_of_pow_eq_of_mem_of_inv_mem.AlgebraicCurve.KummerUnram.ne_top_of_mem_nonunits
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ramificationIndexAlong_eq_one_of_pow_eq_of_mem_of_inv_mem
open _root_.Polynomial
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace KummerUnram
open _root_.AlgebraicCurve
section Transport
variable {K K' : Type*} [Field K] [Field K']
Lean source · statement
theorem ne_top_of_mem_nonunits (A : ValuationSubring K) {x : K} (hx : x ∈ A.nonunits) (hx0 : x ≠ 0)
  : A ≠ ⊤
theorem

mem_nonunits_of_mem_of_not_isUnit

L56 ↗
AlgebraicCurves.Places.Proofs.Place_ramificationIndexAlong_eq_one_of_pow_eq_of_mem_of_inv_mem.AlgebraicCurve.KummerUnram.mem_nonunits_of_mem_of_not_isUnit
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ramificationIndexAlong_eq_one_of_pow_eq_of_mem_of_inv_mem
open _root_.Polynomial
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace KummerUnram
open _root_.AlgebraicCurve
section Transport
variable {K K' : Type*} [Field K] [Field K']
Lean source · statement
theorem mem_nonunits_of_mem_of_not_isUnit (A : ValuationSubring K) {x : K} (hx : x ∈ A) (h : ¬
  IsUnit (⟨x, hx⟩ : A)) :
    x ∈ A.nonunits
theorem

nonunits_mul_mem

L61 ↗
AlgebraicCurves.Places.Proofs.Place_ramificationIndexAlong_eq_one_of_pow_eq_of_mem_of_inv_mem.AlgebraicCurve.KummerUnram.nonunits_mul_mem
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ramificationIndexAlong_eq_one_of_pow_eq_of_mem_of_inv_mem
open _root_.Polynomial
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace KummerUnram
open _root_.AlgebraicCurve
section Transport
variable {K K' : Type*} [Field K] [Field K']
Lean source · statement
theorem nonunits_mul_mem (A : ValuationSubring K) {x y : K} (hx : x ∈ A.nonunits) (hy : y ∈ A) : x
  * y ∈ A.nonunits
theorem

not_mem_nonunits_of_inv_mem

L69 ↗
AlgebraicCurves.Places.Proofs.Place_ramificationIndexAlong_eq_one_of_pow_eq_of_mem_of_inv_mem.AlgebraicCurve.KummerUnram.not_mem_nonunits_of_inv_mem
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ramificationIndexAlong_eq_one_of_pow_eq_of_mem_of_inv_mem
open _root_.Polynomial
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace KummerUnram
open _root_.AlgebraicCurve
section Transport
variable {K K' : Type*} [Field K] [Field K']
Lean source · statement
theorem not_mem_nonunits_of_inv_mem (A : ValuationSubring K) {x : K} (hx0 : x ≠ 0) (hxi : x⁻¹ ∈ A)
  : x ∉ A.nonunits
theorem

valuation_eq_one_of_mem_of_not_mem_nonunits

L74 ↗
AlgebraicCurves.Places.Proofs.Place_ramificationIndexAlong_eq_one_of_pow_eq_of_mem_of_inv_mem.AlgebraicCurve.KummerUnram.valuation_eq_one_of_mem_of_not_mem_nonunits
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ramificationIndexAlong_eq_one_of_pow_eq_of_mem_of_inv_mem
open _root_.Polynomial
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace KummerUnram
open _root_.AlgebraicCurve
section Transport
variable {K K' : Type*} [Field K] [Field K']
Lean source · statement
theorem valuation_eq_one_of_mem_of_not_mem_nonunits (A : ValuationSubring K) {x : K} (hx : x ∈ A)
  (hxn : x ∉ A.nonunits) :
    A.valuation x = 1
theorem

ramificationIndexAlong_eq_one_of_pow_eq_of_mem_of_inv_mem

L85 ↗
AlgebraicCurve.Place.ramificationIndexAlong_eq_one_of_pow_eq_of_mem_of_inv_mem
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ramificationIndexAlong_eq_one_of_pow_eq_of_mem_of_inv_mem
open _root_.Polynomial
open _root_.AlgebraicCurve
open AlgebraicCurve.KummerUnram in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ramificationIndexAlong_eq_one_of_pow_eq_of_mem_of_inv_mem
    {k F F' : Type*} [Field k] [IsAlgClosed k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
    (φ : F →ₐ[k] F') (hφ : φ.toRingHom.IsIntegral)
    (n : ℕ) (hn : (n : k) ≠ 0)
    (c : F') (hgen : Subfield.closure (Set.range φ ∪ {c}) = ⊤)
    (u : F) (hu : φ u = c ^ n)
    (P : AlgebraicCurve.Place k F')
    (hrat : (P.restrictAlong φ hφ).IsRational)
    (huP : u ∈ (P.restrictAlong φ hφ).toValuationSubring ∧ u⁻¹ ∈ (P.restrictAlong φ
      hφ).toValuationSubring) :
    P.ramificationIndexAlong φ = 1

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