internlm/Lean-Github huggingface dataset:
Theorem: DividedPowerAlgebra.rel_isPureHomogeneous
Proof state before:
case h.a
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
a b : M
c d : ℕ
hcd : (c, d) ∈ antidiagonal n
⊢ X ((c, d).1, a) * X ((c, d).2, b) ∈ weightedHomogeneousSubmodule R Prod.fst n
Tactic:
simp only [mem_antidiagonal] at hcd
Proof state after:
case h.a
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
a b : M
c d : ℕ
hcd : c + d = n
⊢ X ((c, d).1, a) * X ((c, d).2, b) ∈ weightedHomogeneousSubmodule R Prod.fst n
Theorem: DividedPowerAlgebra.rel_isPureHomogeneous
Proof state before:
case h.a
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
a b : M
c d : ℕ
hcd : c + d = n
⊢ X ((c, d).1, a) * X ((c, d).2, b) ∈ weightedHomogeneousSubmodule R Prod.fst n
Tactic:
rw [← hcd]
Proof state after:
case h.a
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
a b : M
c d : ℕ
hcd : c + d = n
⊢ X ((c, d).1, a) * X ((c, d).2, b) ∈ weightedHomogeneousSubmodule R Prod.fst (c + d)
Theorem: DividedPowerAlgebra.rel_isPureHomogeneous
Proof state before:
case h.a
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
a b : M
c d : ℕ
hcd : c + d = n
⊢ X ((c, d).1, a) * X ((c, d).2, b) ∈ weightedHomogeneousSubmodule R Prod.fst (c + d)
Tactic:
apply IsWeightedHomogeneous.mul <;> simp only [isWeightedHomogeneous_X]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.mem_grade_iff
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
a : DividedPowerAlgebra R M
n : ℕ
⊢ a ∈ grade R M n ↔ ∃ p ∈ weightedHomogeneousSubmodule R Prod.fst n, mk p = a
Tactic:
simp only [grade, _root_.quotSubmodule, Submodule.mem_map]
Proof state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
a : DividedPowerAlgebra R M
n : ℕ
⊢ (∃ y ∈ weightedHomogeneousSubmodule R Prod.fst n, (mkAlgHom R (Rel R M)) y = a) ↔
    ∃ p ∈ weightedHomogeneousSubmodule R Prod.fst n, mk p = a
Theorem: DividedPowerAlgebra.mem_grade_iff
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
a : DividedPowerAlgebra R M
n : ℕ
⊢ (∃ y ∈ weightedHomogeneousSubmodule R Prod.fst n, (mkAlgHom R (Rel R M)) y = a) ↔
    ∃ p ∈ weightedHomogeneousSubmodule R Prod.fst n, mk p = a
Tactic:
rfl
Proof state after:
no goals
Theorem: DividedPowerAlgebra.mk_comp_toSupported
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ mk.comp ((supported R {nm | 0 < nm.1}).val.comp (toSupported R)) = mk
Tactic:
apply MvPolynomial.algHom_ext
Proof state after:
case hf
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ ∀ (i : ℕ × M), (mk.comp ((supported R {nm | 0 < nm.1}).val.comp (toSupported R))) (X i) = mk (X i)
Theorem: DividedPowerAlgebra.mk_comp_toSupported
Proof state before:
case hf
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ ∀ (i : ℕ × M), (mk.comp ((supported R {nm | 0 < nm.1}).val.comp (toSupported R))) (X i) = mk (X i)
Tactic:
rintro ⟨n, m⟩
Proof state after:
case hf.mk
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
m : M
⊢ (mk.comp ((supported R {nm | 0 < nm.1}).val.comp (toSupported R))) (X (n, m)) = mk (X (n, m))
Theorem: DividedPowerAlgebra.mk_comp_toSupported
Proof state before:
case hf.mk
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
m : M
⊢ (mk.comp ((supported R {nm | 0 < nm.1}).val.comp (toSupported R))) (X (n, m)) = mk (X (n, m))
Tactic:
simp only [AlgHom.coe_comp, mkₐ_eq_mk, Subalgebra.coe_val, Function.comp_apply, aeval_X,
  toSupported]
Proof state after:
case hf.mk
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
m : M
⊢ mk ↑(if h : 0 < n then ⟨X (n, m), ⋯⟩ else 1) = mk (X (n, m))
Theorem: DividedPowerAlgebra.mk_comp_toSupported
Proof state before:
case hf.mk
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
m : M
⊢ mk ↑(if h : 0 < n then ⟨X (n, m), ⋯⟩ else 1) = mk (X (n, m))
Tactic:
split_ifs with h
Proof state after:
case pos
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
m : M
h : 0 < n
⊢ mk ↑⟨X (n, m), ⋯⟩ = mk (X (n, m))

