Commit 2022-08-04 14:20 4d59d4af

feat(number_theory): [S/P^e : R/p] = e * [S/P : R/p], where e is ramification index (#15316) Let S be a Dedekind domain extending the commutative ring R, p a maximal ideal of R, P a prime ideal of S, and e the (nonzero) ramification index of P over p. Because the ramification index is nonzero, we get an inclusion R/p → S/P and we can compute that the degree of the field extension [S/(P^e) : R/p] is exactly e times [S/P : R/p]. This is the next step in showing the fundamental identity of inertia degree and ramification index (#12287). Setting up the ingredients for the proof is quite complicated because it involves taking (P^(i+1) / P^e) as a R/p-subspace of P^i / P^e and basically each part of this structure would produce free metavariables if we naïvely assigned it an instance. In the end, the important parts are an instance for S/(P^e) as R/p-algebra and replacing subspaces with the image of inclusion maps.