internlm/Lean-Github huggingface dataset:
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.isSubDPIdeal (RingHom.ker fg ⊓ K A I J)
Tactic:
rw [roby]
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.isSubDPIdeal
    (Ideal.map Algebra.TensorProduct.includeLeft (RingHom.ker f ⊓ I) ⊔
      Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g ⊓ J))
Theorem: DividedPowerAlgebra.condτ_rel
Proof state before:
case hK
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.isSubDPIdeal (Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g ⊓ J))
Tactic:
exact isSubDPIdeal_map hJ hK hK_pd.2 _ (isSubDPIdeal_ker hJ hJ' hg')
Proof state after:
no goals
Theorem: DividedPowerAlgebra.condτ_rel
Proof state before:
case h.left.left
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)
⊢ Ideal.map (↑(i1 A R' S')) I' ≤ Ideal.map fg (K A I J)
Tactic:
rw [← hK_map]
Proof state after:
case h.left.left
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)
⊢ Ideal.map (↑(i1 A R' S')) I' ≤ K A I' J'
Theorem: DividedPowerAlgebra.condτ_rel
Proof state before:
case h.left.left
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)
⊢ Ideal.map (↑(i1 A R' S')) I' ≤ K A I' J'
Tactic:
rw [Ideal.map_le_iff_le_comap]
Proof state after:
case h.left.left
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)
⊢ I' ≤ comap (↑(i1 A R' S')) (K A I' J')
Theorem: DividedPowerAlgebra.condτ_rel
Proof state before:
case h.left.left
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)
⊢ I' ≤ comap (↑(i1 A R' S')) (K A I' J')
Tactic:
intro a' ha'
Proof state after:
case h.left.left
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)
a' : R'
ha' : a' ∈ I'
⊢ a' ∈ comap (↑(i1 A R' S')) (K A I' J')
Theorem: DividedPowerAlgebra.condτ_rel
Proof state before:
case h.left.left
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)
a' : R'
ha' : a' ∈ I'
⊢ a' ∈ comap (↑(i1 A R' S')) (K A I' J')
Tactic:
rw [Ideal.mem_comap]
Proof state after:
case h.left.left
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)
a' : R'
ha' : a' ∈ I'
⊢ ↑(i1 A R' S') a' ∈ K A I' J'
Theorem: DividedPowerAlgebra.condτ_rel
Proof state before:
case h.left.left
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)
a' : R'
ha' : a' ∈ I'
⊢ ↑(i1 A R' S') a' ∈ K A I' J'
Tactic:
apply Ideal.mem_sup_left
Proof state after:
case h.left.left.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)
a' : R'
ha' : a' ∈ I'
⊢ ↑(i1 A R' S') a' ∈ Ideal.map (i1 A R' S') I'
Theorem: DividedPowerAlgebra.condτ_rel
Proof state before:
case h.left.left.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)
a' : R'
ha' : a' ∈ I'
⊢ ↑(i1 A R' S') a' ∈ Ideal.map (i1 A R' S') I'
Tactic:
apply Ideal.mem_map_of_mem
Proof state after:
case h.left.left.a.h
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)
a' : R'
ha' : a' ∈ I'
⊢ a' ∈ I'
Theorem: DividedPowerAlgebra.condτ_rel
Proof state before:
case h.left.left.a.h
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)
a' : R'
ha' : a' ∈ I'
⊢ a' ∈ I'
Tactic:
exact ha'
Proof state after:
no goals
Theorem: DividedPowerAlgebra.condτ_rel
Proof state before:
case h.left.right
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 ∈ I',
      (Quotient.OfSurjective.dividedPowers hK s_fg hK'_pd).dpow n (↑(i1 A R' S') a) = ↑(i1 A R' S') (hI'.dpow n a)
Tactic:
intro n a' ha'
Proof state after:
case h.left.right
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' : R'
ha' : a' ∈ I'
⊢ (Quotient.OfSurjective.dividedPowers hK s_fg hK'_pd).dpow n (↑(i1 A R' S') a') = ↑(i1 A R' S') (hI'.dpow n a')