internlm/Lean-Github huggingface dataset:
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof state before:
case a.intro.mk
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : mk f ∈ augIdeal R M
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
⊢ ↑c.support ⊆ {nm | 0 < nm.1}
Tactic:
intro nm hnm
Proof state after:
case a.intro.mk
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : mk f ∈ augIdeal R M
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
nm : ℕ × M
hnm : nm ∈ ↑c.support
⊢ nm ∈ {nm | 0 < nm.1}
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof state before:
case a.intro.mk
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : mk f ∈ augIdeal R M
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
nm : ℕ × M
hnm : nm ∈ ↑c.support
⊢ nm ∈ {nm | 0 < nm.1}
Tactic:
apply mem_supported.mp hf
Proof state after:
case a.intro.mk.a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : mk f ∈ augIdeal R M
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
nm : ℕ × M
hnm : nm ∈ ↑c.support
⊢ nm ∈ ↑f.vars
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof state before:
case a.intro.mk.a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : mk f ∈ augIdeal R M
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
nm : ℕ × M
hnm : nm ∈ ↑c.support
⊢ nm ∈ ↑f.vars
Tactic:
simp only [mem_vars, mem_coe, mem_support_iff, ne_eq, Finsupp.mem_support_iff, exists_prop]
Proof state after:
case a.intro.mk.a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : mk f ∈ augIdeal R M
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
nm : ℕ × M
hnm : nm ∈ ↑c.support
⊢ ∃ d, ¬coeff d f = 0 ∧ ¬d nm = 0
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof state before:
case a.intro.mk.a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : mk f ∈ augIdeal R M
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
nm : ℕ × M
hnm : nm ∈ ↑c.support
⊢ ∃ d, ¬coeff d f = 0 ∧ ¬d nm = 0
Tactic:
rw [mem_coe, Finsupp.mem_support_iff] at hnm
Proof state after:
case a.intro.mk.a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : mk f ∈ augIdeal R M
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
nm : ℕ × M
hnm : c nm ≠ 0
⊢ ∃ d, ¬coeff d f = 0 ∧ ¬d nm = 0
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof state before:
case a.intro.mk.a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : mk f ∈ augIdeal R M
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
nm : ℕ × M
hnm : c nm ≠ 0
⊢ ∃ d, ¬coeff d f = 0 ∧ ¬d nm = 0
Tactic:
exact ⟨c, ⟨mem_support_iff.mp hc, hnm⟩⟩
Proof state after:
no goals
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof state before:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ span (Set.image2 (dp R) {n | 0 < n} Set.univ) ≤ augIdeal R M
Tactic:
rw [span_le]
Proof state after:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ Set.image2 (dp R) {n | 0 < n} Set.univ ⊆ ↑(augIdeal R M)
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof state before:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ Set.image2 (dp R) {n | 0 < n} Set.univ ⊆ ↑(augIdeal R M)
Tactic:
intro f
Proof state after:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : DividedPowerAlgebra R M
⊢ f ∈ Set.image2 (dp R) {n | 0 < n} Set.univ → f ∈ ↑(augIdeal R M)
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof state before:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : DividedPowerAlgebra R M
⊢ f ∈ Set.image2 (dp R) {n | 0 < n} Set.univ → f ∈ ↑(augIdeal R M)
Tactic:
simp only [Set.mem_image2, Set.mem_setOf_eq, Set.mem_univ, true_and_iff, exists_and_left,
  SetLike.mem_coe, forall_exists_index, and_imp]