case neg
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
m : M
h : ¬0 < n
⊢ mk ↑1 = mk (X (n, m))
Theorem: DividedPowerAlgebra.mk_comp_toSupported
Proof state before:
case pos
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
m : M
h : 0 < n
⊢ mk ↑⟨X (n, m), ⋯⟩ = mk (X (n, m))
Tactic:
rfl
Proof state after:
no goals
Theorem: DividedPowerAlgebra.mk_comp_toSupported
Proof state before:
case neg
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
m : M
h : ¬0 < n
⊢ mk ↑1 = mk (X (n, m))
Tactic:
simp only [not_lt, le_zero_iff] at h
Proof state after:
case neg
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
m : M
h : n = 0
⊢ mk ↑1 = mk (X (n, m))
Theorem: DividedPowerAlgebra.mk_comp_toSupported
Proof state before:
case neg
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
m : M
h : n = 0
⊢ mk ↑1 = mk (X (n, m))
Tactic:
rw [h, OneMemClass.coe_one, map_one]
Proof state after:
case neg
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
m : M
h : n = 0
⊢ 1 = mk (X (0, m))
Theorem: DividedPowerAlgebra.mk_comp_toSupported
Proof state before:
case neg
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
m : M
h : n = 0
⊢ 1 = mk (X (0, m))
Tactic:
exact (dp_zero R m).symm
Proof state after:
no goals
Theorem: DividedPowerAlgebra.surjective_of_supported
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ Surjective ⇑(mk.comp (supported R {nm | 0 < nm.1}).val)
Tactic:
intro f
Proof state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : DividedPowerAlgebra R M
⊢ ∃ a, (mk.comp (supported R {nm | 0 < nm.1}).val) a = f
Theorem: DividedPowerAlgebra.surjective_of_supported
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : DividedPowerAlgebra R M
⊢ ∃ a, (mk.comp (supported R {nm | 0 < nm.1}).val) a = f
Tactic:
obtain ⟨p', hp'⟩ := DividedPowerAlgebra.mk_surjective f
Proof state after:
case intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : DividedPowerAlgebra R M
p' : MvPolynomial (ℕ × M) R
hp' : mk p' = f
⊢ ∃ a, (mk.comp (supported R {nm | 0 < nm.1}).val) a = f
Theorem: DividedPowerAlgebra.surjective_of_supported
Proof state before:
case intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : DividedPowerAlgebra R M
p' : MvPolynomial (ℕ × M) R
hp' : mk p' = f
⊢ ∃ a, (mk.comp (supported R {nm | 0 < nm.1}).val) a = f
Tactic:
use toSupported R p'
Proof state after:
case h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : DividedPowerAlgebra R M
p' : MvPolynomial (ℕ × M) R
hp' : mk p' = f
⊢ (mk.comp (supported R {nm | 0 < nm.1}).val) ((toSupported R) p') = f
Theorem: DividedPowerAlgebra.surjective_of_supported
Proof state before:
case h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : DividedPowerAlgebra R M
p' : MvPolynomial (ℕ × M) R
hp' : mk p' = f
⊢ (mk.comp (supported R {nm | 0 < nm.1}).val) ((toSupported R) p') = f
Tactic:
rw [← AlgHom.comp_apply, AlgHom.comp_assoc, mk_comp_toSupported, ← hp']
Proof state after:
no goals
Theorem: DividedPowerAlgebra.surjective_of_supported'
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : ↥(grade R M n)
⊢ ∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = ↑p
Tactic:
obtain ⟨p', hpn', hp'⟩ := (mem_grade_iff R M _ _).mpr p.2
Proof state after:
case intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : ↥(grade R M n)
p' : MvPolynomial (ℕ × M) R
hpn' : p' ∈ ↑(weightedHomogeneousSubmodule R Prod.fst n)
hp' : (mkAlgHom R (Rel R M)) p' = ↑p
⊢ ∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = ↑p
Theorem: DividedPowerAlgebra.surjective_of_supported'
Proof state before:
case intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : ↥(grade R M n)
p' : MvPolynomial (ℕ × M) R
hpn' : p' ∈ ↑(weightedHomogeneousSubmodule R Prod.fst n)
hp' : (mkAlgHom R (Rel R M)) p' = ↑p
⊢ ∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = ↑p
Tactic:
use toSupported R p'
Proof state after:
case h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : ↥(grade R M n)
p' : MvPolynomial (ℕ × M) R
hpn' : p' ∈ ↑(weightedHomogeneousSubmodule R Prod.fst n)
hp' : (mkAlgHom R (Rel R M)) p' = ↑p
⊢ IsWeightedHomogeneous Prod.fst (↑((toSupported R) p')) n ∧ mk ↑((toSupported R) p') = ↑p
Theorem: DividedPowerAlgebra.surjective_of_supported'
Proof state before:
case h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : ↥(grade R M n)
p' : MvPolynomial (ℕ × M) R
hpn' : p' ∈ ↑(weightedHomogeneousSubmodule R Prod.fst n)
hp' : (mkAlgHom R (Rel R M)) p' = ↑p
⊢ IsWeightedHomogeneous Prod.fst (↑((toSupported R) p')) n ∧ mk ↑((toSupported R) p') = ↑p
Tactic:
refine ⟨toSupported_isHomogeneous' _ _ _ hpn', ?_⟩
Proof state after:
case h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : ↥(grade R M n)
p' : MvPolynomial (ℕ × M) R
hpn' : p' ∈ ↑(weightedHomogeneousSubmodule R Prod.fst n)
hp' : (mkAlgHom R (Rel R M)) p' = ↑p
⊢ mk ↑((toSupported R) p') = ↑p
Theorem: DividedPowerAlgebra.surjective_of_supported'
Proof state before:
case h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : ↥(grade R M n)
p' : MvPolynomial (ℕ × M) R
hpn' : p' ∈ ↑(weightedHomogeneousSubmodule R Prod.fst n)
hp' : (mkAlgHom R (Rel R M)) p' = ↑p
⊢ mk ↑((toSupported R) p') = ↑p
Tactic:
erw [DFunLike.congr_fun (mk_comp_toSupported R M) p', hp']
Proof state after:
no goals
Theorem: DividedPowerAlgebra.mem_grade_iff'
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : DividedPowerAlgebra R M
⊢ p ∈ grade R M n ↔ ∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = p
Tactic:
constructor
Proof state after:
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : DividedPowerAlgebra R M
⊢ p ∈ grade R M n → ∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = p

case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : DividedPowerAlgebra R M
⊢ (∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = p) → p ∈ grade R M n
Theorem: DividedPowerAlgebra.mem_grade_iff'
Proof state before:
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : DividedPowerAlgebra R M
⊢ p ∈ grade R M n → ∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = p

case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : DividedPowerAlgebra R M
⊢ (∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = p) → p ∈ grade R M n
Tactic:
. intro hp
  rw [← Submodule.coe_mk p hp]
  apply surjective_of_supported'
Proof state after:
case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : DividedPowerAlgebra R M
⊢ (∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = p) → p ∈ grade R M n
Theorem: DividedPowerAlgebra.mem_grade_iff'
Proof state before:
case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : DividedPowerAlgebra R M
⊢ (∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = p) → p ∈ grade R M n
Tactic:
. rintro ⟨q, hq, rfl⟩
  exact ⟨q, hq, rfl⟩
Proof state after:
no goals
Theorem: DividedPowerAlgebra.mem_grade_iff'
Proof state before:
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : DividedPowerAlgebra R M
⊢ p ∈ grade R M n → ∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = p
Tactic:
intro hp
Proof state after:
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : DividedPowerAlgebra R M
hp : p ∈ grade R M n
⊢ ∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = p
Theorem: DividedPowerAlgebra.mem_grade_iff'
Proof state before:
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : DividedPowerAlgebra R M
hp : p ∈ grade R M n
⊢ ∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = p
Tactic:
rw [← Submodule.coe_mk p hp]
Proof state after:
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : DividedPowerAlgebra R M
hp : p ∈ grade R M n
⊢ ∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = ↑⟨p, hp⟩
Theorem: DividedPowerAlgebra.mem_grade_iff'
Proof state before:
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : DividedPowerAlgebra R M
hp : p ∈ grade R M n
⊢ ∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = ↑⟨p, hp⟩
Tactic:
apply surjective_of_supported'
Proof state after:
no goals
Theorem: DividedPowerAlgebra.mem_grade_iff'
Proof state before:
case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
p : DividedPowerAlgebra R M
⊢ (∃ q, IsWeightedHomogeneous Prod.fst (↑q) n ∧ mk ↑q = p) → p ∈ grade R M n
Tactic:
rintro ⟨q, hq, rfl⟩
Proof state after:
case mpr.intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
q : ↥(supported R {nm | 0 < nm.1})
hq : IsWeightedHomogeneous Prod.fst (↑q) n
⊢ mk ↑q ∈ grade R M n
Theorem: DividedPowerAlgebra.mem_grade_iff'
Proof state before:
case mpr.intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
q : ↥(supported R {nm | 0 < nm.1})
hq : IsWeightedHomogeneous Prod.fst (↑q) n
⊢ mk ↑q ∈ grade R M n
Tactic:
exact ⟨q, hq, rfl⟩
Proof state after:
no goals
Theorem: DividedPowerAlgebra.ι_comp_lift
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
⊢ (lift hI φ hφ).toLinearMap ∘ₗ ι R M = φ
Tactic:
ext m
Proof state after:
case h
R : Type u_1
M : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
m : M
⊢ ((lift hI φ hφ).toLinearMap ∘ₗ ι R M) m = φ m
Theorem: DividedPowerAlgebra.ι_comp_lift
Proof state before:
case h
R : Type u_1
M : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
m : M
⊢ ((lift hI φ hφ).toLinearMap ∘ₗ ι R M) m = φ m
Tactic:
simp only [LinearMap.coe_comp, Function.comp_apply, AlgHom.toLinearMap_apply, ι_def,
  liftAlgHom_apply_dp]
Proof state after:
case h
R : Type u_1
M : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
m : M
⊢ hI.dpow 1 (φ m) = φ m
Theorem: DividedPowerAlgebra.ι_comp_lift
Proof state before:
case h
R : Type u_1
M : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
m : M
⊢ hI.dpow 1 (φ m) = φ m
Tactic:
exact hI.dpow_one (hφ m)
Proof state after:
no goals
Theorem: DividedPowerAlgebra.lift_ι_apply
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
x : M
⊢ (lift hI φ hφ) ((ι R M) x) = φ x
Tactic:
conv_rhs => rw [← ι_comp_lift R hI hφ]
Proof state after:
R : Type u_1
M : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
x : M
⊢ (lift hI φ hφ) ((ι R M) x) = ((lift hI φ hφ).toLinearMap ∘ₗ ι R M) x
Theorem: DividedPowerAlgebra.lift_ι_apply
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
x : M
⊢ (lift hI φ hφ) ((ι R M) x) = ((lift hI φ hφ).toLinearMap ∘ₗ ι R M) x
Tactic:
rfl
Proof state after:
no goals
Theorem: DividedPowerAlgebra.liftAux_isHomogeneous
Proof state before:
R : Type u_1
M : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : DecidableEq R
inst✝⁷ : DecidableEq M
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
𝒜 : ℕ → Submodule S A
inst✝ : GradedAlgebra 𝒜
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (x, y) => f (x, u) * f (y, v)
hf : ∀ (n : ℕ) (m : M), f (n, m) ∈ 𝒜 n
⊢ GalgHom.IsHomogeneous (grade R M) 𝒜 (lift' f hf_zero hf_smul hf_mul hf_add)
Tactic:
intro i a
Proof state after:
R : Type u_1
M : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : DecidableEq R
inst✝⁷ : DecidableEq M
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
𝒜 : ℕ → Submodule S A
inst✝ : GradedAlgebra 𝒜
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (x, y) => f (x, u) * f (y, v)
hf : ∀ (n : ℕ) (m : M), f (n, m) ∈ 𝒜 n
i : ℕ
a : DividedPowerAlgebra R M
⊢ a ∈ grade R M i → (lift' f hf_zero hf_smul hf_mul hf_add) a ∈ 𝒜 i
Theorem: DividedPowerAlgebra.liftAux_isHomogeneous
Proof state before:
R : Type u_1
M : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : DecidableEq R
inst✝⁷ : DecidableEq M
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
𝒜 : ℕ → Submodule S A
inst✝ : GradedAlgebra 𝒜
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (x, y) => f (x, u) * f (y, v)
hf : ∀ (n : ℕ) (m : M), f (n, m) ∈ 𝒜 n
i : ℕ
a : DividedPowerAlgebra R M
⊢ a ∈ grade R M i → (lift' f hf_zero hf_smul hf_mul hf_add) a ∈ 𝒜 i
Tactic:
simp only [mem_grade_iff]
Proof state after:
R : Type u_1
M : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : DecidableEq R
inst✝⁷ : DecidableEq M
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
𝒜 : ℕ → Submodule S A
inst✝ : GradedAlgebra 𝒜
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (x, y) => f (x, u) * f (y, v)
hf : ∀ (n : ℕ) (m : M), f (n, m) ∈ 𝒜 n
i : ℕ
a : DividedPowerAlgebra R M
⊢ (∃ p ∈ weightedHomogeneousSubmodule R Prod.fst i, mk p = a) → (lift' f hf_zero hf_smul hf_mul hf_add) a ∈ 𝒜 i