Theorem: DividedPowerAlgebra.T_free_and_D_to_QSplit (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
⊢ CondQSplit A
Tactic:
intro S _ _ I hI S₀ hIS₀
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

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

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
⊢ ∃ 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 R := MvPolynomial S₀ A
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
R : Type u := MvPolynomial (↥S₀) 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

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
⊢ ∃ 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 D := DividedPowerAlgebra A M
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
R : Type u := MvPolynomial (↥S₀) A
D : Type u := DividedPowerAlgebra A M
⊢ ∃ 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

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
⊢ ∃ 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:
obtain ⟨hM, hM_eq⟩ := condD M
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✝)
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
⊢ ∃ 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

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✝)
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
⊢ ∃ 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:
haveI hdpM_free : Module.Free A D := DividedPowerAlgebra.toModule_free A M
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✝)
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
⊢ ∃ 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

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✝)
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
⊢ ∃ 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:
haveI hR_free : Module.Free A R :=
  Module.Free.of_basis (MvPolynomial.basisMonomials _ _)
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✝)
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 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

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✝)
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 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 T := R ⊗[A] D
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✝)
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
⊢ ∃ 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

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✝)
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
⊢ ∃ 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:
use T, by infer_instance, by infer_instance
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 : 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
⊢ ∃ 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

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 : 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
⊢ ∃ 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 idK : Ideal T := K A ⊥ (augIdeal A M)
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 : 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)
⊢ ∃ 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

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 : 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)
⊢ ∃ 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:
have hidK : idK = Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M) := by
  simp only [K, Ideal.map_bot, i2, ge_iff_le, bot_le, sup_of_le_right, idK]
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 : 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)
⊢ ∃ 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

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 : 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)
⊢ ∃ 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:
use idK
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 : 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)
⊢ ∃ hJ T₀,
    ∃ (_ : IsAugmentation (↥T₀) idK),
      ∃ f,
        Ideal.map f idK = I ∧
          Subalgebra.map f T₀ = S₀ ∧ Function.Surjective ⇑f ∧ hJ.isDPMorphism hI ↑f ∧ Module.Free A T

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 : 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)
⊢ ∃ hJ T₀,
    ∃ (_ : IsAugmentation (↥T₀) idK),
      ∃ f,
        Ideal.map f idK = I ∧
          Subalgebra.map f T₀ = S₀ ∧ Function.Surjective ⇑f ∧ hJ.isDPMorphism hI ↑f ∧ Module.Free A T
Tactic:
let hK : DividedPowers idK := (condτ A S I S₀ condTFree hM).choose
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 : 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 ⋯
⊢ ∃ hJ T₀,
    ∃ (_ : IsAugmentation (↥T₀) idK),
      ∃ f,
        Ideal.map f idK = I ∧
          Subalgebra.map f T₀ = S₀ ∧ Function.Surjective ⇑f ∧ hJ.isDPMorphism hI ↑f ∧ Module.Free A T

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 : 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 ⋯
⊢ ∃ hJ T₀,
    ∃ (_ : IsAugmentation (↥T₀) idK),
      ∃ f,
        Ideal.map f idK = I ∧
          Subalgebra.map f T₀ = S₀ ∧ Function.Surjective ⇑f ∧ hJ.isDPMorphism hI ↑f ∧ Module.Free A T
Tactic:
use hK
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 : 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 ⋯
⊢ ∃ T₀,
    ∃ (_ : IsAugmentation (↥T₀) idK),
      ∃ f,
        Ideal.map f idK = I ∧
          Subalgebra.map f T₀ = S₀ ∧ Function.Surjective ⇑f ∧ hK.isDPMorphism hI ↑f ∧ Module.Free A T

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 : 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 ⋯
⊢ ∃ T₀,
    ∃ (_ : IsAugmentation (↥T₀) idK),
      ∃ f,
        Ideal.map f idK = I ∧
          Subalgebra.map f T₀ = S₀ ∧ Function.Surjective ⇑f ∧ hK.isDPMorphism hI ↑f ∧ Module.Free A T
