internlm/Lean-Github huggingface dataset:
Theorem: DividedPowerAlgebra.T_free_and_D_to_QSplit
Proof 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
Proof 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)
Theorem: DividedPowerAlgebra.T_free_and_D_to_QSplit
Proof 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
Proof 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
Theorem: DividedPowerAlgebra.T_free_and_D_to_QSplit
Proof 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
Proof state after:
no goals
Theorem: DividedPowerAlgebra.T_free_and_D_to_QSplit
Proof 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₀
Proof 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)
Theorem: DividedPowerAlgebra.T_free_and_D_to_QSplit
Proof 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]
Proof 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
Theorem: DividedPowerAlgebra.T_free_and_D_to_QSplit
Proof 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₀
Proof state after:
no goals
Theorem: DividedPowerAlgebra.T_free_and_D_to_QSplit
Proof 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
Proof state after:
no goals
Theorem: DividedPowerAlgebra.condτ_rel
Proof state before:
R✝ : Type u
inst✝⁹ : CommRing R✝
A : Type u
inst✝⁸ : CommRing A
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra A R
inst✝² : Algebra A S
inst✝¹ : Algebra A R'
inst✝ : Algebra A S'
f : R →ₐ[A] R'
hf : Function.Surjective ⇑f
I : Ideal R
hI : DividedPowers I
I' : Ideal R'
hI' : DividedPowers I'
hf' : hI.isDPMorphism hI' ↑f
hI'I : I' = Ideal.map f I
g : S →ₐ[A] S'
hg : Function.Surjective ⇑g
J : Ideal S
hJ : DividedPowers J
J' : Ideal S'
hJ' : DividedPowers J'
hg' : hJ.isDPMorphism hJ' ↑g
hJ'J : J' = Ideal.map g J
roby :
  RingHom.ker (Algebra.TensorProduct.map f g) ⊓ K A I J =
    Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f ⊓ I) ⊔
      Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g ⊓ J)
hRS : Condτ A hI hJ
⊢ Condτ A hI' hJ'
Tactic:
obtain ⟨hK, hK_pd⟩ := hRS
Proof state after:
case intro
R✝ : Type u
inst✝⁹ : CommRing R✝
A : Type u
inst✝⁸ : CommRing A
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra A R
inst✝² : Algebra A S
inst✝¹ : Algebra A R'
inst✝ : Algebra A S'
f : R →ₐ[A] R'
hf : Function.Surjective ⇑f
I : Ideal R
hI : DividedPowers I
I' : Ideal R'
hI' : DividedPowers I'
hf' : hI.isDPMorphism hI' ↑f
hI'I : I' = Ideal.map f I
g : S →ₐ[A] S'
hg : Function.Surjective ⇑g
J : Ideal S
hJ : DividedPowers J
J' : Ideal S'
hJ' : DividedPowers J'
hg' : hJ.isDPMorphism hJ' ↑g
hJ'J : J' = Ideal.map g J
roby :
  RingHom.ker (Algebra.TensorProduct.map f g) ⊓ K A I J =
    Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f ⊓ I) ⊔
      Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g ⊓ J)
hK : DividedPowers (K A I J)
hK_pd : hI.isDPMorphism hK ↑(i1 A R S) ∧ hJ.isDPMorphism hK ↑(i2 A R S)
⊢ Condτ A hI' hJ'
Theorem: DividedPowerAlgebra.condτ_rel
Proof state before:
case intro
R✝ : Type u
inst✝⁹ : CommRing R✝
A : Type u
inst✝⁸ : CommRing A
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra A R
inst✝² : Algebra A S
inst✝¹ : Algebra A R'
inst✝ : Algebra A S'
f : R →ₐ[A] R'
hf : Function.Surjective ⇑f
I : Ideal R
hI : DividedPowers I
I' : Ideal R'
hI' : DividedPowers I'
hf' : hI.isDPMorphism hI' ↑f
hI'I : I' = Ideal.map f I
g : S →ₐ[A] S'
hg : Function.Surjective ⇑g
J : Ideal S
hJ : DividedPowers J
J' : Ideal S'
hJ' : DividedPowers J'
hg' : hJ.isDPMorphism hJ' ↑g
hJ'J : J' = Ideal.map g J
roby :
  RingHom.ker (Algebra.TensorProduct.map f g) ⊓ K A I J =
    Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f ⊓ I) ⊔
      Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g ⊓ J)
