internlm/Lean-Github huggingface dataset:
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
⊢ Submodule.IsPrincipal (I ^ finrank K L)
Tactic:
haveI := IsIntegralClosure.isFractionRing_of_finite_extension 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
this : IsFractionRing B L
⊢ 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
this✝ : IsDedekindDomain B
this : IsFractionRing B L
⊢ Submodule.IsPrincipal (I ^ finrank K L)
Tactic:
have hAB : Function.Injective (algebraMap A B)
Proof state after:
case hAB
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
⊢ Function.Injective ⇑(algebraMap A B)

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 : Function.Injective ⇑(algebraMap 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
this✝ : IsDedekindDomain B
this : IsFractionRing B L
hAB : Function.Injective ⇑(algebraMap A B)
⊢ Submodule.IsPrincipal (I ^ finrank K L)
Tactic:
rw [← NoZeroSMulDivisors.iff_algebraMap_injective] at hAB
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
this : IsFractionRing B L
hAB : NoZeroSMulDivisors 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
this✝ : IsDedekindDomain B
this : IsFractionRing B L
hAB : NoZeroSMulDivisors A B
⊢ Submodule.IsPrincipal (I ^ finrank K L)
Tactic:
letI : Algebra (FractionRing A) (FractionRing B) := FractionRing.liftAlgebra _ _
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
this✝ : IsFractionRing B L
hAB : NoZeroSMulDivisors A B
this : Algebra (FractionRing A) (FractionRing B) := FractionRing.liftAlgebra A (FractionRing 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
this✝¹ : IsDedekindDomain B
this✝ : IsFractionRing B L
hAB : NoZeroSMulDivisors A B
this : Algebra (FractionRing A) (FractionRing B) := FractionRing.liftAlgebra A (FractionRing B)
⊢ Submodule.IsPrincipal (I ^ finrank K L)
Tactic:
have : IsScalarTower A (FractionRing A) (FractionRing B) :=
  FractionRing.isScalarTower_liftAlgebra _ _
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
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)
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)
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)
Tactic:
have : IsSeparable (FractionRing A) (FractionRing B) := IsSeparable.of_equiv_equiv _ _ H
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
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)
this : IsSeparable (FractionRing A) (FractionRing 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
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)
this : IsSeparable (FractionRing A) (FractionRing B)
⊢ Submodule.IsPrincipal (I ^ finrank K L)
Tactic:
have hLK : finrank (FractionRing A) (FractionRing B) = finrank K L := by
  simpa only [Cardinal.toNat_lift] using congr_arg Cardinal.toNat
    (Algebra.lift_rank_eq_of_equiv_equiv (FractionRing.algEquiv A K).symm.toRingEquiv
      (FractionRing.algEquiv B L).symm.toRingEquiv H).symm
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
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)
this : IsSeparable (FractionRing A) (FractionRing B)
hLK : finrank (FractionRing A) (FractionRing B) = finrank K L
⊢ 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
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)
this : IsSeparable (FractionRing A) (FractionRing B)
hLK : finrank (FractionRing A) (FractionRing B) = finrank K L
⊢ Submodule.IsPrincipal (I ^ finrank K L)
Tactic:
rw [← hLK, ← Ideal.spanIntNorm_map, ← (I.map (algebraMap A B)).span_singleton_generator,
  Ideal.spanIntNorm_singleton]
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
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)
this : IsSeparable (FractionRing A) (FractionRing B)
hLK : finrank (FractionRing A) (FractionRing B) = finrank K L
⊢ Submodule.IsPrincipal (span {(Algebra.intNorm A B) (Submodule.IsPrincipal.generator (map (algebraMap A B) I))})
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)
H :
  (algebraMap (FractionRing A) (FractionRing B)).comp ↑(FractionRing.algEquiv A K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv B L).symm.toRingEquiv).comp (algebraMap K L)
this : IsSeparable (FractionRing A) (FractionRing B)
hLK : finrank (FractionRing A) (FractionRing B) = finrank K L
⊢ Submodule.IsPrincipal (span {(Algebra.intNorm A B) (Submodule.IsPrincipal.generator (map (algebraMap A B) I))})
Tactic:
exact ⟨⟨_, rfl⟩⟩
Proof state after:
no goals
Theorem: Ideal.isPrincipal_pow_finrank_of_isPrincipal_map
Proof state before:
case hAB
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
⊢ Function.Injective ⇑(algebraMap A B)
Tactic:
refine Function.Injective.of_comp (f := algebraMap B L) ?_
Proof state after:
case hAB
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
⊢ Function.Injective (⇑(algebraMap B L) ∘ ⇑(algebraMap A B))
Theorem: Ideal.isPrincipal_pow_finrank_of_isPrincipal_map
Proof state before:
case hAB
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
⊢ Function.Injective (⇑(algebraMap B L) ∘ ⇑(algebraMap A B))
Tactic:
rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq A K L]
Proof state after:
case hAB
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
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap A K))