internlm/Lean-Github huggingface dataset:
Theorem: MvPolynomial.prod_contains_no
Proof state before:
case refine'_2.h
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
a : MvPolynomial ι R
s : Finset (MvPolynomial ι R)
has : a ∉ s
hs : (∀ p ∈ s, ∀ j ∈ p.support, j i = 0) → degreeOf i (s.prod id) = 0
hp : ∀ p ∈ cons a s has, ∀ j ∈ p.support, j i = 0
⊢ degreeOf i (id a) + 0 ≤ 0
Tactic:
simp only [id, add_zero, le_zero_iff]
Proof state after:
case refine'_2.h
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
a : MvPolynomial ι R
s : Finset (MvPolynomial ι R)
has : a ∉ s
hs : (∀ p ∈ s, ∀ j ∈ p.support, j i = 0) → degreeOf i (s.prod id) = 0
hp : ∀ p ∈ cons a s has, ∀ j ∈ p.support, j i = 0
⊢ degreeOf i a = 0
Theorem: MvPolynomial.prod_contains_no
Proof state before:
case refine'_2.h
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
a : MvPolynomial ι R
s : Finset (MvPolynomial ι R)
has : a ∉ s
hs : (∀ p ∈ s, ∀ j ∈ p.support, j i = 0) → degreeOf i (s.prod id) = 0
hp : ∀ p ∈ cons a s has, ∀ j ∈ p.support, j i = 0
⊢ degreeOf i a = 0
Tactic:
exact (degreeOf_eq_zero_iff _ _).2 (hp a (mem_cons_self _ _))
Proof state after:
no goals
Theorem: MvPolynomial.prod_contains_no
Proof state before:
case refine'_2.h
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
a : MvPolynomial ι R
s : Finset (MvPolynomial ι R)
has : a ∉ s
hs : (∀ p ∈ s, ∀ j ∈ p.support, j i = 0) → degreeOf i (s.prod id) = 0
hp : ∀ p ∈ cons a s has, ∀ j ∈ p.support, j i = 0
⊢ ∀ p ∈ s, ∀ j ∈ p.support, j i = 0
Tactic:
intro p hps m hmp
Proof state after:
case refine'_2.h
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
a : MvPolynomial ι R
s : Finset (MvPolynomial ι R)
has : a ∉ s
hs : (∀ p ∈ s, ∀ j ∈ p.support, j i = 0) → degreeOf i (s.prod id) = 0
hp : ∀ p ∈ cons a s has, ∀ j ∈ p.support, j i = 0
p : MvPolynomial ι R
hps : p ∈ s
m : ι →₀ ℕ
hmp : m ∈ p.support
⊢ m i = 0
Theorem: MvPolynomial.prod_contains_no
Proof state before:
case refine'_2.h
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
a : MvPolynomial ι R
s : Finset (MvPolynomial ι R)
has : a ∉ s
hs : (∀ p ∈ s, ∀ j ∈ p.support, j i = 0) → degreeOf i (s.prod id) = 0
hp : ∀ p ∈ cons a s has, ∀ j ∈ p.support, j i = 0
p : MvPolynomial ι R
hps : p ∈ s
m : ι →₀ ℕ
hmp : m ∈ p.support
⊢ m i = 0
Tactic:
apply hp p _ m hmp
Proof state after:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
a : MvPolynomial ι R
s : Finset (MvPolynomial ι R)
has : a ∉ s
hs : (∀ p ∈ s, ∀ j ∈ p.support, j i = 0) → degreeOf i (s.prod id) = 0
hp : ∀ p ∈ cons a s has, ∀ j ∈ p.support, j i = 0
p : MvPolynomial ι R
hps : p ∈ s
m : ι →₀ ℕ
hmp : m ∈ p.support
⊢ p ∈ cons a s has
Theorem: MvPolynomial.prod_contains_no
Proof state before:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
a : MvPolynomial ι R
s : Finset (MvPolynomial ι R)
has : a ∉ s
hs : (∀ p ∈ s, ∀ j ∈ p.support, j i = 0) → degreeOf i (s.prod id) = 0
hp : ∀ p ∈ cons a s has, ∀ j ∈ p.support, j i = 0
p : MvPolynomial ι R
hps : p ∈ s
m : ι →₀ ℕ
hmp : m ∈ p.support
⊢ p ∈ cons a s has
Tactic:
simp only [hps, mem_cons, or_true_iff]
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_prod
Proof state before:
R : Type ?u.336037
ι : Type u_3
inst✝² : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
P : σ → MvPolynomial ι S
L : Finset σ
⊢ homogenization i (∏ l ∈ L, P l) = ∏ l ∈ L, homogenization i (P l)
Tactic:
induction' L using Finset.induction with p S hS hSi
Proof state after:
case empty
R : Type ?u.336037
ι : Type u_3
inst✝² : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
P : σ → MvPolynomial ι S
⊢ homogenization i (∏ l ∈ ∅, P l) = ∏ l ∈ ∅, homogenization i (P l)

