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
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)
Tactic:
refine ⟨(Ideal.span {β}).comap (algebraMap A B), ?_, ?_⟩
Proof state after:
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 {β}))

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 {β})))