Theorem: DividedPowerAlgebra.dpScalarExtensionInv_unique (DividedPowers/DPAlgebra/BaseChange.lean)

State before:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
⊢ φ = dpScalarExtensionInv R S M
Tactic:
apply AlgHom.ext
State after:
case H
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
⊢ ∀ (x : DividedPowerAlgebra S (S ⊗[R] M)), φ x = (dpScalarExtensionInv R S M) x

State before:
case H
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
⊢ ∀ (x : DividedPowerAlgebra S (S ⊗[R] M)), φ x = (dpScalarExtensionInv R S M) x
Tactic:
intro x
State after:
case H
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
x : DividedPowerAlgebra S (S ⊗[R] M)
⊢ φ x = (dpScalarExtensionInv R S M) x

State before:
case H.h_C
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
a : S
⊢ φ (mk (MvPolynomial.C a)) = (dpScalarExtensionInv R S M) (mk (MvPolynomial.C a))
Tactic:
rw [mk_C, Algebra.algebraMap_eq_smul_one, map_smul, _root_.map_one, map_smul, _root_.map_one]
State after:
no goals

State before:
case H.h_add
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f g : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
hg : φ g = (dpScalarExtensionInv R S M) g
⊢ φ (f + g) = (dpScalarExtensionInv R S M) (f + g)
Tactic:
simp only [map_add, hf, hg]
State after:
no goals

State before:
case H.h_dp
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
n : ℕ
sm : S ⊗[R] M
hf : φ f = (dpScalarExtensionInv R S M) f
⊢ φ (f * dp S n sm) = (dpScalarExtensionInv R S M) (f * dp S n sm)
Tactic:
suffices h_eq : φ (dp S n sm) = (dpScalarExtensionInv R S M) (dp S n sm) by
  rw [_root_.map_mul, _root_.map_mul, hf, h_eq]
State after:
case H.h_dp
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
n : ℕ
sm : S ⊗[R] M
hf : φ f = (dpScalarExtensionInv R S M) f
⊢ φ (dp S n sm) = (dpScalarExtensionInv R S M) (dp S n sm)

State before:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
n : ℕ
sm : S ⊗[R] M
hf : φ f = (dpScalarExtensionInv R S M) f
h_eq : φ (dp S n sm) = (dpScalarExtensionInv R S M) (dp S n sm)
⊢ φ (f * dp S n sm) = (dpScalarExtensionInv R S M) (f * dp S n sm)
Tactic:
rw [_root_.map_mul, _root_.map_mul, hf, h_eq]
State after:
no goals

State before:
case H.h_dp.zero
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
n : ℕ
⊢ φ (dp S n 0) = (dpScalarExtensionInv R S M) (dp S n 0)
Tactic:
rw [dp_null]
State after:
case H.h_dp.zero
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
n : ℕ
⊢ φ (if n = 0 then 1 else 0) = (dpScalarExtensionInv R S M) (if n = 0 then 1 else 0)

State before:
case H.h_dp.zero
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
n : ℕ
⊢ φ (if n = 0 then 1 else 0) = (dpScalarExtensionInv R S M) (if n = 0 then 1 else 0)
Tactic:
split_ifs
State after:
case pos
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
n : ℕ
h✝ : n = 0
⊢ φ 1 = (dpScalarExtensionInv R S M) 1

case neg
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
n : ℕ
h✝ : ¬n = 0
⊢ φ 0 = (dpScalarExtensionInv R S M) 0

State before:
case pos
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
n : ℕ
h✝ : n = 0
⊢ φ 1 = (dpScalarExtensionInv R S M) 1
Tactic:
simp only [_root_.map_one]
State after:
no goals

State before:
case neg
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
n : ℕ
h✝ : ¬n = 0
⊢ φ 0 = (dpScalarExtensionInv R S M) 0
Tactic:
simp only [_root_.map_zero]
State after:
no goals

State before:
case H.h_dp.tmul
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
s : S
m : M
n : ℕ
⊢ φ (dp S n (s ⊗ₜ[R] m)) = (dpScalarExtensionInv R S M) (dp S n (s ⊗ₜ[R] m))
Tactic:
rw [hφ, dpScalarExtensionInv_apply_dp]
State after:
no goals

