internlm/Lean-Github huggingface dataset:
Theorem: DividedPowerAlgebra.T_free_and_D_to_QSplit
Proof state before:
case h.refine_1.mk.disjoint
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
R : Type u := MvPolynomial (↥S₀) A
D : Type u := DividedPowerAlgebra A M
hM : DividedPowers (augIdeal A M)
hM_eq : ∀ (n : ℕ) (x : M), hM.dpow n ((ι A M) x) = dp A n x
hdpM_free : Module.Free A D
hR_free : Module.Free A R
T : Type u := R ⊗[A] D
idK : Ideal T := K A ⊥ (augIdeal A M)
hidK : idK = Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
hK : DividedPowers idK := Exists.choose ⋯
this : MvPolynomial (↥S₀) A →ₐ[A] MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hc :
  Codisjoint (Subalgebra.toSubmodule ⊥)
    (Submodule.restrictScalars (MvPolynomial (↥S₀) A) (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)))
hd : ∀ x ∈ ⊥, x ∈ Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M) → x = 0
⊢ ∀ x ∈ ⊥, x ∈ Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M) → x = 0
Tactic:
intro x hx hx'
Proof state after:
case h.refine_1.mk.disjoint
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
R : Type u := MvPolynomial (↥S₀) A
D : Type u := DividedPowerAlgebra A M
hM : DividedPowers (augIdeal A M)
hM_eq : ∀ (n : ℕ) (x : M), hM.dpow n ((ι A M) x) = dp A n x
hdpM_free : Module.Free A D
hR_free : Module.Free A R
T : Type u := R ⊗[A] D
idK : Ideal T := K A ⊥ (augIdeal A M)
hidK : idK = Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
hK : DividedPowers idK := Exists.choose ⋯
this : MvPolynomial (↥S₀) A →ₐ[A] MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hc :
  Codisjoint (Subalgebra.toSubmodule ⊥)
    (Submodule.restrictScalars (MvPolynomial (↥S₀) A) (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)))
hd : ∀ x ∈ ⊥, x ∈ Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M) → x = 0
x : T
hx : x ∈ ⊥
hx' : x ∈ Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
⊢ x = 0
Theorem: DividedPowerAlgebra.T_free_and_D_to_QSplit
Proof state before:
case h.refine_1.mk.disjoint
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
R : Type u := MvPolynomial (↥S₀) A
D : Type u := DividedPowerAlgebra A M
hM : DividedPowers (augIdeal A M)
hM_eq : ∀ (n : ℕ) (x : M), hM.dpow n ((ι A M) x) = dp A n x
hdpM_free : Module.Free A D
hR_free : Module.Free A R
T : Type u := R ⊗[A] D
idK : Ideal T := K A ⊥ (augIdeal A M)
hidK : idK = Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
hK : DividedPowers idK := Exists.choose ⋯
this : MvPolynomial (↥S₀) A →ₐ[A] MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hc :
  Codisjoint (Subalgebra.toSubmodule ⊥)
    (Submodule.restrictScalars (MvPolynomial (↥S₀) A) (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)))
hd : ∀ x ∈ ⊥, x ∈ Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M) → x = 0
x : T
hx : x ∈ ⊥
hx' : x ∈ Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
⊢ x = 0
Tactic:
refine hd x ?_ hx'
Proof state after:
case h.refine_1.mk.disjoint
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
R : Type u := MvPolynomial (↥S₀) A
D : Type u := DividedPowerAlgebra A M
hM : DividedPowers (augIdeal A M)
hM_eq : ∀ (n : ℕ) (x : M), hM.dpow n ((ι A M) x) = dp A n x
hdpM_free : Module.Free A D
hR_free : Module.Free A R
T : Type u := R ⊗[A] D
idK : Ideal T := K A ⊥ (augIdeal A M)
hidK : idK = Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
hK : DividedPowers idK := Exists.choose ⋯
this : MvPolynomial (↥S₀) A →ₐ[A] MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hc :
  Codisjoint (Subalgebra.toSubmodule ⊥)
    (Submodule.restrictScalars (MvPolynomial (↥S₀) A) (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)))