Tactic:
have : MvPolynomial S₀ A →ₐ[A] MvPolynomial S₀ A ⊗[A] DividedPowerAlgebra A M := by
  apply Algebra.TensorProduct.includeLeft
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 : 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
⊢ ∃ T₀,
    ∃ (_ : IsAugmentation (↥T₀) idK),
      ∃ f,
        Ideal.map f idK = I ∧
          Subalgebra.map f T₀ = S₀ ∧ Function.Surjective ⇑f ∧ hK.isDPMorphism hI ↑f ∧ Module.Free A T

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 : 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
⊢ ∃ T₀,
    ∃ (_ : IsAugmentation (↥T₀) idK),
      ∃ f,
        Ideal.map f idK = I ∧
          Subalgebra.map f T₀ = S₀ ∧ Function.Surjective ⇑f ∧ hK.isDPMorphism hI ↑f ∧ Module.Free A T
Tactic:
use (⊥ : Subalgebra R T).restrictScalars A
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 : 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
⊢ ∃ (_ : IsAugmentation (↥(Subalgebra.restrictScalars A ⊥)) idK),
    ∃ f,
      Ideal.map f idK = I ∧
        Subalgebra.map f (Subalgebra.restrictScalars A ⊥) = S₀ ∧
          Function.Surjective ⇑f ∧ hK.isDPMorphism hI ↑f ∧ Module.Free A T

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 : 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
⊢ ∃ (_ : IsAugmentation (↥(Subalgebra.restrictScalars A ⊥)) idK),
    ∃ f,
      Ideal.map f idK = I ∧
        Subalgebra.map f (Subalgebra.restrictScalars A ⊥) = S₀ ∧
          Function.Surjective ⇑f ∧ hK.isDPMorphism hI ↑f ∧ Module.Free A T
Tactic:
refine ⟨?_, ?_⟩
State after:
case h.refine_1
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
⊢ IsAugmentation (↥(Subalgebra.restrictScalars A ⊥)) idK

case h.refine_2
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
⊢ ∃ f,
    Ideal.map f idK = I ∧
      Subalgebra.map f (Subalgebra.restrictScalars A ⊥) = S₀ ∧
        Function.Surjective ⇑f ∧ hK.isDPMorphism hI ↑f ∧ Module.Free A T

State before:
case h.refine_2
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
⊢ ∃ f,
    Ideal.map f idK = I ∧
      Subalgebra.map f (Subalgebra.restrictScalars A ⊥) = S₀ ∧
        Function.Surjective ⇑f ∧ hK.isDPMorphism hI ↑f ∧ Module.Free A T
Tactic:
use Ψ A S hI S₀
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 : 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 ∧
    Subalgebra.map (Ψ A S hI S₀) (Subalgebra.restrictScalars A ⊥) = S₀ ∧
      Function.Surjective ⇑(Ψ A S hI S₀) ∧ hK.isDPMorphism hI ↑(Ψ A S hI S₀) ∧ Module.Free A T

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 : 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 ∧
    Subalgebra.map (Ψ A S hI S₀) (Subalgebra.restrictScalars A ⊥) = S₀ ∧
      Function.Surjective ⇑(Ψ A S hI S₀) ∧ hK.isDPMorphism hI ↑(Ψ A S hI S₀) ∧ Module.Free A T
Tactic:
have hI_le : Ideal.map (Ψ A S hI S₀) idK ≤ I := by
  convert (dpΨ A S hI S₀ condTFree hM hM_eq).ideal_comp
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 : 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 ∧
    Subalgebra.map (Ψ A S hI S₀) (Subalgebra.restrictScalars A ⊥) = S₀ ∧
      Function.Surjective ⇑(Ψ A S hI S₀) ∧ hK.isDPMorphism hI ↑(Ψ A S hI S₀) ∧ Module.Free A T

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 : 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 ∧
    Subalgebra.map (Ψ A S hI S₀) (Subalgebra.restrictScalars A ⊥) = S₀ ∧
      Function.Surjective ⇑(Ψ A S hI S₀) ∧ hK.isDPMorphism hI ↑(Ψ A S hI S₀) ∧ Module.Free A T
