internlm/Lean-Github huggingface dataset:
Theorem: AlgHom.quotientKerEquivRange_mk
Proof state before:
case H.a
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
s : S
⊢ ↑(((↑(Ideal.quotientKerEquivRange φ)).comp (Ideal.Quotient.mkₐ R (RingHom.ker φ))) s) = ↑(φ.rangeRestrict s)
Tactic:
simp only [AlgEquiv.toAlgHom_eq_coe, coe_comp, AlgHom.coe_coe,
  Ideal.Quotient.mkₐ_eq_mk, Function.comp_apply, coe_codRestrict]
Proof state after:
case H.a
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
s : S
⊢ ↑((Ideal.quotientKerEquivRange φ) ((Ideal.Quotient.mk (RingHom.ker φ)) s)) = φ s
Theorem: AlgHom.quotientKerEquivRange_mk
Proof state before:
case H.a
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
s : S
⊢ ↑((Ideal.quotientKerEquivRange φ) ((Ideal.Quotient.mk (RingHom.ker φ)) s)) = φ s
Tactic:
rfl
Proof state after:
no goals
Theorem: Ideal.kerLiftAlg_eq_val_comp_Equiv
Proof state before:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
⊢ kerLiftAlg φ = φ.range.val.comp ↑(quotientKerEquivRange φ)
Tactic:
apply Ideal.Quotient.algHom_ext
Proof state after:
case h
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
⊢ (kerLiftAlg φ).comp (Quotient.mkₐ R (RingHom.ker φ)) =
    (φ.range.val.comp ↑(quotientKerEquivRange φ)).comp (Quotient.mkₐ R (RingHom.ker φ))
Theorem: Ideal.kerLiftAlg_eq_val_comp_Equiv
Proof state before:
case h
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
⊢ (kerLiftAlg φ).comp (Quotient.mkₐ R (RingHom.ker φ)) =
    (φ.range.val.comp ↑(quotientKerEquivRange φ)).comp (Quotient.mkₐ R (RingHom.ker φ))
Tactic:
ext s
Proof state after:
case h.H
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
s : S
⊢ ((kerLiftAlg φ).comp (Quotient.mkₐ R (RingHom.ker φ))) s =
    ((φ.range.val.comp ↑(quotientKerEquivRange φ)).comp (Quotient.mkₐ R (RingHom.ker φ))) s
Theorem: Ideal.kerLiftAlg_eq_val_comp_Equiv
Proof state before:
case h.H
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
s : S
⊢ ((kerLiftAlg φ).comp (Quotient.mkₐ R (RingHom.ker φ))) s =
    ((φ.range.val.comp ↑(quotientKerEquivRange φ)).comp (Quotient.mkₐ R (RingHom.ker φ))) s
Tactic:
simp only [AlgHom.coe_comp, Quotient.mkₐ_eq_mk, Function.comp_apply, kerLiftAlg_mk,
  AlgEquiv.toAlgHom_eq_coe, Subalgebra.coe_val, AlgHom.coe_coe]
