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
this✝² : IsDedekindDomain B
this✝¹ : IsFractionRing B L
hAB : NoZeroSMulDivisors A B
this✝ : Algebra (FractionRing A) (FractionRing B) := FractionRing.liftAlgebra A (FractionRing B)
this : IsScalarTower A (FractionRing A) (FractionRing B)
⊢ Submodule.IsPrincipal (I ^ finrank K L)
Tactic:
have H : RingHom.comp (algebraMap (FractionRing A) (FractionRing B))
  ↑(FractionRing.algEquiv A K).symm.toRingEquiv =
    RingHom.comp ↑(FractionRing.algEquiv B L).symm.toRingEquiv (algebraMap K L)
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
I : Ideal A
hI : Submodule.IsPrincipal (map (algebraMap A B) I)
this✝⁴ : IsDomain B
this✝³ : IsNoetherian A B
this✝² : IsDedekindDomain B
this✝¹ : IsFractionRing B L
hAB : NoZeroSMulDivisors A B
this✝ : Algebra (FractionRing A) (FractionRing B) := FractionRing.liftAlgebra A (FractionRing B)
this : IsScalarTower A (FractionRing A) (FractionRing B)
⊢ (algebraMap (FractionRing A) (FractionRing B)).comp ↑(FractionRing.algEquiv A K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv B L).symm.toRingEquiv).comp (algebraMap K L)

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
this✝¹ : IsFractionRing B L
hAB : NoZeroSMulDivisors A B
this✝ : Algebra (FractionRing A) (FractionRing B) := FractionRing.liftAlgebra A (FractionRing B)
this : IsScalarTower A (FractionRing A) (FractionRing B)
H :
  (algebraMap (FractionRing A) (FractionRing B)).comp ↑(FractionRing.algEquiv A K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv B L).symm.toRingEquiv).comp (algebraMap K L)
⊢ Submodule.IsPrincipal (I ^ finrank K L)