NYLL
Module

Place_sum_ramificationIndex_mul_inertiaDeg_exchange.lean

Nyll.AlgebraicCurves.Places.Place_sum_ramificationIndex_mul_inertiaDeg_exchange
16 declarations indexed from sourceView source ↗

Module documentation

Place sum ramification Index mul inertia Deg exchange

Imports12
Imported by2

Declarations

theorem

inertiaDegAlong_congr

L42 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange.BifibreW2.inertiaDegAlong_congr
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange
open _root_.AlgebraicCurve
namespace BifibreW2
section AlongBridge
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem inertiaDegAlong_congr {φ φ' : F →ₐ[K] F'} (h : φ = φ') (hφ : φ.toRingHom.IsIntegral)
    (hφ' : φ'.toRingHom.IsIntegral) (w : Place K F') :
    w.inertiaDegAlong φ hφ = w.inertiaDegAlong φ' hφ'
theorem

isIntegral_toAlgHom

L49 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange.BifibreW2.isIntegral_toAlgHom
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange
open _root_.AlgebraicCurve
namespace BifibreW2
section AlongBridge
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable [Algebra F F'] [IsScalarTower K F F']
Lean source · statement
theorem isIntegral_toAlgHom [Algebra.IsIntegral F F'] :
    (IsScalarTower.toAlgHom K F F').toRingHom.IsIntegral
theorem

toAlgHom_comp_toAlgHom

L61 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange.BifibreW2.toAlgHom_comp_toAlgHom
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange
open _root_.AlgebraicCurve
namespace BifibreW2
section Tower
variable {K F E M : Type*} [Field K] [Field F] [Field E] [Field M]
    [Algebra K F] [Algebra K E] [Algebra K M] [Algebra F E] [Algebra E M] [Algebra F M]
    [IsScalarTower F E M] [IsScalarTower K F E] [IsScalarTower K E M] [IsScalarTower K F M]
Lean source · statement
theorem toAlgHom_comp_toAlgHom :
    (IsScalarTower.toAlgHom K E M).comp (IsScalarTower.toAlgHom K F E) =
      IsScalarTower.toAlgHom K F M
theorem

restrict_restrict

L66 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange.BifibreW2.restrict_restrict
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange
open _root_.AlgebraicCurve
namespace BifibreW2
section Tower
variable {K F E M : Type*} [Field K] [Field F] [Field E] [Field M]
    [Algebra K F] [Algebra K E] [Algebra K M] [Algebra F E] [Algebra E M] [Algebra F M]
    [IsScalarTower F E M] [IsScalarTower K F E] [IsScalarTower K E M] [IsScalarTower K F M]
Lean source · statement
theorem restrict_restrict [Algebra.IsIntegral F E] [Algebra.IsIntegral E M]
    [Algebra.IsIntegral F M] (W : Place K M) : (W.restrict E).restrict F = W.restrict F
theorem

ramificationIndex_eq_mul_ramificationIndex_restrict

L88 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange.AlgebraicCurve.Place.ramificationIndex_eq_mul_ramificationIndex_restrict
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange
open _root_.AlgebraicCurve
section TowerRows
variable {K F E M : Type*} [Field K] [Field F] [Field E] [Field M]
    [Algebra K F] [Algebra K E] [Algebra K M] [Algebra F E] [Algebra E M] [Algebra F M]
    [IsScalarTower F E M] [IsScalarTower K F E] [IsScalarTower K E M] [IsScalarTower K F M]
open scoped _root_.AlgebraicCurve _root_.AlgebraicCurve.Place in
Lean source · statement
theorem AlgebraicCurve.Place.ramificationIndex_eq_mul_ramificationIndex_restrict
    [Algebra.IsIntegral F E] [Algebra.IsIntegral E M] (W : Place K M) :
    W.ramificationIndex F = W.ramificationIndex E * (W.restrict E).ramificationIndex F
theorem

inertiaDeg_eq_mul_inertiaDeg_restrict

L100 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange.AlgebraicCurve.Place.inertiaDeg_eq_mul_inertiaDeg_restrict
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange
open _root_.AlgebraicCurve
section TowerRows
variable {K F E M : Type*} [Field K] [Field F] [Field E] [Field M]
    [Algebra K F] [Algebra K E] [Algebra K M] [Algebra F E] [Algebra E M] [Algebra F M]
    [IsScalarTower F E M] [IsScalarTower K F E] [IsScalarTower K E M] [IsScalarTower K F M]
open scoped _root_.AlgebraicCurve _root_.AlgebraicCurve.Place in
Lean source · statement
theorem AlgebraicCurve.Place.inertiaDeg_eq_mul_inertiaDeg_restrict
    [Algebra.IsIntegral F E] [Algebra.IsIntegral E M] [Algebra.IsIntegral F M] (W : Place K M) :
    W.inertiaDeg F = W.inertiaDeg E * (W.restrict E).inertiaDeg F
abbrev

Env

L119 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange.BifibreW2.Env
Documentation

The normal closure of the field extension inside the chosen algebraic closure.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange
open _root_.AlgebraicCurve
namespace BifibreW2
section Envelope
variable (F E : Type*) [Field F] [Field E] [Algebra F E]
Lean source · statement
abbrev Env : Type _
theorem

isGalois_env

L121 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange.BifibreW2.isGalois_env
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange
open _root_.AlgebraicCurve
namespace BifibreW2
section Envelope
variable (F E : Type*) [Field F] [Field E] [Algebra F E]
Lean source · statement
theorem isGalois_env [FiniteDimensional F E] [Algebra.IsSeparable F E] : IsGalois F (Env F E)
def

algebraEnv

L133 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange.BifibreW2.algebraEnv
Documentation

The base-ring algebra structure on the normal closure induced through the extension field.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange
open _root_.AlgebraicCurve
namespace BifibreW2
section Envelope
variable (F E : Type*) [Field F] [Field E] [Algebra F E]
variable (R : Type*) [Field R] [Algebra R E]
Lean source · statement
def algebraEnv : Algebra R (Env F E)
theorem

isScalarTower_env_mid

L136 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange.BifibreW2.isScalarTower_env_mid
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange
open _root_.AlgebraicCurve
namespace BifibreW2
section Envelope
variable (F E : Type*) [Field F] [Field E] [Algebra F E]
variable (R : Type*) [Field R] [Algebra R E]
Lean source · full declaration
theorem isScalarTower_env_mid : letI := algebraEnv F E R; IsScalarTower R E (Env F E) :=
  letI := algebraEnv F E R
  IsScalarTower.of_algebraMap_eq fun _ => rfl
theorem

isScalarTower_env_base

L140 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange.BifibreW2.isScalarTower_env_base
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange
open _root_.AlgebraicCurve
namespace BifibreW2
section Envelope
variable (F E : Type*) [Field F] [Field E] [Algebra F E]
variable (R : Type*) [Field R] [Algebra R E]
Lean source · full declaration
theorem isScalarTower_env_base [Algebra F R] [IsScalarTower F R E] :
    letI := algebraEnv F E R; IsScalarTower F R (Env F E) :=
  letI := algebraEnv F E R
  IsScalarTower.of_algebraMap_eq fun x => Subtype.ext (by
    change algebraMap F (AlgebraicClosure E) x =
      algebraMap E (AlgebraicClosure E) (algebraMap R E (algebraMap F R x))
    rw [← IsScalarTower.algebraMap_apply F R E x,
      ← IsScalarTower.algebraMap_apply F E (AlgebraicClosure E) x])
theorem

isScalarTower_env_bot

L151 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange.BifibreW2.isScalarTower_env_bot
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange
open _root_.AlgebraicCurve
namespace BifibreW2
section Envelope
variable (F E : Type*) [Field F] [Field E] [Algebra F E]
variable (R : Type*) [Field R] [Algebra R E]
variable (K : Type*) [Field K] [Algebra K F] [Algebra K E] [IsScalarTower K F E]
Lean source · full declaration
theorem isScalarTower_env_bot [Algebra K R] [IsScalarTower K R E] :
    letI := algebraEnv F E R; IsScalarTower K R (Env F E) :=
  letI := algebraEnv F E R
  IsScalarTower.of_algebraMap_eq fun x => Subtype.ext (by
    change algebraMap K (AlgebraicClosure E) x =
      algebraMap E (AlgebraicClosure E) (algebraMap R E (algebraMap K R x))
    rw [← IsScalarTower.algebraMap_apply K R E x,
      ← IsScalarTower.algebraMap_apply K E (AlgebraicClosure E) x])
theorem

isScalarTower_env_const

L160 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange.BifibreW2.isScalarTower_env_const
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange
open _root_.AlgebraicCurve
namespace BifibreW2
section Envelope
variable (F E : Type*) [Field F] [Field E] [Algebra F E]
variable (R : Type*) [Field R] [Algebra R E]
variable (K : Type*) [Field K] [Algebra K F] [Algebra K E] [IsScalarTower K F E]
omit [Algebra R E] in
Lean source · statement
theorem isScalarTower_env_const : IsScalarTower K E (Env F E)
theorem

exchange_of_isGalois

L168 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange.BifibreW2.exchange_of_isGalois
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange
open _root_.AlgebraicCurve
namespace BifibreW2
Lean source · statement
theorem exchange_of_isGalois {K F F₁ F₂ E : Type*} (M : Type*)
    [Field K] [Field F] [Field F₁] [Field F₂] [Field E] [Field M]
    [Algebra K F] [Algebra K F₁] [Algebra K F₂] [Algebra K E] [Algebra K M]
    [Algebra F F₁] [Algebra F F₂] [Algebra F E] [Algebra F M]
    [Algebra F₁ E] [Algebra F₂ E] [Algebra F₁ M] [Algebra F₂ M] [Algebra E M]
    [IsScalarTower K F F₁] [IsScalarTower K F F₂] [IsScalarTower K F E] [IsScalarTower K F M]
    [IsScalarTower K F₁ E] [IsScalarTower K F₂ E] [IsScalarTower K F₁ M] [IsScalarTower K F₂ M]
    [IsScalarTower K E M]
    [IsScalarTower F F₁ E] [IsScalarTower F F₂ E] [IsScalarTower F F₁ M] [IsScalarTower F F₂ M]
    [IsScalarTower F E M] [IsScalarTower F₁ E M] [IsScalarTower F₂ E M]
    [FiniteDimensional F F₁] [FiniteDimensional F F₂] [FiniteDimensional F E]
    [FiniteDimensional F₁ E] [FiniteDimensional F₂ E]
    [FiniteDimensional F M] [IsGalois F M]
    (hgen : Algebra.adjoin F (Set.range (algebraMap F₁ E) ∪ Set.range (algebraMap F₂ E)) = ⊤)
    (hLD : Module.finrank F E = Module.finrank F F₁ * Module.finrank F F₂)
    (v : Place K F) (w₁ : Place K F₁) (w₂ : Place K F₂)
    (hw₁ : w₁.restrict F = v) (hw₂ : w₂.restrict F = v)
    (T : Finset (Place K E)) (hT : ∀ W, W ∈ T ↔ W.restrict F₁ = w₁ ∧ W.restrict F₂ = w₂) :
    ∑ W ∈ T, W.ramificationIndex F₁ * W.inertiaDeg F₂ =
      w₁.inertiaDeg F * w₂.ramificationIndex F
theorem

sum_ramificationIndex_mul_inertiaDeg_bifiber_of_isSeparable

L219 ↗
AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange.AlgebraicCurve.Place.sum_ramificationIndex_mul_inertiaDeg_bifiber_of_isSeparable
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange
open _root_.AlgebraicCurve
open scoped _root_.AlgebraicCurve _root_.AlgebraicCurve.Place in
open BifibreW2 in
Lean source · statement
theorem AlgebraicCurve.Place.sum_ramificationIndex_mul_inertiaDeg_bifiber_of_isSeparable
    {K F F₁ F₂ E : Type*} [Field K] [Field F] [Field F₁] [Field F₂] [Field E]
    [Algebra K F] [Algebra K F₁] [Algebra K F₂] [Algebra K E]
    [Algebra F F₁] [Algebra F F₂] [Algebra F E] [Algebra F₁ E] [Algebra F₂ E]
    [IsScalarTower K F F₁] [IsScalarTower K F F₂] [IsScalarTower K F E]
    [IsScalarTower K F₁ E] [IsScalarTower K F₂ E] [IsScalarTower F F₁ E] [IsScalarTower F F₂ E]
    [FiniteDimensional F F₁] [FiniteDimensional F F₂] [FiniteDimensional F E]
    [FiniteDimensional F₁ E] [FiniteDimensional F₂ E] [Algebra.IsSeparable F E]
    (hgen : Algebra.adjoin F (Set.range (algebraMap F₁ E) ∪ Set.range (algebraMap F₂ E)) = ⊤)
    (hLD : Module.finrank F E = Module.finrank F F₁ * Module.finrank F F₂)
    (v : Place K F) (w₁ : Place K F₁) (w₂ : Place K F₂)
    (hw₁ : w₁.restrict F = v) (hw₂ : w₂.restrict F = v)
    (T : Finset (Place K E)) (hT : ∀ W, W ∈ T ↔ W.restrict F₁ = w₁ ∧ W.restrict F₂ = w₂) :
    ∑ W ∈ T, W.ramificationIndex F * W.inertiaDeg F =
      (w₁.ramificationIndex F * w₁.inertiaDeg F) * (w₂.ramificationIndex F * w₂.inertiaDeg F)
theorem

sum_ramificationIndex_mul_inertiaDeg_exchange

L248 ↗
AlgebraicCurve.Place.sum_ramificationIndex_mul_inertiaDeg_exchange
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange
open _root_.AlgebraicCurve
open BifibreW2 in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.sum_ramificationIndex_mul_inertiaDeg_exchange
    {K F F₁ F₂ E : Type*} [Field K] [Field F] [Field F₁] [Field F₂] [Field E]
    [Algebra K F] [Algebra K F₁] [Algebra K F₂] [Algebra K E]
    [Algebra F F₁] [Algebra F F₂] [Algebra F E] [Algebra F₁ E] [Algebra F₂ E]
    [IsScalarTower K F F₁] [IsScalarTower K F F₂] [IsScalarTower K F E]
    [IsScalarTower K F₁ E] [IsScalarTower K F₂ E] [IsScalarTower F F₁ E] [IsScalarTower F F₂ E]
    [FiniteDimensional F F₁] [FiniteDimensional F F₂] [FiniteDimensional F E]
    [FiniteDimensional F₁ E] [FiniteDimensional F₂ E] [Algebra.IsSeparable F E]
    (hgen : Algebra.adjoin F (Set.range (algebraMap F₁ E) ∪ Set.range (algebraMap F₂ E)) = ⊤)
    (hLD : Module.finrank F E = Module.finrank F F₁ * Module.finrank F F₂)
    (v : Place K F) (w₁ : Place K F₁) (w₂ : Place K F₂)
    (hw₁ : w₁.restrict F = v) (hw₂ : w₂.restrict F = v)
    (T : Finset (Place K E)) (hT : ∀ W, W ∈ T ↔ W.restrict F₁ = w₁ ∧ W.restrict F₂ = w₂) :
    ∑ W ∈ T, W.ramificationIndex F₁ * W.inertiaDeg F₂ =
      w₁.inertiaDeg 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.