case insert
R : Type ?u.336037
ι : Type u_3
inst✝² : CommSemiring R
σ : Type u_1
S✝ : Type u_2
inst✝¹ : CommRing S✝
inst✝ : IsDomain S✝
i : ι
P : σ → MvPolynomial ι S✝
p : σ
S : Finset σ
hS : p ∉ S
hSi : homogenization i (∏ l ∈ S, P l) = ∏ l ∈ S, homogenization i (P l)
⊢ homogenization i (∏ l ∈ insert p S, P l) = ∏ l ∈ insert p S, homogenization i (P l)
Theorem: MvPolynomial.homogenization_prod
Proof state before:
case insert
R : Type ?u.336037
ι : Type u_3
inst✝² : CommSemiring R
σ : Type u_1
S✝ : Type u_2
inst✝¹ : CommRing S✝
inst✝ : IsDomain S✝
i : ι
P : σ → MvPolynomial ι S✝
p : σ
S : Finset σ
hS : p ∉ S
hSi : homogenization i (∏ l ∈ S, P l) = ∏ l ∈ S, homogenization i (P l)
⊢ homogenization i (∏ l ∈ insert p S, P l) = ∏ l ∈ insert p S, homogenization i (P l)
Tactic:
simp only [Finset.prod_insert hS]
Proof state after:
case insert
R : Type ?u.336037
ι : Type u_3
inst✝² : CommSemiring R
σ : Type u_1
S✝ : Type u_2
inst✝¹ : CommRing S✝
inst✝ : IsDomain S✝
i : ι
P : σ → MvPolynomial ι S✝
p : σ
S : Finset σ
hS : p ∉ S
hSi : homogenization i (∏ l ∈ S, P l) = ∏ l ∈ S, homogenization i (P l)
⊢ homogenization i (P p * ∏ l ∈ S, P l) = homogenization i (P p) * ∏ l ∈ S, homogenization i (P l)
Theorem: MvPolynomial.homogenization_prod
Proof state before:
case insert
R : Type ?u.336037
ι : Type u_3
inst✝² : CommSemiring R
σ : Type u_1
S✝ : Type u_2
inst✝¹ : CommRing S✝
inst✝ : IsDomain S✝
i : ι
P : σ → MvPolynomial ι S✝
p : σ
S : Finset σ
hS : p ∉ S
hSi : homogenization i (∏ l ∈ S, P l) = ∏ l ∈ S, homogenization i (P l)
⊢ homogenization i (P p * ∏ l ∈ S, P l) = homogenization i (P p) * ∏ l ∈ S, homogenization i (P l)
Tactic:
rw [homogenization_mul]
Proof state after:
case insert
R : Type ?u.336037
ι : Type u_3
inst✝² : CommSemiring R
σ : Type u_1
S✝ : Type u_2
inst✝¹ : CommRing S✝
inst✝ : IsDomain S✝
i : ι
P : σ → MvPolynomial ι S✝
p : σ
S : Finset σ
hS : p ∉ S
hSi : homogenization i (∏ l ∈ S, P l) = ∏ l ∈ S, homogenization i (P l)
⊢ homogenization i (P p) * homogenization i (∏ l ∈ S, P l) = homogenization i (P p) * ∏ l ∈ S, homogenization i (P l)
Theorem: MvPolynomial.homogenization_prod
Proof state before:
case insert
R : Type ?u.336037
ι : Type u_3
inst✝² : CommSemiring R
σ : Type u_1
S✝ : Type u_2
inst✝¹ : CommRing S✝
inst✝ : IsDomain S✝
i : ι
P : σ → MvPolynomial ι S✝
p : σ
S : Finset σ
hS : p ∉ S
hSi : homogenization i (∏ l ∈ S, P l) = ∏ l ∈ S, homogenization i (P l)
⊢ homogenization i (P p) * homogenization i (∏ l ∈ S, P l) = homogenization i (P p) * ∏ l ∈ S, homogenization i (P l)
Tactic:
rw [hSi]
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_prod
Proof state before:
case empty
R : Type ?u.336037
ι : Type u_3
inst✝² : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
P : σ → MvPolynomial ι S
⊢ homogenization i (∏ l ∈ ∅, P l) = ∏ l ∈ ∅, homogenization i (P l)
Tactic:
simp
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_prod_id
Proof state before:
R : Type ?u.338728
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
P : Finset (MvPolynomial ι S)
⊢ homogenization i (P.prod id) = ∏ p ∈ P, homogenization i p
Tactic:
induction' P using Finset.induction with p S hS hSi
Proof state after:
case empty
R : Type ?u.338728
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
⊢ homogenization i (∅.prod id) = ∏ p ∈ ∅, homogenization i p