Proof state after:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : DividedPowerAlgebra R M
⊢ ∀ (x : ℕ), 0 < x → ∀ (x_1 : M), dp R x x_1 = f → f ∈ augIdeal R M
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof state before:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : DividedPowerAlgebra R M
⊢ ∀ (x : ℕ), 0 < x → ∀ (x_1 : M), dp R x x_1 = f → f ∈ augIdeal R M
Tactic:
intro n hn m hf
Proof state after:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : DividedPowerAlgebra R M
n : ℕ
hn : 0 < n
m : M
hf : dp R n m = f
⊢ f ∈ augIdeal R M
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof state before:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : DividedPowerAlgebra R M
n : ℕ
hn : 0 < n
m : M
hf : dp R n m = f
⊢ f ∈ augIdeal R M
Tactic:
rw [← hf, mem_augIdeal_iff, algebraMapInv, liftAlgHom_apply_dp]
Proof state after:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : DividedPowerAlgebra R M
n : ℕ
hn : 0 < n
m : M
hf : dp R n m = f
⊢ (dividedPowersBot R).dpow n (0 m) = 0
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof state before:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : DividedPowerAlgebra R M
n : ℕ
hn : 0 < n
m : M
hf : dp R n m = f
⊢ (dividedPowersBot R).dpow n (0 m) = 0
Tactic:
simp_rw [LinearMap.zero_apply]
Proof state after:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : DividedPowerAlgebra R M
n : ℕ
hn : 0 < n
m : M
hf : dp R n m = f
⊢ (dividedPowersBot R).dpow n 0 = 0
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof state before:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : DividedPowerAlgebra R M
n : ℕ
hn : 0 < n
m : M
hf : dp R n m = f
⊢ (dividedPowersBot R).dpow n 0 = 0
Tactic:
rw [DividedPowers.dpow_eval_zero _ (ne_of_gt hn)]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.right_inv'
Proof state before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : R
⊢ (algebraMapInv R M) ↑((⇑(proj' R M 0) ∘ ⇑(algebraMap R (DividedPowerAlgebra R M))) x) = x
Tactic:
rw [proj'_zero_comp_algebraMap]
Proof state after:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : R
⊢ (algebraMapInv R M) ((algebraMap R (DividedPowerAlgebra R M)) x) = x
Theorem: DividedPowerAlgebra.right_inv'
Proof state before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : R
⊢ (algebraMapInv R M) ((algebraMap R (DividedPowerAlgebra R M)) x) = x
Tactic:
exact algebraMap_leftInverse R M x
Proof state after:
no goals
Theorem: DividedPowerAlgebra.left_inv'
Proof state before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
⊢ (⇑(proj' R M 0) ∘ ⇑(algebraMap R (DividedPowerAlgebra R M))) ((algebraMapInv R M) ↑x) = x
Tactic:
ext
Proof state after:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
⊢ ↑((⇑(proj' R M 0) ∘ ⇑(algebraMap R (DividedPowerAlgebra R M))) ((algebraMapInv R M) ↑x)) = ↑x
Theorem: DividedPowerAlgebra.left_inv'
Proof state before:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
⊢ ↑((⇑(proj' R M 0) ∘ ⇑(algebraMap R (DividedPowerAlgebra R M))) ((algebraMapInv R M) ↑x)) = ↑x
Tactic:
simp only [proj', proj, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply]
Proof state after:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
⊢ ↑(((DirectSum.decompose (grade R M)) ((algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) ↑x))) 0) = ↑x
Theorem: DividedPowerAlgebra.left_inv'
Proof state before:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
⊢ ↑(((DirectSum.decompose (grade R M)) ((algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) ↑x))) 0) = ↑x
Tactic:
conv_rhs => rw [← DirectSum.decompose_of_mem_same _ x.2]
Proof state after:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
⊢ ↑(((DirectSum.decompose (grade R M)) ((algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) ↑x))) 0) =
    ↑(((DirectSum.decompose (grade R M)) ↑x) 0)
Theorem: DividedPowerAlgebra.left_inv'
Proof state before:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
⊢ ↑(((DirectSum.decompose (grade R M)) ((algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) ↑x))) 0) =
    ↑(((DirectSum.decompose (grade R M)) ↑x) 0)
Tactic:
simp only [algebraMap_right_inv_of_degree_zero R M x, decompose_coe, of_eq_same]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.lift_augIdeal_le
Proof state before:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
⊢ Ideal.map (lift hI φ hφ) (augIdeal R M) ≤ I
Tactic:
simp only [augIdeal_eq_span, Ideal.map_span, Ideal.span_le, SetLike.mem_coe]
Proof state after:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
⊢ ⇑(lift hI φ hφ) '' Set.image2 (dp R) {n | 0 < n} Set.univ ⊆ ↑I
Theorem: DividedPowerAlgebra.lift_augIdeal_le
Proof state before:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
⊢ ⇑(lift hI φ hφ) '' Set.image2 (dp R) {n | 0 < n} Set.univ ⊆ ↑I
Tactic:
rintro y ⟨x, ⟨n, hn, m, _, rfl⟩, rfl⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
n : ℕ
hn : n ∈ {n | 0 < n}
m : M
left✝ : m ∈ Set.univ
⊢ (lift hI φ hφ) (dp R n m) ∈ ↑I
Theorem: DividedPowerAlgebra.lift_augIdeal_le
Proof state before:
case intro.intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
n : ℕ
hn : n ∈ {n | 0 < n}
m : M
left✝ : m ∈ Set.univ
⊢ (lift hI φ hφ) (dp R n m) ∈ ↑I
Tactic:
simp only [liftAlgHom_apply_dp]
Proof state after:
case intro.intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
n : ℕ
hn : n ∈ {n | 0 < n}
m : M
left✝ : m ∈ Set.univ
⊢ hI.dpow n (φ m) ∈ ↑I
Theorem: DividedPowerAlgebra.lift_augIdeal_le
Proof state before:
case intro.intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
n : ℕ
hn : n ∈ {n | 0 < n}
m : M
left✝ : m ∈ Set.univ
⊢ hI.dpow n (φ m) ∈ ↑I
Tactic:
refine hI.dpow_mem (ne_of_gt hn) (hφ m)
Proof state after:
no goals
Theorem: DividedPowerAlgebra.algebraMap_mem_grade_zero
Proof state before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ (algebraMap R (DividedPowerAlgebra R M)) r ∈ grade R M 0
Tactic:
rw [mem_grade_iff]
Proof state after:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ ∃ p ∈ weightedHomogeneousSubmodule R Prod.fst 0, mk p = (algebraMap R (DividedPowerAlgebra R M)) r
Theorem: DividedPowerAlgebra.algebraMap_mem_grade_zero
Proof state before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ ∃ p ∈ weightedHomogeneousSubmodule R Prod.fst 0, mk p = (algebraMap R (DividedPowerAlgebra R M)) r
Tactic:
use C r
Proof state after:
case h
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ C r ∈ weightedHomogeneousSubmodule R Prod.fst 0 ∧ mk (C r) = (algebraMap R (DividedPowerAlgebra R M)) r
Theorem: DividedPowerAlgebra.algebraMap_mem_grade_zero
Proof state before:
case h
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ C r ∈ weightedHomogeneousSubmodule R Prod.fst 0 ∧ mk (C r) = (algebraMap R (DividedPowerAlgebra R M)) r
Tactic:
constructor
Proof state after:
case h.left
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ C r ∈ weightedHomogeneousSubmodule R Prod.fst 0

case h.right
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ mk (C r) = (algebraMap R (DividedPowerAlgebra R M)) r
Theorem: DividedPowerAlgebra.algebraMap_mem_grade_zero
Proof state before:
case h.left
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ C r ∈ weightedHomogeneousSubmodule R Prod.fst 0
Tactic:
simp only [mem_weightedHomogeneousSubmodule]
Proof state after:
case h.left
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ IsWeightedHomogeneous Prod.fst (C r) 0
Theorem: DividedPowerAlgebra.algebraMap_mem_grade_zero
Proof state before:
case h.left
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ IsWeightedHomogeneous Prod.fst (C r) 0
Tactic:
exact isWeightedHomogeneous_C Prod.fst r
Proof state after:
no goals
Theorem: DividedPowerAlgebra.algebraMap_mem_grade_zero
Proof state before:
case h.right
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ mk (C r) = (algebraMap R (DividedPowerAlgebra R M)) r
Tactic:
rw [mk_C]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.grade0Subalgebra_eq_bot
Proof state before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ grade0Subalgebra R M = ⊥
Tactic:
rw [eq_bot_iff]
Proof state after:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ grade0Subalgebra R M ≤ ⊥
Theorem: DividedPowerAlgebra.grade0Subalgebra_eq_bot
Proof state before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ grade0Subalgebra R M ≤ ⊥
Tactic:
intro p hp
Proof state after:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
hp : p ∈ grade0Subalgebra R M
⊢ p ∈ ⊥
Theorem: DividedPowerAlgebra.grade0Subalgebra_eq_bot
Proof state before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
hp : p ∈ grade0Subalgebra R M
⊢ p ∈ ⊥
Tactic:
rw [Algebra.mem_bot]
Proof state after:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
hp : p ∈ grade0Subalgebra R M
⊢ p ∈ Set.range ⇑(algebraMap R (DividedPowerAlgebra R M))
Theorem: DividedPowerAlgebra.grade0Subalgebra_eq_bot
Proof state before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
hp : p ∈ grade0Subalgebra R M
⊢ p ∈ Set.range ⇑(algebraMap R (DividedPowerAlgebra R M))
Tactic:
convert Set.mem_range_self ((algebraMapInv R M) p)
Proof state after:
case h.e'_4
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
hp : p ∈ grade0Subalgebra R M
⊢ p = (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) p)
Theorem: DividedPowerAlgebra.grade0Subalgebra_eq_bot
Proof state before:
case h.e'_4
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
p : DividedPowerAlgebra R M
hp : p ∈ grade0Subalgebra R M
⊢ p = (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) p)
Tactic:
exact (algebraMap_right_inv_of_degree_zero R M ⟨p, hp⟩).symm
Proof state after:
no goals
Theorem: DividedPowerAlgebra.isCompl_augIdeal
Proof state before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ IsAugmentation R (augIdeal R M)
Tactic:
apply IsCompl.mk
Proof state after:
case disjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ Disjoint (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars R (augIdeal R M))

case codisjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ Codisjoint (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars R (augIdeal R M))
Theorem: DividedPowerAlgebra.isCompl_augIdeal
Proof state before:
case disjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ Disjoint (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars R (augIdeal R M))
Tactic:
rw [Submodule.disjoint_def]
Proof state after:
case disjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ ∀ x ∈ Subalgebra.toSubmodule ⊥, x ∈ Submodule.restrictScalars R (augIdeal R M) → x = 0
Theorem: DividedPowerAlgebra.isCompl_augIdeal
Proof state before:
case disjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ ∀ x ∈ Subalgebra.toSubmodule ⊥, x ∈ Submodule.restrictScalars R (augIdeal R M) → x = 0
Tactic:
intro x
Proof state after:
case disjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DividedPowerAlgebra R M
⊢ x ∈ Subalgebra.toSubmodule ⊥ → x ∈ Submodule.restrictScalars R (augIdeal R M) → x = 0
Theorem: DividedPowerAlgebra.isCompl_augIdeal
Proof state before:
case disjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DividedPowerAlgebra R M
⊢ x ∈ Subalgebra.toSubmodule ⊥ → x ∈ Submodule.restrictScalars R (augIdeal R M) → x = 0
Tactic:
simp only [Subalgebra.mem_toSubmodule, Algebra.mem_bot]
Proof state after:
case disjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DividedPowerAlgebra R M
⊢ x ∈ Set.range ⇑(algebraMap R (DividedPowerAlgebra R M)) → x ∈ Submodule.restrictScalars R (augIdeal R M) → x = 0
Theorem: DividedPowerAlgebra.isCompl_augIdeal
Proof state before:
case disjoint
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DividedPowerAlgebra R M
⊢ x ∈ Set.range ⇑(algebraMap R (DividedPowerAlgebra R M)) → x ∈ Submodule.restrictScalars R (augIdeal R M) → x = 0
Tactic:
rintro ⟨r, rfl⟩
Proof state after:
case disjoint.intro
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ (algebraMap R (DividedPowerAlgebra R M)) r ∈ Submodule.restrictScalars R (augIdeal R M) →
    (algebraMap R (DividedPowerAlgebra R M)) r = 0
Theorem: DividedPowerAlgebra.isCompl_augIdeal
Proof state before:
case disjoint.intro
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ (algebraMap R (DividedPowerAlgebra R M)) r ∈ Submodule.restrictScalars R (augIdeal R M) →
    (algebraMap R (DividedPowerAlgebra R M)) r = 0
Tactic:
simp only [Submodule.restrictScalars_mem, mem_augIdeal_iff, AlgHom.commutes,
  Algebra.id.map_eq_id, RingHom.id_apply]
Proof state after:
case disjoint.intro
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
⊢ r = 0 → (algebraMap R (DividedPowerAlgebra R M)) r = 0