Theorem: DividedPowerAlgebra.roby4.Ψ_map_eq (DividedPowers/DPAlgebra/Dpow.lean)

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
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₀

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]
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₀

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]
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₀

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
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

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⟩
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₀

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]
State after:
no goals

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
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

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⟩
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

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]
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

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]
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

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]
State after:
no goals