internlm/Lean-Github huggingface dataset:
Theorem: DividedPowerAlgebra.cond_D_uniqueness
Proof state before:
case left
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
s : S
⊢ s ∈ ⇑↑(lift hJ f hf) '' Set.image2 (dp R) {n | 0 < n} Set.univ → s ∈ ↑J
Tactic:
rintro ⟨a, ⟨n, hn : 0 < n, m, _, rfl⟩, rfl⟩
Proof state after:
case left.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
hn : 0 < n
m : M
left✝ : m ∈ Set.univ
⊢ ↑(lift hJ f hf) (dp R n m) ∈ ↑J
Theorem: DividedPowerAlgebra.cond_D_uniqueness
Proof state before:
case left.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
hn : 0 < n
m : M
left✝ : m ∈ Set.univ
⊢ ↑(lift hJ f hf) (dp R n m) ∈ ↑J
Tactic:
simp only [AlgHom.coe_toRingHom, SetLike.mem_coe]
Proof state after:
case left.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
hn : 0 < n
m : M
left✝ : m ∈ Set.univ
⊢ (lift hJ f hf) (dp R n m) ∈ J
Theorem: DividedPowerAlgebra.cond_D_uniqueness
Proof state before:
case left.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
hn : 0 < n
m : M
left✝ : m ∈ Set.univ
⊢ (lift hJ f hf) (dp R n m) ∈ J
Tactic:
rw [liftAlgHom_apply_dp]
Proof state after:
case left.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
hn : 0 < n
m : M
left✝ : m ∈ Set.univ
⊢ hJ.dpow n (f m) ∈ J
Theorem: DividedPowerAlgebra.cond_D_uniqueness
Proof state before:
case left.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
hn : 0 < n
m : M
left✝ : m ∈ Set.univ
⊢ hJ.dpow n (f m) ∈ J
Tactic:
apply hJ.dpow_mem (ne_of_gt hn) (hf m)
Proof state after:
no goals
Theorem: DividedPowerAlgebra.cond_D_uniqueness
Proof state before:
case right
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
⊢ ∀ (n : ℕ), ∀ a ∈ augIdeal R M, hJ.dpow n (↑(lift hJ f hf) a) = ↑(lift hJ f hf) (h.dpow n a)
Tactic:
intro n a ha
Proof state after:
case right
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
⊢ hJ.dpow n (↑(lift hJ f hf) a) = ↑(lift hJ f hf) (h.dpow n a)
Theorem: DividedPowerAlgebra.cond_D_uniqueness
Proof state before:
case right
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
⊢ hJ.dpow n (↑(lift hJ f hf) a) = ↑(lift hJ f hf) (h.dpow n a)
Tactic:
apply symm
Proof state after:
case right.a
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
⊢ ↑(lift hJ f hf) (h.dpow n a) = hJ.dpow n (↑(lift hJ f hf) a)
Theorem: DividedPowerAlgebra.cond_D_uniqueness
Proof state before:
case right.a
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
⊢ ↑(lift hJ f hf) (h.dpow n a) = hJ.dpow n (↑(lift hJ f hf) a)
Tactic:
rw [(dp_uniqueness h hJ (lift hJ f hf) (augIdeal_eq_span R M) _ _) n a ha]
Proof state after:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
⊢ ∀ s ∈ Set.image2 (dp R) {n | 0 < n} Set.univ, ↑(lift hJ f hf) s ∈ J