hd : ∀ x ∈ ⊥, x ∈ Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M) → x = 0
x : T
hx : x ∈ ⊥
hx' : x ∈ Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
⊢ x ∈ ⊥
Theorem: DividedPowerAlgebra.T_free_and_D_to_QSplit
Proof state before:
case h.refine_1.mk.disjoint
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
R : Type u := MvPolynomial (↥S₀) A
D : Type u := DividedPowerAlgebra A M
hM : DividedPowers (augIdeal A M)
hM_eq : ∀ (n : ℕ) (x : M), hM.dpow n ((ι A M) x) = dp A n x
hdpM_free : Module.Free A D
hR_free : Module.Free A R
T : Type u := R ⊗[A] D
idK : Ideal T := K A ⊥ (augIdeal A M)
hidK : idK = Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
hK : DividedPowers idK := Exists.choose ⋯
this : MvPolynomial (↥S₀) A →ₐ[A] MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hc :
  Codisjoint (Subalgebra.toSubmodule ⊥)
    (Submodule.restrictScalars (MvPolynomial (↥S₀) A) (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)))
hd : ∀ x ∈ ⊥, x ∈ Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M) → x = 0
x : T
hx : x ∈ ⊥
hx' : x ∈ Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
⊢ x ∈ ⊥
Tactic:
rw [Algebra.mem_bot] at hx
Proof state after:
case h.refine_1.mk.disjoint
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
R : Type u := MvPolynomial (↥S₀) A
D : Type u := DividedPowerAlgebra A M
hM : DividedPowers (augIdeal A M)
hM_eq : ∀ (n : ℕ) (x : M), hM.dpow n ((ι A M) x) = dp A n x
hdpM_free : Module.Free A D
hR_free : Module.Free A R
T : Type u := R ⊗[A] D
idK : Ideal T := K A ⊥ (augIdeal A M)
hidK : idK = Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
hK : DividedPowers idK := Exists.choose ⋯
this : MvPolynomial (↥S₀) A →ₐ[A] MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hc :
  Codisjoint (Subalgebra.toSubmodule ⊥)
    (Submodule.restrictScalars (MvPolynomial (↥S₀) A) (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)))
hd : ∀ x ∈ ⊥, x ∈ Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M) → x = 0
x : T
hx : x ∈ Set.range ⇑(algebraMap (↥(Subalgebra.restrictScalars A ⊥)) T)
hx' : x ∈ Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
⊢ x ∈ ⊥
Theorem: DividedPowerAlgebra.T_free_and_D_to_QSplit
Proof state before:
case h.refine_1.mk.disjoint.intro.mk.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 : 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
R : Type u := MvPolynomial (↥S₀) A
D : Type u := DividedPowerAlgebra A M
hM : DividedPowers (augIdeal A M)
hM_eq : ∀ (n : ℕ) (x : M), hM.dpow n ((ι A M) x) = dp A n x
hdpM_free : Module.Free A D
hR_free : Module.Free A R
T : Type u := R ⊗[A] D
idK : Ideal T := K A ⊥ (augIdeal A M)
hidK : idK = Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
hK : DividedPowers idK := Exists.choose ⋯
this : MvPolynomial (↥S₀) A →ₐ[A] MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hc :
  Codisjoint (Subalgebra.toSubmodule ⊥)
    (Submodule.restrictScalars (MvPolynomial (↥S₀) A) (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)))
hd : ∀ x ∈ ⊥, x ∈ Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M) → x = 0
x : R
hx : (algebraMap R T) x ∈ Subalgebra.restrictScalars A ⊥
hx' :
  (algebraMap (↥(Subalgebra.restrictScalars A ⊥)) T) ⟨(algebraMap R T) x, hx⟩ ∈
    Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
⊢ (algebraMap (↥(Subalgebra.restrictScalars A ⊥)) T) ⟨(algebraMap R T) x, hx⟩ ∈
    Set.range ⇑(algebraMap (MvPolynomial (↥S₀) A) (MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M))
Tactic:
exact ⟨x, rfl⟩
Proof state after:
no goals
Theorem: DividedPowerAlgebra.T_free_and_D_to_QSplit
Proof state before:
case h.refine_1.mk.codisjoint.intro.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 : 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
R : Type u := MvPolynomial (↥S₀) A
D : Type u := DividedPowerAlgebra A M
hM : DividedPowers (augIdeal A M)
hM_eq : ∀ (n : ℕ) (x : M), hM.dpow n ((ι A M) x) = dp A n x
hdpM_free : Module.Free A D
hR_free : Module.Free A R
T : Type u := R ⊗[A] D
idK : Ideal T := K A ⊥ (augIdeal A M)
hidK : idK = Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
hK : DividedPowers idK := Exists.choose ⋯
this : MvPolynomial (↥S₀) A →ₐ[A] MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hd :
  Disjoint (Subalgebra.toSubmodule ⊥)
    (Submodule.restrictScalars (MvPolynomial (↥S₀) A) (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)))
