internlm/Lean-Github huggingface dataset:
Theorem: DividedPowerAlgebra.condτ_rel
Proof state before:
case h.right.right.intro.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_map : K A I' J' = Ideal.map fg (K A I J)
hK'_pd : hK.isSubDPIdeal (RingHom.ker fg ⊓ K A I J)
n : ℕ
a : S
ha : a ∈ J
⊢ (Quotient.OfSurjective.dividedPowers hK s_fg hK'_pd).dpow n (1 ⊗ₜ[A] g a) = 1 ⊗ₜ[A] hJ'.dpow n (g a)
Tactic:
suffices ∀ y : S, fg.toRingHom (1 ⊗ₜ[A] y) = 1 ⊗ₜ[A] g y by
  rw [← this]
  rw [Quotient.OfSurjective.dpow_apply hK s_fg]
  have that := hg'.2 n a ha
  simp only [AlgHom.coe_toRingHom] at that ; rw [that]
  rw [← this]
  apply congr_arg
  simp only [← Algebra.TensorProduct.includeRight_apply]
  exact hK_pd.2.2 n a ha
  apply Ideal.mem_sup_right
  apply Ideal.mem_map_of_mem _ ha
Proof state after:
case h.right.right.intro.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_map : K A I' J' = Ideal.map fg (K A I J)
hK'_pd : hK.isSubDPIdeal (RingHom.ker fg ⊓ K A I J)
n : ℕ
a : S
ha : a ∈ J
⊢ ∀ (y : S), fg.toRingHom (1 ⊗ₜ[A] y) = 1 ⊗ₜ[A] g y
Theorem: DividedPowerAlgebra.condτ_rel
Proof state before:
case h.right.right.intro.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_map : K A I' J' = Ideal.map fg (K A I J)
hK'_pd : hK.isSubDPIdeal (RingHom.ker fg ⊓ K A I J)
n : ℕ
a : S
ha : a ∈ J
⊢ ∀ (y : S), fg.toRingHom (1 ⊗ₜ[A] y) = 1 ⊗ₜ[A] g y
Tactic:
intro x
Proof state after:
case h.right.right.intro.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_map : K A I' J' = Ideal.map fg (K A I J)
hK'_pd : hK.isSubDPIdeal (RingHom.ker fg ⊓ K A I J)
n : ℕ
a : S
ha : a ∈ J
x : S
⊢ fg.toRingHom (1 ⊗ₜ[A] x) = 1 ⊗ₜ[A] g x
Theorem: DividedPowerAlgebra.condτ_rel
Proof state before:
case h.right.right.intro.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_map : K A I' J' = Ideal.map fg (K A I J)
hK'_pd : hK.isSubDPIdeal (RingHom.ker fg ⊓ K A I J)
n : ℕ
a : S
ha : a ∈ J
x : S
⊢ fg.toRingHom (1 ⊗ₜ[A] x) = 1 ⊗ₜ[A] g x
Tactic:
simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, Algebra.TensorProduct.map_tmul, map_one,
  fg]
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)
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_map : K A I' J' = Ideal.map fg (K A I J)
hK'_pd : hK.isSubDPIdeal (RingHom.ker fg ⊓ K A I J)
n : ℕ
a : S
ha : a ∈ J
this : ∀ (y : S), fg.toRingHom (1 ⊗ₜ[A] y) = 1 ⊗ₜ[A] g y
⊢ (Quotient.OfSurjective.dividedPowers hK s_fg hK'_pd).dpow n (1 ⊗ₜ[A] g a) = 1 ⊗ₜ[A] hJ'.dpow n (g a)
Tactic:
rw [← this]
Proof state after:
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_map : K A I' J' = Ideal.map fg (K A I J)
hK'_pd : hK.isSubDPIdeal (RingHom.ker fg ⊓ K A I J)
n : ℕ
a : S
ha : a ∈ J
this : ∀ (y : S), fg.toRingHom (1 ⊗ₜ[A] y) = 1 ⊗ₜ[A] g y
⊢ (Quotient.OfSurjective.dividedPowers hK s_fg hK'_pd).dpow n (fg.toRingHom (1 ⊗ₜ[A] a)) = 1 ⊗ₜ[A] hJ'.dpow n (g a)
Theorem: DividedPowerAlgebra.condτ_rel
Proof state before:
case ha
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_map : K A I' J' = Ideal.map fg (K A I J)
hK'_pd : hK.isSubDPIdeal (RingHom.ker fg ⊓ K A I J)
n : ℕ
a : S
ha : a ∈ J
this : ∀ (y : S), fg.toRingHom (1 ⊗ₜ[A] y) = 1 ⊗ₜ[A] g y
⊢ 1 ⊗ₜ[A] a ∈ K A I J
Tactic:
apply Ideal.mem_sup_right
Proof state after:
case ha.a
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_map : K A I' J' = Ideal.map fg (K A I J)
hK'_pd : hK.isSubDPIdeal (RingHom.ker fg ⊓ K A I J)
n : ℕ
a : S
ha : a ∈ J
this : ∀ (y : S), fg.toRingHom (1 ⊗ₜ[A] y) = 1 ⊗ₜ[A] g y
⊢ 1 ⊗ₜ[A] a ∈ Ideal.map (i2 A R S) J
Theorem: DividedPowerAlgebra.condτ_rel
Proof state before:
case ha.a
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_map : K A I' J' = Ideal.map fg (K A I J)
hK'_pd : hK.isSubDPIdeal (RingHom.ker fg ⊓ K A I J)
n : ℕ
a : S
ha : a ∈ J
this : ∀ (y : S), fg.toRingHom (1 ⊗ₜ[A] y) = 1 ⊗ₜ[A] g y
⊢ 1 ⊗ₜ[A] a ∈ Ideal.map (i2 A R S) J
Tactic:
apply Ideal.mem_map_of_mem _ ha
Proof state after:
no goals
Theorem: DividedPowerAlgebra.Ideal.map_coe_toRingHom
Proof state before:
R✝ : Type u
inst✝⁵ : CommRing R✝
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra A R
inst✝ : Algebra A S
f : R →ₐ[A] S
I : Ideal R
⊢ Ideal.map f I = Ideal.map f.toRingHom I
Tactic:
rfl
Proof state after:
no goals
Theorem: DividedPowerAlgebra.condQ_and_condTFree_imply_condT
Proof state before:
R : Type u
inst✝¹ : CommRing R
A : Type u_1
inst✝ : CommRing A
hQ : CondQ A
hT_free : CondTFree A
⊢ CondT A
Tactic:
intro R' _ _ I' hI' S' _ _ J' hJ'
Proof state after:
R : Type u
inst✝⁵ : CommRing R
A : Type u_1
inst✝⁴ : CommRing A
hQ : CondQ A
hT_free : CondTFree A
R' : Type u_1
inst✝³ : CommRing R'
inst✝² : Algebra A R'
I' : Ideal R'
hI' : DividedPowers I'
S' : Type u_1
inst✝¹ : CommRing S'
inst✝ : Algebra A S'
J' : Ideal S'
hJ' : DividedPowers J'
⊢ Condτ A hI' hJ'
Theorem: DividedPowerAlgebra.condQ_and_condTFree_imply_condT
Proof state before:
R : Type u
inst✝⁵ : CommRing R
A : Type u_1
inst✝⁴ : CommRing A
hQ : CondQ A
hT_free : CondTFree A
R' : Type u_1
inst✝³ : CommRing R'
inst✝² : Algebra A R'
I' : Ideal R'
hI' : DividedPowers I'
S' : Type u_1
inst✝¹ : CommRing S'
inst✝ : Algebra A S'
J' : Ideal S'
hJ' : DividedPowers J'
⊢ Condτ A hI' hJ'
Tactic:
simp only [CondQ] at hQ
Proof state after:
R : Type u
inst✝⁵ : CommRing R
A : Type u_1
inst✝⁴ : CommRing A
hQ :
  ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Algebra A R] (I : Ideal R) (hI : DividedPowers I),
    ∃ T x x_1,
      ∃ (_ : Module.Free A T), ∃ f J hJ, ∃ (_ : hJ.isDPMorphism hI ↑f), I = Ideal.map f J ∧ Function.Surjective ⇑f
hT_free : CondTFree A
R' : Type u_1
inst✝³ : CommRing R'
inst✝² : Algebra A R'
I' : Ideal R'
hI' : DividedPowers I'
S' : Type u_1
inst✝¹ : CommRing S'
inst✝ : Algebra A S'
J' : Ideal S'
hJ' : DividedPowers J'
⊢ Condτ A hI' hJ'
Theorem: DividedPowerAlgebra.condQ_and_condTFree_imply_condT
Proof state before:
R : Type u
inst✝⁵ : CommRing R
A : Type u_1
inst✝⁴ : CommRing A
hQ :
  ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Algebra A R] (I : Ideal R) (hI : DividedPowers I),
    ∃ T x x_1,
      ∃ (_ : Module.Free A T), ∃ f J hJ, ∃ (_ : hJ.isDPMorphism hI ↑f), I = Ideal.map f J ∧ Function.Surjective ⇑f
