internlm/Lean-Github huggingface dataset:
Theorem: DividedPowerAlgebra.roby4.Ψ_surjective
Proof state before:
case h
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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
s₀ : S
hs₀ : s₀ ∈ Subalgebra.toSubmodule S₀
s₁ : S
hs₁ : s₁ ∈ Submodule.restrictScalars A I
a✝ : s₀ + s₁ ∈ ⊤
⊢ (Ψ A S hI S₀).toRingHom (X ⟨s₀, hs₀⟩ ⊗ₜ[A] 1) = s₀
Tactic:
simp only [Ψ, AlgHom.toRingHom_eq_coe, RingHom.coe_coe,
  Algebra.TensorProduct.productMap_apply_tmul, AlgHom.coe_comp, Subalgebra.coe_val,
  IsScalarTower.coe_toAlgHom', algebraMap_eq, Function.comp_apply, aeval_X, id_eq, map_one,
  mul_one]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.roby4.Ψ_surjective
Proof state before:
case intro.intro.intro.intro.hy
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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
s₀ : S
hs₀ : s₀ ∈ Subalgebra.toSubmodule S₀
s₁ : S
hs₁ : s₁ ∈ Submodule.restrictScalars A I
a✝ : s₀ + s₁ ∈ ⊤
⊢ s₁ ∈ (Ψ A S hI S₀).range
Tactic:
use 1 ⊗ₜ[A] (ι A _ (Finsupp.single ⟨s₁, hs₁⟩ 1))
Proof state after:
case h
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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
s₀ : S
hs₀ : s₀ ∈ Subalgebra.toSubmodule S₀
s₁ : S
hs₁ : s₁ ∈ Submodule.restrictScalars A I
a✝ : s₀ + s₁ ∈ ⊤
⊢ (Ψ A S hI S₀).toRingHom (1 ⊗ₜ[A] (ι A (↥I →₀ A)) (Finsupp.single ⟨s₁, hs₁⟩ 1)) = s₁
Theorem: DividedPowerAlgebra.roby4.Ψ_surjective
Proof state before:
case h
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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
s₀ : S
hs₀ : s₀ ∈ Subalgebra.toSubmodule S₀
s₁ : S
hs₁ : s₁ ∈ Submodule.restrictScalars A I
a✝ : s₀ + s₁ ∈ ⊤
⊢ (Ψ A S hI S₀).toRingHom (1 ⊗ₜ[A] (ι A (↥I →₀ A)) (Finsupp.single ⟨s₁, hs₁⟩ 1)) = s₁
Tactic:
simp only [Ψ, Φ, f, AlgHom.toRingHom_eq_coe, RingHom.coe_coe,
  Algebra.TensorProduct.productMap_apply_tmul, map_one, lift_ι_apply, one_mul]
Proof state after:
case h
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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
s₀ : S
hs₀ : s₀ ∈ Subalgebra.toSubmodule S₀
s₁ : S
hs₁ : s₁ ∈ Submodule.restrictScalars A I
a✝ : s₀ + s₁ ∈ ⊤
⊢ ((Finsupp.basisSingleOne.constr A) fun i => ↑i) (Finsupp.single ⟨s₁, hs₁⟩ 1) = s₁
Theorem: DividedPowerAlgebra.roby4.Ψ_surjective
Proof state before:
case h
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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
s₀ : S
hs₀ : s₀ ∈ Subalgebra.toSubmodule S₀
s₁ : S
hs₁ : s₁ ∈ Submodule.restrictScalars A I
a✝ : s₀ + s₁ ∈ ⊤
⊢ ((Finsupp.basisSingleOne.constr A) fun i => ↑i) (Finsupp.single ⟨s₁, hs₁⟩ 1) = s₁
Tactic:
simp only [Basis.constr_apply, Finsupp.basisSingleOne_repr, LinearEquiv.refl_apply, zero_smul,
  Finsupp.sum_single_index, one_smul]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.roby4.Ψ_map_eq
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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
⊢ Subalgebra.map (Ψ A S hI S₀) (Subalgebra.restrictScalars A ⊥) = S₀
Tactic:
ext x
Proof state after:
case h
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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
x : S
⊢ x ∈ Subalgebra.map (Ψ A S hI S₀) (Subalgebra.restrictScalars A ⊥) ↔ x ∈ S₀
Theorem: DividedPowerAlgebra.roby4.Ψ_map_eq
Proof state before:
case h
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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
x : S
⊢ x ∈ Subalgebra.map (Ψ A S hI S₀) (Subalgebra.restrictScalars A ⊥) ↔ x ∈ S₀
Tactic:
simp only [Subalgebra.mem_map, Subalgebra.mem_restrictScalars]
Proof state after:
case h
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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
x : S
⊢ (∃ x_1 ∈ ⊥, (Ψ A S hI S₀) x_1 = x) ↔ x ∈ S₀
Theorem: DividedPowerAlgebra.roby4.Ψ_map_eq
Proof state before:
case h
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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
x : S
⊢ (∃ x_1 ∈ ⊥, (Ψ A S hI S₀) x_1 = x) ↔ x ∈ S₀
Tactic:
simp only [Algebra.mem_bot, Set.mem_range, Algebra.TensorProduct.algebraMap_apply,
  Algebra.id.map_eq_id, RingHom.id_apply, exists_exists_eq_and]
