NYLL
Module

Place_evalAt_norm_eq_prod_fiber.lean

Nyll.AlgebraicCurves.Places.Place_evalAt_norm_eq_prod_fiber
38 declarations indexed from sourceView source ↗

Module documentation

Place eval At norm eq prod fiber

Imports17
Imported by2

Declarations

instance

(anonymous instance)

L61 ↗
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
instance : DecidableEq (Place K F')
instance

(anonymous instance)

L65 ↗
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
Lean source · statement
instance : Module.Free v.toValuationSubring (integralClosureAt F' v)
abbrev

conductorIdeal

L69 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.conductorIdeal
Documentation

The extension of the maximal ideal of the base valuation ring to the integral closure.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
Lean source · statement
abbrev conductorIdeal : Ideal (integralClosureAt F' v)
theorem

conductorIdeal_ne_top

L74 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.conductorIdeal_ne_top
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
omit [Algebra K F'] [IsScalarTower K F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F']
  [CharZero F] in
Lean source · statement
theorem conductorIdeal_ne_top : conductorIdeal (F' := F') v ≠ ⊤
theorem

conductorIdeal_ne_bot

L86 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.conductorIdeal_ne_bot
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
omit [Algebra K F'] [IsScalarTower K F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F']
  [CharZero F] in
Lean source · statement
theorem conductorIdeal_ne_bot : conductorIdeal (F' := F') v ≠ ⊥
instance

conductorQuotientAlgebra

L95 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.conductorQuotientAlgebra
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
Lean source · statement
instance conductorQuotientAlgebra :
    Algebra (IsLocalRing.ResidueField v.toValuationSubring)
      (integralClosureAt F' v ⧸ conductorIdeal (F' := F') v)
theorem

residue_norm_eq_norm_mk

L101 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.residue_norm_eq_norm_mk
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
local instance : DecidableEq (Place K F') := Classical.decEq _
variable (v : Place K F)
omit [Algebra K F'] [IsScalarTower K F F'] [CharZero F] in
Lean source · statement
theorem residue_norm_eq_norm_mk (c : integralClosureAt F' v) :
    IsLocalRing.residue v.toValuationSubring
        (Algebra.norm v.toValuationSubring c)
      = Algebra.norm (IsLocalRing.ResidueField v.toValuationSubring)
          (Ideal.Quotient.mk (conductorIdeal (F' := F') v) c)
abbrev

fiberCenterPow

L138 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.fiberCenterPow
Documentation

The ideal of the fibre centre raised to its ramification index.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {v : Place K F} {w : Place K F'}
Lean source · statement
abbrev fiberCenterPow (hw : w.restrict F = v) : Ideal (integralClosureAt F' v)
theorem

conductorIdeal_le_fiberCenterPow

L143 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.conductorIdeal_le_fiberCenterPow
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {v : Place K F} {w : Place K F'}
omit [CharZero F] in
Lean source · statement
theorem conductorIdeal_le_fiberCenterPow (hw : w.restrict F = v) :
    conductorIdeal (F' := F') v ≤ fiberCenterPow hw
theorem

fiberCenterPow_ne_top

L147 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.fiberCenterPow_ne_top
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {v : Place K F} {w : Place K F'}
omit [CharZero F] in
Lean source · statement
theorem fiberCenterPow_ne_top (hw : w.restrict F = v) : fiberCenterPow hw ≠ ⊤
instance

fiberCenterPowQuotientAlgebra

L159 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.fiberCenterPowQuotientAlgebra
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {v : Place K F} {w : Place K F'}
Lean source · statement
instance fiberCenterPowQuotientAlgebra (hw : w.restrict F = v) :
    Algebra (IsLocalRing.ResidueField v.toValuationSubring)
      (integralClosureAt F' v ⧸ fiberCenterPow hw)
instance

(anonymous instance)

L165 ↗
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {v : Place K F} {w : Place K F'}
Lean source · statement
instance (hw : w.restrict F = v) :
    Module.Finite (IsLocalRing.ResidueField v.toValuationSubring)
      (integralClosureAt F' v ⧸ fiberCenterPow hw)
theorem

isNilpotent_mk_sub_algebraMap

L176 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.isNilpotent_mk_sub_algebraMap
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {v : Place K F} {w : Place K F'}
omit [CharZero F] in
Lean source · statement
theorem isNilpotent_mk_sub_algebraMap (hw : w.restrict F = v) {c : integralClosureAt F' v}
    {r : v.toValuationSubring}
    (hr : c - algebraMap v.toValuationSubring (integralClosureAt F' v) r
      ∈ (fiberCenter F' v hw).asIdeal) :
    IsNilpotent (Ideal.Quotient.mk (fiberCenterPow hw) c
      - algebraMap (IsLocalRing.ResidueField v.toValuationSubring)
          (integralClosureAt F' v ⧸ fiberCenterPow hw)
          (IsLocalRing.residue v.toValuationSubring r))
theorem

norm_mk_fiberCenterPow

L194 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.norm_mk_fiberCenterPow
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {v : Place K F} {w : Place K F'}
omit [CharZero F] in
Lean source · statement
theorem norm_mk_fiberCenterPow (hw : w.restrict F = v) {c : integralClosureAt F' v}
    {r : v.toValuationSubring}
    (hr : c - algebraMap v.toValuationSubring (integralClosureAt F' v) r
      ∈ (fiberCenter F' v hw).asIdeal) :
    Algebra.norm (IsLocalRing.ResidueField v.toValuationSubring)
        (Ideal.Quotient.mk (fiberCenterPow hw) c)
      = IsLocalRing.residue v.toValuationSubring r
          ^ Module.finrank (IsLocalRing.ResidueField v.toValuationSubring)
              (integralClosureAt F' v ⧸ fiberCenterPow hw)
theorem

finrank_fiberCenterPow

L206 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.finrank_fiberCenterPow
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {v : Place K F} {w : Place K F'}
omit [CharZero F] in
Lean source · statement
theorem finrank_fiberCenterPow (hw : w.restrict F = v) (hwrat : w.IsRational)
    (hvrat : v.IsRational) :
    Module.finrank (IsLocalRing.ResidueField v.toValuationSubring)
        (integralClosureAt F' v ⧸ fiberCenterPow hw)
      = w.ramificationIndex F
instance

(anonymous instance)

L240 ↗
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F) [HasPrincipalDivisors K F']
Lean source · statement
instance : DecidableEq (Place K F')
def

fiberIdeal

L244 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.fiberIdeal
Documentation

The ramification power for a place above v, and the unit ideal for other places.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F) [HasPrincipalDivisors K F']
local instance : DecidableEq (Place K F') := Classical.decEq _
omit [CharZero F] [HasPrincipalDivisors K F'] in
Lean source · statement
def fiberIdeal (w : Place K F') : Ideal (integralClosureAt F' v)
theorem

fiberIdeal_of_mem

L247 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.fiberIdeal_of_mem
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F) [HasPrincipalDivisors K F']
local instance : DecidableEq (Place K F') := Classical.decEq _
omit [CharZero F] [HasPrincipalDivisors K F'] in
Lean source · statement
theorem fiberIdeal_of_mem {w : Place K F'} (hw : w.restrict F = v) :
    fiberIdeal v w = fiberCenterPow hw
theorem

fiberIdeal_of_notMem

L250 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.fiberIdeal_of_notMem
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F) [HasPrincipalDivisors K F']
local instance : DecidableEq (Place K F') := Classical.decEq _
omit [CharZero F] [HasPrincipalDivisors K F'] in
Lean source · statement
theorem fiberIdeal_of_notMem {w : Place K F'} (hw : ¬w.restrict F = v) :
    fiberIdeal v w = ⊤
theorem

conductorIdeal_le_fiberIdeal

L253 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.conductorIdeal_le_fiberIdeal
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F) [HasPrincipalDivisors K F']
local instance : DecidableEq (Place K F') := Classical.decEq _
omit [CharZero F] [HasPrincipalDivisors K F'] in
Lean source · statement
theorem conductorIdeal_le_fiberIdeal (w : Place K F') :
    conductorIdeal (F' := F') v ≤ fiberIdeal v w
theorem

isCoprime_fiberIdeal

L261 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.isCoprime_fiberIdeal
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F) [HasPrincipalDivisors K F']
local instance : DecidableEq (Place K F') := Classical.decEq _
omit [CharZero F] [HasPrincipalDivisors K F'] in
Lean source · statement
theorem isCoprime_fiberIdeal {w w' : Place K F'} (hne : w ≠ w') :
    IsCoprime (fiberIdeal v w) (fiberIdeal v w')
theorem

count_normalizedFactors_conductorIdeal

L278 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.count_normalizedFactors_conductorIdeal
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F) [HasPrincipalDivisors K F']
local instance : DecidableEq (Place K F') := Classical.decEq _
omit [CharZero F] [HasPrincipalDivisors K F'] in
Lean source · statement
theorem count_normalizedFactors_conductorIdeal {w : Place K F'} (hw : w.restrict F = v) :
    (normalizedFactors (conductorIdeal (F' := F') v)).count (fiberCenter F' v hw).asIdeal
      = (IsLocalRing.maximalIdeal v.toValuationSubring).ramificationIdx'
          (fiberCenter F' v hw).asIdeal
theorem

conductorIdeal_eq_prod_fiber

L286 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.conductorIdeal_eq_prod_fiber
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F) [HasPrincipalDivisors K F']
local instance : DecidableEq (Place K F') := Classical.decEq _
omit [CharZero F] in
Lean source · statement
theorem conductorIdeal_eq_prod_fiber :
    conductorIdeal (F' := F') v = ∏ w ∈ v.fiber F', fiberIdeal v w
theorem

prod_fiberIdeal_le_of_subset

L330 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.prod_fiberIdeal_le_of_subset
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F) [HasPrincipalDivisors K F']
local instance : DecidableEq (Place K F') := Classical.decEq _
omit [CharZero F] [HasPrincipalDivisors K F'] in
Lean source · statement
theorem prod_fiberIdeal_le_of_subset {s t : Finset (Place K F')} (hst : s ⊆ t) :
    ∏ w ∈ t, fiberIdeal v w ≤ ∏ w ∈ s, fiberIdeal v w
theorem

conductorIdeal_le_prod_fiberIdeal

L336 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.conductorIdeal_le_prod_fiberIdeal
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F) [HasPrincipalDivisors K F']
local instance : DecidableEq (Place K F') := Classical.decEq _
omit [CharZero F] in
Lean source · statement
theorem conductorIdeal_le_prod_fiberIdeal (s : Finset (Place K F')) :
    conductorIdeal (F' := F') v ≤ ∏ w ∈ s, fiberIdeal v w
instance

(anonymous instance)

L356 ↗
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F) [HasPrincipalDivisors K F']
Lean source · statement
instance : DecidableEq (Place K F')
instance

fiberIdealQuotientAlgebra

L358 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.fiberIdealQuotientAlgebra
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F) [HasPrincipalDivisors K F']
local instance : DecidableEq (Place K F') := Classical.decEq _
Lean source · statement
instance fiberIdealQuotientAlgebra (w : Place K F') :
    Algebra (IsLocalRing.ResidueField v.toValuationSubring)
      (integralClosureAt F' v ⧸ fiberIdeal v w)
instance

prodFiberIdealQuotientAlgebra

L364 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.prodFiberIdealQuotientAlgebra
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F) [HasPrincipalDivisors K F']
local instance : DecidableEq (Place K F') := Classical.decEq _
Lean source · statement
instance prodFiberIdealQuotientAlgebra (s : Finset (Place K F')) :
    Algebra (IsLocalRing.ResidueField v.toValuationSubring)
      (integralClosureAt F' v ⧸ ∏ w ∈ s, fiberIdeal v w)
theorem

finite_quotient_of_conductorLE

L371 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.finite_quotient_of_conductorLE
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F) [HasPrincipalDivisors K F']
local instance : DecidableEq (Place K F') := Classical.decEq _
omit [Algebra K F'] [IsScalarTower K F F'] [CharZero F] [HasPrincipalDivisors K F'] in
Lean source · statement
theorem finite_quotient_of_conductorLE (Q : Ideal (integralClosureAt F' v))
    [Algebra (IsLocalRing.ResidueField v.toValuationSubring) (integralClosureAt F' v ⧸ Q)]
    [IsScalarTower v.toValuationSubring (IsLocalRing.ResidueField v.toValuationSubring)
      (integralClosureAt F' v ⧸ Q)] :
    Module.Finite (IsLocalRing.ResidueField v.toValuationSubring)
      (integralClosureAt F' v ⧸ Q)
theorem

norm_mk_prod_fiberIdeal

L380 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.norm_mk_prod_fiberIdeal
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F) [HasPrincipalDivisors K F']
local instance : DecidableEq (Place K F') := Classical.decEq _
omit [CharZero F] in
Lean source · statement
theorem norm_mk_prod_fiberIdeal (c : integralClosureAt F' v) (s : Finset (Place K F')) :
    Algebra.norm (IsLocalRing.ResidueField v.toValuationSubring)
        (Ideal.Quotient.mk (∏ w ∈ s, fiberIdeal v w) c)
      = ∏ w ∈ s,
          Algebra.norm (IsLocalRing.ResidueField v.toValuationSubring)
            (Ideal.Quotient.mk (fiberIdeal v w) c)
theorem

norm_mk_conductor_eq_prod_fiber

L459 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.norm_mk_conductor_eq_prod_fiber
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F) [HasPrincipalDivisors K F']
local instance : DecidableEq (Place K F') := Classical.decEq _
omit [CharZero F] in
Lean source · statement
theorem norm_mk_conductor_eq_prod_fiber (c : integralClosureAt F' v) :
    Algebra.norm (IsLocalRing.ResidueField v.toValuationSubring)
        (Ideal.Quotient.mk (conductorIdeal (F' := F') v) c)
      = ∏ w ∈ v.fiber F',
          Algebra.norm (IsLocalRing.ResidueField v.toValuationSubring)
            (Ideal.Quotient.mk (fiberIdeal v w) c)
theorem

sub_algebraMap_evalAt_mem_fiberCenter

L489 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.sub_algebraMap_evalAt_mem_fiberCenter
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {v : Place K F} [HasPrincipalDivisors K F']
omit [CharZero F] [HasPrincipalDivisors K F'] in
Lean source · statement
theorem sub_algebraMap_evalAt_mem_fiberCenter {w : Place K F'} (hw : w.restrict F = v)
    (hwrat : w.IsRational) {c : integralClosureAt F' v}
    (_hc : algebraMap (integralClosureAt F' v) F' c ≠ 0)
    (_hord : w.ord (algebraMap (integralClosureAt F' v) F' c) = 0) :
    c - algebraMap v.toValuationSubring (integralClosureAt F' v)
        (algebraMap K v.toValuationSubring
          (w.evalAt (algebraMap (integralClosureAt F' v) F' c)))
      ∈ (fiberCenter F' v hw).asIdeal
instance

(anonymous instance)

L544 ↗
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {v : Place K F} [HasPrincipalDivisors K F']
Lean source · statement
instance : DecidableEq (Place K F')
theorem

algebraMap_evalAt_coe

L547 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.algebraMap_evalAt_coe
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {v : Place K F} [HasPrincipalDivisors K F']
local instance : DecidableEq (Place K F') := Classical.decEq _
omit [CharZero F] in
Lean source · statement
theorem algebraMap_evalAt_coe (hv : v.IsRational) (r : v.toValuationSubring) :
    algebraMap K v.ResidueField
        (v.evalAt (algebraMap v.toValuationSubring F r))
      = IsLocalRing.residue v.toValuationSubring r
theorem

residue_algebraMap

L556 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.residue_algebraMap
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {v : Place K F} [HasPrincipalDivisors K F']
local instance : DecidableEq (Place K F') := Classical.decEq _
omit [CharZero F] in
Lean source · statement
theorem residue_algebraMap (lam : K) :
    IsLocalRing.residue v.toValuationSubring (algebraMap K v.toValuationSubring lam)
      = algebraMap K v.ResidueField lam
theorem

norm_mk_fiberIdeal_eq_norm_mk_fiberCenterPow

L561 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.norm_mk_fiberIdeal_eq_norm_mk_fiberCenterPow
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {v : Place K F} [HasPrincipalDivisors K F']
local instance : DecidableEq (Place K F') := Classical.decEq _
omit [CharZero F] [HasPrincipalDivisors K F'] in
Lean source · statement
theorem norm_mk_fiberIdeal_eq_norm_mk_fiberCenterPow {w : Place K F'}
    (hw : w.restrict F = v) (c : integralClosureAt F' v) :
    Algebra.norm (IsLocalRing.ResidueField v.toValuationSubring)
        (Ideal.Quotient.mk (fiberIdeal v w) c)
      = Algebra.norm (IsLocalRing.ResidueField v.toValuationSubring)
          (Ideal.Quotient.mk (fiberCenterPow hw) c)
theorem

residue_norm_eq_prod_evalAt

L579 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place.residue_norm_eq_prod_evalAt
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
noncomputable section
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {v : Place K F} [HasPrincipalDivisors K F']
local instance : DecidableEq (Place K F') := Classical.decEq _
omit [CharZero F] in
Lean source · statement
theorem residue_norm_eq_prod_evalAt (hv : v.IsRational)
    (hrat : ∀ w ∈ v.fiber F', Place.IsRational w) {c : integralClosureAt F' v}
    (hc : algebraMap (integralClosureAt F' v) F' c ≠ 0)
    (hord : ∀ w ∈ v.fiber F', w.ord (algebraMap (integralClosureAt F' v) F' c) = 0) :
    IsLocalRing.residue v.toValuationSubring (Algebra.norm v.toValuationSubring c)
      = ∏ w ∈ v.fiber F',
          algebraMap K v.ResidueField
              (w.evalAt (algebraMap (integralClosureAt F' v) F' c))
            ^ w.ramificationIndex F
theorem

evalAt_norm_eq_prod_fiber

L606 ↗
AlgebraicCurve.Place.evalAt_norm_eq_prod_fiber
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
open IsDedekindDomain IsLocalRing UniqueFactorizationMonoid _root_.AlgebraicCurve
  _root_.AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve
  _root_.AlgebraicCurve.Place
  _root_.AlgebraicCurves.Places.Proofs.Place_evalAt_norm_eq_prod_fiber.AlgebraicCurve.Place in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.evalAt_norm_eq_prod_fiber {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'] [HasPrincipalDivisors K F'] (v : Place K F) (f : F') (hf : f ≠
  0) (hv : v.IsRational) (hrat : ∀ w ∈ v.fiber F', Place.IsRational w) (hord : ∀ w ∈ v.fiber F',
  w.ord f = 0) : v.evalAt (Algebra.norm F f) = ∏ w ∈ v.fiber F', w.evalAt f ^ (w.ramificationIndex
  F)

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