internlm/Lean-Github huggingface dataset:
Theorem: TrivSqZeroExt.mem_kerIdeal_iff_exists
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
x : TrivSqZeroExt R M
⊢ x = inr x.snd ↔ ∃ m, x = inr m
Tactic:
exact ⟨fun h => ⟨x.snd, h⟩, fun ⟨m, hm⟩ => by rw [hm]; rfl⟩
Proof state after:
no goals
Theorem: TrivSqZeroExt.mem_kerIdeal_iff_exists
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
x : TrivSqZeroExt R M
x✝ : ∃ m, x = inr m
m : M
hm : x = inr m
⊢ x = inr x.snd
Tactic:
rw [hm]
Proof state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
x : TrivSqZeroExt R M
x✝ : ∃ m, x = inr m
m : M
hm : x = inr m
⊢ inr m = inr (inr m).snd
Theorem: TrivSqZeroExt.mem_kerIdeal_iff_exists
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
x : TrivSqZeroExt R M
x✝ : ∃ m, x = inr m
m : M
hm : x = inr m
⊢ inr m = inr (inr m).snd
Tactic:
rfl
Proof state after:
no goals
Theorem: TrivSqZeroExt.sqZero
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ kerIdeal R M ^ 2 = ⊥
Tactic:
simp only [pow_two, zero_eq_bot, eq_bot_iff, mul_le, mem_kerIdeal_iff_inr]
Proof state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ ∀ (r : TrivSqZeroExt R M), r = inr r.snd → ∀ (s : TrivSqZeroExt R M), s = inr s.snd → r * s ∈ ⊥
Theorem: TrivSqZeroExt.sqZero
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ ∀ (r : TrivSqZeroExt R M), r = inr r.snd → ∀ (s : TrivSqZeroExt R M), s = inr s.snd → r * s ∈ ⊥
Tactic:
rintro x hx y hy
Proof state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
x : TrivSqZeroExt R M
hx : x = inr x.snd
y : TrivSqZeroExt R M
hy : y = inr y.snd
⊢ x * y ∈ ⊥
Theorem: TrivSqZeroExt.sqZero
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
x : TrivSqZeroExt R M
hx : x = inr x.snd
y : TrivSqZeroExt R M
hy : y = inr y.snd
⊢ x * y ∈ ⊥
Tactic:
rw [hx, hy, mem_bot, inr_mul_inr]
Proof state after:
no goals
Theorem: Finsupp.prod.mem_grade
Proof state before:
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
⊢ (c.prod fun s e => f s ^ e) ∈ 𝒜 (c.sum fun s e => e • d s)
Tactic:
rw [Finsupp.prod, Finsupp.sum]
Proof state after:
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
⊢ ∏ a ∈ c.support, f a ^ c a ∈ 𝒜 (∑ a ∈ c.support, c a • d a)
Theorem: Finsupp.prod.mem_grade
Proof state before:
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
⊢ ∏ a ∈ c.support, f a ^ c a ∈ 𝒜 (∑ a ∈ c.support, c a • d a)
Tactic:
let p : Finset σ → Prop := fun s =>
  s ⊆ c.support → (s.prod fun i => f i ^ c i) ∈ 𝒜 (s.sum fun i => c i • d i)
Proof state after:
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
p : Finset σ → Prop := fun s => s ⊆ c.support → ∏ i ∈ s, f i ^ c i ∈ 𝒜 (∑ i ∈ s, c i • d i)
⊢ ∏ a ∈ c.support, f a ^ c a ∈ 𝒜 (∑ a ∈ c.support, c a • d a)
Theorem: Finsupp.prod.mem_grade
Proof state before:
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
p : Finset σ → Prop := fun s => s ⊆ c.support → ∏ i ∈ s, f i ^ c i ∈ 𝒜 (∑ i ∈ s, c i • d i)
⊢ ∏ a ∈ c.support, f a ^ c a ∈ 𝒜 (∑ a ∈ c.support, c a • d a)
Tactic:
apply @Finset.induction_on σ p _ c.support
Proof state after:
case empty
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
p : Finset σ → Prop := fun s => s ⊆ c.support → ∏ i ∈ s, f i ^ c i ∈ 𝒜 (∑ i ∈ s, c i • d i)
⊢ p ∅

