internlm/Lean-Github huggingface dataset:
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
⊢ (∃ p ∈ weightedHomogeneousSubmodule R Prod.fst i, mk p = a) → (lift' f hf_zero hf_smul hf_mul hf_add) a ∈ 𝒜 i
Tactic:
rintro ⟨p, hp, rfl⟩
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
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 : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
⊢ (lift' f hf_zero hf_smul hf_mul hf_add) (mk p) ∈ 𝒜 i
Theorem: DividedPowerAlgebra.liftAux_isHomogeneous
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
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 : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
⊢ (lift' f hf_zero hf_smul hf_mul hf_add) (mk p) ∈ 𝒜 i
Tactic:
rw [lift'AlgHom_apply, p.as_sum, aeval_sum]
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
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 : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
⊢ ∑ i ∈ p.support, (aeval f) ((monomial i) (coeff i p)) ∈ 𝒜 i
Theorem: DividedPowerAlgebra.liftAux_isHomogeneous
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
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 : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
⊢ ∑ i ∈ p.support, (aeval f) ((monomial i) (coeff i p)) ∈ 𝒜 i
Tactic:
apply _root_.sum_mem
Proof state after:
case intro.intro.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
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 : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
⊢ ∀ c ∈ p.support, (aeval f) ((monomial c) (coeff c p)) ∈ 𝒜 i
Theorem: DividedPowerAlgebra.liftAux_isHomogeneous
Proof state before:
case intro.intro.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
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 : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
⊢ ∀ c ∈ p.support, (aeval f) ((monomial c) (coeff c p)) ∈ 𝒜 i
Tactic:
intro c hc
Proof state after:
case intro.intro.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
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 : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
c : ℕ × M →₀ ℕ
hc : c ∈ p.support
⊢ (aeval f) ((monomial c) (coeff c p)) ∈ 𝒜 i
Theorem: DividedPowerAlgebra.liftAux_isHomogeneous
Proof state before:
case intro.intro.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
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 : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
c : ℕ × M →₀ ℕ
hc : c ∈ p.support
⊢ (aeval f) ((monomial c) (coeff c p)) ∈ 𝒜 i
Tactic:
rw [aeval_monomial, ← smul_eq_mul, algebraMap_smul A, algebra_compatible_smul S (coeff c p)]
Proof state after:
case intro.intro.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
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 : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
c : ℕ × M →₀ ℕ
hc : c ∈ p.support
⊢ ((algebraMap R S) (coeff c p) • c.prod fun i k => f i ^ k) ∈ 𝒜 i
Theorem: DividedPowerAlgebra.liftAux_isHomogeneous
Proof state before:
case intro.intro.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
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 : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
c : ℕ × M →₀ ℕ
hc : c ∈ p.support
⊢ ((algebraMap R S) (coeff c p) • c.prod fun i k => f i ^ k) ∈ 𝒜 i
Tactic:
apply Submodule.smul_mem
Proof state after:
case intro.intro.h.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
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 : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
c : ℕ × M →₀ ℕ
hc : c ∈ p.support
⊢ (c.prod fun i k => f i ^ k) ∈ 𝒜 i
Theorem: DividedPowerAlgebra.liftAux_isHomogeneous
Proof state before:
case intro.intro.h.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
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 : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
c : ℕ × M →₀ ℕ
hc : c ∈ p.support
⊢ (c.prod fun i k => f i ^ k) ∈ 𝒜 i
Tactic:
rw [← hp (mem_support_iff.mp hc)]
Proof state after:
case intro.intro.h.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
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 : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
c : ℕ × M →₀ ℕ
hc : c ∈ p.support
⊢ (c.prod fun i k => f i ^ k) ∈ 𝒜 ((weightedDegree Prod.fst) c)
Theorem: DividedPowerAlgebra.liftAux_isHomogeneous
Proof state before:
case intro.intro.h.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
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 : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
c : ℕ × M →₀ ℕ
hc : c ∈ p.support
⊢ (c.prod fun i k => f i ^ k) ∈ 𝒜 ((weightedDegree Prod.fst) c)
Tactic:
exact Finsupp.prod.mem_grade _ _ _ _ fun ⟨n, m⟩ _ => hf n m
Proof state after:
no goals
Theorem: DividedPowerAlgebra.lift_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
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
I : Ideal A
hI : DividedPowers I
hI' : HasGradedDpow 𝒜 hI
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
hφ' : ∀ (m : M), φ m ∈ 𝒜 1
⊢ GalgHom.IsHomogeneous (grade R M) 𝒜 (lift hI φ hφ)
Tactic:
apply liftAux_isHomogeneous
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
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
I : Ideal A
hI : DividedPowers I
hI' : HasGradedDpow 𝒜 hI
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
hφ' : ∀ (m : M), φ m ∈ 𝒜 1
⊢ ∀ (n : ℕ) (m : M), hI.dpow (n, m).1 (φ (n, m).2) ∈ 𝒜 n
Theorem: DividedPowerAlgebra.lift_isHomogeneous
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
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
I : Ideal A
hI : DividedPowers I
hI' : HasGradedDpow 𝒜 hI
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
hφ' : ∀ (m : M), φ m ∈ 𝒜 1
⊢ ∀ (n : ℕ) (m : M), hI.dpow (n, m).1 (φ (n, m).2) ∈ 𝒜 n
Tactic:
intro n m
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
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
I : Ideal A
hI : DividedPowers I
hI' : HasGradedDpow 𝒜 hI
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
hφ' : ∀ (m : M), φ m ∈ 𝒜 1
n : ℕ
m : M
⊢ hI.dpow (n, m).1 (φ (n, m).2) ∈ 𝒜 n
Theorem: DividedPowerAlgebra.lift_isHomogeneous
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
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
I : Ideal A
hI : DividedPowers I
hI' : HasGradedDpow 𝒜 hI
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
hφ' : ∀ (m : M), φ m ∈ 𝒜 1
n : ℕ
m : M
⊢ hI.dpow (n, m).1 (φ (n, m).2) ∈ 𝒜 n
Tactic:
simpa only [Algebra.id.smul_eq_mul, mul_one] using hI' (φ m) (hφ m) 1 (hφ' m) n
Proof state after:
no goals
Theorem: DividedPowerAlgebra.proj'_zero_one
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
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : DecidableEq S
inst✝³ : DecidableEq N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
⊢ (proj' R M 0) 1 = 1
Tactic:
rw [proj', proj, LinearMap.coe_mk, AddHom.coe_mk, decompose_one]
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
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : DecidableEq S
inst✝³ : DecidableEq N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
⊢ 1 0 = 1
Theorem: DividedPowerAlgebra.proj'_zero_one
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
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : DecidableEq S
inst✝³ : DecidableEq N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
⊢ 1 0 = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: DividedPowerAlgebra.proj'_zero_mul
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
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : DecidableEq S
inst✝³ : DecidableEq N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x y : DividedPowerAlgebra R M
⊢ (proj' R M 0) (x * y) = (proj' R M 0) x * (proj' R M 0) y
Tactic:
simp only [proj', ← projZeroRingHom'_apply, _root_.map_mul]
Proof state after:
no goals
Theorem: Ideal.image_eq_map_of_surjective
Proof state before:
A : Type u_1
B : Type u_2
inst✝¹ : Semiring A
inst✝ : Semiring B
f : A →+* B
I : Ideal A
hf : Function.Surjective ⇑f
⊢ ⇑f '' ↑I = ↑(map f I)
Tactic:
symm
Proof state after:
A : Type u_1
B : Type u_2
inst✝¹ : Semiring A
inst✝ : Semiring B
f : A →+* B
I : Ideal A
hf : Function.Surjective ⇑f
⊢ ↑(map f I) = ⇑f '' ↑I
Theorem: Ideal.image_eq_map_of_surjective
Proof state before:
A : Type u_1
B : Type u_2
inst✝¹ : Semiring A
inst✝ : Semiring B
f : A →+* B
I : Ideal A
hf : Function.Surjective ⇑f
⊢ ↑(map f I) = ⇑f '' ↑I
Tactic:
ext x
Proof state after:
case h
A : Type u_1
B : Type u_2
inst✝¹ : Semiring A
inst✝ : Semiring B
f : A →+* B
I : Ideal A
hf : Function.Surjective ⇑f
x : B
⊢ x ∈ ↑(map f I) ↔ x ∈ ⇑f '' ↑I
Theorem: Ideal.image_eq_map_of_surjective
Proof state before:
case h
A : Type u_1
B : Type u_2
inst✝¹ : Semiring A
inst✝ : Semiring B
f : A →+* B
I : Ideal A
hf : Function.Surjective ⇑f
x : B
⊢ x ∈ ↑(map f I) ↔ x ∈ ⇑f '' ↑I
Tactic:
simp only [Set.mem_image, SetLike.mem_coe]
Proof state after:
case h
A : Type u_1
B : Type u_2
inst✝¹ : Semiring A
inst✝ : Semiring B
f : A →+* B
I : Ideal A
hf : Function.Surjective ⇑f
x : B
⊢ x ∈ map f I ↔ ∃ x_1 ∈ I, f x_1 = x
Theorem: Ideal.image_eq_map_of_surjective
Proof state before:
case h
A : Type u_1
B : Type u_2
inst✝¹ : Semiring A
inst✝ : Semiring B
f : A →+* B
I : Ideal A
hf : Function.Surjective ⇑f
x : B
⊢ x ∈ map f I ↔ ∃ x_1 ∈ I, f x_1 = x
Tactic:
apply Ideal.mem_map_iff_of_surjective _ hf
Proof state after:
no goals
Theorem: DividedPowerAlgebra.algebraMapInv_eq
Proof state before:
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
⊢ (algebraMapInv R M) (mk f) = (aeval fun nm => if 0 < nm.1 then 0 else 1) f
Tactic:
rw [← AlgHom.comp_apply]
Proof state after:
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
⊢ ((algebraMapInv R M).comp mk) f = (aeval fun nm => if 0 < nm.1 then 0 else 1) f
Theorem: DividedPowerAlgebra.algebraMapInv_eq
Proof state before:
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
⊢ ((algebraMapInv R M).comp mk) f = (aeval fun nm => if 0 < nm.1 then 0 else 1) f
Tactic:
apply AlgHom.congr_fun
Proof state after:
case H
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
⊢ (algebraMapInv R M).comp mk = aeval fun nm => if 0 < nm.1 then 0 else 1
Theorem: DividedPowerAlgebra.algebraMapInv_eq
Proof state before:
case H
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
⊢ (algebraMapInv R M).comp mk = aeval fun nm => if 0 < nm.1 then 0 else 1
Tactic:
ext ⟨n, m⟩
Proof state after:
case H.hf.mk
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
⊢ ((algebraMapInv R M).comp mk) (X (n, m)) = (aeval fun nm => if 0 < nm.1 then 0 else 1) (X (n, m))
Theorem: DividedPowerAlgebra.algebraMapInv_eq
Proof state before:
case H.hf.mk
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
⊢ ((algebraMapInv R M).comp mk) (X (n, m)) = (aeval fun nm => if 0 < nm.1 then 0 else 1) (X (n, m))
Tactic:
simp only [algebraMapInv, AlgHom.comp_apply, aeval_X]
Proof state after:
case H.hf.mk
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
n : ℕ
m : M
⊢ (lift (dividedPowersBot R) 0 ⋯) (mk (X (n, m))) = if 0 < n then 0 else 1