case insert
R : Type ?u.338728
ι : Type u_2
inst✝² : CommSemiring R
S✝ : Type u_1
inst✝¹ : CommRing S✝
inst✝ : IsDomain S✝
i : ι
p : MvPolynomial ι S✝
S : Finset (MvPolynomial ι S✝)
hS : p ∉ S
hSi : homogenization i (S.prod id) = ∏ p ∈ S, homogenization i p
⊢ homogenization i ((insert p S).prod id) = ∏ p ∈ insert p S, homogenization i p
Theorem: MvPolynomial.homogenization_prod_id
Proof state before:
case insert
R : Type ?u.338728
ι : Type u_2
inst✝² : CommSemiring R
S✝ : Type u_1
inst✝¹ : CommRing S✝
inst✝ : IsDomain S✝
i : ι
p : MvPolynomial ι S✝
S : Finset (MvPolynomial ι S✝)
hS : p ∉ S
hSi : homogenization i (S.prod id) = ∏ p ∈ S, homogenization i p
⊢ homogenization i ((insert p S).prod id) = ∏ p ∈ insert p S, homogenization i p
Tactic:
simp only [Finset.prod_insert hS]
Proof state after:
case insert
R : Type ?u.338728
ι : Type u_2
inst✝² : CommSemiring R
S✝ : Type u_1
inst✝¹ : CommRing S✝
inst✝ : IsDomain S✝
i : ι
p : MvPolynomial ι S✝
S : Finset (MvPolynomial ι S✝)
hS : p ∉ S
hSi : homogenization i (S.prod id) = ∏ p ∈ S, homogenization i p
⊢ homogenization i (id p * ∏ x ∈ S, id x) = homogenization i p * ∏ p ∈ S, homogenization i p
Theorem: MvPolynomial.homogenization_prod_id
Proof state before:
case insert
R : Type ?u.338728
ι : Type u_2
inst✝² : CommSemiring R
S✝ : Type u_1
inst✝¹ : CommRing S✝
inst✝ : IsDomain S✝
i : ι
p : MvPolynomial ι S✝
S : Finset (MvPolynomial ι S✝)
hS : p ∉ S
hSi : homogenization i (S.prod id) = ∏ p ∈ S, homogenization i p
⊢ homogenization i (id p * ∏ x ∈ S, id x) = homogenization i p * ∏ p ∈ S, homogenization i p
Tactic:
rw [homogenization_mul]
Proof state after:
case insert
R : Type ?u.338728
ι : Type u_2
inst✝² : CommSemiring R
S✝ : Type u_1
inst✝¹ : CommRing S✝
inst✝ : IsDomain S✝
i : ι
p : MvPolynomial ι S✝
S : Finset (MvPolynomial ι S✝)
hS : p ∉ S
hSi : homogenization i (S.prod id) = ∏ p ∈ S, homogenization i p
⊢ homogenization i (id p) * homogenization i (∏ x ∈ S, id x) = homogenization i p * ∏ p ∈ S, homogenization i p
Theorem: MvPolynomial.homogenization_prod_id
Proof state before:
case insert
R : Type ?u.338728
ι : Type u_2
inst✝² : CommSemiring R
S✝ : Type u_1
inst✝¹ : CommRing S✝
inst✝ : IsDomain S✝
i : ι
p : MvPolynomial ι S✝
S : Finset (MvPolynomial ι S✝)
hS : p ∉ S
hSi : homogenization i (S.prod id) = ∏ p ∈ S, homogenization i p
⊢ homogenization i (id p) * homogenization i (∏ x ∈ S, id x) = homogenization i p * ∏ p ∈ S, homogenization i p
Tactic:
rw [hSi]
Proof state after:
case insert
R : Type ?u.338728
ι : Type u_2
inst✝² : CommSemiring R
S✝ : Type u_1
inst✝¹ : CommRing S✝
inst✝ : IsDomain S✝
i : ι
p : MvPolynomial ι S✝
S : Finset (MvPolynomial ι S✝)
hS : p ∉ S
hSi : homogenization i (S.prod id) = ∏ p ∈ S, homogenization i p
⊢ homogenization i (id p) * ∏ p ∈ S, homogenization i p = homogenization i p * ∏ p ∈ S, homogenization i p
Theorem: MvPolynomial.homogenization_prod_id
Proof state before:
case insert
R : Type ?u.338728
ι : Type u_2
inst✝² : CommSemiring R
S✝ : Type u_1
inst✝¹ : CommRing S✝
inst✝ : IsDomain S✝
i : ι
p : MvPolynomial ι S✝
S : Finset (MvPolynomial ι S✝)
hS : p ∉ S
hSi : homogenization i (S.prod id) = ∏ p ∈ S, homogenization i p
⊢ homogenization i (id p) * ∏ p ∈ S, homogenization i p = homogenization i p * ∏ p ∈ S, homogenization i p
Tactic:
rw [id]
Proof state after:
no goals
Theorem: MvPolynomial.homogenization_prod_id
Proof state before:
case empty
R : Type ?u.338728
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
⊢ homogenization i (∅.prod id) = ∏ p ∈ ∅, homogenization i p
Tactic:
simp
Proof state after:
no goals
Theorem: Ideal.spanIntNorm_bot
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✝² : Nontrivial S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
x : R
hx : x ∈ ⇑(Algebra.intNorm R S) '' ↑⊥
⊢ x = 0
Tactic:
simpa using hx
Proof state after:
no goals
Theorem: Ideal.spanIntNorm_eq_bot_iff
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
I : Ideal S
⊢ spanIntNorm R I = ⊥ ↔ I = ⊥
Tactic:
simp only [spanIntNorm, span_eq_bot, Set.mem_image, SetLike.mem_coe, forall_exists_index, and_imp,
  forall_apply_eq_imp_iff₂, Algebra.intNorm_eq_zero, @eq_bot_iff _ _ _ I, SetLike.le_def]
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
I : Ideal S
⊢ (∀ a ∈ I, a = 0) ↔ ∀ ⦃x : S⦄, x ∈ I → x ∈ ⊥
Theorem: Ideal.spanIntNorm_eq_bot_iff
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
I : Ideal S
⊢ (∀ a ∈ I, a = 0) ↔ ∀ ⦃x : S⦄, x ∈ I → x ∈ ⊥
Tactic:
rfl
Proof state after:
no goals
Theorem: Ideal.spanIntNorm_singleton
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)
r : S
x : R
hx : x ∈ ⇑(Algebra.intNorm R S) '' ↑(span {r})
⊢ (Algebra.intNorm R S) r ∣ x
Tactic:
obtain ⟨x, hx', rfl⟩ := (Set.mem_image _ _ _).mp hx
Proof state after:
case 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)
r x : S
hx' : x ∈ ↑(span {r})
hx : (Algebra.intNorm R S) x ∈ ⇑(Algebra.intNorm R S) '' ↑(span {r})
⊢ (Algebra.intNorm R S) r ∣ (Algebra.intNorm R S) x
Theorem: Ideal.spanIntNorm_singleton
Proof state before:
case 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)
r x : S
hx' : x ∈ ↑(span {r})
hx : (Algebra.intNorm R S) x ∈ ⇑(Algebra.intNorm R S) '' ↑(span {r})
⊢ (Algebra.intNorm R S) r ∣ (Algebra.intNorm R S) x
Tactic:
exact map_dvd _ (mem_span_singleton.mp hx')
Proof state after:
no goals
Theorem: Ideal.spanIntNorm_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)
⊢ spanIntNorm R ⊤ = ⊤
Tactic:
rw [← Ideal.span_singleton_one, spanIntNorm_singleton]
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)
⊢ span {(Algebra.intNorm R S) 1} = ⊤
Theorem: Ideal.spanIntNorm_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)
⊢ span {(Algebra.intNorm R S) 1} = ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: Ideal.map_spanIntNorm
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
T : Type u_3
inst✝ : CommRing T
f : R →+* T
⊢ map f (spanIntNorm R I) = span (⇑f ∘ ⇑(Algebra.intNorm R S) '' ↑I)
Tactic:
rw [spanIntNorm, map_span, Set.image_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 : Ideal S
T : Type u_3
inst✝ : CommRing T
f : R →+* T
⊢ span ((fun x => f ((Algebra.intNorm R S) x)) '' ↑I) = span (⇑f ∘ ⇑(Algebra.intNorm R S) '' ↑I)
Theorem: Ideal.map_spanIntNorm
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
T : Type u_3
inst✝ : CommRing T
f : R →+* T
⊢ span ((fun x => f ((Algebra.intNorm R S) x)) '' ↑I) = span (⇑f ∘ ⇑(Algebra.intNorm R S) '' ↑I)
Tactic:
rfl
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ₘ)
⊢ spanIntNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanIntNorm R I)
Tactic:
let K := FractionRing 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)
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
⊢ spanIntNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanIntNorm R I)
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
⊢ spanIntNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanIntNorm R I)
Tactic:
let f : Rₘ →+* K := IsLocalization.map _ (T := R⁰) (RingHom.id R) hM
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 : 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
⊢ spanIntNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanIntNorm R I)
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
⊢ spanIntNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanIntNorm R I)
Tactic:
letI := f.toAlgebra
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 : 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
⊢ spanIntNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanIntNorm R I)