internlm/Lean-Github huggingface dataset:
Theorem: Hilbert90_integral
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
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) σ) ε = ε
Tactic:
obtain ⟨x, y, rfl⟩ := IsLocalization.mk'_surjective (Algebra.algebraMapSubmonoid B A⁰) ε
Proof state after:
case intro.intro.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
x : B
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
hε : (algebraMap B L) η = IsLocalization.mk' L x y / σ (IsLocalization.mk' L x y)
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε
Theorem: Hilbert90_integral
Proof state before:
case intro.intro.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
x : B
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
hε : (algebraMap B L) η = IsLocalization.mk' L x y / σ (IsLocalization.mk' L x y)
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε
Tactic:
obtain ⟨t, ht, ht'⟩ := y.prop
Proof state after:
case intro.intro.intro.intro.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
x : B
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
hε : (algebraMap B L) η = IsLocalization.mk' L x y / σ (IsLocalization.mk' L x y)
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε
Theorem: Hilbert90_integral
Proof state before:
case intro.intro.intro.intro.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
x : B
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
hε : (algebraMap B L) η = IsLocalization.mk' L x y / σ (IsLocalization.mk' L x y)
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε
Tactic:
have : t • IsLocalization.mk' L x y = algebraMap _ _ x := by
  rw [Algebra.smul_def, IsScalarTower.algebraMap_apply A B L, ht', IsLocalization.mk'_spec']
Proof state after:
case intro.intro.intro.intro.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
x : B
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
hε : (algebraMap B L) η = IsLocalization.mk' L x y / σ (IsLocalization.mk' L x y)
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
this : t • IsLocalization.mk' L x y = (algebraMap B L) x
⊢ ∃ ε, ε ≠ 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
⊢ NoZeroSMulDivisors A L
Tactic:
rw [NoZeroSMulDivisors.iff_algebraMap_injective, IsScalarTower.algebraMap_eq A K L]
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
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap A K))
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
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap A K))
Tactic:
exact (algebraMap K L).injective.comp (IsFractionRing.injective A K)
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
this✝¹ : NoZeroSMulDivisors A L
this✝ : IsFractionRing B L
this : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
x : B
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
hε : (algebraMap B L) η = IsLocalization.mk' L x y / σ (IsLocalization.mk' L x y)
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
⊢ t • IsLocalization.mk' L x y = (algebraMap B L) x
Tactic:
rw [Algebra.smul_def, IsScalarTower.algebraMap_apply A B L, ht', IsLocalization.mk'_spec']
Proof state after:
no goals
Theorem: Hilbert90_integral
Proof state before:
case intro.intro.intro.intro.intro.refine_1
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
x : B
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
hε : (algebraMap B L) η = IsLocalization.mk' L x y / σ (IsLocalization.mk' L x y)
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
this : t • IsLocalization.mk' L x y = (algebraMap B L) x
⊢ x ≠ 0
Tactic:
rintro rfl
Proof state after:
case intro.intro.intro.intro.intro.refine_1
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
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
hε : (algebraMap B L) η = IsLocalization.mk' L 0 y / σ (IsLocalization.mk' L 0 y)
this : t • IsLocalization.mk' L 0 y = (algebraMap B L) 0
⊢ False
Theorem: Hilbert90_integral
Proof state before:
case intro.intro.intro.intro.intro.refine_1
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
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
hε : (algebraMap B L) η = IsLocalization.mk' L 0 y / σ (IsLocalization.mk' L 0 y)
this : t • IsLocalization.mk' L 0 y = (algebraMap B L) 0
⊢ False
Tactic:
simp only [IsLocalization.mk'_zero, _root_.map_zero, ne_eq, not_true, div_zero] at hε
Proof state after:
case intro.intro.intro.intro.intro.refine_1
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
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
this : t • IsLocalization.mk' L 0 y = (algebraMap B L) 0
hε : (algebraMap B L) η = 0
⊢ False
Theorem: Hilbert90_integral
Proof state before:
case intro.intro.intro.intro.intro.refine_1
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
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
this : t • IsLocalization.mk' L 0 y = (algebraMap B L) 0
hε : (algebraMap B L) η = 0
⊢ False
Tactic:
rw [hε, Algebra.norm_zero] at hη
Proof state after:
case intro.intro.intro.intro.intro.refine_1
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η : 0 = 1
this✝² : NoZeroSMulDivisors A L
this✝¹ : IsFractionRing B L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
this : t • IsLocalization.mk' L 0 y = (algebraMap B L) 0
hε : (algebraMap B L) η = 0
⊢ False
Theorem: Hilbert90_integral
Proof state before:
case intro.intro.intro.intro.intro.refine_1
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η : 0 = 1
this✝² : NoZeroSMulDivisors A L
this✝¹ : IsFractionRing B L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
this : t • IsLocalization.mk' L 0 y = (algebraMap B L) 0
hε : (algebraMap B L) η = 0
⊢ False
Tactic:
exact zero_ne_one hη
Proof state after:
no goals
Theorem: Hilbert90_integral
Proof state before:
case intro.intro.intro.intro.intro.refine_2
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
x : B
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
hε : (algebraMap B L) η = IsLocalization.mk' L x y / σ (IsLocalization.mk' L x y)
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
this : t • IsLocalization.mk' L x y = (algebraMap B L) x
⊢ σ (IsLocalization.mk' L x y) ≠ 0
Tactic:
intro e
Proof state after:
case intro.intro.intro.intro.intro.refine_2
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
x : B
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
hε : (algebraMap B L) η = IsLocalization.mk' L x y / σ (IsLocalization.mk' L x y)
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
this : t • IsLocalization.mk' L x y = (algebraMap B L) x
e : σ (IsLocalization.mk' L x y) = 0
⊢ False
Theorem: Hilbert90_integral
Proof state before:
case intro.intro.intro.intro.intro.refine_2
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
x : B
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
hε : (algebraMap B L) η = IsLocalization.mk' L x y / σ (IsLocalization.mk' L x y)
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
this : t • IsLocalization.mk' L x y = (algebraMap B L) x
e : σ (IsLocalization.mk' L x y) = 0
⊢ False
Tactic:
rw [(map_eq_zero _).mp e, zero_div] at hε
Proof state after:
case intro.intro.intro.intro.intro.refine_2
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
x : B
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
hε : (algebraMap B L) η = 0
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
this : t • IsLocalization.mk' L x y = (algebraMap B L) x
e : σ (IsLocalization.mk' L x y) = 0
⊢ False