ModuleLocalTameCharacterGroupMap.lean
Nyll.ValuedFieldTheory.Ramification.HilbertRamification.LocalTameCharacterGroupMap
3 declarations indexed from sourceView source ↗ Module documentation
Group objects for the local tame character
Defines group objects for local inertia and the roots of unity of the tame order. It presents the finite local tame character as a homomorphism between them.
Declarations
RamificationTheory.HilbertRamification.DiscreteValuationRing.localInertiaGroupObject
DocumentationThe native group of actual local inertia.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
universe u v
RamificationTheory.HilbertRamification.DiscreteValuationRing.localTameRootsGroupObject
DocumentationThe actual full root group of the computed finite tame order.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
universe u v
RamificationTheory.HilbertRamification.DiscreteValuationRing.localTameCharacterGroupMap
DocumentationThe actual finite local character, retained as its ordinary monoid homomorphism.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
universe u v