hK : DividedPowers (K A I J)
hK_pd : hI.isDPMorphism hK ↑(i1 A R S) ∧ hJ.isDPMorphism hK ↑(i2 A R S)
⊢ Condτ A hI' hJ'
Tactic:
simp only [Condτ]
Proof state after:
case intro
R✝ : Type u
inst✝⁹ : CommRing R✝
A : Type u
inst✝⁸ : CommRing A
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra A R
inst✝² : Algebra A S
inst✝¹ : Algebra A R'
inst✝ : Algebra A S'
f : R →ₐ[A] R'
hf : Function.Surjective ⇑f
I : Ideal R
hI : DividedPowers I
I' : Ideal R'
hI' : DividedPowers I'
hf' : hI.isDPMorphism hI' ↑f
hI'I : I' = Ideal.map f I
g : S →ₐ[A] S'
hg : Function.Surjective ⇑g
J : Ideal S
hJ : DividedPowers J
J' : Ideal S'
hJ' : DividedPowers J'
hg' : hJ.isDPMorphism hJ' ↑g
hJ'J : J' = Ideal.map g J
roby :
  RingHom.ker (Algebra.TensorProduct.map f g) ⊓ K A I J =
    Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f ⊓ I) ⊔
      Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g ⊓ J)
hK : DividedPowers (K A I J)
hK_pd : hI.isDPMorphism hK ↑(i1 A R S) ∧ hJ.isDPMorphism hK ↑(i2 A R S)
⊢ ∃ hK, hI'.isDPMorphism hK ↑(i1 A R' S') ∧ hJ'.isDPMorphism hK ↑(i2 A R' S')
Theorem: DividedPowerAlgebra.condτ_rel
Proof state before:
case intro
R✝ : Type u
inst✝⁹ : CommRing R✝
A : Type u
inst✝⁸ : CommRing A
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra A R
inst✝² : Algebra A S
inst✝¹ : Algebra A R'
inst✝ : Algebra A S'
f : R →ₐ[A] R'
hf : Function.Surjective ⇑f
I : Ideal R
hI : DividedPowers I
I' : Ideal R'
hI' : DividedPowers I'
hf' : hI.isDPMorphism hI' ↑f
hI'I : I' = Ideal.map f I
g : S →ₐ[A] S'
hg : Function.Surjective ⇑g
J : Ideal S
hJ : DividedPowers J
J' : Ideal S'
hJ' : DividedPowers J'
hg' : hJ.isDPMorphism hJ' ↑g
hJ'J : J' = Ideal.map g J
roby :
  RingHom.ker (Algebra.TensorProduct.map f g) ⊓ K A I J =
    Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f ⊓ I) ⊔
      Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g ⊓ J)
hK : DividedPowers (K A I J)
hK_pd : hI.isDPMorphism hK ↑(i1 A R S) ∧ hJ.isDPMorphism hK ↑(i2 A R S)
⊢ ∃ hK, hI'.isDPMorphism hK ↑(i1 A R' S') ∧ hJ'.isDPMorphism hK ↑(i2 A R' S')
Tactic:
let fg := Algebra.TensorProduct.map f g
Proof state after:
case intro
R✝ : Type u
inst✝⁹ : CommRing R✝
A : Type u
inst✝⁸ : CommRing A
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra A R
inst✝² : Algebra A S
inst✝¹ : Algebra A R'
inst✝ : Algebra A S'
f : R →ₐ[A] R'
hf : Function.Surjective ⇑f
I : Ideal R
hI : DividedPowers I
I' : Ideal R'
hI' : DividedPowers I'
hf' : hI.isDPMorphism hI' ↑f
hI'I : I' = Ideal.map f I
g : S →ₐ[A] S'
hg : Function.Surjective ⇑g
J : Ideal S
hJ : DividedPowers J
J' : Ideal S'
hJ' : DividedPowers J'
hg' : hJ.isDPMorphism hJ' ↑g
hJ'J : J' = Ideal.map g J
roby :
  RingHom.ker (Algebra.TensorProduct.map f g) ⊓ K A I J =
    Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f ⊓ I) ⊔
      Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g ⊓ J)