R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
⊢ ∀ (n : ℕ), ∀ a ∈ Set.image2 (dp R) {n | 0 < n} Set.univ, ↑(lift hJ f hf) (h.dpow n a) = hJ.dpow n (↑(lift hJ f hf) a)
Theorem: DividedPowerAlgebra.cond_D_uniqueness
Proof state before:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
⊢ ∀ s ∈ Set.image2 (dp R) {n | 0 < n} Set.univ, ↑(lift hJ f hf) s ∈ J
Tactic:
rintro a ⟨q, hq : 0 < q, m, _, rfl⟩
Proof state after:
case intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ ↑(lift hJ f hf) (dp R q m) ∈ J
Theorem: DividedPowerAlgebra.cond_D_uniqueness
Proof state before:
case intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ ↑(lift hJ f hf) (dp R q m) ∈ J
Tactic:
simp only [AlgHom.coe_toRingHom, liftAlgHom_apply_dp]
Proof state after:
case intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ hJ.dpow q (f m) ∈ J
Theorem: DividedPowerAlgebra.cond_D_uniqueness
Proof state before:
case intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ hJ.dpow q (f m) ∈ J
Tactic:
exact hJ.dpow_mem (ne_of_gt hq) (hf m)
Proof state after:
no goals
Theorem: DividedPowerAlgebra.cond_D_uniqueness
Proof state before:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
⊢ ∀ (n : ℕ), ∀ a ∈ Set.image2 (dp R) {n | 0 < n} Set.univ, ↑(lift hJ f hf) (h.dpow n a) = hJ.dpow n (↑(lift hJ f hf) a)
Tactic:
rintro n a ⟨q, hq : 0 < q, m, _, rfl⟩
Proof state after:
case intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n✝ : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ ↑(lift hJ f hf) (h.dpow n (dp R q m)) = hJ.dpow n (↑(lift hJ f hf) (dp R q m))
Theorem: DividedPowerAlgebra.cond_D_uniqueness
Proof state before:
case intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n✝ : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ ↑(lift hJ f hf) (h.dpow n (dp R q m)) = hJ.dpow n (↑(lift hJ f hf) (dp R q m))
Tactic:
simp only [AlgHom.coe_toRingHom, liftAlgHom_apply_dp]
Proof state after:
case intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n✝ : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ (lift hJ f hf) (h.dpow n (dp R q m)) = hJ.dpow n (hJ.dpow q (f m))
Theorem: DividedPowerAlgebra.cond_D_uniqueness
Proof state before:
case intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n✝ : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ (lift hJ f hf) (h.dpow n (dp R q m)) = hJ.dpow n (hJ.dpow q (f m))
Tactic:
rw [hJ.dpow_comp n (ne_of_gt hq) (hf m),← hh q m,
  h.dpow_comp n (ne_of_gt hq) (ι_mem_augIdeal R M m), _root_.map_mul, map_natCast]
