-
Notifications
You must be signed in to change notification settings - Fork 307
/
Tower.lean
92 lines (63 loc) · 2.85 KB
/
Tower.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
/-
Copyright (c) 2020 Kenny Lau. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kenny Lau, Yuyang Zhao
-/
import Mathlib.Algebra.Algebra.Tower
import Mathlib.Data.Polynomial.AlgebraMap
#align_import ring_theory.polynomial.tower from "leanprover-community/mathlib"@"bb168510ef455e9280a152e7f31673cabd3d7496"
/-!
# Algebra towers for polynomial
This file proves some basic results about the algebra tower structure for the type `R[X]`.
This structure itself is provided elsewhere as `Polynomial.isScalarTower`
When you update this file, you can also try to make a corresponding update in
`RingTheory.MvPolynomial.Tower`.
-/
open Polynomial
variable (R A B : Type*)
namespace Polynomial
section Semiring
variable [CommSemiring R] [CommSemiring A] [Semiring B]
variable [Algebra R A] [Algebra A B] [Algebra R B]
variable [IsScalarTower R A B]
variable {R B}
@[simp]
theorem aeval_map_algebraMap (x : B) (p : R[X]) : aeval x (map (algebraMap R A) p) = aeval x p := by
rw [aeval_def, aeval_def, eval₂_map, IsScalarTower.algebraMap_eq R A B]
#align polynomial.aeval_map_algebra_map Polynomial.aeval_map_algebraMap
@[simp]
lemma eval_map_algebraMap (P : R[X]) (a : A) :
(map (algebraMap R A) P).eval a = aeval a P := by
rw [← aeval_map_algebraMap (A := A), coe_aeval_eq_eval]
end Semiring
section CommSemiring
variable [CommSemiring R] [CommSemiring A] [Semiring B]
variable [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B]
variable {R A}
theorem aeval_algebraMap_apply (x : A) (p : R[X]) :
aeval (algebraMap A B x) p = algebraMap A B (aeval x p) := by
rw [aeval_def, aeval_def, hom_eval₂, ← IsScalarTower.algebraMap_eq]
#align polynomial.aeval_algebra_map_apply Polynomial.aeval_algebraMap_apply
@[simp]
theorem aeval_algebraMap_eq_zero_iff [NoZeroSMulDivisors A B] [Nontrivial B] (x : A) (p : R[X]) :
aeval (algebraMap A B x) p = 0 ↔ aeval x p = 0 := by
rw [aeval_algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_eq_zero,
iff_false_intro (one_ne_zero' B), or_false_iff]
#align polynomial.aeval_algebra_map_eq_zero_iff Polynomial.aeval_algebraMap_eq_zero_iff
variable {B}
theorem aeval_algebraMap_eq_zero_iff_of_injective {x : A} {p : R[X]}
(h : Function.Injective (algebraMap A B)) : aeval (algebraMap A B x) p = 0 ↔ aeval x p = 0 := by
rw [aeval_algebraMap_apply, ← (algebraMap A B).map_zero, h.eq_iff]
#align polynomial.aeval_algebra_map_eq_zero_iff_of_injective Polynomial.aeval_algebraMap_eq_zero_iff_of_injective
end CommSemiring
end Polynomial
namespace Subalgebra
open Polynomial
section CommSemiring
variable {R A} [CommSemiring R] [CommSemiring A] [Algebra R A]
@[simp]
theorem aeval_coe (S : Subalgebra R A) (x : S) (p : R[X]) : aeval (x : A) p = aeval x p :=
aeval_algebraMap_apply A x p
#align subalgebra.aeval_coe Subalgebra.aeval_coe
end CommSemiring
end Subalgebra