State before:
case H.h_dp.add
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
x y : S ⊗[R] M
hx : ∀ (n : ℕ), φ (dp S n x) = (dpScalarExtensionInv R S M) (dp S n x)
hy : ∀ (n : ℕ), φ (dp S n y) = (dpScalarExtensionInv R S M) (dp S n y)
n : ℕ
⊢ φ (dp S n (x + y)) = (dpScalarExtensionInv R S M) (dp S n (x + y))
Tactic:
simp only [dp_add, map_sum, _root_.map_mul]
State after:
case H.h_dp.add
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
x y : S ⊗[R] M
hx : ∀ (n : ℕ), φ (dp S n x) = (dpScalarExtensionInv R S M) (dp S n x)
hy : ∀ (n : ℕ), φ (dp S n y) = (dpScalarExtensionInv R S M) (dp S n y)
n : ℕ
⊢ ∑ x_1 ∈ Finset.antidiagonal n, φ (dp S x_1.1 x) * φ (dp S x_1.2 y) =
    ∑ x_1 ∈ Finset.antidiagonal n,
      (dpScalarExtensionInv R S M) (dp S x_1.1 x) * (dpScalarExtensionInv R S M) (dp S x_1.2 y)

State before:
case H.h_dp.add
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
x y : S ⊗[R] M
hx : ∀ (n : ℕ), φ (dp S n x) = (dpScalarExtensionInv R S M) (dp S n x)
hy : ∀ (n : ℕ), φ (dp S n y) = (dpScalarExtensionInv R S M) (dp S n y)
n : ℕ
⊢ ∑ x_1 ∈ Finset.antidiagonal n, φ (dp S x_1.1 x) * φ (dp S x_1.2 y) =
    ∑ x_1 ∈ Finset.antidiagonal n,
      (dpScalarExtensionInv R S M) (dp S x_1.1 x) * (dpScalarExtensionInv R S M) (dp S x_1.2 y)
Tactic:
apply Finset.sum_congr rfl
State after:
case H.h_dp.add
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
x y : S ⊗[R] M
hx : ∀ (n : ℕ), φ (dp S n x) = (dpScalarExtensionInv R S M) (dp S n x)
hy : ∀ (n : ℕ), φ (dp S n y) = (dpScalarExtensionInv R S M) (dp S n y)
n : ℕ
⊢ ∀ x_1 ∈ Finset.antidiagonal n,
    φ (dp S x_1.1 x) * φ (dp S x_1.2 y) =
      (dpScalarExtensionInv R S M) (dp S x_1.1 x) * (dpScalarExtensionInv R S M) (dp S x_1.2 y)

State before:
case H.h_dp.add
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
x y : S ⊗[R] M
hx : ∀ (n : ℕ), φ (dp S n x) = (dpScalarExtensionInv R S M) (dp S n x)
hy : ∀ (n : ℕ), φ (dp S n y) = (dpScalarExtensionInv R S M) (dp S n y)
n : ℕ
⊢ ∀ x_1 ∈ Finset.antidiagonal n,
    φ (dp S x_1.1 x) * φ (dp S x_1.2 y) =
      (dpScalarExtensionInv R S M) (dp S x_1.1 x) * (dpScalarExtensionInv R S M) (dp S x_1.2 y)
Tactic:
intro nn _hnn
State after:
case H.h_dp.add
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
x y : S ⊗[R] M
hx : ∀ (n : ℕ), φ (dp S n x) = (dpScalarExtensionInv R S M) (dp S n x)
hy : ∀ (n : ℕ), φ (dp S n y) = (dpScalarExtensionInv R S M) (dp S n y)
n : ℕ
nn : ℕ × ℕ
_hnn : nn ∈ Finset.antidiagonal n
⊢ φ (dp S nn.1 x) * φ (dp S nn.2 y) =
    (dpScalarExtensionInv R S M) (dp S nn.1 x) * (dpScalarExtensionInv R S M) (dp S nn.2 y)

State before:
case H.h_dp.add
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
x y : S ⊗[R] M
hx : ∀ (n : ℕ), φ (dp S n x) = (dpScalarExtensionInv R S M) (dp S n x)
hy : ∀ (n : ℕ), φ (dp S n y) = (dpScalarExtensionInv R S M) (dp S n y)
n : ℕ
nn : ℕ × ℕ
_hnn : nn ∈ Finset.antidiagonal n
⊢ φ (dp S nn.1 x) * φ (dp S nn.2 y) =
    (dpScalarExtensionInv R S M) (dp S nn.1 x) * (dpScalarExtensionInv R S M) (dp S nn.2 y)
Tactic:
rw [hx nn.1, hy nn.2]
State after:
no goals