internlm/Lean-Github huggingface dataset:
Theorem: PowerSeries.isExponential_map
Proof state before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
φ : R →+* S
f : R⟦X⟧
hf : f.IsExponential
⊢ (constantCoeff S) ((map φ) f) = 1 ∧
    ∀ (p q : ℕ), ↑((p + q).choose p) * (coeff S (p + q)) ((map φ) f) = (coeff S p) ((map φ) f) * (coeff S q) ((map φ) f)
Tactic:
constructor
Proof state after:
case left
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
φ : R →+* S
f : R⟦X⟧
hf : f.IsExponential
⊢ (constantCoeff S) ((map φ) f) = 1

case right
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
φ : R →+* S
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (p q : ℕ), ↑((p + q).choose p) * (coeff S (p + q)) ((map φ) f) = (coeff S p) ((map φ) f) * (coeff S q) ((map φ) f)
Theorem: PowerSeries.isExponential_map
Proof state before:
case left
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
φ : R →+* S
f : R⟦X⟧
hf : f.IsExponential
⊢ (constantCoeff S) ((map φ) f) = 1
Tactic:
rw [← coeff_zero_eq_constantCoeff_apply, coeff_map,
  coeff_zero_eq_constantCoeff, hf.constantCoeff, map_one]
Proof state after:
no goals
Theorem: PowerSeries.isExponential_map
Proof state before:
case right
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
φ : R →+* S
f : R⟦X⟧
hf : f.IsExponential
⊢ ∀ (p q : ℕ), ↑((p + q).choose p) * (coeff S (p + q)) ((map φ) f) = (coeff S p) ((map φ) f) * (coeff S q) ((map φ) f)
Tactic:
intro p q
Proof state after:
case right
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
φ : R →+* S
f : R⟦X⟧
hf : f.IsExponential
p q : ℕ
⊢ ↑((p + q).choose p) * (coeff S (p + q)) ((map φ) f) = (coeff S p) ((map φ) f) * (coeff S q) ((map φ) f)
Theorem: PowerSeries.isExponential_map
Proof state before:
case right
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
φ : R →+* S
f : R⟦X⟧
hf : f.IsExponential
p q : ℕ
⊢ ↑((p + q).choose p) * (coeff S (p + q)) ((map φ) f) = (coeff S p) ((map φ) f) * (coeff S q) ((map φ) f)
Tactic:
simp only [coeff_map, ← map_mul, ← ((isExponential_iff f).mp hf).2 p q]
Proof state after:
case right
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
φ : R →+* S
f : R⟦X⟧
hf : f.IsExponential
p q : ℕ
⊢ ↑((p + q).choose p) * φ ((coeff R (p + q)) f) = φ (↑((p + q).choose p) * (coeff R (p + q)) f)
Theorem: PowerSeries.isExponential_map
Proof state before:
case right
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
φ : R →+* S
f : R⟦X⟧
hf : f.IsExponential
p q : ℕ
⊢ ↑((p + q).choose p) * φ ((coeff R (p + q)) f) = φ (↑((p + q).choose p) * (coeff R (p + q)) f)
Tactic:
simp only [map_mul, map_natCast]
Proof state after:
no goals
Theorem: ExponentialModule.coe_injective
Proof state before:
A✝ : Type u_1
R✝ : Type u_2
inst✝⁵ : CommRing A✝
inst✝⁴ : CommRing R✝
inst✝³ : Algebra A✝ R✝
A : Type u_3
R : Type u_4
inst✝² : CommRing A
inst✝¹ : CommRing R
inst✝ : Algebra A R
f g : ↥(ExponentialModule R)
⊢ ↑f = ↑g → f = g
Tactic:
simp only [toPowerSeries, EmbeddingLike.apply_eq_iff_eq, SetLike.coe_eq_coe, imp_self]
Proof state after:
no goals
Theorem: ExponentialModule.coe_add
Proof state before:
A✝ : Type u_1
R✝ : Type u_2
inst✝⁵ : CommRing A✝
inst✝⁴ : CommRing R✝
inst✝³ : Algebra A✝ R✝
A : Type u_3
R : Type u_4
inst✝² : CommRing A
inst✝¹ : CommRing R
inst✝ : Algebra A R
f g : ↥(ExponentialModule R)
⊢ ↑(f + g) = ↑f * ↑g
Tactic:
simp only [toPowerSeries, AddSubmonoid.coe_add, toMul_add]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.gamma_toFun
Proof state before:
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S ⊗[R] M
⊢ (gamma R M n).toFun S m = (dpScalarExtensionEquiv R S M).symm (dp S n m)
Tactic:
obtain ⟨k, ψ, p, rfl⟩ := PolynomialMap.exists_lift m
Proof state after:
case intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
ψ : MvPolynomial (Fin k) R →ₐ[R] S
p : MvPolynomial (Fin k) R ⊗[R] M
⊢ (gamma R M n).toFun S ((LinearMap.rTensor M ψ.toLinearMap) p) =
    (dpScalarExtensionEquiv R S M).symm (dp S n ((LinearMap.rTensor M ψ.toLinearMap) p))