hc :
  Codisjoint (Subalgebra.toSubmodule ⊥)
    (Submodule.restrictScalars (MvPolynomial (↥S₀) A) (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)))
z : MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hz : z ∈ Submodule.restrictScalars (MvPolynomial (↥S₀) A) (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M))
y : MvPolynomial (↥S₀) A
a✝ : (algebraMap (MvPolynomial (↥S₀) A) (MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M)) y + z ∈ ⊤
⊢ ∃ y_1, (algebraMap R T) y_1 = y ⊗ₜ[A] 1
Tactic:
exact ⟨y, rfl⟩
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
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
R : Type u := MvPolynomial (↥S₀) A
D : Type u := DividedPowerAlgebra A M
hM : DividedPowers (augIdeal A M)
hM_eq : ∀ (n : ℕ) (x : M), hM.dpow n ((ι A M) x) = dp A n x
hdpM_free : Module.Free A D
hR_free : Module.Free A R
T : Type u := R ⊗[A] D
idK : Ideal T := K A ⊥ (augIdeal A M)
hidK : idK = Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
hK : DividedPowers idK := Exists.choose ⋯
this : MvPolynomial (↥S₀) A →ₐ[A] MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
⊢ Ideal.map (Ψ A S hI S₀) idK ≤ I
Tactic:
convert (dpΨ A S hI S₀ condTFree hM hM_eq).ideal_comp
Proof state after:
no goals
Theorem: DividedPowerAlgebra.T_free_and_D_to_QSplit
Proof state before:
case h.left
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
R : Type u := MvPolynomial (↥S₀) A
D : Type u := DividedPowerAlgebra A M
hM : DividedPowers (augIdeal A M)
hM_eq : ∀ (n : ℕ) (x : M), hM.dpow n ((ι A M) x) = dp A n x
hdpM_free : Module.Free A D
hR_free : Module.Free A R
T : Type u := R ⊗[A] D
idK : Ideal T := K A ⊥ (augIdeal A M)
hidK : idK = Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
hK : DividedPowers idK := Exists.choose ⋯
this : MvPolynomial (↥S₀) A →ₐ[A] MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hI_le : Ideal.map (Ψ A S hI S₀) idK ≤ I
⊢ Ideal.map (Ψ A S hI S₀) idK = I
Tactic:
refine le_antisymm hI_le ?_
Proof state after:
case h.left
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
R : Type u := MvPolynomial (↥S₀) A
D : Type u := DividedPowerAlgebra A M
hM : DividedPowers (augIdeal A M)
hM_eq : ∀ (n : ℕ) (x : M), hM.dpow n ((ι A M) x) = dp A n x
hdpM_free : Module.Free A D
hR_free : Module.Free A R
T : Type u := R ⊗[A] D
idK : Ideal T := K A ⊥ (augIdeal A M)
hidK : idK = Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
hK : DividedPowers idK := Exists.choose ⋯
this : MvPolynomial (↥S₀) A →ₐ[A] MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hI_le : Ideal.map (Ψ A S hI S₀) idK ≤ I
⊢ I ≤ Ideal.map (Ψ A S hI S₀) idK
Theorem: DividedPowerAlgebra.T_free_and_D_to_QSplit
Proof state before:
case h.left
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
R : Type u := MvPolynomial (↥S₀) A
D : Type u := DividedPowerAlgebra A M
hM : DividedPowers (augIdeal A M)
hM_eq : ∀ (n : ℕ) (x : M), hM.dpow n ((ι A M) x) = dp A n x
hdpM_free : Module.Free A D
hR_free : Module.Free A R
T : Type u := R ⊗[A] D
idK : Ideal T := K A ⊥ (augIdeal A M)
hidK : idK = Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
hK : DividedPowers idK := Exists.choose ⋯
this : MvPolynomial (↥S₀) A →ₐ[A] MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hI_le : Ideal.map (Ψ A S hI S₀) idK ≤ I
⊢ I ≤ Ideal.map (Ψ A S hI S₀) idK
Tactic:
intro i hi
Proof state after:
case h.left
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
R : Type u := MvPolynomial (↥S₀) A
D : Type u := DividedPowerAlgebra A M
hM : DividedPowers (augIdeal A M)
hM_eq : ∀ (n : ℕ) (x : M), hM.dpow n ((ι A M) x) = dp A n x
hdpM_free : Module.Free A D
hR_free : Module.Free A R
T : Type u := R ⊗[A] D
idK : Ideal T := K A ⊥ (augIdeal A M)
hidK : idK = Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
hK : DividedPowers idK := Exists.choose ⋯
this : MvPolynomial (↥S₀) A →ₐ[A] MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hI_le : Ideal.map (Ψ A S hI S₀) idK ≤ I
i : S
hi : i ∈ I
⊢ i ∈ Ideal.map (Ψ A S hI S₀) idK
Theorem: DividedPowerAlgebra.T_free_and_D_to_QSplit
Proof state before:
case h.left
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
R : Type u := MvPolynomial (↥S₀) A
D : Type u := DividedPowerAlgebra A M
hM : DividedPowers (augIdeal A M)
hM_eq : ∀ (n : ℕ) (x : M), hM.dpow n ((ι A M) x) = dp A n x
hdpM_free : Module.Free A D
hR_free : Module.Free A R
T : Type u := R ⊗[A] D
idK : Ideal T := K A ⊥ (augIdeal A M)
hidK : idK = Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
hK : DividedPowers idK := Exists.choose ⋯
this : MvPolynomial (↥S₀) A →ₐ[A] MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hI_le : Ideal.map (Ψ A S hI S₀) idK ≤ I
i : S
hi : i ∈ I
⊢ i ∈ Ideal.map (Ψ A S hI S₀) idK
Tactic:
rw [← Ψ_eq A S hI S₀ i hi]
Proof state after:
case h.left
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
R : Type u := MvPolynomial (↥S₀) A
D : Type u := DividedPowerAlgebra A M
hM : DividedPowers (augIdeal A M)
hM_eq : ∀ (n : ℕ) (x : M), hM.dpow n ((ι A M) x) = dp A n x
hdpM_free : Module.Free A D
hR_free : Module.Free A R
T : Type u := R ⊗[A] D
idK : Ideal T := K A ⊥ (augIdeal A M)
hidK : idK = Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
hK : DividedPowers idK := Exists.choose ⋯
this : MvPolynomial (↥S₀) A →ₐ[A] MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hI_le : Ideal.map (Ψ A S hI S₀) idK ≤ I
i : S
hi : i ∈ I
⊢ (Ψ A S hI S₀) (Algebra.TensorProduct.includeRight ((ι A (↥I →₀ A)) (Finsupp.single ⟨i, hi⟩ 1))) ∈
    Ideal.map (Ψ A S hI S₀) idK