Proof state after:
case intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n✝ : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ ↑(mchoose n q) * (lift hJ f hf) (h.dpow (n * q) ((ι R M) m)) = ↑(mchoose n q) * hJ.dpow (n * q) (f m)
Theorem: DividedPowerAlgebra.cond_D_uniqueness
Proof state before:
case intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n✝ : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ ↑(mchoose n q) * (lift hJ f hf) (h.dpow (n * q) ((ι R M) m)) = ↑(mchoose n q) * hJ.dpow (n * q) (f m)
Tactic:
apply congr_arg₂ _ rfl
Proof state after:
case intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n✝ : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ (lift hJ f hf) (h.dpow (n * q) ((ι R M) m)) = hJ.dpow (n * q) (f m)
Theorem: DividedPowerAlgebra.cond_D_uniqueness
Proof state before:
case intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n✝ : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ (lift hJ f hf) (h.dpow (n * q) ((ι R M) m)) = hJ.dpow (n * q) (f m)
Tactic:
rw [hh]
Proof state after:
case intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n✝ : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ (lift hJ f hf) (dp R (n * q) m) = hJ.dpow (n * q) (f m)
Theorem: DividedPowerAlgebra.cond_D_uniqueness
Proof state before:
case intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n✝ : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ (lift hJ f hf) (dp R (n * q) m) = hJ.dpow (n * q) (f m)
Tactic:
rw [liftAlgHom_apply_dp]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.roby4.Algebra.mem_bot_of_subalgebra_iff
Proof state before:
R✝ : Type u
inst✝⁷ : CommRing R✝
A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : DecidableEq A
S✝ : Type u
inst✝⁴ : CommRing S✝
inst✝³ : Algebra A S✝
I : Ideal S✝
hI : DividedPowers I
S₀✝ : Subalgebra A S✝
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀✝) (Submodule.restrictScalars A I)
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
s : S
⊢ s ∈ ⊥ ↔ s ∈ S₀
Tactic:
simp only [Algebra.mem_bot, Set.mem_range, Subtype.exists]
Proof state after:
R✝ : Type u
inst✝⁷ : CommRing R✝
A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : DecidableEq A
S✝ : Type u
inst✝⁴ : CommRing S✝
inst✝³ : Algebra A S✝
I : Ideal S✝
hI : DividedPowers I
S₀✝ : Subalgebra A S✝
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀✝) (Submodule.restrictScalars A I)
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
s : S
⊢ (∃ a, ∃ (b : a ∈ S₀), (algebraMap (↥S₀) S) ⟨a, b⟩ = s) ↔ s ∈ S₀
Theorem: DividedPowerAlgebra.roby4.Algebra.mem_bot_of_subalgebra_iff
Proof state before:
R✝ : Type u
inst✝⁷ : CommRing R✝
A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : DecidableEq A
S✝ : Type u
inst✝⁴ : CommRing S✝
inst✝³ : Algebra A S✝
I : Ideal S✝
hI : DividedPowers I
S₀✝ : Subalgebra A S✝
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀✝) (Submodule.restrictScalars A I)
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
s : S
⊢ (∃ a, ∃ (b : a ∈ S₀), (algebraMap (↥S₀) S) ⟨a, b⟩ = s) ↔ s ∈ S₀
Tactic:
constructor
Proof state after:
case mp
R✝ : Type u
inst✝⁷ : CommRing R✝
A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : DecidableEq A
S✝ : Type u
inst✝⁴ : CommRing S✝
inst✝³ : Algebra A S✝
I : Ideal S✝
hI : DividedPowers I
S₀✝ : Subalgebra A S✝
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀✝) (Submodule.restrictScalars A I)
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
s : S
⊢ (∃ a, ∃ (b : a ∈ S₀), (algebraMap (↥S₀) S) ⟨a, b⟩ = s) → s ∈ S₀