Tactic:
constructor
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
⊢ Ideal.map (Ψ A S hI S₀) idK = I

case h.right
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
⊢ Subalgebra.map (Ψ A S hI S₀) (Subalgebra.restrictScalars A ⊥) = S₀ ∧
    Function.Surjective ⇑(Ψ A S hI S₀) ∧ hK.isDPMorphism hI ↑(Ψ A S hI S₀) ∧ Module.Free A T

State before:
case h.right
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
⊢ Subalgebra.map (Ψ A S hI S₀) (Subalgebra.restrictScalars A ⊥) = S₀ ∧
    Function.Surjective ⇑(Ψ A S hI S₀) ∧ hK.isDPMorphism hI ↑(Ψ A S hI S₀) ∧ Module.Free A T
Tactic:
constructor
State after:
case h.right.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
⊢ Subalgebra.map (Ψ A S hI S₀) (Subalgebra.restrictScalars A ⊥) = S₀

case h.right.right
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
⊢ Function.Surjective ⇑(Ψ A S hI S₀) ∧ hK.isDPMorphism hI ↑(Ψ A S hI S₀) ∧ Module.Free A T

State before:
case h.right.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
⊢ Subalgebra.map (Ψ A S hI S₀) (Subalgebra.restrictScalars A ⊥) = S₀

case h.right.right
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
⊢ Function.Surjective ⇑(Ψ A S hI S₀) ∧ hK.isDPMorphism hI ↑(Ψ A S hI S₀) ∧ Module.Free A T
Tactic:
apply Ψ_map_eq
State after:
case h.right.right
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
⊢ Function.Surjective ⇑(Ψ A S hI S₀) ∧ hK.isDPMorphism hI ↑(Ψ A S hI S₀) ∧ Module.Free A T

State before:
case h.right.right
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
⊢ Function.Surjective ⇑(Ψ A S hI S₀) ∧ hK.isDPMorphism hI ↑(Ψ A S hI S₀) ∧ Module.Free A T
Tactic:
constructor
State after:
case h.right.right.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
⊢ Function.Surjective ⇑(Ψ A S hI S₀)

case h.right.right.right
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
⊢ hK.isDPMorphism hI ↑(Ψ A S hI S₀) ∧ Module.Free A T

State before:
case h.right.right.right
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
⊢ hK.isDPMorphism hI ↑(Ψ A S hI S₀) ∧ Module.Free A T
Tactic:
constructor
State after:
case h.right.right.right.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
⊢ hK.isDPMorphism hI ↑(Ψ A S hI S₀)

case h.right.right.right.right
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
⊢ Module.Free A T

State before:
case h.right.right.right.right
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
⊢ Module.Free A T
Tactic:
infer_instance
State after:
no goals

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
⊢ CommRing T
Tactic:
infer_instance
State after:
no goals

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
⊢ Algebra A T
Tactic:
infer_instance
State after:
no goals

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)
⊢ idK = Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
Tactic:
simp only [K, Ideal.map_bot, i2, ge_iff_le, bot_le, sup_of_le_right, idK]
State after:
no goals

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 ⋯
⊢ MvPolynomial (↥S₀) A →ₐ[A] MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
Tactic:
apply Algebra.TensorProduct.includeLeft
State after:
no goals

State before:
case h.refine_1
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
⊢ IsAugmentation (↥(Subalgebra.restrictScalars A ⊥)) idK
Tactic:
rw [hidK]
State after:
case h.refine_1
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
⊢ IsAugmentation (↥(Subalgebra.restrictScalars A ⊥)) (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M))

State before:
case h.refine_1
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
⊢ IsAugmentation (↥(Subalgebra.restrictScalars A ⊥)) (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M))
Tactic:
obtain ⟨hd, hc⟩ := Ideal.isAugmentation_baseChange (isCompl_augIdeal A M) (R := MvPolynomial S₀ A)
State after:
case h.refine_1.mk
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)))
⊢ IsAugmentation (↥(Subalgebra.restrictScalars A ⊥)) (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M))