hT_free : CondTFree A
R' : Type u_1
inst✝³ : CommRing R'
inst✝² : Algebra A R'
I' : Ideal R'
hI' : DividedPowers I'
S' : Type u_1
inst✝¹ : CommRing S'
inst✝ : Algebra A S'
J' : Ideal S'
hJ' : DividedPowers J'
⊢ Condτ A hI' hJ'
Tactic:
obtain ⟨R, _, _, hR_free, f, I, hI, hfDP, hfI, hf⟩ := hQ R' I' hI'
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R✝ : Type u
inst✝⁵ : CommRing R✝
A : Type u_1
inst✝⁴ : CommRing A
hQ :
  ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Algebra A R] (I : Ideal R) (hI : DividedPowers I),
    ∃ T x x_1,
      ∃ (_ : Module.Free A T), ∃ f J hJ, ∃ (_ : hJ.isDPMorphism hI ↑f), I = Ideal.map f J ∧ Function.Surjective ⇑f
hT_free : CondTFree A
R' : Type u_1
inst✝³ : CommRing R'
inst✝² : Algebra A R'
I' : Ideal R'
hI' : DividedPowers I'
S' : Type u_1
inst✝¹ : CommRing S'
inst✝ : Algebra A S'
J' : Ideal S'
hJ' : DividedPowers J'
R : Type u_1
w✝¹ : CommRing R
w✝ : Algebra A R
hR_free : Module.Free A R
f : R →ₐ[A] R'
I : Ideal R
hI : DividedPowers I
hfDP : hI.isDPMorphism hI' ↑f
hfI : I' = Ideal.map f I
hf : Function.Surjective ⇑f
⊢ Condτ A hI' hJ'
Theorem: DividedPowerAlgebra.condQ_and_condTFree_imply_condT
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R✝ : Type u
inst✝⁵ : CommRing R✝
A : Type u_1
inst✝⁴ : CommRing A
hQ :
  ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Algebra A R] (I : Ideal R) (hI : DividedPowers I),
    ∃ T x x_1,
      ∃ (_ : Module.Free A T), ∃ f J hJ, ∃ (_ : hJ.isDPMorphism hI ↑f), I = Ideal.map f J ∧ Function.Surjective ⇑f
