internlm/Lean-Github huggingface dataset:
Theorem: Ideal.spanIntNorm_localization
Proof state before:
R : Type u_1
inst✝²⁵ : CommRing R
S : Type u_2
inst✝²⁴ : CommRing S
inst✝²³ : Algebra R S
inst✝²² : IsIntegrallyClosed R
inst✝²¹ : IsDomain R
inst✝²⁰ : IsDomain S
inst✝¹⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹⁸ : IsIntegrallyClosed S
inst✝¹⁷ : IsSeparable (FractionRing R) (FractionRing S)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this✝² : Algebra Rₘ K := f.toAlgebra
this✝¹ : IsScalarTower R Rₘ K
this✝ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
L : Type u_2 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
this : Algebra Sₘ L := g.toAlgebra
⊢ algebraMap S L = (algebraMap Sₘ L).comp (algebraMap S Sₘ)
Tactic:
rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq]
Proof state after:
no goals
Theorem: Ideal.spanIntNorm_localization
Proof state before:
R : Type u_1
inst✝²⁵ : CommRing R
S : Type u_2
inst✝²⁴ : CommRing S
inst✝²³ : Algebra R S
inst✝²² : IsIntegrallyClosed R
inst✝²¹ : IsDomain R
inst✝²⁰ : IsDomain S
inst✝¹⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹⁸ : IsIntegrallyClosed S
inst✝¹⁷ : IsSeparable (FractionRing R) (FractionRing S)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this✝⁵ : Algebra Rₘ K := f.toAlgebra
this✝⁴ : IsScalarTower R Rₘ K
this✝³ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
L : Type u_2 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
this✝² : Algebra Sₘ L := g.toAlgebra
this✝¹ : IsScalarTower S Sₘ L
this✝ : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
this : IsScalarTower Rₘ K L
⊢ IsScalarTower Rₘ Sₘ L
Tactic:
apply IsScalarTower.of_algebraMap_eq'
Proof state after:
case h
R : Type u_1
inst✝²⁵ : CommRing R
S : Type u_2
inst✝²⁴ : CommRing S
inst✝²³ : Algebra R S
inst✝²² : IsIntegrallyClosed R
inst✝²¹ : IsDomain R
inst✝²⁰ : IsDomain S
inst✝¹⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹⁸ : IsIntegrallyClosed S
inst✝¹⁷ : IsSeparable (FractionRing R) (FractionRing S)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this✝⁵ : Algebra Rₘ K := f.toAlgebra
this✝⁴ : IsScalarTower R Rₘ K
this✝³ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
L : Type u_2 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
this✝² : Algebra Sₘ L := g.toAlgebra
this✝¹ : IsScalarTower S Sₘ L
this✝ : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
this : IsScalarTower Rₘ K L
⊢ algebraMap Rₘ L = (algebraMap Sₘ L).comp (algebraMap Rₘ Sₘ)
Theorem: Ideal.spanIntNorm_localization
Proof state before:
case h
R : Type u_1
inst✝²⁵ : CommRing R
S : Type u_2
inst✝²⁴ : CommRing S
inst✝²³ : Algebra R S
inst✝²² : IsIntegrallyClosed R
inst✝²¹ : IsDomain R
inst✝²⁰ : IsDomain S
inst✝¹⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹⁸ : IsIntegrallyClosed S
inst✝¹⁷ : IsSeparable (FractionRing R) (FractionRing S)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this✝⁵ : Algebra Rₘ K := f.toAlgebra
this✝⁴ : IsScalarTower R Rₘ K
this✝³ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
L : Type u_2 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
this✝² : Algebra Sₘ L := g.toAlgebra
this✝¹ : IsScalarTower S Sₘ L
this✝ : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
this : IsScalarTower Rₘ K L
⊢ algebraMap Rₘ L = (algebraMap Sₘ L).comp (algebraMap Rₘ Sₘ)
Tactic:
apply IsLocalization.ringHom_ext M
Proof state after:
case h.h
R : Type u_1
inst✝²⁵ : CommRing R
S : Type u_2
inst✝²⁴ : CommRing S
inst✝²³ : Algebra R S
inst✝²² : IsIntegrallyClosed R
inst✝²¹ : IsDomain R
inst✝²⁰ : IsDomain S
inst✝¹⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹⁸ : IsIntegrallyClosed S
inst✝¹⁷ : IsSeparable (FractionRing R) (FractionRing S)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this✝⁵ : Algebra Rₘ K := f.toAlgebra
this✝⁴ : IsScalarTower R Rₘ K
this✝³ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
L : Type u_2 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
this✝² : Algebra Sₘ L := g.toAlgebra
this✝¹ : IsScalarTower S Sₘ L
this✝ : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
this : IsScalarTower Rₘ K L
⊢ (algebraMap Rₘ L).comp (algebraMap R Rₘ) = ((algebraMap Sₘ L).comp (algebraMap Rₘ Sₘ)).comp (algebraMap R Rₘ)
Theorem: Ideal.spanIntNorm_localization
Proof state before:
case h.h
R : Type u_1
inst✝²⁵ : CommRing R
S : Type u_2
inst✝²⁴ : CommRing S
inst✝²³ : Algebra R S
inst✝²² : IsIntegrallyClosed R
inst✝²¹ : IsDomain R
inst✝²⁰ : IsDomain S
inst✝¹⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹⁸ : IsIntegrallyClosed S
inst✝¹⁷ : IsSeparable (FractionRing R) (FractionRing S)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this✝⁵ : Algebra Rₘ K := f.toAlgebra
this✝⁴ : IsScalarTower R Rₘ K
this✝³ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
L : Type u_2 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
this✝² : Algebra Sₘ L := g.toAlgebra
this✝¹ : IsScalarTower S Sₘ L
this✝ : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
this : IsScalarTower Rₘ K L
⊢ (algebraMap Rₘ L).comp (algebraMap R Rₘ) = ((algebraMap Sₘ L).comp (algebraMap Rₘ Sₘ)).comp (algebraMap R Rₘ)
Tactic:
rw [RingHom.algebraMap_toAlgebra, RingHom.algebraMap_toAlgebra (R := Sₘ), RingHom.comp_assoc,
  RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R S Sₘ,
  IsLocalization.map_comp, RingHom.comp_id, ← RingHom.comp_assoc, IsLocalization.map_comp,
  RingHom.comp_id, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
Proof state after:
no goals
Theorem: Ideal.spanIntNorm_localization
Proof state before:
case refine_1.intro.mk.intro.mk.intro.intro.a
R : Type u_1
inst✝²⁵ : CommRing R
S : Type u_2
inst✝²⁴ : CommRing S
inst✝²³ : Algebra R S
inst✝²² : IsIntegrallyClosed R
inst✝²¹ : IsDomain R
inst✝²⁰ : IsDomain S
inst✝¹⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹⁸ : IsIntegrallyClosed S
inst✝¹⁷ : IsSeparable (FractionRing R) (FractionRing S)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this✝⁸ : Algebra Rₘ K := f.toAlgebra
this✝⁷ : IsScalarTower R Rₘ K
this✝⁶ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
L : Type u_2 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
this✝⁵ : Algebra Sₘ L := g.toAlgebra
this✝⁴ : IsScalarTower S Sₘ L
this✝³ : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
this✝² : IsScalarTower Rₘ K L
this✝¹ : IsScalarTower Rₘ Sₘ L
this✝ : IsFractionRing Sₘ L :=
  IsFractionRing.isFractionRing_of_isDomain_of_isLocalization (Algebra.algebraMapSubmonoid S M) Sₘ L
this : IsIntegralClosure Sₘ Rₘ L
a' : Sₘ
a : S
ha : a ∈ I
s : R
hs : s ∈ ↑M
has :
  (Algebra.norm K) ((algebraMap Sₘ L) a') * (algebraMap R K) s ^ FiniteDimensional.finrank K L =
    (Algebra.norm K) ((algebraMap S L) a)
⊢ (algebraMap Rₘ K) ((Algebra.intNorm Rₘ Sₘ) a') *
      (algebraMap Rₘ K) ((algebraMap R Rₘ) s) ^ FiniteDimensional.finrank K L =
    (algebraMap Rₘ K) ((algebraMap R Rₘ) ((Algebra.intNorm R S) a))
Tactic:
rwa [Algebra.algebraMap_intNorm (L := L), ← IsScalarTower.algebraMap_apply,
  ← IsScalarTower.algebraMap_apply, Algebra.algebraMap_intNorm (L := L)]
Proof state after:
no goals
Theorem: Ideal.spanIntNorm_localization
Proof state before:
case refine_2
R : Type u_1
inst✝²⁵ : CommRing R
S : Type u_2
inst✝²⁴ : CommRing S
inst✝²³ : Algebra R S
inst✝²² : IsIntegrallyClosed R
inst✝²¹ : IsDomain R
inst✝²⁰ : IsDomain S
inst✝¹⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹⁸ : IsIntegrallyClosed S
inst✝¹⁷ : IsSeparable (FractionRing R) (FractionRing S)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
this✝⁸ : Algebra Rₘ K := f.toAlgebra
this✝⁷ : IsScalarTower R Rₘ K
this✝⁶ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
L : Type u_2 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
this✝⁵ : Algebra Sₘ L := g.toAlgebra
this✝⁴ : IsScalarTower S Sₘ L
this✝³ : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
this✝² : IsScalarTower Rₘ K L
this✝¹ : IsScalarTower Rₘ Sₘ L
this✝ : IsFractionRing Sₘ L :=
  IsFractionRing.isFractionRing_of_isDomain_of_isLocalization (Algebra.algebraMapSubmonoid S M) Sₘ L
this : IsIntegralClosure Sₘ Rₘ L
a : S
ha : a ∈ ↑I
⊢ (Algebra.intNorm Rₘ Sₘ) ((algebraMap S Sₘ) a) ∈
    ↑(Submodule.span Rₘ (⇑(Algebra.intNorm Rₘ Sₘ) '' ↑(map (algebraMap S Sₘ) I)))
Tactic:
exact subset_span (Set.mem_image_of_mem _ (mem_map_of_mem _ ha))
Proof state after:
no goals
Theorem: Ideal.spanIntNorm_mul_spanIntNorm_le
Proof state before:
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹ : IsIntegrallyClosed S
inst✝ : IsSeparable (FractionRing R) (FractionRing S)
I J : Ideal S
⊢ spanIntNorm R I * spanIntNorm R J ≤ spanIntNorm R (I * J)
Tactic:
rw [spanIntNorm, spanIntNorm, spanIntNorm, Ideal.span_mul_span', ← Set.image_mul]
Proof state after:
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹ : IsIntegrallyClosed S
inst✝ : IsSeparable (FractionRing R) (FractionRing S)
I J : Ideal S
⊢ span (⇑(Algebra.intNorm R S) '' (↑I * ↑J)) ≤ span (⇑(Algebra.intNorm R S) '' ↑(I * J))
Theorem: Ideal.spanIntNorm_mul_spanIntNorm_le
Proof state before:
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹ : IsIntegrallyClosed S
inst✝ : IsSeparable (FractionRing R) (FractionRing S)
I J : Ideal S
⊢ span (⇑(Algebra.intNorm R S) '' (↑I * ↑J)) ≤ span (⇑(Algebra.intNorm R S) '' ↑(I * J))
Tactic:
refine Ideal.span_mono (Set.monotone_image ?_)
Proof state after:
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹ : IsIntegrallyClosed S
inst✝ : IsSeparable (FractionRing R) (FractionRing S)
I J : Ideal S
⊢ ↑I * ↑J ≤ ↑(I * J)
Theorem: Ideal.spanIntNorm_mul_spanIntNorm_le
Proof state before:
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹ : IsIntegrallyClosed S
inst✝ : IsSeparable (FractionRing R) (FractionRing S)
I J : Ideal S
⊢ ↑I * ↑J ≤ ↑(I * J)
Tactic:
rintro _ ⟨x, hxI, y, hyJ, rfl⟩
Proof state after:
case intro.intro.intro.intro
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹ : IsIntegrallyClosed S
inst✝ : IsSeparable (FractionRing R) (FractionRing S)
I J : Ideal S
x : S
hxI : x ∈ ↑I
y : S
hyJ : y ∈ ↑J
⊢ (fun x x_1 => x * x_1) x y ∈ ↑(I * J)
Theorem: Ideal.spanIntNorm_mul_spanIntNorm_le
Proof state before:
case intro.intro.intro.intro
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹ : IsIntegrallyClosed S
inst✝ : IsSeparable (FractionRing R) (FractionRing S)
I J : Ideal S
x : S
hxI : x ∈ ↑I
y : S
hyJ : y ∈ ↑J
⊢ (fun x x_1 => x * x_1) x y ∈ ↑(I * J)
Tactic:
exact Ideal.mul_mem_mul hxI hyJ
Proof state after:
no goals
Theorem: Ideal.spanIntNorm_mul_of_bot_or_top
Proof state before:
R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : IsIntegrallyClosed R
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : IsSeparable (FractionRing R) (FractionRing S)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
⊢ spanIntNorm R (I * J) = spanIntNorm R I * spanIntNorm R J
Tactic:
refine le_antisymm ?_ (spanIntNorm_mul_spanIntNorm_le R _ _)
Proof state after:
R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : IsIntegrallyClosed R
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : IsSeparable (FractionRing R) (FractionRing S)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
⊢ spanIntNorm R (I * J) ≤ spanIntNorm R I * spanIntNorm R J
Theorem: Ideal.spanIntNorm_mul_of_bot_or_top
Proof state before:
R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : IsIntegrallyClosed R
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : IsSeparable (FractionRing R) (FractionRing S)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
⊢ spanIntNorm R (I * J) ≤ spanIntNorm R I * spanIntNorm R J
Tactic:
cases' eq_bot_or_top (spanIntNorm R I) with hI hI
Proof state after:
case inl
R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : IsIntegrallyClosed R
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : IsSeparable (FractionRing R) (FractionRing S)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊥
⊢ spanIntNorm R (I * J) ≤ spanIntNorm R I * spanIntNorm R J

case inr
R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : IsIntegrallyClosed R
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : IsSeparable (FractionRing R) (FractionRing S)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊤
⊢ spanIntNorm R (I * J) ≤ spanIntNorm R I * spanIntNorm R J
Theorem: Ideal.spanIntNorm_mul_of_bot_or_top
Proof state before:
case inr
R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : IsIntegrallyClosed R
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : IsSeparable (FractionRing R) (FractionRing S)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊤
⊢ spanIntNorm R (I * J) ≤ spanIntNorm R I * spanIntNorm R J
Tactic:
rw [hI, Ideal.top_mul]
Proof state after:
case inr
R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : IsIntegrallyClosed R
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : IsSeparable (FractionRing R) (FractionRing S)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊤
⊢ spanIntNorm R (I * J) ≤ spanIntNorm R J
Theorem: Ideal.spanIntNorm_mul_of_bot_or_top
Proof state before:
case inr
R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : IsIntegrallyClosed R
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : IsSeparable (FractionRing R) (FractionRing S)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊤
⊢ spanIntNorm R (I * J) ≤ spanIntNorm R J
Tactic:
cases' eq_bot_or_top (spanIntNorm R J) with hJ hJ
Proof state after:
case inr.inl
R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : IsIntegrallyClosed R
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : IsSeparable (FractionRing R) (FractionRing S)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊤
hJ : spanIntNorm R J = ⊥
⊢ spanIntNorm R (I * J) ≤ spanIntNorm R J

case inr.inr
R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : IsIntegrallyClosed R
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : IsSeparable (FractionRing R) (FractionRing S)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊤
hJ : spanIntNorm R J = ⊤
⊢ spanIntNorm R (I * J) ≤ spanIntNorm R J
Theorem: Ideal.spanIntNorm_mul_of_bot_or_top
Proof state before:
case inr.inr
R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : IsIntegrallyClosed R
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : IsSeparable (FractionRing R) (FractionRing S)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊤
hJ : spanIntNorm R J = ⊤
⊢ spanIntNorm R (I * J) ≤ spanIntNorm R J
Tactic:
rw [hJ]
Proof state after:
case inr.inr
R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : IsIntegrallyClosed R
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : IsSeparable (FractionRing R) (FractionRing S)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊤
hJ : spanIntNorm R J = ⊤
⊢ spanIntNorm R (I * J) ≤ ⊤