theorem
L17 ↗additiveH2_finite
GaloisCohomology.additiveH2_finite
A trace-one element gives a primitive for every additive two-cocycle.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace GaloisCohomology
universe u v
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
[IsGalois K Ω] [FiniteDimensional K Ω]Lean source · statement
theorem additiveH2_finite
(z : Gal(Ω/K) → Gal(Ω/K) → Ω)
(hz : ∀ σ τ υ : Gal(Ω/K),
z σ (τ * υ) + σ (z τ υ) = z (σ * τ) υ + z σ τ) :
∃ b : Gal(Ω/K) → Ω, ∀ σ τ : Gal(Ω/K),
σ (b τ) - b (σ * τ) + b σ = z σ τ