Theorem: PolynomialMap.φ_range (DividedPowers/PolynomialMap/Basic.lean)

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
⊢ (PolynomialMap.φ R s).range = Algebra.adjoin R ↑s
Tactic:
apply le_antisymm
State after:
case a
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
⊢ (PolynomialMap.φ R s).range ≤ Algebra.adjoin R ↑s

case a
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
⊢ Algebra.adjoin R ↑s ≤ (PolynomialMap.φ R s).range

State before:
case a
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
⊢ (PolynomialMap.φ R s).range ≤ Algebra.adjoin R ↑s
Tactic:
rintro _ ⟨p, rfl⟩
State after:
case a.intro
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R
⊢ (PolynomialMap.φ R s).toRingHom p ∈ Algebra.adjoin R ↑s

State before:
case a.intro
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R
⊢ (PolynomialMap.φ R s).toRingHom p ∈ Algebra.adjoin R ↑s
Tactic:
induction p using MvPolynomial.induction_on with
| h_C r => simp only [toRingHom_eq_coe, ← algebraMap_eq, RingHom.coe_coe, commutes,
    algebraMap_mem]
| h_add p q hp hq => simp only [map_add, add_mem hp hq]
| h_X p n hp =>
  rw [_root_.map_mul]
  apply mul_mem hp
  apply Algebra.subset_adjoin
  simp [φ]
State after:
no goals

State before:
case a.intro.h_C
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
r : R
⊢ (PolynomialMap.φ R s).toRingHom (C r) ∈ Algebra.adjoin R ↑s
Tactic:
simp only [toRingHom_eq_coe, ← algebraMap_eq, RingHom.coe_coe, commutes,
algebraMap_mem]
State after:
no goals

State before:
case a.intro.h_add
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p q : MvPolynomial (Fin s.card) R
hp : (PolynomialMap.φ R s).toRingHom p ∈ Algebra.adjoin R ↑s
hq : (PolynomialMap.φ R s).toRingHom q ∈ Algebra.adjoin R ↑s
⊢ (PolynomialMap.φ R s).toRingHom (p + q) ∈ Algebra.adjoin R ↑s
Tactic:
simp only [map_add, add_mem hp hq]
State after:
no goals

State before:
case a.intro.h_X
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R
n : Fin s.card
hp : (PolynomialMap.φ R s).toRingHom p ∈ Algebra.adjoin R ↑s
⊢ (PolynomialMap.φ R s).toRingHom (p * X n) ∈ Algebra.adjoin R ↑s
Tactic:
rw [_root_.map_mul]
State after:
case a.intro.h_X
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R
n : Fin s.card
hp : (PolynomialMap.φ R s).toRingHom p ∈ Algebra.adjoin R ↑s
⊢ (PolynomialMap.φ R s).toRingHom p * (PolynomialMap.φ R s).toRingHom (X n) ∈ Algebra.adjoin R ↑s

State before:
case a.intro.h_X
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R
n : Fin s.card
hp : (PolynomialMap.φ R s).toRingHom p ∈ Algebra.adjoin R ↑s
⊢ (PolynomialMap.φ R s).toRingHom p * (PolynomialMap.φ R s).toRingHom (X n) ∈ Algebra.adjoin R ↑s
Tactic:
apply mul_mem hp
State after:
case a.intro.h_X
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R
n : Fin s.card
hp : (PolynomialMap.φ R s).toRingHom p ∈ Algebra.adjoin R ↑s
⊢ (PolynomialMap.φ R s).toRingHom (X n) ∈ Algebra.adjoin R ↑s

State before:
case a.intro.h_X
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R
n : Fin s.card
hp : (PolynomialMap.φ R s).toRingHom p ∈ Algebra.adjoin R ↑s
⊢ (PolynomialMap.φ R s).toRingHom (X n) ∈ Algebra.adjoin R ↑s
Tactic:
apply Algebra.subset_adjoin
State after:
case a.intro.h_X.a
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R
n : Fin s.card
hp : (PolynomialMap.φ R s).toRingHom p ∈ Algebra.adjoin R ↑s
⊢ (PolynomialMap.φ R s).toRingHom (X n) ∈ ↑s

State before:
case a.intro.h_X.a
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
p : MvPolynomial (Fin s.card) R
n : Fin s.card
hp : (PolynomialMap.φ R s).toRingHom p ∈ Algebra.adjoin R ↑s
⊢ (PolynomialMap.φ R s).toRingHom (X n) ∈ ↑s
Tactic:
simp [φ]
State after:
no goals

State before:
case a
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
⊢ Algebra.adjoin R ↑s ≤ (PolynomialMap.φ R s).range
Tactic:
rw [Algebra.adjoin_le_iff]
State after:
case a
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
⊢ ↑s ⊆ ↑(PolynomialMap.φ R s).range

State before:
case a
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
⊢ ↑s ⊆ ↑(PolynomialMap.φ R s).range
Tactic:
intro x
State after:
case a
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
x : S
⊢ x ∈ ↑s → x ∈ ↑(PolynomialMap.φ R s).range

State before:
case a
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
x : S
⊢ x ∈ ↑s → x ∈ ↑(PolynomialMap.φ R s).range
Tactic:
simp only [Finset.mem_coe, φ, coe_range, Set.mem_range]
State after:
case a
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
x : S
⊢ x ∈ s → ∃ y, (aeval fun n => ↑(s.equivFin.symm n)) y = x

State before:
case a
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
x : S
⊢ x ∈ s → ∃ y, (aeval fun n => ↑(s.equivFin.symm n)) y = x
Tactic:
intro hx
State after:
case a
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
x : S
hx : x ∈ s
⊢ ∃ y, (aeval fun n => ↑(s.equivFin.symm n)) y = x

State before:
case a
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
x : S
hx : x ∈ s
⊢ ∃ y, (aeval fun n => ↑(s.equivFin.symm n)) y = x
Tactic:
use X (s.equivFin ⟨x, hx⟩)
State after:
case h
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
x : S
hx : x ∈ s
⊢ (aeval fun n => ↑(s.equivFin.symm n)) (X (s.equivFin ⟨x, hx⟩)) = x

State before:
case h
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : Finset S
x : S
hx : x ∈ s
⊢ (aeval fun n => ↑(s.equivFin.symm n)) (X (s.equivFin ⟨x, hx⟩)) = x
Tactic:
simp only [aeval_X, Equiv.symm_apply_apply]
State after:
no goals