Theorem: DividedPowerAlgebra.gamma_toFun
Proof state before:
case intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
ψ : MvPolynomial (Fin k) R →ₐ[R] S
p : MvPolynomial (Fin k) R ⊗[R] M
⊢ (gamma R M n).toFun S ((LinearMap.rTensor M ψ.toLinearMap) p) =
    (dpScalarExtensionEquiv R S M).symm (dp S n ((LinearMap.rTensor M ψ.toLinearMap) p))
Tactic:
rw [← (gamma R M n).isCompat_apply, PolynomialMap.toFun_eq_toFun']
Proof state after:
case intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
ψ : MvPolynomial (Fin k) R →ₐ[R] S
p : MvPolynomial (Fin k) R ⊗[R] M
⊢ (LinearMap.rTensor (DividedPowerAlgebra R M) ψ.toLinearMap) ((gamma R M n).toFun' (MvPolynomial (Fin k) R) p) =
    (dpScalarExtensionEquiv R S M).symm (dp S n ((LinearMap.rTensor M ψ.toLinearMap) p))
Theorem: DividedPowerAlgebra.gamma_toFun
Proof state before:
case intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
ψ : MvPolynomial (Fin k) R →ₐ[R] S
p : MvPolynomial (Fin k) R ⊗[R] M
⊢ (LinearMap.rTensor (DividedPowerAlgebra R M) ψ.toLinearMap) ((gamma R M n).toFun' (MvPolynomial (Fin k) R) p) =
    (dpScalarExtensionEquiv R S M).symm (dp S n ((LinearMap.rTensor M ψ.toLinearMap) p))
Tactic:
simp only [gamma, rTensor_comp_dpScalarExtensionEquiv_symm_eq]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.isHomogeneousOfDegree_gamma
Proof state before:
R : Type u
inst✝² : CommRing R
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
⊢ PolynomialMap.IsHomogeneousOfDegree n (gamma R M n)
Tactic:
intro S _ _ r sm
Proof state after:
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
sm : S ⊗[R] M
⊢ (gamma R M n).toFun' S (r • sm) = r ^ n • (gamma R M n).toFun' S sm
Theorem: DividedPowerAlgebra.isHomogeneousOfDegree_gamma
Proof state before:
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
sm : S ⊗[R] M
⊢ (gamma R M n).toFun' S (r • sm) = r ^ n • (gamma R M n).toFun' S sm
Tactic:
simp only [gamma]
Proof state after:
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
sm : S ⊗[R] M
⊢ (dpScalarExtensionEquiv R S M).symm (dp S n (r • sm)) = r ^ n • (dpScalarExtensionEquiv R S M).symm (dp S n sm)
Theorem: DividedPowerAlgebra.isHomogeneousOfDegree_gamma
Proof state before:
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
sm : S ⊗[R] M
⊢ (dpScalarExtensionEquiv R S M).symm (dp S n (r • sm)) = r ^ n • (dpScalarExtensionEquiv R S M).symm (dp S n sm)
Tactic:
apply (dpScalarExtensionEquiv R S M).injective
Proof state after:
case a
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
sm : S ⊗[R] M
⊢ (dpScalarExtensionEquiv R S M) ((dpScalarExtensionEquiv R S M).symm (dp S n (r • sm))) =
    (dpScalarExtensionEquiv R S M) (r ^ n • (dpScalarExtensionEquiv R S M).symm (dp S n sm))
Theorem: DividedPowerAlgebra.isHomogeneousOfDegree_gamma
Proof state before:
case a
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
sm : S ⊗[R] M
⊢ (dpScalarExtensionEquiv R S M) ((dpScalarExtensionEquiv R S M).symm (dp S n (r • sm))) =
    (dpScalarExtensionEquiv R S M) (r ^ n • (dpScalarExtensionEquiv R S M).symm (dp S n sm))
Tactic:
simp only [apply_symm_apply, LinearMapClass.map_smul]
Proof state after:
case a
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
sm : S ⊗[R] M
⊢ dp S n (r • sm) = r ^ n • dp S n sm
Theorem: DividedPowerAlgebra.isHomogeneousOfDegree_gamma
Proof state before:
case a
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
sm : S ⊗[R] M
⊢ dp S n (r • sm) = r ^ n • dp S n sm
Tactic:
rw [dp_smul]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case zero
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
⊢ (gamma R M n).toFun S 0 ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
simp only [gamma_toFun, dp_null]
Proof state after:
case zero
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
⊢ (dpScalarExtensionEquiv R S M).symm (if n = 0 then 1 else 0) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case zero
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
⊢ (dpScalarExtensionEquiv R S M).symm (if n = 0 then 1 else 0) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
split_ifs with h
Proof state after:
case pos
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
h : n = 0
⊢ (dpScalarExtensionEquiv R S M).symm 1 ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)

case neg
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
h : ¬n = 0
⊢ (dpScalarExtensionEquiv R S M).symm 0 ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case pos
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
h : n = 0
⊢ (dpScalarExtensionEquiv R S M).symm 1 ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
rw [AlgEquiv.map_one, h]
Proof state after:
case pos
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
h : n = 0
⊢ 1 ∈ LinearMap.range (LinearMap.lTensor S (grade R M 0).subtype)
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case pos
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
h : n = 0
⊢ 1 ∈ LinearMap.range (LinearMap.lTensor S (grade R M 0).subtype)
Tactic:
simp only [LinearMap.mem_range]
Proof state after:
case pos
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
h : n = 0
⊢ ∃ y, (LinearMap.lTensor S (grade R M 0).subtype) y = 1
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case pos
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
h : n = 0
⊢ ∃ y, (LinearMap.lTensor S (grade R M 0).subtype) y = 1
Tactic:
use (1 : S) ⊗ₜ[R] ⟨(1 : DividedPowerAlgebra R M), one_mem R M⟩
Proof state after:
case h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
h : n = 0
⊢ (LinearMap.lTensor S (grade R M 0).subtype) (1 ⊗ₜ[R] ⟨1, ⋯⟩) = 1
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
h : n = 0
⊢ (LinearMap.lTensor S (grade R M 0).subtype) (1 ⊗ₜ[R] ⟨1, ⋯⟩) = 1
Tactic:
simp only [LinearMap.lTensor_tmul, Submodule.coeSubtype]
Proof state after:
case h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
h : n = 0
⊢ 1 ⊗ₜ[R] 1 = 1
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
h : n = 0
⊢ 1 ⊗ₜ[R] 1 = 1
Tactic:
rw [Algebra.TensorProduct.one_def]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case neg
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
n : ℕ
h : ¬n = 0
⊢ (dpScalarExtensionEquiv R S M).symm 0 ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
simp only [map_zero, zero_mem]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case tmul
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
m : M
n : ℕ
⊢ (gamma R M n).toFun S (s ⊗ₜ[R] m) ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
simp only [gamma_toFun, dpScalarExtensionEquiv]
Proof state after:
case tmul
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
m : M
n : ℕ
⊢ (ofAlgHom (dpScalarExtension R S M) (dpScalarExtensionInv R S M) ⋯ ⋯).symm (dp S n (s ⊗ₜ[R] m)) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case tmul
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
m : M
n : ℕ
⊢ (ofAlgHom (dpScalarExtension R S M) (dpScalarExtensionInv R S M) ⋯ ⋯).symm (dp S n (s ⊗ₜ[R] m)) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
simp only [ofAlgHom_symm_apply]
Proof state after:
case tmul
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
m : M
n : ℕ
⊢ (dpScalarExtensionInv R S M) (dp S n (s ⊗ₜ[R] m)) ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case tmul
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
m : M
n : ℕ
⊢ (dpScalarExtensionInv R S M) (dp S n (s ⊗ₜ[R] m)) ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
rw [dpScalarExtensionInv_apply_dp]
Proof state after:
case tmul
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
m : M
n : ℕ
⊢ (s ^ n) ⊗ₜ[R] dp R n m ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case tmul
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
m : M
n : ℕ
⊢ (s ^ n) ⊗ₜ[R] dp R n m ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
simp only [LinearMap.mem_range]
Proof state after:
case tmul
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
m : M
n : ℕ
⊢ ∃ y, (LinearMap.lTensor S (grade R M n).subtype) y = (s ^ n) ⊗ₜ[R] dp R n m
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case tmul
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
m : M
n : ℕ
⊢ ∃ y, (LinearMap.lTensor S (grade R M n).subtype) y = (s ^ n) ⊗ₜ[R] dp R n m
Tactic:
use (s ^ n) ⊗ₜ[R] ⟨dp R n m, dp_mem_grade R M n m⟩
Proof state after:
case h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
m : M
n : ℕ
⊢ (LinearMap.lTensor S (grade R M n).subtype) ((s ^ n) ⊗ₜ[R] ⟨dp R n m, ⋯⟩) = (s ^ n) ⊗ₜ[R] dp R n m
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case h
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
m : M
n : ℕ
⊢ (LinearMap.lTensor S (grade R M n).subtype) ((s ^ n) ⊗ₜ[R] ⟨dp R n m, ⋯⟩) = (s ^ n) ⊗ₜ[R] dp R n m
Tactic:
simp only [LinearMap.lTensor_tmul, Submodule.coeSubtype]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case add
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hx : ∀ (n : ℕ), (gamma R M n).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n : ℕ
⊢ (gamma R M n).toFun S (x + y) ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
simp only [gamma_toFun, dpScalarExtensionEquiv, ofAlgHom_symm_apply]
Proof state after:
case add
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hx : ∀ (n : ℕ), (gamma R M n).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n : ℕ
⊢ (dpScalarExtensionInv R S M) (dp S n (x + y)) ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case add
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hx : ∀ (n : ℕ), (gamma R M n).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n : ℕ
⊢ (dpScalarExtensionInv R S M) (dp S n (x + y)) ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
simp only [dp_add, _root_.map_sum]
Proof state after:
case add
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hx : ∀ (n : ℕ), (gamma R M n).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n : ℕ
⊢ ∑ x_1 ∈ Finset.antidiagonal n, (dpScalarExtensionInv R S M) (dp S x_1.1 x * dp S x_1.2 y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case add
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hx : ∀ (n : ℕ), (gamma R M n).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n : ℕ
⊢ ∑ x_1 ∈ Finset.antidiagonal n, (dpScalarExtensionInv R S M) (dp S x_1.1 x * dp S x_1.2 y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
apply Submodule.sum_mem
Proof state after:
case add.a
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hx : ∀ (n : ℕ), (gamma R M n).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n : ℕ
⊢ ∀ c ∈ Finset.antidiagonal n,
    (dpScalarExtensionInv R S M) (dp S c.1 x * dp S c.2 y) ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case add.a
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hx : ∀ (n : ℕ), (gamma R M n).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n : ℕ
⊢ ∀ c ∈ Finset.antidiagonal n,
    (dpScalarExtensionInv R S M) (dp S c.1 x * dp S c.2 y) ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
rintro ⟨k, l⟩ hkl
Proof state after:
case add.a.mk
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hx : ∀ (n : ℕ), (gamma R M n).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
⊢ (dpScalarExtensionInv R S M) (dp S (k, l).1 x * dp S (k, l).2 y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case add.a.mk
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hx : ∀ (n : ℕ), (gamma R M n).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
⊢ (dpScalarExtensionInv R S M) (dp S (k, l).1 x * dp S (k, l).2 y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
simp only [_root_.map_mul]
Proof state after:
case add.a.mk
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hx : ∀ (n : ℕ), (gamma R M n).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
⊢ (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)