internlm/Lean-Github huggingface dataset:
Theorem: is_cocycle
Proof state before:
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
⊢ IsMulOneCocycle (cocycle hσ hη)
Tactic:
intro α β
Proof state after:
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
α β : L ≃ₐ[K] L
⊢ cocycle hσ hη (α * β) = α • cocycle hσ hη β * cocycle hσ hη α
Theorem: is_cocycle
Proof state before:
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
α β : L ≃ₐ[K] L
⊢ cocycle hσ hη (α * β) = α • cocycle hσ hη β * cocycle hσ hη α
Tactic:
simp [← Units.eq_iff, is_cocycle_aux hσ hη α β]
Proof state after:
no goals
Theorem: Hilbert90
Proof state before:
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
⊢ ∃ ε, η = ε / σ ε
Tactic:
by_cases hone : orderOf σ = 1
Proof state after:
case pos
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : orderOf σ = 1
⊢ ∃ ε, η = ε / σ ε

case neg
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : ¬orderOf σ = 1
⊢ ∃ ε, η = ε / σ ε
Theorem: Hilbert90
Proof state before:
case neg
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : ¬orderOf σ = 1
⊢ ∃ ε, η = ε / σ ε
Tactic:
obtain ⟨ε, hε⟩ := isMulOneCoboundary_of_isMulOneCocycle_of_aut_to_units _ (is_cocycle hσ hη)
Proof state after:
case neg.intro
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : ¬orderOf σ = 1
ε : Lˣ
hε : ∀ (g : L ≃ₐ[K] L), g • ε / ε = cocycle hσ hη g
⊢ ∃ ε, η = ε / σ ε
Theorem: Hilbert90
Proof state before:
case neg.intro
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : ¬orderOf σ = 1
ε : Lˣ
hε : ∀ (g : L ≃ₐ[K] L), g • ε / ε = cocycle hσ hη g
⊢ ∃ ε, η = ε / σ ε
Tactic:
use ε⁻¹
Proof state after:
case h
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : ¬orderOf σ = 1
ε : Lˣ
hε : ∀ (g : L ≃ₐ[K] L), g • ε / ε = cocycle hσ hη g
⊢ η = (↑ε)⁻¹ / σ (↑ε)⁻¹
Theorem: Hilbert90
Proof state before:
case h
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : ¬orderOf σ = 1
ε : Lˣ
hε : ∀ (g : L ≃ₐ[K] L), g • ε / ε = cocycle hσ hη g
⊢ η = (↑ε)⁻¹ / σ (↑ε)⁻¹
Tactic:
simp only [map_inv₀, div_inv_eq_mul]
Proof state after:
case h
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : ¬orderOf σ = 1
ε : Lˣ
hε : ∀ (g : L ≃ₐ[K] L), g • ε / ε = cocycle hσ hη g
⊢ η = (↑ε)⁻¹ * σ ↑ε
Theorem: Hilbert90
Proof state before:
case h
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : ¬orderOf σ = 1
ε : Lˣ
hε : ∀ (g : L ≃ₐ[K] L), g • ε / ε = cocycle hσ hη g
⊢ η = (↑ε)⁻¹ * σ ↑ε
Tactic:
specialize hε σ
Proof state after:
case h
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : ¬orderOf σ = 1
ε : Lˣ
hε : σ • ε / ε = cocycle hσ hη σ
⊢ η = (↑ε)⁻¹ * σ ↑ε
Theorem: Hilbert90
Proof state before:
case h
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : ¬orderOf σ = 1
ε : Lˣ
hε : σ • ε / ε = cocycle hσ hη σ
⊢ η = (↑ε)⁻¹ * σ ↑ε
Tactic:
nth_rewrite 2 [← inv_inv ε] at hε
Proof state after:
case h
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : ¬orderOf σ = 1
ε : Lˣ
hε : σ • ε / ε⁻¹⁻¹ = cocycle hσ hη σ
⊢ η = (↑ε)⁻¹ * σ ↑ε
Theorem: Hilbert90
Proof state before:
case h
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : ¬orderOf σ = 1
ε : Lˣ
hε : σ • ε / ε⁻¹⁻¹ = cocycle hσ hη σ
⊢ η = (↑ε)⁻¹ * σ ↑ε
Tactic:
rw [div_inv_eq_mul, cocycle_spec hσ hη hone, mul_inv_eq_iff_eq_mul, mul_comm, ← Units.eq_iff] at hε
Proof state after:
case h
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : ¬orderOf σ = 1
ε : Lˣ
hε : ↑(σ • ε) = ↑(ε * ηu hη)
⊢ η = (↑ε)⁻¹ * σ ↑ε
Theorem: Hilbert90
Proof state before:
case h
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : ¬orderOf σ = 1
ε : Lˣ
hε : ↑(σ • ε) = ↑(ε * ηu hη)
⊢ η = (↑ε)⁻¹ * σ ↑ε
Tactic:
simp only [AlgEquiv.smul_units_def, Units.coe_map, MonoidHom.coe_coe, Units.val_mul] at hε
Proof state after:
case h
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : ¬orderOf σ = 1
ε : Lˣ
hε : σ ↑ε = ↑ε * ↑(ηu hη)
⊢ η = (↑ε)⁻¹ * σ ↑ε
Theorem: Hilbert90
Proof state before:
case h
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : ¬orderOf σ = 1
ε : Lˣ
hε : σ ↑ε = ↑ε * ↑(ηu hη)
⊢ η = (↑ε)⁻¹ * σ ↑ε
Tactic:
symm
Proof state after:
case h
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : ¬orderOf σ = 1
ε : Lˣ
hε : σ ↑ε = ↑ε * ↑(ηu hη)
⊢ (↑ε)⁻¹ * σ ↑ε = η
Theorem: Hilbert90
Proof state before:
case h
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : ¬orderOf σ = 1
ε : Lˣ
hε : σ ↑ε = ↑ε * ↑(ηu hη)
⊢ (↑ε)⁻¹ * σ ↑ε = η
Tactic:
rw [inv_mul_eq_iff_eq_mul₀ ε.ne_zero, hε]
Proof state after:
case h
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : ¬orderOf σ = 1
ε : Lˣ
hε : σ ↑ε = ↑ε * ↑(ηu hη)
⊢ ↑ε * ↑(ηu hη) = ↑ε * η
Theorem: Hilbert90
Proof state before:
case h
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : ¬orderOf σ = 1
ε : Lˣ
hε : σ ↑ε = ↑ε * ↑(ηu hη)
⊢ ↑ε * ↑(ηu hη) = ↑ε * η
Tactic:
rfl
Proof state after:
no goals
Theorem: Hilbert90
Proof state before:
case pos
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : orderOf σ = 1
⊢ ∃ ε, η = ε / σ ε
Tactic:
suffices finrank K L = 1 by
  obtain ⟨a, ha⟩ := mem_span_singleton.1 <| (eq_top_iff'.1 <|
    (finrank_eq_one_iff_of_nonzero _ one_ne_zero).1 this) η
  rw [← Algebra.algebraMap_eq_smul_one] at ha
  rw [← ha, Algebra.norm_algebraMap, this, pow_one] at hη
  exact ⟨1, by simp [← ha, hη]⟩