State before:
case h.refine_1.mk
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)))
⊢ IsAugmentation (↥(Subalgebra.restrictScalars A ⊥)) (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M))
Tactic:
apply IsCompl.mk
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
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)))
⊢ Disjoint (Subalgebra.toSubmodule ⊥)
    (Submodule.restrictScalars (↥(Subalgebra.restrictScalars A ⊥))
      (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)))

case h.refine_1.mk.codisjoint
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)))
⊢ Codisjoint (Subalgebra.toSubmodule ⊥)
    (Submodule.restrictScalars (↥(Subalgebra.restrictScalars A ⊥))
      (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)))

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
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)))
⊢ Disjoint (Subalgebra.toSubmodule ⊥)
    (Submodule.restrictScalars (↥(Subalgebra.restrictScalars A ⊥))
      (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)))
Tactic:
simp only [Submodule.disjoint_def, Subalgebra.mem_toSubmodule, Submodule.restrictScalars_mem] at hd ⊢
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 ∈ ⊥, x ∈ Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M) → x = 0

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

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'
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 ∈ ⊥

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

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 ∈ Set.range ⇑(algebraMap (↥(Subalgebra.restrictScalars A ⊥)) T)
hx' : x ∈ Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
⊢ x ∈ ⊥
Tactic:
obtain ⟨⟨x, hx⟩, rfl⟩ := hx
State after:
case h.refine_1.mk.disjoint.intro.mk
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 ∈ Subalgebra.restrictScalars A ⊥
hx' :
  (algebraMap (↥(Subalgebra.restrictScalars A ⊥)) T) ⟨x, hx⟩ ∈
    Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
⊢ (algebraMap (↥(Subalgebra.restrictScalars A ⊥)) T) ⟨x, hx⟩ ∈ ⊥

State before:
case h.refine_1.mk.disjoint.intro.mk
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 ∈ Subalgebra.restrictScalars A ⊥
hx' :
  (algebraMap (↥(Subalgebra.restrictScalars A ⊥)) T) ⟨x, hx⟩ ∈
    Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
⊢ (algebraMap (↥(Subalgebra.restrictScalars A ⊥)) T) ⟨x, hx⟩ ∈ ⊥
Tactic:
simp only [Subalgebra.mem_restrictScalars, Algebra.mem_bot] at hx
State after:
case h.refine_1.mk.disjoint.intro.mk
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 ∈ Subalgebra.restrictScalars A ⊥
hx' :
  (algebraMap (↥(Subalgebra.restrictScalars A ⊥)) T) ⟨x, hx✝⟩ ∈
    Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
hx : x ∈ Set.range ⇑(algebraMap R T)
⊢ (algebraMap (↥(Subalgebra.restrictScalars A ⊥)) T) ⟨x, hx✝⟩ ∈ ⊥

State before:
case h.refine_1.mk.disjoint.intro.mk
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 ∈ Subalgebra.restrictScalars A ⊥
hx' :
  (algebraMap (↥(Subalgebra.restrictScalars A ⊥)) T) ⟨x, hx✝⟩ ∈
    Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)
hx : x ∈ Set.range ⇑(algebraMap R T)
⊢ (algebraMap (↥(Subalgebra.restrictScalars A ⊥)) T) ⟨x, hx✝⟩ ∈ ⊥
Tactic:
obtain ⟨x, rfl⟩ := hx
State after:
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⟩ ∈ ⊥

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⟩ ∈ ⊥
Tactic:
rw [Algebra.mem_bot]
State after:
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))

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

State before:
case h.refine_1.mk.codisjoint
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)))
⊢ Codisjoint (Subalgebra.toSubmodule ⊥)
    (Submodule.restrictScalars (↥(Subalgebra.restrictScalars A ⊥))
      (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)))
