ModuleLocalTameRootsPowerMap.lean
Nyll.ValuedFieldTheory.Ramification.HilbertRamification.LocalTameRootsPowerMap
3 declarations indexed from sourceView source ↗ Module documentation
Power maps on local tame root groups
Defines power homomorphisms on the local tame root group and proves injectivity for exponential- characteristic powers. These maps are surjective when the acting group is finite.
Declarations
RamificationTheory.HilbertRamification.DiscreteValuationRing.localTameRootsPowerGroupMap
DocumentationThe canonical power map on the actual finite root group.
Source context 5 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]
(G : Type v) [Group G] [MulSemiringAction G R]
RamificationTheory.HilbertRamification.DiscreteValuationRing.localTameRootsPowerGroupMap_injective
DocumentationExponential-characteristic powers are injective on the actual roots, by the native residue-field Frobenius argument.
Source context 5 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]
(G : Type v) [Group G] [MulSemiringAction G R]
RamificationTheory.HilbertRamification.DiscreteValuationRing.localTameRootsPowerGroupMap_surjective
DocumentationExponential-characteristic power maps are bijective on these actual finite root groups, with no perfectness premise.
Source context 5 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]
(G : Type v) [Group G] [MulSemiringAction G R]