case insert
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
p : Finset σ → Prop := fun s => s ⊆ c.support → ∏ i ∈ s, f i ^ c i ∈ 𝒜 (∑ i ∈ s, c i • d i)
⊢ ∀ ⦃a : σ⦄ {s : Finset σ}, a ∉ s → p s → p (insert a s)

case a
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
p : Finset σ → Prop := fun s => s ⊆ c.support → ∏ i ∈ s, f i ^ c i ∈ 𝒜 (∑ i ∈ s, c i • d i)
⊢ c.support ⊆ c.support
Theorem: Finsupp.prod.mem_grade
Proof state before:
case empty
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
p : Finset σ → Prop := fun s => s ⊆ c.support → ∏ i ∈ s, f i ^ c i ∈ 𝒜 (∑ i ∈ s, c i • d i)
⊢ p ∅
Tactic:
exact imp_intro (SetLike.one_mem_graded 𝒜)
Proof state after:
no goals
Theorem: Finsupp.prod.mem_grade
Proof state before:
case insert
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
p : Finset σ → Prop := fun s => s ⊆ c.support → ∏ i ∈ s, f i ^ c i ∈ 𝒜 (∑ i ∈ s, c i • d i)
⊢ ∀ ⦃a : σ⦄ {s : Finset σ}, a ∉ s → p s → p (insert a s)
Tactic:
intro a s ha hs hs'
Proof state after:
case insert
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
p : Finset σ → Prop := fun s => s ⊆ c.support → ∏ i ∈ s, f i ^ c i ∈ 𝒜 (∑ i ∈ s, c i • d i)
a : σ
s : Finset σ
ha : a ∉ s
hs : p s
hs' : insert a s ⊆ c.support
⊢ ∏ i ∈ insert a s, f i ^ c i ∈ 𝒜 (∑ i ∈ insert a s, c i • d i)
Theorem: Finsupp.prod.mem_grade
Proof state before:
case insert
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
p : Finset σ → Prop := fun s => s ⊆ c.support → ∏ i ∈ s, f i ^ c i ∈ 𝒜 (∑ i ∈ s, c i • d i)
a : σ
s : Finset σ
ha : a ∉ s
hs : p s
hs' : insert a s ⊆ c.support
⊢ ∏ i ∈ insert a s, f i ^ c i ∈ 𝒜 (∑ i ∈ insert a s, c i • d i)
Tactic:
rw [Finset.prod_insert ha, Finset.sum_insert ha]
Proof state after:
case insert
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
p : Finset σ → Prop := fun s => s ⊆ c.support → ∏ i ∈ s, f i ^ c i ∈ 𝒜 (∑ i ∈ s, c i • d i)
a : σ
s : Finset σ
ha : a ∉ s
hs : p s
hs' : insert a s ⊆ c.support
⊢ f a ^ c a * ∏ x ∈ s, f x ^ c x ∈ 𝒜 (c a • d a + ∑ x ∈ s, c x • d x)
Theorem: Finsupp.prod.mem_grade
Proof state before:
case insert
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
p : Finset σ → Prop := fun s => s ⊆ c.support → ∏ i ∈ s, f i ^ c i ∈ 𝒜 (∑ i ∈ s, c i • d i)
a : σ
s : Finset σ
ha : a ∉ s
hs : p s
hs' : insert a s ⊆ c.support
⊢ f a ^ c a * ∏ x ∈ s, f x ^ c x ∈ 𝒜 (c a • d a + ∑ x ∈ s, c x • d x)
Tactic:
exact
  SetLike.mul_mem_graded (SetLike.pow_mem_graded _ (hc a (hs' (mem_insert_self a s))))
    (hs (subset_trans (subset_insert a s) hs'))
Proof state after:
no goals
Theorem: Finsupp.prod.mem_grade
Proof state before:
case a
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
p : Finset σ → Prop := fun s => s ⊆ c.support → ∏ i ∈ s, f i ^ c i ∈ 𝒜 (∑ i ∈ s, c i • d i)
⊢ c.support ⊆ c.support
Tactic:
exact subset_rfl
Proof state after:
no goals
Theorem: GalgHom.isHomogeneous'_aeval
Proof state before:
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
⊢ isHomogeneous' (MvPolynomial σ R) (weightedHomogeneousSubmodule R w) A 𝒜 (⇑φ) (aeval f)
Tactic:
intro i p hp
Proof state after:
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : p ∈ weightedHomogeneousSubmodule R w i
⊢ (aeval f) p ∈ 𝒜 (φ i)
Theorem: GalgHom.isHomogeneous'_aeval
Proof state before:
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : p ∈ weightedHomogeneousSubmodule R w i
⊢ (aeval f) p ∈ 𝒜 (φ i)
Tactic:
simp only [mem_weightedHomogeneousSubmodule, IsWeightedHomogeneous] at hp
Proof state after:
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
⊢ (aeval f) p ∈ 𝒜 (φ i)
Theorem: GalgHom.isHomogeneous'_aeval
Proof state before:
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
⊢ (aeval f) p ∈ 𝒜 (φ i)
Tactic:
rw [p.as_sum, map_sum]
Proof state after:
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
⊢ ∑ x ∈ p.support, (aeval f) ((monomial x) (coeff x p)) ∈ 𝒜 (φ i)
Theorem: GalgHom.isHomogeneous'_aeval
Proof state before:
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
⊢ ∑ x ∈ p.support, (aeval f) ((monomial x) (coeff x p)) ∈ 𝒜 (φ i)
Tactic:
apply Submodule.sum_mem
Proof state after:
case a
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
⊢ ∀ c ∈ p.support, (aeval f) ((monomial c) (coeff c p)) ∈ 𝒜 (φ i)
Theorem: GalgHom.isHomogeneous'_aeval
Proof state before:
case a
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
⊢ ∀ c ∈ p.support, (aeval f) ((monomial c) (coeff c p)) ∈ 𝒜 (φ i)
Tactic:
intro c hc
Proof state after:
case a
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ (aeval f) ((monomial c) (coeff c p)) ∈ 𝒜 (φ i)
Theorem: GalgHom.isHomogeneous'_aeval
Proof state before:
case a
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ (aeval f) ((monomial c) (coeff c p)) ∈ 𝒜 (φ i)
Tactic:
rw [aeval_monomial, ← smul_eq_mul, algebraMap_smul]
Proof state after:
case a
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ (coeff c p • c.prod fun i k => f i ^ k) ∈ 𝒜 (φ i)
Theorem: GalgHom.isHomogeneous'_aeval
Proof state before:
case a
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ (coeff c p • c.prod fun i k => f i ^ k) ∈ 𝒜 (φ i)
Tactic:
apply Submodule.smul_mem
Proof state after:
case a.h
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ (c.prod fun i k => f i ^ k) ∈ 𝒜 (φ i)
Theorem: GalgHom.isHomogeneous'_aeval
Proof state before:
case a.h
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ (c.prod fun i k => f i ^ k) ∈ 𝒜 (φ i)
Tactic:
convert Finsupp.prod.mem_grade 𝒜 c f _ fun s _ => h s
Proof state after:
case h.e'_5.h.e'_1
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ φ i = c.sum fun s e => e • φ (w s)
Theorem: GalgHom.isHomogeneous'_aeval
Proof state before:
case h.e'_5.h.e'_1
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ φ i = c.sum fun s e => e • φ (w s)
Tactic:
rw [← hp (mem_support_iff.mp hc), MvPolynomial.weightedDegree_apply]
Proof state after:
case h.e'_5.h.e'_1
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ φ (c.sum fun i c => c • w i) = c.sum fun s e => e • φ (w s)
Theorem: GalgHom.isHomogeneous'_aeval
Proof state before:
case h.e'_5.h.e'_1
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ φ (c.sum fun i c => c • w i) = c.sum fun s e => e • φ (w s)
Tactic:
rw [Finsupp.sum, map_sum, Finsupp.sum_of_support_subset _ le_rfl]
Proof state after:
case h.e'_5.h.e'_1
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ ∑ x ∈ c.support, φ (c x • w x) = ∑ x ∈ c.support, c x • φ (w x)

case h.e'_5.h.e'_1.h
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ ∀ i ∈ c.support, 0 • φ (w i) = 0