ModuleRingFiniteTameCharacter.lean
Nyll.ValuedFieldTheory.Ramification.HilbertRamification.RingFiniteTameCharacter
6 declarations indexed from sourceView source ↗ Module documentation
Finite tame characters of discrete valuation rings
Defines the tame order as the size of the inertia-character image and constructs a surjective character onto all roots of unity of that order. It identifies the principal-unit kernel and produces a primitive root in the residue field.
Declarations
RamificationTheory.HilbertRamification.DiscreteValuationRing.tameOrder
DocumentationThe order of the image of the actual, constructed DVR inertia character.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
universe u v
variable (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable (G : Type v) [Group G] [MulSemiringAction G R]
RamificationTheory.HilbertRamification.DiscreteValuationRing.tameOrder_pos
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
universe u v
variable (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable (G : Type v) [Group G] [MulSemiringAction G R]
variable [Finite G]
RamificationTheory.HilbertRamification.DiscreteValuationRing.tameCharacter
DocumentationThe actual finite DVR inertia character with its full root-group target.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
universe u v
variable (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable (G : Type v) [Group G] [MulSemiringAction G R]
variable [Finite G]
RamificationTheory.HilbertRamification.DiscreteValuationRing.tameCharacter_surjective
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
universe u v
variable (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable (G : Type v) [Group G] [MulSemiringAction G R]
variable [Finite G]
RamificationTheory.HilbertRamification.DiscreteValuationRing.tameCharacter_ker
DocumentationThe full root-codomain character has the actual principal-unit kernel.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
universe u v
variable (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable (G : Type v) [Group G] [MulSemiringAction G R]
variable [Finite G]
RamificationTheory.HilbertRamification.DiscreteValuationRing.exists_primitiveRoot_tameOrder
DocumentationAll finite tame orders occur as actual primitive roots in the residue field.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
universe u v
variable (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable (G : Type v) [Group G] [MulSemiringAction G R]
variable [Finite G]