Theorem: DividedPowerAlgebra.T_free_and_D_to_QSplit
Proof state before:
case h.left
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
R : Type u := MvPolynomial (↥S₀) A
D : Type u := DividedPowerAlgebra A M
hM : DividedPowers (augIdeal A M)
hM_eq : ∀ (n : ℕ) (x : M), hM.dpow n ((ι A M) x) = dp A n x
hdpM_free : Module.Free A D
hR_free : Module.Free A R
T : Type u := R ⊗[A] D
idK : Ideal T := K A ⊥ (augIdeal A M)
hidK : idK = Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
hK : DividedPowers idK := Exists.choose ⋯
this : MvPolynomial (↥S₀) A →ₐ[A] MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hI_le : Ideal.map (Ψ A S hI S₀) idK ≤ I
i : S
hi : i ∈ I
⊢ (Ψ A S hI S₀) (Algebra.TensorProduct.includeRight ((ι A (↥I →₀ A)) (Finsupp.single ⟨i, hi⟩ 1))) ∈
    Ideal.map (Ψ A S hI S₀) idK
Tactic:
apply Ideal.mem_map_of_mem
Proof state after:
case h.left.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 : 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
R : Type u := MvPolynomial (↥S₀) A
D : Type u := DividedPowerAlgebra A M
hM : DividedPowers (augIdeal A M)
hM_eq : ∀ (n : ℕ) (x : M), hM.dpow n ((ι A M) x) = dp A n x
hdpM_free : Module.Free A D
hR_free : Module.Free A R
T : Type u := R ⊗[A] D
idK : Ideal T := K A ⊥ (augIdeal A M)
hidK : idK = Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
hK : DividedPowers idK := Exists.choose ⋯
this : MvPolynomial (↥S₀) A →ₐ[A] MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hI_le : Ideal.map (Ψ A S hI S₀) idK ≤ I
i : S
hi : i ∈ I
⊢ Algebra.TensorProduct.includeRight ((ι A (↥I →₀ A)) (Finsupp.single ⟨i, hi⟩ 1)) ∈ idK