LocalFieldTheory.DiscreteValuationField.averageMap_ker_divisible_of_action_sub_divisible
If the action is trivial modulo c, the kernel of its averaging projection is c-divisible. This is the actual augmentation submodule: averaging is a projection, so its kernel is the image of 1 - average.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory.DiscreteValuationField
open scoped BigOperators
variable {R Λ M : Type*} [CommRing R] [Group Λ] [Fintype Λ]
[AddCommGroup M] [Module R M] [Invertible (Fintype.card Λ : R)]Lean source · statement
theorem averageMap_ker_divisible_of_action_sub_divisible
(ρ : Representation R Λ M) (c : R)
(hdiv : ∀ (g : Λ) (x : M), ∃ y : M, ρ g x - x = c • y)
(x : M) (hx : ρ.averageMap x = 0) :
∃ y : M, ρ.averageMap y = 0 ∧ c • y = x