Proof state after:
case pos
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : orderOf σ = 1
⊢ finrank K L = 1
Theorem: Hilbert90
Proof state before:
case pos
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : orderOf σ = 1
⊢ finrank K L = 1
Tactic:
rw [← IsGalois.card_aut_eq_finrank, Fintype.card_eq_one_iff]
Proof state after:
case pos
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : orderOf σ = 1
⊢ ∃ x, ∀ (y : L ≃ₐ[K] L), y = x
Theorem: Hilbert90
Proof state before:
case pos
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : orderOf σ = 1
⊢ ∃ x, ∀ (y : L ≃ₐ[K] L), y = x
Tactic:
refine ⟨σ, fun τ ↦ ?_⟩
Proof state after:
case pos
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : orderOf σ = 1
τ : L ≃ₐ[K] L
⊢ τ = σ
Theorem: Hilbert90
Proof state before:
case pos
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : orderOf σ = 1
τ : L ≃ₐ[K] L
⊢ τ = σ
Tactic:
simp only [orderOf_eq_one_iff.1 hone, Subgroup.zpowers_one_eq_bot, Subgroup.mem_bot] at hσ
Proof state after:
case pos
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
η : L
hη : (Algebra.norm K) η = 1
hone : orderOf σ = 1
τ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x = 1
⊢ τ = σ
Theorem: Hilbert90
Proof state before:
case pos
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
η : L
hη : (Algebra.norm K) η = 1
hone : orderOf σ = 1
τ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x = 1
⊢ τ = σ
Tactic:
rw [orderOf_eq_one_iff.1 hone, hσ τ]
Proof state after:
no goals
Theorem: Hilbert90
Proof state before:
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : orderOf σ = 1
this : finrank K L = 1
⊢ ∃ ε, η = ε / σ ε
Tactic:
obtain ⟨a, ha⟩ := mem_span_singleton.1 <| (eq_top_iff'.1 <|
  (finrank_eq_one_iff_of_nonzero _ one_ne_zero).1 this) η
