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
that : hJ'.dpow n (↑g a) = ↑g (hJ.dpow n a)
⊢ fg.toRingHom (hK.dpow n (1 ⊗ₜ[A] a)) = 1 ⊗ₜ[A] hJ'.dpow n (g a)

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:
simp only [AlgHom.coe_toRingHom] at that
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
that : hJ'.dpow n (g a) = g (hJ.dpow n a)
⊢ fg.toRingHom (hK.dpow n (1 ⊗ₜ[A] a)) = 1 ⊗ₜ[A] hJ'.dpow n (g a)

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