internlm/Lean-Github huggingface dataset:
Theorem: exists_not_isPrincipal_and_isPrincipal_map_aux
Proof state before:
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)
Tactic:
haveI : IsDomain B :=
  (IsIntegralClosure.equiv A B L (integralClosure A L)).toMulEquiv.isDomain (integralClosure A L)
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) σ) β = β
this : IsDomain B
⊢ ∃ I, ¬Submodule.IsPrincipal I ∧ Submodule.IsPrincipal (Ideal.map (algebraMap A B) I)
Theorem: exists_not_isPrincipal_and_isPrincipal_map_aux
Proof state before:
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) σ) β = β
this : IsDomain B
⊢ ∃ I, ¬Submodule.IsPrincipal I ∧ Submodule.IsPrincipal (Ideal.map (algebraMap A B) I)
Tactic:
have hβ' := comap_map_eq_of_isUnramified K L _
  (comap_span_galRestrict_eq_of_cyclic σ hσ (A := A) (B := B) β η 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) σ) β = β
this : IsDomain B
hβ' : Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) (Ideal.span {β})) = Ideal.span {β}
⊢ ∃ I, ¬Submodule.IsPrincipal I ∧ Submodule.IsPrincipal (Ideal.map (algebraMap A B) I)
Theorem: exists_not_isPrincipal_and_isPrincipal_map_aux
Proof state before:
case intro.intro.refine_1
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) σ) β = β
this : IsDomain B
hβ' : Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) (Ideal.span {β})) = Ideal.span {β}
⊢ ¬Submodule.IsPrincipal (Ideal.comap (algebraMap A B) (Ideal.span {β}))
Tactic:
rintro ⟨⟨γ, hγ : _ = Ideal.span _⟩⟩
Proof state after:
case intro.intro.refine_1.mk.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) σ) β = β
this : IsDomain B
hβ' : Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) (Ideal.span {β})) = Ideal.span {β}
γ : A
hγ : Ideal.comap (algebraMap A B) (Ideal.span {β}) = Ideal.span {γ}
⊢ False
Theorem: exists_not_isPrincipal_and_isPrincipal_map_aux
Proof state before:
case intro.intro.refine_1.mk.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) σ) β = β
this : IsDomain B
hβ' : Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) (Ideal.span {β})) = Ideal.span {β}
γ : A
hγ : Ideal.comap (algebraMap A B) (Ideal.span {β}) = Ideal.span {γ}
⊢ False
Tactic:
rw [hγ, Ideal.map_span, Set.image_singleton, Ideal.span_singleton_eq_span_singleton] at hβ'
Proof state after:
case intro.intro.refine_1.mk.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) σ) β = β
this : IsDomain B
γ : A
hβ' : Associated ((algebraMap A B) γ) β
hγ : Ideal.comap (algebraMap A B) (Ideal.span {β}) = Ideal.span {γ}
⊢ False
Theorem: exists_not_isPrincipal_and_isPrincipal_map_aux
Proof state before:
case intro.intro.refine_1.mk.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) σ) β = β
this : IsDomain B
γ : A
hβ' : Associated ((algebraMap A B) γ) β
hγ : Ideal.comap (algebraMap A B) (Ideal.span {β}) = Ideal.span {γ}
⊢ False
Tactic:
obtain ⟨a, rfl⟩ := hβ'
Proof state after:
case intro.intro.refine_1.mk.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) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) ((algebraMap A B) γ * ↑a) = (algebraMap A B) γ * ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ False
Theorem: exists_not_isPrincipal_and_isPrincipal_map_aux
Proof state before:
case h
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) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) ↑a = ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap B L) (((galRestrict A K L B) σ) ↑a) ≠ 0
Tactic:
rw [ne_eq, (injective_iff_map_eq_zero' _).mp (IsIntegralClosure.algebraMap_injective B A L),
  (injective_iff_map_eq_zero' _).mp (galRestrict A K L B σ).injective]
Proof state after:
case h
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) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) ↑a = ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ ¬↑a = 0
Theorem: exists_not_isPrincipal_and_isPrincipal_map_aux
Proof state before:
case h
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) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : ↑η * ((galRestrict A K L B) σ) ↑a = ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ ¬↑a = 0
Tactic:
exact a.isUnit.ne_zero
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) ↑α)
this : IsDomain B
γ : A
a : Bˣ
hβ_zero : (algebraMap A B) γ * ↑a ≠ 0
hβ : (algebraMap A B) γ * (↑η * ((galRestrict A K L B) σ) ↑a) = (algebraMap A B) γ * ↑a
hγ : Ideal.comap (algebraMap A B) (Ideal.span {(algebraMap A B) γ * ↑a}) = Ideal.span {γ}
⊢ (algebraMap A B) γ ≠ 0
Tactic:
exact (mul_ne_zero_iff.mp hβ_zero).1
Proof state after:
no goals
Theorem: exists_not_isPrincipal_and_isPrincipal_map_aux
Proof state before:
case intro.intro.refine_2
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) σ) β = β
this : IsDomain B
hβ' : Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) (Ideal.span {β})) = Ideal.span {β}
⊢ Submodule.IsPrincipal (Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) (Ideal.span {β})))
Tactic:
rw [hβ']
Proof state after:
case intro.intro.refine_2
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) σ) β = β
this : IsDomain B
hβ' : Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) (Ideal.span {β})) = Ideal.span {β}
⊢ Submodule.IsPrincipal (Ideal.span {β})
Theorem: exists_not_isPrincipal_and_isPrincipal_map_aux
Proof state before:
case intro.intro.refine_2
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) σ) β = β
this : IsDomain B
hβ' : Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) (Ideal.span {β})) = Ideal.span {β}
⊢ Submodule.IsPrincipal (Ideal.span {β})
Tactic:
exact ⟨⟨_, rfl⟩⟩
Proof state after:
no goals
Theorem: Ideal.isPrincipal_pow_finrank_of_isPrincipal_map
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
I : Ideal A
hI : Submodule.IsPrincipal (map (algebraMap A B) I)
⊢ Submodule.IsPrincipal (I ^ finrank K L)
Tactic:
haveI : IsDomain B :=
  (IsIntegralClosure.equiv A B L (integralClosure A L)).toMulEquiv.isDomain (integralClosure A L)
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 : 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
I : Ideal A
hI : Submodule.IsPrincipal (map (algebraMap A B) I)
this : IsDomain B
⊢ Submodule.IsPrincipal (I ^ finrank K L)
Theorem: Ideal.isPrincipal_pow_finrank_of_isPrincipal_map
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
I : Ideal A
hI : Submodule.IsPrincipal (map (algebraMap A B) I)
this : IsDomain B
⊢ Submodule.IsPrincipal (I ^ finrank K L)
Tactic:
haveI := IsIntegralClosure.isNoetherian A K L B
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 : 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
I : Ideal A
hI : Submodule.IsPrincipal (map (algebraMap A B) I)
this✝ : IsDomain B
this : IsNoetherian A B
⊢ Submodule.IsPrincipal (I ^ finrank K L)
Theorem: Ideal.isPrincipal_pow_finrank_of_isPrincipal_map
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
I : Ideal A
hI : Submodule.IsPrincipal (map (algebraMap A B) I)
this✝ : IsDomain B
this : IsNoetherian A B
⊢ Submodule.IsPrincipal (I ^ finrank K L)
Tactic:
haveI := IsIntegralClosure.isDedekindDomain A K L B
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 : 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
I : Ideal A
hI : Submodule.IsPrincipal (map (algebraMap A B) I)
this✝¹ : IsDomain B
this✝ : IsNoetherian A B
this : IsDedekindDomain B
⊢ Submodule.IsPrincipal (I ^ finrank K L)