AlgebraicCurve.Place.sum_ramificationIndex_mul_inertiaDeg_exchange_add
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_ramificationIndex_mul_inertiaDeg_exchange_add
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Place.sum_ramificationIndex_mul_inertiaDeg_exchange_add
{K F F₁ F₂ Z Z' : Type*} [Field K] [Field F] [Field F₁] [Field F₂] [Field Z] [Field Z']
[Algebra K F] [Algebra K F₁] [Algebra K F₂] [Algebra K Z] [Algebra K Z']
[Algebra F F₁] [Algebra F F₂] [Algebra F Z] [Algebra F₁ Z] [Algebra F₂ Z]
[Algebra F Z'] [Algebra F₁ Z'] [Algebra F₂ Z']
[IsScalarTower K F F₁] [IsScalarTower K F F₂] [IsScalarTower K F Z] [IsScalarTower K F Z']
[IsScalarTower K F₁ Z] [IsScalarTower K F₂ Z] [IsScalarTower K F₁ Z'] [IsScalarTower K F₂ Z']
[IsScalarTower F F₁ Z] [IsScalarTower F F₂ Z] [IsScalarTower F F₁ Z'] [IsScalarTower F F₂ Z']
[FiniteDimensional F F₁] [FiniteDimensional F F₂]
[FiniteDimensional F₁ Z] [FiniteDimensional F₂ Z] [FiniteDimensional F₁ Z'] [FiniteDimensional
F₂ Z']
[CharZero F]
(hgen : Algebra.adjoin F (Set.range (algebraMap F₁ Z) ∪ Set.range (algebraMap F₂ Z)) = ⊤)
(hgen' : Algebra.adjoin F (Set.range (algebraMap F₁ Z') ∪ Set.range (algebraMap F₂ Z')) = ⊤)
(hdeg : Module.finrank F₁ Z + Module.finrank F₁ Z' = Module.finrank F F₂)
(hne : ∃ (a : F₂) (b : F₁), algebraMap F₂ Z' a = algebraMap F₁ Z' b ∧
algebraMap F₂ Z a ≠ algebraMap F₁ Z b)
(w₁ : Place K F₁) (w₂ : Place K F₂) (hw : w₁.restrict F = w₂.restrict F)
(T : Finset (Place K Z)) (hT : ∀ W, W ∈ T ↔ W.restrict F₁ = w₁ ∧ W.restrict F₂ = w₂)
(T' : Finset (Place K Z')) (hT' : ∀ W, W ∈ T' ↔ W.restrict F₁ = w₁ ∧ W.restrict F₂ = w₂) :
∑ W ∈ T, W.ramificationIndex F₁ * W.inertiaDeg F₂
+ ∑ W ∈ T', W.ramificationIndex F₁ * W.inertiaDeg F₂
= w₁.inertiaDeg F * w₂.ramificationIndex F