Theorem: MvPolynomial.aeval_range (DividedPowers/PolynomialMap/Basic.lean)

State before:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
⊢ (aeval s).range = Algebra.adjoin R (Set.range s)
Tactic:
apply le_antisymm
State after:
case a
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
⊢ (aeval s).range ≤ Algebra.adjoin R (Set.range s)

case a
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
⊢ Algebra.adjoin R (Set.range s) ≤ (aeval s).range

State before:
case a
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
⊢ (aeval s).range ≤ Algebra.adjoin R (Set.range s)
Tactic:
rintro x ⟨p, rfl⟩
State after:
case a.intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
p : MvPolynomial σ R
⊢ (aeval s).toRingHom p ∈ Algebra.adjoin R (Set.range s)

State before:
case a.intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
p : MvPolynomial σ R
⊢ (aeval s).toRingHom p ∈ Algebra.adjoin R (Set.range s)
Tactic:
simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe]
State after:
case a.intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
p : MvPolynomial σ R
⊢ (aeval s) p ∈ Algebra.adjoin R (Set.range s)

State before:
case a.intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
p : MvPolynomial σ R
⊢ (aeval s) p ∈ Algebra.adjoin R (Set.range s)
Tactic:
induction p using induction_on with
| h_C a =>
  simp only [aeval_C, Algebra.mem_adjoin_iff]
  apply Subsemiring.subset_closure
  left
  use a
| h_add p q hp hq => simp only [map_add]; exact Subalgebra.add_mem _ hp hq
| h_X p n h =>
  simp only [map_mul, aeval_X]
  apply Subalgebra.mul_mem _ h
  apply Algebra.subset_adjoin
  use n
State after:
no goals

State before:
case a.intro.h_C
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
a : R
⊢ (aeval s) (C a) ∈ Algebra.adjoin R (Set.range s)
Tactic:
simp only [aeval_C, Algebra.mem_adjoin_iff]
State after:
case a.intro.h_C
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
a : R
⊢ (algebraMap R S) a ∈ Algebra.adjoin R (Set.range s)

State before:
case a.intro.h_C
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
a : R
⊢ (algebraMap R S) a ∈ Algebra.adjoin R (Set.range s)
Tactic:
apply Subsemiring.subset_closure
State after:
case a.intro.h_C.a
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
a : R
⊢ (algebraMap R S) a ∈ Set.range ⇑(algebraMap R S) ∪ Set.range s

State before:
case a.intro.h_C.a
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
a : R
⊢ (algebraMap R S) a ∈ Set.range ⇑(algebraMap R S) ∪ Set.range s
Tactic:
left
State after:
case a.intro.h_C.a.h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
a : R
⊢ (algebraMap R S) a ∈ Set.range ⇑(algebraMap R S)

State before:
case a.intro.h_C.a.h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
a : R
⊢ (algebraMap R S) a ∈ Set.range ⇑(algebraMap R S)
Tactic:
use a
State after:
no goals

State before:
case a.intro.h_add
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
p q : MvPolynomial σ R
hp : (aeval s) p ∈ Algebra.adjoin R (Set.range s)
hq : (aeval s) q ∈ Algebra.adjoin R (Set.range s)
⊢ (aeval s) (p + q) ∈ Algebra.adjoin R (Set.range s)
Tactic:
simp only [map_add]
State after:
case a.intro.h_add
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
p q : MvPolynomial σ R
hp : (aeval s) p ∈ Algebra.adjoin R (Set.range s)
hq : (aeval s) q ∈ Algebra.adjoin R (Set.range s)
⊢ (aeval s) p + (aeval s) q ∈ Algebra.adjoin R (Set.range s)

State before:
case a.intro.h_add
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
p q : MvPolynomial σ R
hp : (aeval s) p ∈ Algebra.adjoin R (Set.range s)
hq : (aeval s) q ∈ Algebra.adjoin R (Set.range s)
⊢ (aeval s) p + (aeval s) q ∈ Algebra.adjoin R (Set.range s)
Tactic:
exact Subalgebra.add_mem _ hp hq
State after:
no goals

State before:
case a.intro.h_X
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
p : MvPolynomial σ R
n : σ
h : (aeval s) p ∈ Algebra.adjoin R (Set.range s)
⊢ (aeval s) (p * X n) ∈ Algebra.adjoin R (Set.range s)
Tactic:
simp only [map_mul, aeval_X]
State after:
case a.intro.h_X
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
p : MvPolynomial σ R
n : σ
h : (aeval s) p ∈ Algebra.adjoin R (Set.range s)
⊢ (aeval s) p * s n ∈ Algebra.adjoin R (Set.range s)

State before:
case a.intro.h_X
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
p : MvPolynomial σ R
n : σ
h : (aeval s) p ∈ Algebra.adjoin R (Set.range s)
⊢ (aeval s) p * s n ∈ Algebra.adjoin R (Set.range s)
Tactic:
apply Subalgebra.mul_mem _ h
State after:
case a.intro.h_X
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
p : MvPolynomial σ R
n : σ
h : (aeval s) p ∈ Algebra.adjoin R (Set.range s)
⊢ s n ∈ Algebra.adjoin R (Set.range s)

State before:
case a.intro.h_X
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
p : MvPolynomial σ R
n : σ
h : (aeval s) p ∈ Algebra.adjoin R (Set.range s)
⊢ s n ∈ Algebra.adjoin R (Set.range s)
Tactic:
apply Algebra.subset_adjoin
State after:
case a.intro.h_X.a
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
p : MvPolynomial σ R
n : σ
h : (aeval s) p ∈ Algebra.adjoin R (Set.range s)
⊢ s n ∈ Set.range s

State before:
case a.intro.h_X.a
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
p : MvPolynomial σ R
n : σ
h : (aeval s) p ∈ Algebra.adjoin R (Set.range s)
⊢ s n ∈ Set.range s
Tactic:
use n
State after:
no goals

State before:
case a
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
⊢ Algebra.adjoin R (Set.range s) ≤ (aeval s).range
Tactic:
rw [Algebra.adjoin_le_iff]
State after:
case a
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
⊢ Set.range s ⊆ ↑(aeval s).range

State before:
case a
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
⊢ Set.range s ⊆ ↑(aeval s).range
Tactic:
rintro x ⟨i, rfl⟩
State after:
case a.intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
i : σ
⊢ s i ∈ ↑(aeval s).range

State before:
case a.intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
i : σ
⊢ s i ∈ ↑(aeval s).range
Tactic:
use X i
State after:
case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
i : σ
⊢ (aeval s).toRingHom (X i) = s i

State before:
case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
σ : Type u_3
s : σ → S
i : σ
⊢ (aeval s).toRingHom (X i) = s i
Tactic:
simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, aeval_X]
State after:
no goals