hK : DividedPowers (K A I J)
hK_pd : hI.isDPMorphism hK ↑(i1 A R S) ∧ hJ.isDPMorphism hK ↑(i2 A R S)
fg : R ⊗[A] S →ₐ[A] R' ⊗[A] S' := Algebra.TensorProduct.map f g
⊢ ∃ hK, hI'.isDPMorphism hK ↑(i1 A R' S') ∧ hJ'.isDPMorphism hK ↑(i2 A R' S')
Theorem: DividedPowerAlgebra.condτ_rel
Proof state before:
case intro
R✝ : Type u
inst✝⁹ : CommRing R✝
A : Type u
inst✝⁸ : CommRing A
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra A R
inst✝² : Algebra A S
inst✝¹ : Algebra A R'
inst✝ : Algebra A S'
f : R →ₐ[A] R'
hf : Function.Surjective ⇑f
I : Ideal R
hI : DividedPowers I
I' : Ideal R'
hI' : DividedPowers I'
hf' : hI.isDPMorphism hI' ↑f
hI'I : I' = Ideal.map f I
g : S →ₐ[A] S'
hg : Function.Surjective ⇑g
J : Ideal S
hJ : DividedPowers J
J' : Ideal S'
hJ' : DividedPowers J'
hg' : hJ.isDPMorphism hJ' ↑g
hJ'J : J' = Ideal.map g J
roby :
  RingHom.ker (Algebra.TensorProduct.map f g) ⊓ K A I J =
    Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f ⊓ I) ⊔
      Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g ⊓ J)
hK : DividedPowers (K A I J)
hK_pd : hI.isDPMorphism hK ↑(i1 A R S) ∧ hJ.isDPMorphism hK ↑(i2 A R S)
fg : R ⊗[A] S →ₐ[A] R' ⊗[A] S' := Algebra.TensorProduct.map f g
⊢ ∃ hK, hI'.isDPMorphism hK ↑(i1 A R' S') ∧ hJ'.isDPMorphism hK ↑(i2 A R' S')
Tactic:
have s_fg : Function.Surjective fg := TensorProduct.map_surjective hf hg
Proof state after:
case intro
R✝ : Type u
inst✝⁹ : CommRing R✝
A : Type u
inst✝⁸ : CommRing A
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra A R
inst✝² : Algebra A S
inst✝¹ : Algebra A R'
inst✝ : Algebra A S'
f : R →ₐ[A] R'
hf : Function.Surjective ⇑f
I : Ideal R
hI : DividedPowers I
I' : Ideal R'
hI' : DividedPowers I'
hf' : hI.isDPMorphism hI' ↑f
hI'I : I' = Ideal.map f I
g : S →ₐ[A] S'
hg : Function.Surjective ⇑g
J : Ideal S
hJ : DividedPowers J
J' : Ideal S'
hJ' : DividedPowers J'
hg' : hJ.isDPMorphism hJ' ↑g
hJ'J : J' = Ideal.map g J
roby :
  RingHom.ker (Algebra.TensorProduct.map f g) ⊓ K A I J =
    Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f ⊓ I) ⊔
      Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g ⊓ J)
hK : DividedPowers (K A I J)
hK_pd : hI.isDPMorphism hK ↑(i1 A R S) ∧ hJ.isDPMorphism hK ↑(i2 A R S)
fg : R ⊗[A] S →ₐ[A] R' ⊗[A] S' := Algebra.TensorProduct.map f g
s_fg : Function.Surjective ⇑fg
⊢ ∃ hK, hI'.isDPMorphism hK ↑(i1 A R' S') ∧ hJ'.isDPMorphism hK ↑(i2 A R' S')