internlm/Lean-Github huggingface dataset:
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 (Submodule.restrictScalars A (Subalgebra.toSubmodule ⊥))
      (Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I)) ↔
    IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
Tactic:
suffices Submodule.restrictScalars A (Submodule.restrictScalars S₀ I) =
  Submodule.restrictScalars A I by
  rw [this]
  suffices Submodule.restrictScalars A _ = Subalgebra.toSubmodule S₀ by
    rw [this]
  ext x
  simp only [Submodule.restrictScalars_mem, Subalgebra.mem_toSubmodule]
  apply Algebra.mem_bot_of_subalgebra_iff
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)
⊢ Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) = 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)
⊢ Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) = Submodule.restrictScalars A I
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)
x : S
⊢ x ∈ Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) ↔ x ∈ Submodule.restrictScalars A I
Theorem: DividedPowerAlgebra.roby4.isAugmentation_iff_isCompl
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)
x : S
⊢ x ∈ Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) ↔ x ∈ Submodule.restrictScalars A I
Tactic:
simp only [Submodule.restrictScalars_mem]
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)
this : Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) = 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)
Tactic:
rw [this]
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)
this : Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) = Submodule.restrictScalars A I
⊢ IsCompl (Submodule.restrictScalars A (Subalgebra.toSubmodule ⊥)) (Submodule.restrictScalars A 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)
this : Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) = Submodule.restrictScalars A I
⊢ IsCompl (Submodule.restrictScalars A (Subalgebra.toSubmodule ⊥)) (Submodule.restrictScalars A I) ↔
    IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
Tactic:
suffices Submodule.restrictScalars A _ = Subalgebra.toSubmodule S₀ by
  rw [this]
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)
this : Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) = Submodule.restrictScalars A I
⊢ Submodule.restrictScalars A (Subalgebra.toSubmodule ⊥) = Subalgebra.toSubmodule S₀
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)
this : Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) = Submodule.restrictScalars A I
⊢ Submodule.restrictScalars A (Subalgebra.toSubmodule ⊥) = Subalgebra.toSubmodule 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)
this : Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) = Submodule.restrictScalars A I
x : S
⊢ x ∈ Submodule.restrictScalars A (Subalgebra.toSubmodule ⊥) ↔ x ∈ Subalgebra.toSubmodule S₀
Theorem: DividedPowerAlgebra.roby4.isAugmentation_iff_isCompl
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)
this : Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) = Submodule.restrictScalars A I
x : S
⊢ x ∈ Submodule.restrictScalars A (Subalgebra.toSubmodule ⊥) ↔ x ∈ Subalgebra.toSubmodule S₀
Tactic:
simp only [Submodule.restrictScalars_mem, Subalgebra.mem_toSubmodule]
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)
this : Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) = Submodule.restrictScalars A I
x : S
⊢ x ∈ ⊥ ↔ x ∈ S₀
Theorem: DividedPowerAlgebra.roby4.isAugmentation_iff_isCompl
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)
this : Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) = Submodule.restrictScalars A I
x : S
⊢ x ∈ ⊥ ↔ x ∈ S₀
Tactic:
apply Algebra.mem_bot_of_subalgebra_iff
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)
this✝ : Submodule.restrictScalars A (Submodule.restrictScalars (↥S₀) I) = Submodule.restrictScalars A I
this : Submodule.restrictScalars A ?m.89183 = Subalgebra.toSubmodule S₀
⊢ IsCompl (Submodule.restrictScalars A (Subalgebra.toSubmodule ⊥)) (Submodule.restrictScalars A I) ↔
    IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