case mpr
R✝ : Type u
inst✝⁷ : CommRing R✝
A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : DecidableEq A
S✝ : Type u
inst✝⁴ : CommRing S✝
inst✝³ : Algebra A S✝
I : Ideal S✝
hI : DividedPowers I
S₀✝ : Subalgebra A S✝
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀✝) (Submodule.restrictScalars A I)
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
s : S
⊢ s ∈ S₀ → ∃ a, ∃ (b : a ∈ S₀), (algebraMap (↥S₀) S) ⟨a, b⟩ = s
Theorem: DividedPowerAlgebra.roby4.Algebra.mem_bot_of_subalgebra_iff
Proof state before:
case mp
R✝ : Type u
inst✝⁷ : CommRing R✝
A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : DecidableEq A
S✝ : Type u
inst✝⁴ : CommRing S✝
inst✝³ : Algebra A S✝
I : Ideal S✝
hI : DividedPowers I
S₀✝ : Subalgebra A S✝
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀✝) (Submodule.restrictScalars A I)
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
s : S
⊢ (∃ a, ∃ (b : a ∈ S₀), (algebraMap (↥S₀) S) ⟨a, b⟩ = s) → s ∈ S₀
Tactic:
rintro ⟨s, hs, rfl⟩
Proof state after:
case mp.intro.intro
R✝ : Type u
inst✝⁷ : CommRing R✝
A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : DecidableEq A
S✝ : Type u
inst✝⁴ : CommRing S✝
inst✝³ : Algebra A S✝
I : Ideal S✝
hI : DividedPowers I
S₀✝ : Subalgebra A S✝
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀✝) (Submodule.restrictScalars A I)
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
s : S
hs : s ∈ S₀
⊢ (algebraMap (↥S₀) S) ⟨s, hs⟩ ∈ S₀
Theorem: DividedPowerAlgebra.roby4.Algebra.mem_bot_of_subalgebra_iff
Proof state before:
case mp.intro.intro
R✝ : Type u
inst✝⁷ : CommRing R✝
A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : DecidableEq A
S✝ : Type u
inst✝⁴ : CommRing S✝
inst✝³ : Algebra A S✝
I : Ideal S✝
hI : DividedPowers I
S₀✝ : Subalgebra A S✝
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀✝) (Submodule.restrictScalars A I)
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
s : S
hs : s ∈ S₀
⊢ (algebraMap (↥S₀) S) ⟨s, hs⟩ ∈ S₀
Tactic:
exact hs
Proof state after:
no goals
Theorem: DividedPowerAlgebra.roby4.Algebra.mem_bot_of_subalgebra_iff
Proof state before:
case mpr
R✝ : Type u
inst✝⁷ : CommRing R✝
A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : DecidableEq A
S✝ : Type u
inst✝⁴ : CommRing S✝
inst✝³ : Algebra A S✝
I : Ideal S✝
hI : DividedPowers I
S₀✝ : Subalgebra A S✝
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀✝) (Submodule.restrictScalars A I)
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
s : S
⊢ s ∈ S₀ → ∃ a, ∃ (b : a ∈ S₀), (algebraMap (↥S₀) S) ⟨a, b⟩ = s
Tactic:
intro hs
Proof state after:
case mpr
R✝ : Type u
inst✝⁷ : CommRing R✝
A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : DecidableEq A
S✝ : Type u
inst✝⁴ : CommRing S✝
inst✝³ : Algebra A S✝
I : Ideal S✝
hI : DividedPowers I
S₀✝ : Subalgebra A S✝
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀✝) (Submodule.restrictScalars A I)
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
s : S
hs : s ∈ S₀
⊢ ∃ a, ∃ (b : a ∈ S₀), (algebraMap (↥S₀) S) ⟨a, b⟩ = s
Theorem: DividedPowerAlgebra.roby4.Algebra.mem_bot_of_subalgebra_iff
Proof state before:
case mpr
R✝ : Type u
inst✝⁷ : CommRing R✝
A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : DecidableEq A
S✝ : Type u
inst✝⁴ : CommRing S✝
inst✝³ : Algebra A S✝
I : Ideal S✝
hI : DividedPowers I
S₀✝ : Subalgebra A S✝
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀✝) (Submodule.restrictScalars A I)
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
S₀ : Subalgebra R S
s : S
hs : s ∈ S₀
⊢ ∃ a, ∃ (b : a ∈ S₀), (algebraMap (↥S₀) S) ⟨a, b⟩ = s
Tactic:
exact ⟨s, hs, rfl⟩
Proof state after:
no goals
Theorem: DividedPowerAlgebra.roby4.isAugmentation_iff_isCompl
Proof state before:
R : Type u
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
⊢ IsAugmentation (↥S₀) I ↔ IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
Tactic:
unfold IsAugmentation
Proof state after:
R : Type u
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
⊢ IsCompl (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars (↥S₀) I) ↔
    IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
Theorem: DividedPowerAlgebra.roby4.isAugmentation_iff_isCompl
Proof state before:
R : Type u
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
⊢ IsCompl (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars (↥S₀) I) ↔
    IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
Tactic:
rw [← Submodule.isCompl_restrictScalars_iff A]
Proof state after:
R : Type u
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
⊢ IsCompl (Submodule.restrictScalars A (Subalgebra.toSubmodule ⊥))
      (Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I)) ↔
    IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)