internlm/Lean-Github huggingface dataset:
Theorem: FltRegular.caseII
Proof state before:
case intro.intro.inr
K : Type u_1
p✝ : ℕ+
hpri✝ : Fact p✝.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p✝} ℚ K
hp : p✝ ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg✝ : (↑p✝).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
hgcd : {a, b, c}.gcd id = 1
caseII : ↑p ∣ a * b * c
e : a ^ p + b ^ p = c ^ p
c0 : ¬c = 0
a0 : ¬a = 0
b0 : ¬b = 0
hodd' : Odd p
hc : ↑p ∣ c
⊢ False
Tactic:
exact not_exists_Int_solution' hreg hodd ⟨a, b, c, hgcd, hc, c0, e⟩
Proof state after:
no goals
Theorem: comap_span_galRestrict_eq_of_cyclic
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
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✝ : IsIntegralClosure B A L
β : B
η : Bˣ
hβ : ↑η * ((galRestrict A K L B) σ) β = β
σ' : L ≃ₐ[K] L
⊢ Ideal.comap ((galRestrict A K L B) σ') (Ideal.span {β}) = Ideal.span {β}
Tactic:
suffices : (Ideal.span {β}).map
    (galRestrict A K L B σ'⁻¹).toRingEquiv.toRingHom = Ideal.span {β}
Proof state after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
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✝ : IsIntegralClosure B A L
β : B
η : Bˣ
hβ : ↑η * ((galRestrict A K L B) σ) β = β
σ' : L ≃ₐ[K] L
this : Ideal.map ((galRestrict A K L B) σ'⁻¹).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.comap ((galRestrict A K L B) σ') (Ideal.span {β}) = Ideal.span {β}

case this
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
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✝ : IsIntegralClosure B A L
β : B
η : Bˣ
hβ : ↑η * ((galRestrict A K L B) σ) β = β
σ' : L ≃ₐ[K] L
⊢ Ideal.map ((galRestrict A K L B) σ'⁻¹).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
Theorem: comap_span_galRestrict_eq_of_cyclic
Proof state before:
case this
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
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✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.span {↑η * ((galRestrict A K L B) σ) β} = Ideal.span {β}
⊢ Ideal.map ((galRestrict A K L B) σ'⁻¹).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
Tactic:
rw [← Ideal.span_singleton_mul_span_singleton, Ideal.span_singleton_eq_top.mpr η.isUnit,
  ← Ideal.one_eq_top, one_mul, ← Set.image_singleton, ← Ideal.map_span] at hβ
Proof state after:
case this
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
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✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map ((galRestrict A K L B) σ) (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map ((galRestrict A K L B) σ'⁻¹).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
Theorem: comap_span_galRestrict_eq_of_cyclic
Proof state before:
case this
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
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✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map ((galRestrict A K L B) σ) (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map ((galRestrict A K L B) σ'⁻¹).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
Tactic:
change Ideal.map (galRestrict A K L B σ : B →+* B) _ = _ at hβ
Proof state after:
case this
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
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✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map ((galRestrict A K L B) σ'⁻¹).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
Theorem: comap_span_galRestrict_eq_of_cyclic
Proof state before:
case this
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
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✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map ((galRestrict A K L B) σ'⁻¹).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
Tactic:
generalize σ'⁻¹ = σ'
Proof state after:
case this
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
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✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ'✝ : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
σ' : L ≃ₐ[K] L
⊢ Ideal.map ((galRestrict A K L B) σ').toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
Theorem: comap_span_galRestrict_eq_of_cyclic
Proof state before:
case this
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
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✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ'✝ : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
σ' : L ≃ₐ[K] L
⊢ Ideal.map ((galRestrict A K L B) σ').toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
Tactic:
obtain ⟨n, rfl : σ ^ n = σ'⟩ := mem_powers_iff_mem_zpowers.mpr (hσ σ')
Proof state after:
case this.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
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✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
n : ℕ
⊢ Ideal.map ((galRestrict A K L B) (σ ^ n)).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
Theorem: comap_span_galRestrict_eq_of_cyclic
Proof state before:
case this.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
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✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
n : ℕ
⊢ Ideal.map ((galRestrict A K L B) (σ ^ n)).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
Tactic:
rw [map_pow]
Proof state after:
case this.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
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✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
n : ℕ
⊢ Ideal.map ((galRestrict A K L B) σ ^ n).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
Theorem: comap_span_galRestrict_eq_of_cyclic
Proof state before:
case this.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
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✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
n : ℕ
⊢ Ideal.map ((galRestrict A K L B) σ ^ n).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
Tactic:
induction n with
| zero =>
  simp only [Nat.zero_eq, pow_zero, AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toRingHom_eq_coe]
  exact Ideal.map_id _
| succ n IH =>
  simp only [AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toRingHom_eq_coe, pow_succ] at IH ⊢
  conv_lhs at IH => rw [← hβ, Ideal.map_map]
  exact IH
Proof state after:
no goals
Theorem: comap_span_galRestrict_eq_of_cyclic
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
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✝ : IsIntegralClosure B A L
β : B
η : Bˣ
hβ : ↑η * ((galRestrict A K L B) σ) β = β
σ' : L ≃ₐ[K] L
this : Ideal.map ((galRestrict A K L B) σ'⁻¹).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.comap ((galRestrict A K L B) σ') (Ideal.span {β}) = Ideal.span {β}
Tactic:
rwa [RingEquiv.toRingHom_eq_coe, Ideal.map_comap_of_equiv, map_inv] at this
Proof state after:
no goals
Theorem: comap_span_galRestrict_eq_of_cyclic
Proof state before:
case this.intro.zero
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
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✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map ((galRestrict A K L B) σ ^ 0).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
Tactic:
simp only [Nat.zero_eq, pow_zero, AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toRingHom_eq_coe]
Proof state after:
case this.intro.zero
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
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✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map (↑↑1) (Ideal.span {β}) = Ideal.span {β}
Theorem: comap_span_galRestrict_eq_of_cyclic
Proof state before:
case this.intro.zero
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
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✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map (↑↑1) (Ideal.span {β}) = Ideal.span {β}
Tactic:
exact Ideal.map_id _
Proof state after:
no goals
Theorem: comap_span_galRestrict_eq_of_cyclic
Proof state before:
case this.intro.succ
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
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✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
n : ℕ
IH : Ideal.map ((galRestrict A K L B) σ ^ n).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map ((galRestrict A K L B) σ ^ (n + 1)).toRingEquiv.toRingHom (Ideal.span {β}) = Ideal.span {β}
Tactic:
simp only [AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toRingHom_eq_coe, pow_succ] at IH ⊢
Proof state after:
case this.intro.succ
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
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✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
n : ℕ
IH : Ideal.map (↑↑((galRestrict A K L B) σ ^ n)) (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map (↑↑((galRestrict A K L B) σ ^ n * (galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
Theorem: comap_span_galRestrict_eq_of_cyclic
Proof state before:
case this.intro.succ
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
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✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
n : ℕ
IH : Ideal.map (↑↑((galRestrict A K L B) σ ^ n)) (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map (↑↑((galRestrict A K L B) σ ^ n * (galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
Tactic:
conv_lhs at IH => rw [← hβ, Ideal.map_map]
Proof state after:
case this.intro.succ
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
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✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
n : ℕ
IH : Ideal.map ((↑↑((galRestrict A K L B) σ ^ n)).comp ↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map (↑↑((galRestrict A K L B) σ ^ n * (galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
Theorem: comap_span_galRestrict_eq_of_cyclic
Proof state before:
case this.intro.succ
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹³ : Field L
inst✝¹² : Algebra K L
inst✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : FiniteDimensional.finrank K L = ↑p
A : Type u_3
B : Type u_2
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✝ : IsIntegralClosure B A L
β : B
η : Bˣ
σ' : L ≃ₐ[K] L
hβ : Ideal.map (↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
n : ℕ
IH : Ideal.map ((↑↑((galRestrict A K L B) σ ^ n)).comp ↑((galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
⊢ Ideal.map (↑↑((galRestrict A K L B) σ ^ n * (galRestrict A K L B) σ)) (Ideal.span {β}) = Ideal.span {β}
Tactic:
exact IH
Proof state after:
no goals
Theorem: exists_not_isPrincipal_and_isPrincipal_map_aux
Proof state before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁸ : Field K
inst✝¹⁷ : NumberField K
inst✝¹⁶ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : finrank K L = ↑p
A : Type u_2
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✝² : IsIntegralClosure B A L
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
⊢ ∃ I, ¬Submodule.IsPrincipal I ∧ Submodule.IsPrincipal (Ideal.map (algebraMap A B) I)
Tactic:
obtain ⟨β, hβ_zero, hβ⟩ := Hilbert90_integral (A := A) (B := B) σ hσ η hη
Proof state after:
case intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁸ : Field K
inst✝¹⁷ : NumberField K
inst✝¹⁶ : Fintype (ClassGroup (𝓞 K))
L : Type u_4
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
hKL : finrank K L = ↑p
A : Type u_2
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✝² : IsIntegralClosure B A L
inst✝¹ : IsDedekindDomain A
inst✝ : IsUnramified A B
η : Bˣ
hη : (Algebra.norm K) ((algebraMap B L) ↑η) = 1
hη' : ¬∃ α, (algebraMap B L) ↑η = (algebraMap B L) ↑α / σ ((algebraMap B L) ↑α)
β : B
hβ_zero : β ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) β = β
⊢ ∃ I, ¬Submodule.IsPrincipal I ∧ Submodule.IsPrincipal (Ideal.map (algebraMap A B) I)