Tactic:
simp only [codisjoint_iff, eq_top_iff]
State after:
case h.refine_1.mk.codisjoint
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)))
⊢ ⊤ ≤
    Subalgebra.toSubmodule ⊥ ⊔
      Submodule.restrictScalars (↥(Subalgebra.restrictScalars A ⊥))
        (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M))

State before:
case h.refine_1.mk.codisjoint
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)))
⊢ ⊤ ≤
    Subalgebra.toSubmodule ⊥ ⊔
      Submodule.restrictScalars (↥(Subalgebra.restrictScalars A ⊥))
        (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M))
Tactic:
intro x _
State after:
case h.refine_1.mk.codisjoint
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)))
x : T
a✝ : x ∈ ⊤
⊢ x ∈
    Subalgebra.toSubmodule ⊥ ⊔
      Submodule.restrictScalars (↥(Subalgebra.restrictScalars A ⊥))
        (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M))

State before:
case h.refine_1.mk.codisjoint
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)))
x : T
a✝ : x ∈ ⊤
⊢ x ∈
    Subalgebra.toSubmodule ⊥ ⊔
      Submodule.restrictScalars (↥(Subalgebra.restrictScalars A ⊥))
        (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M))
Tactic:
rw [Submodule.mem_sup]
State after:
case h.refine_1.mk.codisjoint
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)))
x : T
a✝ : x ∈ ⊤
⊢ ∃ y ∈ Subalgebra.toSubmodule ⊥,
    ∃
      z ∈
        Submodule.restrictScalars (↥(Subalgebra.restrictScalars A ⊥))
          (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)),
      y + z = x

State before:
case h.refine_1.mk.codisjoint
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)))
x : T
a✝ : x ∈ ⊤
⊢ ∃ y ∈ Subalgebra.toSubmodule ⊥,
    ∃
      z ∈
        Submodule.restrictScalars (↥(Subalgebra.restrictScalars A ⊥))
          (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)),
      y + z = x
Tactic:
obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.exists_add_eq_of_codisjoint hc x
State after:
case h.refine_1.mk.codisjoint.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)))
y : MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hy : y ∈ Subalgebra.toSubmodule ⊥
z : MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hz : z ∈ Submodule.restrictScalars (MvPolynomial (↥S₀) A) (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M))
a✝ : y + z ∈ ⊤
⊢ ∃ y_1 ∈ Subalgebra.toSubmodule ⊥,
    ∃
      z_1 ∈
        Submodule.restrictScalars (↥(Subalgebra.restrictScalars A ⊥))
          (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)),
      y_1 + z_1 = y + z

State before:
case h.refine_1.mk.codisjoint.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)))
y : MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hy : y ∈ Subalgebra.toSubmodule ⊥
z : MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hz : z ∈ Submodule.restrictScalars (MvPolynomial (↥S₀) A) (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M))
a✝ : y + z ∈ ⊤
⊢ ∃ y_1 ∈ Subalgebra.toSubmodule ⊥,
    ∃
      z_1 ∈
        Submodule.restrictScalars (↥(Subalgebra.restrictScalars A ⊥))
          (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M)),
      y_1 + z_1 = y + z
Tactic:
refine ⟨y, ?_, z, hz, rfl⟩
State after:
case h.refine_1.mk.codisjoint.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)))
y : MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hy : y ∈ Subalgebra.toSubmodule ⊥
z : MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hz : z ∈ Submodule.restrictScalars (MvPolynomial (↥S₀) A) (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M))
a✝ : y + z ∈ ⊤
⊢ y ∈ Subalgebra.toSubmodule ⊥

State before:
case h.refine_1.mk.codisjoint.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)))
y : MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hy : y ∈ Subalgebra.toSubmodule ⊥
z : MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hz : z ∈ Submodule.restrictScalars (MvPolynomial (↥S₀) A) (Ideal.map Algebra.TensorProduct.includeRight (augIdeal A M))
a✝ : y + z ∈ ⊤
⊢ y ∈ Subalgebra.toSubmodule ⊥
Tactic:
rw [Subalgebra.mem_toSubmodule, Algebra.mem_bot] at hy ⊢
State after:
case h.refine_1.mk.codisjoint.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)))
y : MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hy : y ∈ Set.range ⇑(algebraMap (MvPolynomial (↥S₀) A) (MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra 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))
a✝ : y + z ∈ ⊤
⊢ y ∈ Set.range ⇑(algebraMap (↥(Subalgebra.restrictScalars A ⊥)) T)