Proof state after:
case h.H
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
s : S
⊢ φ s = ↑((quotientKerEquivRange φ) ((Quotient.mk (RingHom.ker φ)) s))
Theorem: Ideal.kerLiftAlg_eq_val_comp_Equiv
Proof state before:
case h.H
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
s : S
⊢ φ s = ↑((quotientKerEquivRange φ) ((Quotient.mk (RingHom.ker φ)) s))
Tactic:
rfl
Proof state after:
no goals
Theorem: MvPolynomial.aeval_range
Proof 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
Proof 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
Theorem: MvPolynomial.aeval_range
Proof 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⟩
Proof 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)
Theorem: MvPolynomial.aeval_range
Proof 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]
Proof 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)
Theorem: MvPolynomial.aeval_range
Proof 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
Proof state after:
no goals
Theorem: MvPolynomial.aeval_range
Proof 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]
Proof 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)
Theorem: MvPolynomial.aeval_range
Proof 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
Proof 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
Theorem: MvPolynomial.aeval_range
Proof 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
Proof 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)
Theorem: MvPolynomial.aeval_range
Proof 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
Proof state after:
no goals
Theorem: MvPolynomial.aeval_range
Proof 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]
Proof 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)
Theorem: MvPolynomial.aeval_range
Proof 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
Proof state after:
no goals
Theorem: MvPolynomial.aeval_range
Proof 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]
Proof 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)
Theorem: MvPolynomial.aeval_range
Proof 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
Proof 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)
Theorem: MvPolynomial.aeval_range
Proof 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
Proof 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
Theorem: MvPolynomial.aeval_range
Proof 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
Proof state after:
no goals
Theorem: MvPolynomial.aeval_range
Proof 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]
Proof 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
Theorem: MvPolynomial.aeval_range
Proof 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⟩
Proof 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
Theorem: MvPolynomial.aeval_range
Proof 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
Proof 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
Theorem: MvPolynomial.aeval_range
Proof 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]
Proof state after:
no goals
Theorem: TensorProduct.includeRight_lid
Proof state before:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : R ⊗[R] M
⊢ 1 ⊗ₜ[R] (TensorProduct.lid R M) m = (rTensor M (algebraMap' R S).toLinearMap) m
Tactic:
suffices ∀ m, (rTensor M (algebraMap' R S).toLinearMap).comp
  (TensorProduct.lid R M).symm.toLinearMap m = 1 ⊗ₜ[R] m by
  simp only [← this, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    LinearEquiv.symm_apply_apply]
Proof state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : R ⊗[R] M
⊢ ∀ (m : M), (rTensor M (algebraMap' R S).toLinearMap ∘ₗ ↑(TensorProduct.lid R M).symm) m = 1 ⊗ₜ[R] m
Theorem: TensorProduct.includeRight_lid
Proof state before:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : R ⊗[R] M
⊢ ∀ (m : M), (rTensor M (algebraMap' R S).toLinearMap ∘ₗ ↑(TensorProduct.lid R M).symm) m = 1 ⊗ₜ[R] m
Tactic:
intro z
Proof state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : R ⊗[R] M
z : M
⊢ (rTensor M (algebraMap' R S).toLinearMap ∘ₗ ↑(TensorProduct.lid R M).symm) z = 1 ⊗ₜ[R] z
Theorem: TensorProduct.includeRight_lid
Proof state before:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : R ⊗[R] M
z : M
⊢ (rTensor M (algebraMap' R S).toLinearMap ∘ₗ ↑(TensorProduct.lid R M).symm) z = 1 ⊗ₜ[R] z
Tactic:
simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, lid_symm_apply, rTensor_tmul,
  AlgHom.toLinearMap_apply, _root_.map_one]
Proof state after:
no goals
Theorem: TensorProduct.includeRight_lid
Proof state before:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : R ⊗[R] M
this : ∀ (m : M), (rTensor M (algebraMap' R S).toLinearMap ∘ₗ ↑(TensorProduct.lid R M).symm) m = 1 ⊗ₜ[R] m
⊢ 1 ⊗ₜ[R] (TensorProduct.lid R M) m = (rTensor M (algebraMap' R S).toLinearMap) m
Tactic:
simp only [← this, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
  LinearEquiv.symm_apply_apply]
Proof state after:
no goals
Theorem: PolynomialMap.isCompat_apply'
Proof 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 : M →ₚ[R] N
S : Type u
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
x : S ⊗[R] M
⊢ (LinearMap.rTensor N φ.toLinearMap) (f.toFun' S x) = f.toFun' S' ((LinearMap.rTensor M φ.toLinearMap) x)
Tactic:
simpa only using _root_.congr_fun (f.isCompat' φ) x
Proof state after:
no goals
Theorem: PolynomialMap.φ_range
Proof 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
Proof 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
Theorem: PolynomialMap.φ_range
Proof 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⟩
Proof 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
Theorem: PolynomialMap.φ_range
Proof 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 [φ]
Proof state after:
no goals
Theorem: PolynomialMap.φ_range
Proof 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]
Proof state after:
no goals
Theorem: PolynomialMap.φ_range
Proof 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]
Proof state after:
no goals
Theorem: PolynomialMap.φ_range
Proof 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]
Proof 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
Theorem: PolynomialMap.φ_range
Proof 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
Proof 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
Theorem: PolynomialMap.φ_range
Proof 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
Proof 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
Theorem: PolynomialMap.φ_range
Proof 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 [φ]
Proof state after:
no goals
Theorem: PolynomialMap.φ_range
Proof 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]
Proof 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
Theorem: PolynomialMap.φ_range
Proof 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
Proof 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