English
For a tower of algebras with maximal p and P lying over p and I lying over P, the inertia degrees satisfy inertiaDeg p I = inertiaDeg p P · inertiaDeg P I.
Русский
Для башни алгебр с p надp и P над p, I над P: inertiaDeg p I = inertiaDeg p P · inertiaDeg P I.
LaTeX
$$$\\\\operatorname{inertiaDeg} p I = \\\\operatorname{inertiaDeg} p P \\\\cdot \\\\operatorname{inertiaDeg} P I$$$
Lean4
/-- Let `T / S / R` be a tower of algebras, `p, P, I` be ideals in `R, S, T`, respectively,
and `p` and `P` are maximal. If `p = P ∩ S` and `P = I ∩ S`,
then `f (I | p) = f (P | p) * f (I | P)`. -/
theorem inertiaDeg_algebra_tower (p : Ideal R) (P : Ideal S) (I : Ideal T) [p.IsMaximal] [P.IsMaximal] [P.LiesOver p]
[I.LiesOver P] : inertiaDeg p I = inertiaDeg p P * inertiaDeg P I :=
by
have h₁ := P.over_def p
have h₂ := I.over_def P
have h₃ := (LiesOver.trans I P p).over
simp only [inertiaDeg, dif_pos h₁.symm, dif_pos h₂.symm, dif_pos h₃.symm]
letI : Algebra (R ⧸ p) (S ⧸ P) := Ideal.Quotient.algebraQuotientOfLEComap h₁.le
letI : Algebra (S ⧸ P) (T ⧸ I) := Ideal.Quotient.algebraQuotientOfLEComap h₂.le
letI : Algebra (R ⧸ p) (T ⧸ I) := Ideal.Quotient.algebraQuotientOfLEComap h₃.le
letI : IsScalarTower (R ⧸ p) (S ⧸ P) (T ⧸ I) :=
IsScalarTower.of_algebraMap_eq <| by rintro ⟨x⟩; exact congr_arg _ (IsScalarTower.algebraMap_apply R S T x)
exact (finrank_mul_finrank (R ⧸ p) (S ⧸ P) (T ⧸ I)).symm
