NYLL
Module

Place_inertiaDeg_eq_inertiaDeg_fiberCenter.lean

Nyll.AlgebraicCurves.Places.Place_inertiaDeg_eq_inertiaDeg_fiberCenter
14 declarations indexed from sourceView source ↗

Module documentation

Place inertia Deg eq inertia Deg fiber Center

Imports3
Imported by5

Declarations

def

toValuationSubringOfRestrictEq

L48 ↗
AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber.AlgebraicCurve.Place.toValuationSubringOfRestrictEq
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber
open _root_.AlgebraicCurves.Places.Proofs
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {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'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
def toValuationSubringOfRestrictEq (hw : w.restrict F = v) :
    integralClosureAt F' v →+* w.toValuationSubring
theorem

coe_toValuationSubringOfRestrictEq

L55 ↗
AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber.AlgebraicCurve.Place.coe_toValuationSubringOfRestrictEq
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber
open _root_.AlgebraicCurves.Places.Proofs
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {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'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
omit [FiniteDimensional F F'] in
Lean source · statement
theorem coe_toValuationSubringOfRestrictEq (hw : w.restrict F = v)
    (c : integralClosureAt F' v) :
    (toValuationSubringOfRestrictEq hw c : F')
      = algebraMap (integralClosureAt F' v) F' c
def

residueOfCenter

L60 ↗
AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber.AlgebraicCurve.Place.residueOfCenter
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber
open _root_.AlgebraicCurves.Places.Proofs
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {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'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
def residueOfCenter (hw : w.restrict F = v) :
    integralClosureAt F' v →+* w.ResidueField
theorem

residueOfCenter_apply

L65 ↗
AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber.AlgebraicCurve.Place.residueOfCenter_apply
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber
open _root_.AlgebraicCurves.Places.Proofs
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {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'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
omit [FiniteDimensional F F'] in
Lean source · statement
theorem residueOfCenter_apply (hw : w.restrict F = v) (c : integralClosureAt F' v) :
    residueOfCenter hw c = IsLocalRing.residue w.toValuationSubring
      (toValuationSubringOfRestrictEq hw c)
theorem

ker_residueOfCenter

L69 ↗
AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber.AlgebraicCurve.Place.ker_residueOfCenter
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber
open _root_.AlgebraicCurves.Places.Proofs
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {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'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem ker_residueOfCenter (hw : w.restrict F = v) :
    RingHom.ker (residueOfCenter hw) = (fiberCenter F' v hw).asIdeal
theorem

surjective_residueOfCenter

L75 ↗
AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber.AlgebraicCurve.Place.surjective_residueOfCenter
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber
open _root_.AlgebraicCurves.Places.Proofs
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {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'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem surjective_residueOfCenter (hw : w.restrict F = v) :
    Function.Surjective (residueOfCenter hw)
def

residueFieldEquivQuotientCenter

L137 ↗
AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber.AlgebraicCurve.Place.residueFieldEquivQuotientCenter
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber
open _root_.AlgebraicCurves.Places.Proofs
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {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'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
def residueFieldEquivQuotientCenter (hw : w.restrict F = v) :
    integralClosureAt F' v ⧸ (fiberCenter F' v hw).asIdeal ≃+* w.ResidueField
theorem

residueFieldEquivQuotientCenter_mk

L142 ↗
AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber.AlgebraicCurve.Place.residueFieldEquivQuotientCenter_mk
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber
open _root_.AlgebraicCurves.Places.Proofs
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {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'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem residueFieldEquivQuotientCenter_mk (hw : w.restrict F = v)
    (c : integralClosureAt F' v) :
    residueFieldEquivQuotientCenter hw (Ideal.Quotient.mk _ c) = residueOfCenter hw c
def

placeCongrEquiv

L151 ↗
AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber.AlgebraicCurve.Place.placeCongrEquiv
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber
open _root_.AlgebraicCurves.Places.Proofs
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {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'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · full declaration
def placeCongrEquiv {u u' : Place K F} (h : u = u') :
    u.toValuationSubring ≃+* u'.toValuationSubring where
  toFun x := ⟨x.1, h ▸ x.2⟩
  invFun x := ⟨x.1, h.symm ▸ x.2⟩
  left_inv _ := rfl
  right_inv _ := rfl
  map_mul' _ _ := rfl
  map_add' _ _ := rfl
theorem

coe_placeCongrEquiv

L160 ↗
AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber.AlgebraicCurve.Place.coe_placeCongrEquiv
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber
open _root_.AlgebraicCurves.Places.Proofs
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {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'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem coe_placeCongrEquiv {u u' : Place K F} (h : u = u') (x : u.toValuationSubring) :
    (placeCongrEquiv h x : F) = (x : F)
def

restrictResidueFieldEquiv

L163 ↗
AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber.AlgebraicCurve.Place.restrictResidueFieldEquiv
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber
open _root_.AlgebraicCurves.Places.Proofs
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {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'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
def restrictResidueFieldEquiv (hw : w.restrict F = v) :
    (w.restrict F).ResidueField ≃+* IsLocalRing.ResidueField v.toValuationSubring
theorem

restrictResidueFieldEquiv_residue

L168 ↗
AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber.AlgebraicCurve.Place.restrictResidueFieldEquiv_residue
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber
open _root_.AlgebraicCurves.Places.Proofs
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {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'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
omit [FiniteDimensional F F'] in
Lean source · statement
theorem restrictResidueFieldEquiv_residue (hw : w.restrict F = v)
    (a : (w.restrict F).toValuationSubring) :
    restrictResidueFieldEquiv hw (IsLocalRing.residue _ a)
      = IsLocalRing.residue _ (placeCongrEquiv hw a)
theorem

inertiaDeg_eq_inertiaDeg_fiberCenter

L175 ↗
AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber.AlgebraicCurve.Place.inertiaDeg_eq_inertiaDeg_fiberCenter
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber
open _root_.AlgebraicCurves.Places.Proofs
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {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'] [Algebra.IsSeparable F F']
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem inertiaDeg_eq_inertiaDeg_fiberCenter (hw : w.restrict F = v) :
    w.inertiaDeg F =
      (fiberCenter F' v hw).asIdeal.inertiaDeg v.toValuationSubring
theorem

inertiaDeg_eq_inertiaDeg_fiberCenter

L214 ↗
AlgebraicCurve.Place.inertiaDeg_eq_inertiaDeg_fiberCenter
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceInertiaDegInertiaDegFiber
open _root_.AlgebraicCurves.Places.Proofs
open _root_.AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.Place.inertiaDeg_eq_inertiaDeg_fiberCenter {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'] [Algebra.IsSeparable F F'] (v : Place K F) {w : Place K F'}
    (hw : w.restrict F = v) :
    w.inertiaDeg F = (Place.fiberCenter F' v hw).asIdeal.inertiaDeg v.toValuationSubring

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