R : Type u
S : Type ?u.741072
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
⊢ LinearMap.ker (↑(aeval f) (p * q)) ≤ LinearMap.ker (↑(aeval f) p) ⊔ LinearMap.ker (↑(aeval f) q)
R : Type u
S : Type ?u.741072
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
⊢ LinearMap.ker (↑(aeval f) p) ⊔ LinearMap.ker (↑(aeval f) q) = LinearMap.ker (↑(aeval f) (p * q))
apply le_antisymm sup_ker_aeval_le_ker_aeval_mul
R : Type u
S : Type ?u.741072
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
v : M
hv : v ∈ LinearMap.ker (↑(aeval f) (p * q))
⊢ v ∈ LinearMap.ker (↑(aeval f) p) ⊔ LinearMap.ker (↑(aeval f) q)
R : Type u
S : Type ?u.741072
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
⊢ LinearMap.ker (↑(aeval f) (p * q)) ≤ LinearMap.ker (↑(aeval f) p) ⊔ LinearMap.ker (↑(aeval f) q)
intro v hv
R : Type u
S : Type ?u.741072
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
v : M
hv : v ∈ LinearMap.ker (↑(aeval f) (p * q))
⊢ ∃ y, y ∈ LinearMap.ker (↑(aeval f) p) ∧ ∃ z, z ∈ LinearMap.ker (↑(aeval f) q) ∧ y + z = v
R : Type u
S : Type ?u.741072
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
v : M
hv : v ∈ LinearMap.ker (↑(aeval f) (p * q))
⊢ v ∈ LinearMap.ker (↑(aeval f) p) ⊔ LinearMap.ker (↑(aeval f) q)
rw [Submodule.mem_sup]
case intro.intro
R : Type u
S : Type ?u.741072
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker (↑(aeval f) (p * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ∃ y, y ∈ LinearMap.ker (↑(aeval f) p) ∧ ∃ z, z ∈ LinearMap.ker (↑(aeval f) q) ∧ y + z = v
R : Type u
S : Type ?u.741072
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
v : M
hv : v ∈ LinearMap.ker (↑(aeval f) (p * q))
⊢ ∃ y, y ∈ LinearMap.ker (↑(aeval f) p) ∧ ∃ z, z ∈ LinearMap.ker (↑(aeval f) q) ∧ y + z = v
rcases hpq with ⟨p', q', hpq'⟩
case intro.intro
R : Type u
S : Type ?u.741072
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker (↑(aeval f) (p * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ↑(↑(aeval f) (q * (p * p'))) v = 0
⊢ ∃ y, y ∈ LinearMap.ker (↑(aeval f) p) ∧ ∃ z, z ∈ LinearMap.ker (↑(aeval f) q) ∧ y + z = v
case intro.intro
R : Type u
S : Type ?u.741072
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker (↑(aeval f) (p * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ∃ y, y ∈ LinearMap.ker (↑(aeval f) p) ∧ ∃ z, z ∈ LinearMap.ker (↑(aeval f) q) ∧ y + z = v
have h_eval₂_qpp' :=
  calc
    aeval f (q * (p * p')) v = aeval f (p' * (p * q)) v := by
      rw [mul_comm, mul_assoc, mul_comm, mul_assoc, mul_comm q p]
    _ = 0 := by rw [aeval_mul, LinearMap.mul_apply, LinearMap.mem_ker.1 hv, LinearMap.map_zero]
case intro.intro
R : Type u
S : Type ?u.741072
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker (↑(aeval f) (p * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ↑(↑(aeval f) (q * (p * p'))) v = 0
h_eval₂_pqq' : ↑(↑(aeval f) (p * (q * q'))) v = 0
⊢ ∃ y, y ∈ LinearMap.ker (↑(aeval f) p) ∧ ∃ z, z ∈ LinearMap.ker (↑(aeval f) q) ∧ y + z = v
case intro.intro
R : Type u
S : Type ?u.741072
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker (↑(aeval f) (p * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ↑(↑(aeval f) (q * (p * p'))) v = 0
⊢ ∃ y, y ∈ LinearMap.ker (↑(aeval f) p) ∧ ∃ z, z ∈ LinearMap.ker (↑(aeval f) q) ∧ y + z = v
have h_eval₂_pqq' :=
  calc
    aeval f (p * (q * q')) v = aeval f (q' * (p * q)) v := by rw [← mul_assoc, mul_comm]
    _ = 0 := by rw [aeval_mul, LinearMap.mul_apply, LinearMap.mem_ker.1 hv, LinearMap.map_zero]
case intro.intro
R : Type u
S : Type ?u.741072
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker (↑(aeval f) (p * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ↑(↑(aeval f) q * ↑(aeval f) (p * p')) v = 0
h_eval₂_pqq' : ↑(↑(aeval f) p * ↑(aeval f) (q * q')) v = 0
⊢ ∃ y, y ∈ LinearMap.ker (↑(aeval f) p) ∧ ∃ z, z ∈ LinearMap.ker (↑(aeval f) q) ∧ y + z = v
case intro.intro
R : Type u
S : Type ?u.741072
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker (↑(aeval f) (p * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ↑(↑(aeval f) (q * (p * p'))) v = 0
h_eval₂_pqq' : ↑(↑(aeval f) (p * (q * q'))) v = 0
⊢ ∃ y, y ∈ LinearMap.ker (↑(aeval f) p) ∧ ∃ z, z ∈ LinearMap.ker (↑(aeval f) q) ∧ y + z = v
rw [aeval_mul] at h_eval₂_qpp' h_eval₂_pqq'
case intro.intro
R : Type u
S : Type ?u.741072
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker (↑(aeval f) (p * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ↑(↑(aeval f) q * ↑(aeval f) (p * p')) v = 0
h_eval₂_pqq' : ↑(↑(aeval f) p * ↑(aeval f) (q * q')) v = 0
⊢ ↑(↑(aeval f) (q * q')) v + ↑(↑(aeval f) (p * p')) v = v
case intro.intro
R : Type u
S : Type ?u.741072
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker (↑(aeval f) (p * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ↑(↑(aeval f) q * ↑(aeval f) (p * p')) v = 0
h_eval₂_pqq' : ↑(↑(aeval f) p * ↑(aeval f) (q * q')) v = 0
⊢ ∃ y, y ∈ LinearMap.ker (↑(aeval f) p) ∧ ∃ z, z ∈ LinearMap.ker (↑(aeval f) q) ∧ y + z = v
refine'
  ⟨aeval f (q * q') v, LinearMap.mem_ker.1 h_eval₂_pqq', aeval f (p * p') v,
    LinearMap.mem_ker.1 h_eval₂_qpp', _⟩
case intro.intro
R : Type u
S : Type ?u.741072
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker (↑(aeval f) (p * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ↑(↑(aeval f) q * ↑(aeval f) (p * p')) v = 0
h_eval₂_pqq' : ↑(↑(aeval f) p * ↑(aeval f) (q * q')) v = 0
⊢ ↑(↑(aeval f) (p' * p)) v + ↑(↑(aeval f) (q' * q)) v = v
case intro.intro
R : Type u
S : Type ?u.741072
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker (↑(aeval f) (p * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ↑(↑(aeval f) q * ↑(aeval f) (p * p')) v = 0
h_eval₂_pqq' : ↑(↑(aeval f) p * ↑(aeval f) (q * q')) v = 0
⊢ ↑(↑(aeval f) (q * q')) v + ↑(↑(aeval f) (p * p')) v = v
rw [add_comm, mul_comm p p', mul_comm q q']
no goals
case intro.intro
R : Type u
S : Type ?u.741072
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker (↑(aeval f) (p * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ↑(↑(aeval f) q * ↑(aeval f) (p * p')) v = 0
h_eval₂_pqq' : ↑(↑(aeval f) p * ↑(aeval f) (q * q')) v = 0
⊢ ↑(↑(aeval f) (p' * p)) v + ↑(↑(aeval f) (q' * q)) v = v
simpa only [map_add, map_mul, aeval_one] using congr_arg (fun p : R[X] => aeval f p v) hpq'
no goals
R : Type u
S : Type ?u.741072
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker (↑(aeval f) (p * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ↑(↑(aeval f) (q * (p * p'))) v = ↑(↑(aeval f) (p' * (p * q))) v
rw [mul_comm, mul_assoc, mul_comm, mul_assoc, mul_comm q p]
no goals
R : Type u
S : Type ?u.741072
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker (↑(aeval f) (p * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ↑(↑(aeval f) (p' * (p * q))) v = 0
rw [aeval_mul, LinearMap.mul_apply, LinearMap.mem_ker.1 hv, LinearMap.map_zero]
no goals
R : Type u
S : Type ?u.741072
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker (↑(aeval f) (p * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ↑(↑(aeval f) (q * (p * p'))) v = 0
⊢ ↑(↑(aeval f) (p * (q * q'))) v = ↑(↑(aeval f) (q' * (p * q))) v
rw [← mul_assoc, mul_comm]
no goals
R : Type u
S : Type ?u.741072
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker (↑(aeval f) (p * q))
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ↑(↑(aeval f) (q * (p * p'))) v = 0
⊢ ↑(↑(aeval f) (q' * (p * q))) v = 0
rw [aeval_mul, LinearMap.mul_apply, LinearMap.mem_ker.1 hv, LinearMap.map_zero]