Proof state after:
case intro
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : orderOf σ = 1
this : finrank K L = 1
a : K
ha : a • 1 = η
⊢ ∃ ε, η = ε / σ ε
Theorem: Hilbert90
Proof state before:
case intro
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : orderOf σ = 1
this : finrank K L = 1
a : K
ha : a • 1 = η
⊢ ∃ ε, η = ε / σ ε
Tactic:
rw [← Algebra.algebraMap_eq_smul_one] at ha
Proof state after:
case intro
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : orderOf σ = 1
this : finrank K L = 1
a : K
ha : (algebraMap K L) a = η
⊢ ∃ ε, η = ε / σ ε
Theorem: Hilbert90
Proof state before:
case intro
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : orderOf σ = 1
this : finrank K L = 1
a : K
ha : (algebraMap K L) a = η
⊢ ∃ ε, η = ε / σ ε
Tactic:
rw [← ha, Algebra.norm_algebraMap, this, pow_one] at hη
Proof state after:
case intro
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hone : orderOf σ = 1
this : finrank K L = 1
a : K
hη : a = 1
ha : (algebraMap K L) a = η
⊢ ∃ ε, η = ε / σ ε
Theorem: Hilbert90
Proof state before:
case intro
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hone : orderOf σ = 1
this : finrank K L = 1
a : K
hη : a = 1
ha : (algebraMap K L) a = η
⊢ ∃ ε, η = ε / σ ε
Tactic:
exact ⟨1, by simp [← ha, hη]⟩
Proof state after:
no goals
Theorem: Hilbert90
Proof state before:
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hone : orderOf σ = 1
this : finrank K L = 1
a : K
hη : a = 1
ha : (algebraMap K L) a = η
⊢ η = 1 / σ 1
Tactic:
simp [← ha, hη]
Proof state after:
no goals
Theorem: Hilbert90_integral
Proof state before:
K : Type u_1
L : Type u_2
inst✝¹⁷ : Field K
inst✝¹⁶ : Field L
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Algebra K L
inst✝¹³ : IsGalois K L
inst✝¹² : FiniteDimensional K L
σ✝ : L ≃ₐ[K] L
hσ✝ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ✝
η✝ : L
hη✝ : (Algebra.norm K) η✝ = 1
A : Type u_4
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra A L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsFractionRing A K
inst✝² : IsDomain A
inst✝¹ : IsIntegralClosure B A L
inst✝ : IsDomain B
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε
Tactic:
haveI : NoZeroSMulDivisors A L := by
  rw [NoZeroSMulDivisors.iff_algebraMap_injective, IsScalarTower.algebraMap_eq A K L]
  exact (algebraMap K L).injective.comp (IsFractionRing.injective A K)
