Mod-3 hardly ramified representations

A mod-3 hardly ramified representation is shown to be an extension of the trivial character by the mod-3 cyclotomic character.

theorem GaloisRepresentation.IsHardlyRamified.mod_three {k : Type u} [Finite k] [Field k] [Algebra ℤ_[3] k] [TopologicalSpace k] [DiscreteTopology k] (V : Type u_1) [AddCommGroup V] [Module k V] [Module.Finite k V] [Module.Free k V] (hV : Module.rank k V = 2) {ρ : GaloisRep ℚ k V} (hρ : IsHardlyRamified ⋯ hV ρ) : ∃ (π : V →ₗ[k] k) (_ : Function.Surjective ⇑π), ∀ (g : Field.absoluteGaloisGroup ℚ) (v : V), π ((ρ g) v) = π v

A mod 3 hardly ramified representation is an extension of trivial by cyclo