ModuleFiniteSubgroupRootsOfUnity.lean
Nyll.ValuedFieldTheory.Ramification.HilbertRamification.FiniteSubgroupRootsOfUnity
7 declarations indexed from sourceView source ↗ Module documentation
Finite multiplicative subgroups and roots of unity
Identifies a finite subgroup of field units with all roots of unity of its order and produces a primitive root. Finite characters are then expressed as surjections onto these root groups with the corresponding kernel quotient.
Imports3
- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
- Mathlib.GroupTheory.QuotientGroup.Basic
- Mathlib.Algebra.Group.Subgroup.Finite
Imported by2
Declarations
RamificationTheory.HilbertRamification.finiteSubgroup_eq_rootsOfUnity
DocumentationA finite subgroup of field units is the full root group of its order.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace RamificationTheory.HilbertRamification
universe u v
variable {k : Type u} [Field k]
RamificationTheory.HilbertRamification.exists_primitiveRoot_card_finiteSubgroup
DocumentationA finite multiplicative subgroup yields an actual primitive root in the field.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace RamificationTheory.HilbertRamification
universe u v
variable {k : Type u} [Field k]
RamificationTheory.HilbertRamification.finiteImageRootsCharacter
DocumentationAny actual finite residue-unit homomorphism lands onto all roots of its image order.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace RamificationTheory.HilbertRamification
universe u v
variable {k : Type u} [Field k]
variable {G : Type v} [Group G] [Finite G]
RamificationTheory.HilbertRamification.finiteImageRootsCharacter_surjective
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace RamificationTheory.HilbertRamification
universe u v
variable {k : Type u} [Field k]
variable {G : Type v} [Group G] [Finite G]
RamificationTheory.HilbertRamification.finiteImageRootsCharacter_ker
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace RamificationTheory.HilbertRamification
universe u v
variable {k : Type u} [Field k]
variable {G : Type v} [Group G] [Finite G]
RamificationTheory.HilbertRamification.finiteImageRootsCharacter_degree
DocumentationThe actual image order is the order of the actual kernel quotient.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace RamificationTheory.HilbertRamification
universe u v
variable {k : Type u} [Field k]
variable {G : Type v} [Group G] [Finite G]
omit [Finite G] in
RamificationTheory.HilbertRamification.finiteImageQuotientEquivRootsOfUnity
DocumentationA finite image in the units of a field identifies the kernel quotient with the full roots-of-unity group of the image order.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace RamificationTheory.HilbertRamification
universe u v
variable {k : Type u} [Field k]
variable {G : Type v} [Group G] [Finite G]