Proof state after:
case h
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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
x : S
⊢ (∃ a, (Ψ A S hI S₀) (a ⊗ₜ[A] 1) = x) ↔ x ∈ S₀
Theorem: DividedPowerAlgebra.roby4.Ψ_map_eq
Proof state before:
case h
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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
x : S
⊢ (∃ a, (Ψ A S hI S₀) (a ⊗ₜ[A] 1) = x) ↔ x ∈ S₀
Tactic:
constructor
Proof state after:
case h.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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
x : S
⊢ (∃ a, (Ψ A S hI S₀) (a ⊗ₜ[A] 1) = x) → x ∈ S₀

case h.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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
x : S
⊢ x ∈ S₀ → ∃ a, (Ψ A S hI S₀) (a ⊗ₜ[A] 1) = x
Theorem: DividedPowerAlgebra.roby4.Ψ_map_eq
Proof state before:
case h.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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
x : S
⊢ (∃ a, (Ψ A S hI S₀) (a ⊗ₜ[A] 1) = x) → x ∈ S₀
Tactic:
rintro ⟨p, rfl⟩
Proof state after:
case h.mp.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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
p : MvPolynomial (↥S₀) A
⊢ (Ψ A S hI S₀) (p ⊗ₜ[A] 1) ∈ S₀
Theorem: DividedPowerAlgebra.roby4.Ψ_map_eq
Proof state before:
case h.mp.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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
p : MvPolynomial (↥S₀) A
⊢ (Ψ A S hI S₀) (p ⊗ₜ[A] 1) ∈ S₀
Tactic:
simp only [Ψ, Algebra.TensorProduct.productMap_apply_tmul, AlgHom.coe_comp, Subalgebra.coe_val,
  IsScalarTower.coe_toAlgHom', Function.comp_apply, map_one, mul_one, SetLike.coe_mem]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.roby4.Ψ_map_eq
Proof state before:
case h.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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
x : S
⊢ x ∈ S₀ → ∃ a, (Ψ A S hI S₀) (a ⊗ₜ[A] 1) = x
Tactic:
intro hx
Proof state after:
case h.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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
x : S
hx : x ∈ S₀
⊢ ∃ a, (Ψ A S hI S₀) (a ⊗ₜ[A] 1) = x
Theorem: DividedPowerAlgebra.roby4.Ψ_map_eq
Proof state before:
case h.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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
x : S
hx : x ∈ S₀
⊢ ∃ a, (Ψ A S hI S₀) (a ⊗ₜ[A] 1) = x
Tactic:
use MvPolynomial.X ⟨x, hx⟩
Proof state after:
case h
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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
x : S
hx : x ∈ S₀
⊢ (Ψ A S hI S₀) (X ⟨x, hx⟩ ⊗ₜ[A] 1) = x
Theorem: DividedPowerAlgebra.roby4.Ψ_map_eq
Proof state before:
case h
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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
x : S
hx : x ∈ S₀
⊢ (Ψ A S hI S₀) (X ⟨x, hx⟩ ⊗ₜ[A] 1) = x
Tactic:
simp only [Ψ, Algebra.TensorProduct.productMap_apply_tmul, AlgHom.coe_comp, Subalgebra.coe_val,
  IsScalarTower.coe_toAlgHom', Function.comp_apply, map_one, mul_one]
Proof state after:
case h
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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
x : S
hx : x ∈ S₀
⊢ ↑((algebraMap (MvPolynomial (↥S₀) A) ↥S₀) (X ⟨x, hx⟩)) = x
Theorem: DividedPowerAlgebra.roby4.Ψ_map_eq
Proof state before:
case h
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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
x : S
hx : x ∈ S₀
⊢ ↑((algebraMap (MvPolynomial (↥S₀) A) ↥S₀) (X ⟨x, hx⟩)) = x
Tactic:
rw [algebraMap_eq]
Proof state after:
case h
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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
x : S
hx : x ∈ S₀
⊢ ↑((aeval id).toRingHom (X ⟨x, hx⟩)) = x
Theorem: DividedPowerAlgebra.roby4.Ψ_map_eq
Proof state before:
case h
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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
x : S
hx : x ∈ S₀
⊢ ↑((aeval id).toRingHom (X ⟨x, hx⟩)) = x
Tactic:
simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, aeval_X, id_eq]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.roby4.K_eq_span
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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
⊢ K A ⊥ (augIdeal A (↥I →₀ A)) = span (Set.image2 (fun n a => 1 ⊗ₜ[A] dp A n a) {n | 0 < n} Set.univ)
Tactic:
simp [K, i1, i2]
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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
⊢ Ideal.map Algebra.TensorProduct.includeRight (augIdeal A (↥I →₀ A)) =
    span (Set.image2 (fun n a => 1 ⊗ₜ[A] dp A n a) {n | 0 < n} Set.univ)
Theorem: DividedPowerAlgebra.roby4.K_eq_span
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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
⊢ Ideal.map Algebra.TensorProduct.includeRight (augIdeal A (↥I →₀ A)) =
    span (Set.image2 (fun n a => 1 ⊗ₜ[A] dp A n a) {n | 0 < n} Set.univ)
Tactic:
rw [augIdeal_eq_span, Ideal.map_span]
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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
⊢ span (⇑Algebra.TensorProduct.includeRight '' Set.image2 (dp A) {n | 0 < n} Set.univ) =
    span (Set.image2 (fun n a => 1 ⊗ₜ[A] dp A n a) {n | 0 < n} Set.univ)
Theorem: DividedPowerAlgebra.roby4.K_eq_span
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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
⊢ span (⇑Algebra.TensorProduct.includeRight '' Set.image2 (dp A) {n | 0 < n} Set.univ) =
    span (Set.image2 (fun n a => 1 ⊗ₜ[A] dp A n a) {n | 0 < n} Set.univ)
Tactic:
simp only [Algebra.TensorProduct.includeRight_apply, Set.image_image2]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.T_free_and_D_to_QSplit
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)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
⊢ CondQSplit A
Tactic:
intro S _ _ I hI S₀ hIS₀
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✝)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I✝ →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I✝ →₀ A), hM.dpow n ((ι A (↥I✝ →₀ A)) x) = dp A n x
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsAugmentation (↥S₀) I
⊢ ∃ T x x_1 J hJ T₀,
    ∃ (_ : IsAugmentation (↥T₀) J),
      ∃ f,
        Ideal.map f J = I ∧ Subalgebra.map f T₀ = S₀ ∧ Function.Surjective ⇑f ∧ hJ.isDPMorphism hI ↑f ∧ Module.Free A T
Theorem: DividedPowerAlgebra.T_free_and_D_to_QSplit
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✝)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I✝ →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I✝ →₀ A), hM.dpow n ((ι A (↥I✝ →₀ A)) x) = dp A n x
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsAugmentation (↥S₀) I
⊢ ∃ T x x_1 J hJ T₀,
    ∃ (_ : IsAugmentation (↥T₀) J),
      ∃ f,
        Ideal.map f J = I ∧ Subalgebra.map f T₀ = S₀ ∧ Function.Surjective ⇑f ∧ hJ.isDPMorphism hI ↑f ∧ Module.Free A T
Tactic:
let M := I →₀ 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✝)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I✝ →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I✝ →₀ A), hM.dpow n ((ι A (↥I✝ →₀ A)) x) = dp A n x
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsAugmentation (↥S₀) I
M : Type u := ↥I →₀ A
⊢ ∃ T x x_1 J hJ T₀,
    ∃ (_ : IsAugmentation (↥T₀) J),
      ∃ f,
        Ideal.map f J = I ∧ Subalgebra.map f T₀ = S₀ ∧ Function.Surjective ⇑f ∧ hJ.isDPMorphism hI ↑f ∧ Module.Free A T