ModuleInertiaCardinality.lean
Nyll.ValuedFieldTheory.Ramification.InertiaCardinality
2 declarations indexed from sourceView source ↗ Module documentation
The finite-group count in the global cyclotomic inertia argument
The global Kronecker--Weber proof generates the full Galois group by the inertia groups at the finitely many ramified primes. Since the group is abelian, the cardinality of the subgroup that they generate is at most the product of their cardinalities. This file isolates that elementary count from the arithmetic part of the proof.
Imports3
- Mathlib.Algebra.Group.Subgroup.Finite
- Mathlib.Algebra.Group.Subgroup.Lattice
- Mathlib.SetTheory.Cardinal.NatCard
Imported by2
Declarations
RamificationTheory.natCard_sup_le_mul_natCard
DocumentationIn a finite abelian group, the supremum of two subgroups has cardinality at most the product of their cardinalities.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace RamificationTheory
open scoped BigOperators
variable {G ι : Type*} [CommGroup G] [Finite G]
RamificationTheory.natCard_finsetSup_le_prod_natCard
DocumentationFinite-family form of the inertia-group cardinality bound used in the proof of the global cyclotomic inertia argument.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace RamificationTheory
open scoped BigOperators
variable {G ι : Type*} [CommGroup G] [Finite G]