Yamaguchi26AbfaithfulGalois.h1_reduction_surjective_of_finiteCocycle_lifting
Lifting finite cocycles proves surjectivity of the actual H¹ reduction.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Yamaguchi26AbfaithfulGalois
universe uLean source · statement
theorem h1_reduction_surjective_of_finiteCocycle_lifting
{ℓ : ℕ} [Fact ℓ.Prime]
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(θ : Orientation ℓ G) (H : Subgroup G) (n : ℕ) (hn : 1 ≤ n)
(hlift : ∀ c : FiniteCocycle θ H 1, ∃ d : FiniteCocycle θ H n,
∀ g : H, ZMod.castHom (pow_dvd_pow ℓ hn) (ZMod (ℓ ^ 1)) (d.toFun g) = c.toFun g) :
HasH1ReductionSurjective θ H n hn