Theorem: DividedPowerAlgebra.roby4.Ψ_surjective (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
⊢ Function.Surjective ⇑(Ψ A S hI S₀)
Tactic:
rw [← Algebra.range_top_iff_surjective _, eq_top_iff]
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
⊢ ⊤ ≤ (Ψ A S hI S₀).range

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
⊢ ⊤ ≤ (Ψ A S hI S₀).range
Tactic:
intro s _
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 : S
a✝ : s ∈ ⊤
⊢ s ∈ (Ψ A S hI S₀).range

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 : S
a✝ : s ∈ ⊤
⊢ s ∈ (Ψ A S hI S₀).range
Tactic:
obtain ⟨s₀, hs₀, s₁, hs₁, rfl⟩ := Submodule.exists_add_eq_of_codisjoint (hIS₀.codisjoint) s
State after:
case intro.intro.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)
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₀ + s₁ ∈ (Ψ A S hI S₀).range

State before:
case intro.intro.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)
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₀ + s₁ ∈ (Ψ A S hI S₀).range
Tactic:
apply Subalgebra.add_mem
State after:
case intro.intro.intro.intro.hx
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

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

State before:
case intro.intro.intro.intro.hx
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 (X ⟨s₀, hs₀⟩) ⊗ₜ[A] 1
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 (X ⟨s₀, hs₀⟩ ⊗ₜ[A] 1) = 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
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]
State after:
no goals

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

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

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