Proof state after:
K : Type u_1
L : Type u_2
inst✝¹⁷ : Field K
inst✝¹⁶ : Field L
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Algebra K L
inst✝¹³ : IsGalois K L
inst✝¹² : FiniteDimensional K L
σ✝ : L ≃ₐ[K] L
hσ✝ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ✝
η✝ : L
hη✝ : (Algebra.norm K) η✝ = 1
A : Type u_4
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra A L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsFractionRing A K
inst✝² : IsDomain A
inst✝¹ : IsIntegralClosure B A L
inst✝ : IsDomain B
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this : NoZeroSMulDivisors A L
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε
Theorem: Hilbert90_integral
Proof state before:
K : Type u_1
L : Type u_2
inst✝¹⁷ : Field K
inst✝¹⁶ : Field L
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Algebra K L
inst✝¹³ : IsGalois K L
inst✝¹² : FiniteDimensional K L
σ✝ : L ≃ₐ[K] L
hσ✝ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ✝
η✝ : L
hη✝ : (Algebra.norm K) η✝ = 1
A : Type u_4
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra A L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsFractionRing A K
inst✝² : IsDomain A
inst✝¹ : IsIntegralClosure B A L
inst✝ : IsDomain B
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this : NoZeroSMulDivisors A L
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε
Tactic:
haveI := IsIntegralClosure.isFractionRing_of_finite_extension A K L B
Proof state after:
K : Type u_1
L : Type u_2
inst✝¹⁷ : Field K
inst✝¹⁶ : Field L
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Algebra K L
inst✝¹³ : IsGalois K L
inst✝¹² : FiniteDimensional K L
σ✝ : L ≃ₐ[K] L
hσ✝ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ✝
η✝ : L
hη✝ : (Algebra.norm K) η✝ = 1
A : Type u_4
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra A L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsFractionRing A K
inst✝² : IsDomain A
inst✝¹ : IsIntegralClosure B A L
inst✝ : IsDomain B
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝ : NoZeroSMulDivisors A L
this : IsFractionRing B L
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε
Theorem: Hilbert90_integral
Proof state before:
K : Type u_1
L : Type u_2
inst✝¹⁷ : Field K
inst✝¹⁶ : Field L
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Algebra K L
inst✝¹³ : IsGalois K L
inst✝¹² : FiniteDimensional K L
σ✝ : L ≃ₐ[K] L
hσ✝ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ✝
η✝ : L
hη✝ : (Algebra.norm K) η✝ = 1
A : Type u_4
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra A L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsFractionRing A K
inst✝² : IsDomain A
inst✝¹ : IsIntegralClosure B A L
inst✝ : IsDomain B
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝ : NoZeroSMulDivisors A L
this : IsFractionRing B L
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε
Tactic:
have : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L :=
  IsIntegralClosure.isLocalization A K L B
Proof state after:
K : Type u_1
L : Type u_2
inst✝¹⁷ : Field K
inst✝¹⁶ : Field L
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Algebra K L
inst✝¹³ : IsGalois K L
inst✝¹² : FiniteDimensional K L
σ✝ : L ≃ₐ[K] L
hσ✝ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ✝
η✝ : L
hη✝ : (Algebra.norm K) η✝ = 1
A : Type u_4
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra A L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsFractionRing A K
inst✝² : IsDomain A
inst✝¹ : IsIntegralClosure B A L
inst✝ : IsDomain B
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝¹ : NoZeroSMulDivisors A L
this✝ : IsFractionRing B L
this : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε
Theorem: Hilbert90_integral
Proof state before:
K : Type u_1
L : Type u_2
inst✝¹⁷ : Field K
inst✝¹⁶ : Field L
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Algebra K L
inst✝¹³ : IsGalois K L
inst✝¹² : FiniteDimensional K L
σ✝ : L ≃ₐ[K] L
hσ✝ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ✝
η✝ : L
hη✝ : (Algebra.norm K) η✝ = 1
A : Type u_4
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra A L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsFractionRing A K
inst✝² : IsDomain A
inst✝¹ : IsIntegralClosure B A L
inst✝ : IsDomain B
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝¹ : NoZeroSMulDivisors A L
this✝ : IsFractionRing B L
this : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε
Tactic:
obtain ⟨ε, hε⟩ := Hilbert90 hσ hη
Proof state after:
case intro
K : Type u_1
L : Type u_2
inst✝¹⁷ : Field K
inst✝¹⁶ : Field L
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Algebra K L
inst✝¹³ : IsGalois K L
inst✝¹² : FiniteDimensional K L
σ✝ : L ≃ₐ[K] L
hσ✝ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ✝
η✝ : L
hη✝ : (Algebra.norm K) η✝ = 1
A : Type u_4
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra A L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsFractionRing A K
inst✝² : IsDomain A
inst✝¹ : IsIntegralClosure B A L
inst✝ : IsDomain B
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝¹ : NoZeroSMulDivisors A L
this✝ : IsFractionRing B L
this : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
ε : L
hε : (algebraMap B L) η = ε / σ ε
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε