Theorem: DividedPowerAlgebra.condτ_rel
Proof state before:
case h.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)
⊢ hJ'.isDPMorphism (Quotient.OfSurjective.dividedPowers hK s_fg hK'_pd) ↑(i2 A R' S')
Tactic:
constructor
Proof state after:
case h.right.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 (↑(i2 A R' S')) J' ≤ Ideal.map fg (K A I J)

case h.right.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 ∈ J',
      (Quotient.OfSurjective.dividedPowers hK s_fg hK'_pd).dpow n (↑(i2 A R' S') a) = ↑(i2 A R' S') (hJ'.dpow n a)