State before:
case h.refine_1.mk.codisjoint.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)))
y : MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M
hy : y ∈ Set.range ⇑(algebraMap (MvPolynomial (↥S₀) A) (MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra 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))
a✝ : y + z ∈ ⊤
⊢ y ∈ Set.range ⇑(algebraMap (↥(Subalgebra.restrictScalars A ⊥)) T)
Tactic:
obtain ⟨y, rfl⟩ := hy
State after:
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 ∈ ⊤
⊢ (algebraMap (MvPolynomial (↥S₀) A) (MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M)) y ∈
    Set.range ⇑(algebraMap (↥(Subalgebra.restrictScalars A ⊥)) T)

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 ∈ ⊤
⊢ (algebraMap (MvPolynomial (↥S₀) A) (MvPolynomial (↥S₀) A ⊗[A] DividedPowerAlgebra A M)) y ∈
    Set.range ⇑(algebraMap (↥(Subalgebra.restrictScalars A ⊥)) T)
Tactic:
simp only [Algebra.TensorProduct.algebraMap_apply, Algebra.id.map_eq_id,
  RingHom.id_apply, Set.mem_range, Subtype.exists,
  Subalgebra.mem_restrictScalars]
State after:
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 ∈ ⊤
⊢ ∃ a, ∃ (h : a ∈ ⊥), (algebraMap (↥(Subalgebra.restrictScalars A ⊥)) T) ⟨a, ⋯⟩ = y ⊗ₜ[A] 1

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 ∈ ⊤
⊢ ∃ a, ∃ (h : a ∈ ⊥), (algebraMap (↥(Subalgebra.restrictScalars A ⊥)) T) ⟨a, ⋯⟩ = y ⊗ₜ[A] 1
Tactic:
refine ⟨y ⊗ₜ[A] 1, ?_, rfl⟩
State after:
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 ⊗ₜ[A] 1 ∈ ⊥

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 ⊗ₜ[A] 1 ∈ ⊥
Tactic:
rw [Algebra.mem_bot, Set.mem_range]
State after:
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

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

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

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

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

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

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

State before:
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
Tactic:
apply Ideal.mem_sup_right
State after:
case h.left.h.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✝)
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)) ∈ Ideal.map (i2 A R D) (augIdeal A M)

State before:
case h.left.h.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✝)
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)) ∈ Ideal.map (i2 A R D) (augIdeal A M)
Tactic:
apply Ideal.mem_map_of_mem
State after:
case h.left.h.a.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
⊢ (ι A (↥I →₀ A)) (Finsupp.single ⟨i, hi⟩ 1) ∈ augIdeal A M

State before:
case h.left.h.a.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
⊢ (ι A (↥I →₀ A)) (Finsupp.single ⟨i, hi⟩ 1) ∈ augIdeal A M
Tactic:
apply ι_mem_augIdeal
State after:
no goals

State before:
case h.right.right.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
⊢ Function.Surjective ⇑(Ψ A S hI S₀)
Tactic:
apply Ψ_surjective A S hI S₀
State after:
case h.right.right.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
⊢ IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)

State before:
case h.right.right.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
⊢ IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
Tactic:
rw [← isAugmentation_iff_isCompl]
State after:
case h.right.right.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
⊢ IsAugmentation (↥S₀) I

State before:
case h.right.right.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
⊢ IsAugmentation (↥S₀) I
Tactic:
exact hIS₀
State after:
no goals

State before:
case h.right.right.right.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
⊢ hK.isDPMorphism hI ↑(Ψ A S hI S₀)
Tactic:
exact (dpΨ A S hI S₀ condTFree hM hM_eq).isDPMorphism
State after:
no goals