hT_free : CondTFree A
R' : Type u_1
inst✝³ : CommRing R'
inst✝² : Algebra A R'
I' : Ideal R'
hI' : DividedPowers I'
S' : Type u_1
inst✝¹ : CommRing S'
inst✝ : Algebra A S'
J' : Ideal S'
hJ' : DividedPowers J'
R : Type u_1
w✝¹ : CommRing R
w✝ : Algebra A R
hR_free : Module.Free A R
f : R →ₐ[A] R'
I : Ideal R
hI : DividedPowers I
hfDP : hI.isDPMorphism hI' ↑f
hfI : I' = Ideal.map f I
hf : Function.Surjective ⇑f
⊢ Condτ A hI' hJ'
Tactic:
obtain ⟨S, _, _, hS_free, g, J, hJ, hgDP, hgJ, hg⟩ := hQ S' J' hJ'
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R✝ : Type u
inst✝⁵ : CommRing R✝
A : Type u_1
inst✝⁴ : CommRing A
hQ :
  ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Algebra A R] (I : Ideal R) (hI : DividedPowers I),
    ∃ T x x_1,
      ∃ (_ : Module.Free A T), ∃ f J hJ, ∃ (_ : hJ.isDPMorphism hI ↑f), I = Ideal.map f J ∧ Function.Surjective ⇑f
