Additive Hilbert's theorem 90

TheoremAdditive Hilbert 90 for cyclic extensions#✓fully proved

Let \(L/K\) be a finite-dimensional Galois extension and let \(\sigma\) be a \(K\)-algebra automorphism of \(L\) that generates its Galois group, that is, every \(K\)-algebra automorphism of \(L\) is an integer power of \(\sigma\). Then the kernel of the trace \(\operatorname{Tr}_{L/K} \colon L \to K\) equals the image of the \(K\)-linear map \(\sigma - 1 \colon L \to L\), \(y \mapsto \sigma(y) - y\).

theorem ker_trace_eq_range_algEquiv_sub_id (σ : L ≃ₐ[K] L)
    (hσ : ∀ τ : L ≃ₐ[K] L, τ ∈ Subgroup.zpowers σ) :
    LinearMap.ker (Algebra.trace K L) =
      LinearMap.range (σ.toLinearMap - LinearMap.id)

Used by 1

Used byAdditive Hilbert 90, pointwise form

TheoremAdditive Hilbert 90, pointwise form#✓fully proved

Let \(L/K\) be a finite-dimensional Galois extension and let \(\sigma\) be a \(K\)-algebra automorphism of \(L\) that generates its Galois group, that is, every \(K\)-algebra automorphism of \(L\) is an integer power of \(\sigma\). If \(x \in L\) satisfies \(\operatorname{Tr}_{L/K}(x) = 0\), then there is \(y \in L\) with \(\sigma(y) - y = x\).

theorem exists_algEquiv_sub_eq_of_trace_eq_zero (σ : L ≃ₐ[K] L)
    (hσ : ∀ τ : L ≃ₐ[K] L, τ ∈ Subgroup.zpowers σ) {x : L}
    (hx : Algebra.trace K L x = 0) :
    ∃ y : L, σ y - y = x

Uses 1

Proof usesAdditive Hilbert 90 for cyclic extensions

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.