Tactic:
rw [this]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.roby4.f_mem_I
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)
p : ↥I →₀ A
⊢ (f A I) p ∈ I
Tactic:
suffices LinearMap.range (f A I) ≤ Submodule.restrictScalars A I by
  apply this
  simp only [LinearMap.mem_range, exists_apply_eq_apply]
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)
p : ↥I →₀ A
⊢ LinearMap.range (f A I) ≤ Submodule.restrictScalars A I
Theorem: DividedPowerAlgebra.roby4.f_mem_I
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)
p : ↥I →₀ A
⊢ LinearMap.range (f A I) ≤ Submodule.restrictScalars A I
Tactic:
simp only [f, Basis.constr_range, Submodule.span_le]
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)
p : ↥I →₀ A
⊢ (Set.range fun i => ↑i) ⊆ ↑(Submodule.restrictScalars A I)
Theorem: DividedPowerAlgebra.roby4.f_mem_I
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)
p : ↥I →₀ A
⊢ (Set.range fun i => ↑i) ⊆ ↑(Submodule.restrictScalars A I)
Tactic:
rintro _ ⟨i, rfl⟩
Proof state after:
case 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)
p : ↥I →₀ A
i : ↥I
⊢ (fun i => ↑i) i ∈ ↑(Submodule.restrictScalars A I)
Theorem: DividedPowerAlgebra.roby4.f_mem_I
Proof state before:
case 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)
p : ↥I →₀ A
i : ↥I
⊢ (fun i => ↑i) i ∈ ↑(Submodule.restrictScalars A I)
Tactic:
simp only [Submodule.coe_restrictScalars, SetLike.mem_coe, SetLike.coe_mem]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.roby4.f_mem_I
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)
p : ↥I →₀ A
this : LinearMap.range (f A I) ≤ Submodule.restrictScalars A I
⊢ (f A I) p ∈ I
Tactic:
apply this
Proof state after:
case a
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)
p : ↥I →₀ A
this : LinearMap.range (f A I) ≤ Submodule.restrictScalars A I
⊢ (f A I) p ∈ LinearMap.range (f A I)
Theorem: DividedPowerAlgebra.roby4.f_mem_I
Proof state before:
case a
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)
p : ↥I →₀ A
this : LinearMap.range (f A I) ≤ Submodule.restrictScalars A I
⊢ (f A I) p ∈ LinearMap.range (f A I)
Tactic:
simp only [LinearMap.mem_range, exists_apply_eq_apply]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.roby4.condτ
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
⊢ Condτ A (dividedPowersBot (MvPolynomial (↥S₀) A)) hM
Tactic:
apply condTFree
Proof state after:
case x
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
⊢ Module.Free A (MvPolynomial (↥S₀) A)

case x
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
⊢ Module.Free A (DividedPowerAlgebra A (↥I →₀ A))
Theorem: DividedPowerAlgebra.roby4.condτ
Proof state before:
case x
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
⊢ Module.Free A (MvPolynomial (↥S₀) A)

case x
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
⊢ Module.Free A (DividedPowerAlgebra A (↥I →₀ A))
Tactic:
infer_instance
Proof state after:
case x
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
⊢ Module.Free A (DividedPowerAlgebra A (↥I →₀ A))
Theorem: DividedPowerAlgebra.roby4.condτ
Proof state before:
case x
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
⊢ Module.Free A (DividedPowerAlgebra A (↥I →₀ A))
Tactic:
infer_instance
Proof state after:
no goals
Theorem: DividedPowerAlgebra.roby4.Ψ_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
i : S
hi : i ∈ I
⊢ (Ψ A S hI S₀) (Algebra.TensorProduct.includeRight ((ι A (↥I →₀ A)) (Finsupp.single ⟨i, hi⟩ 1))) = i
Tactic:
simp [Ψ, Φ, f, Basis.constr_apply]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.roby4.Ψ_surjective
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
⊢ Function.Surjective ⇑(Ψ A S hI S₀)
Tactic:
rw [← Algebra.range_top_iff_surjective _, eq_top_iff]
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
⊢ ⊤ ≤ (Ψ A S hI S₀).range
Theorem: DividedPowerAlgebra.roby4.Ψ_surjective
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
⊢ ⊤ ≤ (Ψ A S hI S₀).range
Tactic:
intro s _
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 : S
a✝ : s ∈ ⊤
⊢ s ∈ (Ψ A S hI S₀).range
Theorem: DividedPowerAlgebra.roby4.Ψ_surjective
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 : 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
Proof 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
Theorem: DividedPowerAlgebra.roby4.Ψ_surjective
Proof 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
Proof 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
Theorem: DividedPowerAlgebra.roby4.Ψ_surjective
Proof 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
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 (X ⟨s₀, hs₀⟩ ⊗ₜ[A] 1) = s₀