hT_free : CondTFree A
R' : Type u_1
inst✝³ : CommRing R'
inst✝² : Algebra A R'
I' : Ideal R'
hI' : DividedPowers I'
S' : Type u_1
inst✝¹ : CommRing S'
inst✝ : Algebra A S'
J' : Ideal S'
hJ' : DividedPowers J'
R : Type u_1
w✝³ : CommRing R
w✝² : Algebra A R
hR_free : Module.Free A R
f : R →ₐ[A] R'
I : Ideal R
hI : DividedPowers I
hfDP : hI.isDPMorphism hI' ↑f
hfI : I' = Ideal.map f I
hf : Function.Surjective ⇑f
S : Type u_1
w✝¹ : CommRing S
w✝ : Algebra A S
hS_free : Module.Free A S
g : S →ₐ[A] S'
J : Ideal S
hJ : DividedPowers J
hgDP : hJ.isDPMorphism hJ' ↑g
hgJ : J' = Ideal.map g J
hg : Function.Surjective ⇑g
⊢ Condτ A hI' hJ'
Theorem: DividedPowerAlgebra.condQ_and_condTFree_imply_condT
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.roby
R✝ : Type u
inst✝⁵ : CommRing R✝
A : Type u_1
inst✝⁴ : CommRing A
hQ :
  ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Algebra A R] (I : Ideal R) (hI : DividedPowers I),
    ∃ T x x_1,
      ∃ (_ : Module.Free A T), ∃ f J hJ, ∃ (_ : hJ.isDPMorphism hI ↑f), I = Ideal.map f J ∧ Function.Surjective ⇑f
hT_free : CondTFree A
R' : Type u_1
inst✝³ : CommRing R'
inst✝² : Algebra A R'
I' : Ideal R'
hI' : DividedPowers I'
S' : Type u_1
inst✝¹ : CommRing S'
inst✝ : Algebra A S'
J' : Ideal S'
hJ' : DividedPowers J'
R : Type u_1
w✝³ : CommRing R
w✝² : Algebra A R
hR_free : Module.Free A R
f : R →ₐ[A] R'
I : Ideal R
hI : DividedPowers I
hfDP : hI.isDPMorphism hI' ↑f
hfI : I' = Ideal.map f I
hf : Function.Surjective ⇑f
S : Type u_1
w✝¹ : CommRing S
w✝ : Algebra A S
hS_free : Module.Free A S
g : S →ₐ[A] S'
J : Ideal S
hJ : DividedPowers J
hgDP : hJ.isDPMorphism hJ' ↑g
hgJ : J' = Ideal.map g J
hg : Function.Surjective ⇑g
⊢ 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)
Tactic:
rw [Algebra.TensorProduct.map_ker _ _ hf hg]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.roby
R✝ : Type u
inst✝⁵ : CommRing R✝
A : Type u_1
inst✝⁴ : CommRing A
hQ :
  ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Algebra A R] (I : Ideal R) (hI : DividedPowers I),
    ∃ T x x_1,
      ∃ (_ : Module.Free A T), ∃ f J hJ, ∃ (_ : hJ.isDPMorphism hI ↑f), I = Ideal.map f J ∧ Function.Surjective ⇑f
hT_free : CondTFree A
R' : Type u_1
inst✝³ : CommRing R'
inst✝² : Algebra A R'
I' : Ideal R'
hI' : DividedPowers I'
S' : Type u_1
inst✝¹ : CommRing S'
inst✝ : Algebra A S'
J' : Ideal S'
hJ' : DividedPowers J'
R : Type u_1
w✝³ : CommRing R
w✝² : Algebra A R
hR_free : Module.Free A R
f : R →ₐ[A] R'
I : Ideal R
hI : DividedPowers I
hfDP : hI.isDPMorphism hI' ↑f
hfI : I' = Ideal.map f I
hf : Function.Surjective ⇑f
S : Type u_1
w✝¹ : CommRing S
w✝ : Algebra A S
hS_free : Module.Free A S
g : S →ₐ[A] S'
J : Ideal S
hJ : DividedPowers J
hgDP : hJ.isDPMorphism hJ' ↑g
hgJ : J' = Ideal.map g J
hg : Function.Surjective ⇑g
⊢ (Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f) ⊔
        Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g)) ⊓
      K A I J =
    Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f ⊓ I) ⊔
      Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g ⊓ J)
Theorem: DividedPowerAlgebra.condQ_and_condTFree_imply_condT
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.roby
R✝ : Type u
inst✝⁵ : CommRing R✝
A : Type u_1
inst✝⁴ : CommRing A
hQ :
  ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Algebra A R] (I : Ideal R) (hI : DividedPowers I),
    ∃ T x x_1,
      ∃ (_ : Module.Free A T), ∃ f J hJ, ∃ (_ : hJ.isDPMorphism hI ↑f), I = Ideal.map f J ∧ Function.Surjective ⇑f
hT_free : CondTFree A
R' : Type u_1
inst✝³ : CommRing R'
inst✝² : Algebra A R'
I' : Ideal R'
hI' : DividedPowers I'
S' : Type u_1
inst✝¹ : CommRing S'
inst✝ : Algebra A S'
J' : Ideal S'
hJ' : DividedPowers J'
R : Type u_1
w✝³ : CommRing R
w✝² : Algebra A R
hR_free : Module.Free A R
f : R →ₐ[A] R'
I : Ideal R
hI : DividedPowers I
hfDP : hI.isDPMorphism hI' ↑f
hfI : I' = Ideal.map f I
hf : Function.Surjective ⇑f
S : Type u_1
w✝¹ : CommRing S
w✝ : Algebra A S
hS_free : Module.Free A S
g : S →ₐ[A] S'
J : Ideal S
hJ : DividedPowers J
hgDP : hJ.isDPMorphism hJ' ↑g
hgJ : J' = Ideal.map g J
hg : Function.Surjective ⇑g
⊢ (Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f) ⊔
        Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g)) ⊓
      K A I J =
    Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f ⊓ I) ⊔
      Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g ⊓ J)
Tactic:
sorry
Proof state after:
no goals
Theorem: DividedPowerAlgebra.condQ_and_condTFree_imply_condT
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.hRS.x
R✝ : Type u
inst✝⁵ : CommRing R✝
A : Type u_1
inst✝⁴ : CommRing A
hQ :
  ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Algebra A R] (I : Ideal R) (hI : DividedPowers I),
    ∃ T x x_1,
      ∃ (_ : Module.Free A T), ∃ f J hJ, ∃ (_ : hJ.isDPMorphism hI ↑f), I = Ideal.map f J ∧ Function.Surjective ⇑f
hT_free : CondTFree A
R' : Type u_1
inst✝³ : CommRing R'
inst✝² : Algebra A R'
I' : Ideal R'
hI' : DividedPowers I'
S' : Type u_1
inst✝¹ : CommRing S'
inst✝ : Algebra A S'
J' : Ideal S'
hJ' : DividedPowers J'
R : Type u_1
w✝³ : CommRing R
w✝² : Algebra A R
hR_free : Module.Free A R
f : R →ₐ[A] R'
I : Ideal R
hI : DividedPowers I
hfDP : hI.isDPMorphism hI' ↑f
hfI : I' = Ideal.map f I
hf : Function.Surjective ⇑f
S : Type u_1
w✝¹ : CommRing S
w✝ : Algebra A S
hS_free : Module.Free A S
g : S →ₐ[A] S'
J : Ideal S
hJ : DividedPowers J
hgDP : hJ.isDPMorphism hJ' ↑g
hgJ : J' = Ideal.map g J
hg : Function.Surjective ⇑g
⊢ Module.Free A S
Tactic:
exact hS_free
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dp_comp
Proof state before:
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
M : Type u
inst✝¹ : AddCommGroup M
inst✝ : Module A M
x : M
n m : ℕ
hn : n ≠ 0
⊢ (dividedPowers' A M).dpow m (dp A n x) = ↑(mchoose m n) * dp A (m * n) x
Tactic:
erw [← (roby_D A M).choose_spec, dpow_comp _ m hn (ι_mem_augIdeal A M x), dpow_ι]
Proof state after:
no goals