Theorem: DividedPowerAlgebra.on_tensorProduct_unique (DividedPowers/DPAlgebra/Dpow.lean)

State before:
A R S : Type u
inst✝⁴ : CommRing A
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal R
J : Ideal S
hI : DividedPowers I
hJ : DividedPowers J
hK hK' : DividedPowers (K A I J)
hIK : hI.isDPMorphism hK ↑(i1 A R S)
hIK' : hI.isDPMorphism hK' ↑(i1 A R S)
hJK : hJ.isDPMorphism hK ↑(i2 A R S)
hJK' : hJ.isDPMorphism hK' ↑(i2 A R S)
⊢ hK = hK'
Tactic:
apply eq_of_eq_on_ideal
State after:
case h_eq
A R S : Type u
inst✝⁴ : CommRing A
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal R
J : Ideal S
hI : DividedPowers I
hJ : DividedPowers J
hK hK' : DividedPowers (K A I J)
hIK : hI.isDPMorphism hK ↑(i1 A R S)
hIK' : hI.isDPMorphism hK' ↑(i1 A R S)
hJK : hJ.isDPMorphism hK ↑(i2 A R S)
hJK' : hJ.isDPMorphism hK' ↑(i2 A R S)
⊢ ∀ (n : ℕ) {x : R ⊗[A] S}, x ∈ K A I J → hK.dpow n x = hK'.dpow n x

State before:
case h_eq
A R S : Type u
inst✝⁴ : CommRing A
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal R
J : Ideal S
hI : DividedPowers I
hJ : DividedPowers J
hK hK' : DividedPowers (K A I J)
hIK : hI.isDPMorphism hK ↑(i1 A R S)
hIK' : hI.isDPMorphism hK' ↑(i1 A R S)
hJK : hJ.isDPMorphism hK ↑(i2 A R S)
hJK' : hJ.isDPMorphism hK' ↑(i2 A R S)
⊢ ∀ (n : ℕ) {x : R ⊗[A] S}, x ∈ K A I J → hK.dpow n x = hK'.dpow n x
Tactic:
intro n x hx
State after:
case h_eq
A R S : Type u
inst✝⁴ : CommRing A
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal R
J : Ideal S
hI : DividedPowers I
hJ : DividedPowers J
hK hK' : DividedPowers (K A I J)
hIK : hI.isDPMorphism hK ↑(i1 A R S)
hIK' : hI.isDPMorphism hK' ↑(i1 A R S)
hJK : hJ.isDPMorphism hK ↑(i2 A R S)
hJK' : hJ.isDPMorphism hK' ↑(i2 A R S)
n : ℕ
x : R ⊗[A] S
hx : x ∈ K A I J
⊢ hK.dpow n x = hK'.dpow n x

State before:
case h_eq
A R S : Type u
inst✝⁴ : CommRing A
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal R
J : Ideal S
hI : DividedPowers I
hJ : DividedPowers J
hK hK' : DividedPowers (K A I J)
hIK : hI.isDPMorphism hK ↑(i1 A R S)
hIK' : hI.isDPMorphism hK' ↑(i1 A R S)
hJK : hJ.isDPMorphism hK ↑(i2 A R S)
hJK' : hJ.isDPMorphism hK' ↑(i2 A R S)
n : ℕ
x : R ⊗[A] S
hx : x ∈ K A I J
⊢ hK.dpow n x = hK'.dpow n x
Tactic:
suffices x ∈ dpEqualizer hK hK' by exact ((mem_dpEqualizer_iff _ _).mp this).2 n
State after:
case h_eq
A R S : Type u
inst✝⁴ : CommRing A
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal R
J : Ideal S
hI : DividedPowers I
hJ : DividedPowers J
hK hK' : DividedPowers (K A I J)
hIK : hI.isDPMorphism hK ↑(i1 A R S)
hIK' : hI.isDPMorphism hK' ↑(i1 A R S)
hJK : hJ.isDPMorphism hK ↑(i2 A R S)
hJK' : hJ.isDPMorphism hK' ↑(i2 A R S)
n : ℕ
x : R ⊗[A] S
hx : x ∈ K A I J
⊢ x ∈ hK.dpEqualizer hK'

State before:
case h_eq
A R S : Type u
inst✝⁴ : CommRing A
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal R
J : Ideal S
hI : DividedPowers I
hJ : DividedPowers J
hK hK' : DividedPowers (K A I J)
hIK : hI.isDPMorphism hK ↑(i1 A R S)
hIK' : hI.isDPMorphism hK' ↑(i1 A R S)
hJK : hJ.isDPMorphism hK ↑(i2 A R S)
hJK' : hJ.isDPMorphism hK' ↑(i2 A R S)
n : ℕ
x : R ⊗[A] S
hx : x ∈ K A I J
⊢ x ∈ hK.dpEqualizer hK'
Tactic:
suffices h_ss : K A I J ≤ dpEqualizer hK hK' by
  exact h_ss hx
State after:
case h_eq
A R S : Type u
inst✝⁴ : CommRing A
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal R
J : Ideal S
hI : DividedPowers I
hJ : DividedPowers J
hK hK' : DividedPowers (K A I J)
hIK : hI.isDPMorphism hK ↑(i1 A R S)
hIK' : hI.isDPMorphism hK' ↑(i1 A R S)
hJK : hJ.isDPMorphism hK ↑(i2 A R S)
hJK' : hJ.isDPMorphism hK' ↑(i2 A R S)
n : ℕ
x : R ⊗[A] S
hx : x ∈ K A I J
⊢ K A I J ≤ hK.dpEqualizer hK'

State before:
case h_eq
A R S : Type u
inst✝⁴ : CommRing A
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal R
J : Ideal S
hI : DividedPowers I
hJ : DividedPowers J
hK hK' : DividedPowers (K A I J)
hIK : hI.isDPMorphism hK ↑(i1 A R S)
hIK' : hI.isDPMorphism hK' ↑(i1 A R S)
hJK : hJ.isDPMorphism hK ↑(i2 A R S)
hJK' : hJ.isDPMorphism hK' ↑(i2 A R S)
n : ℕ
x : R ⊗[A] S
hx : x ∈ K A I J
⊢ K A I J ≤ hK.dpEqualizer hK'
Tactic:
dsimp only [K]
State after:
case h_eq
A R S : Type u
inst✝⁴ : CommRing A
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal R
J : Ideal S
hI : DividedPowers I
hJ : DividedPowers J
hK hK' : DividedPowers (K A I J)
hIK : hI.isDPMorphism hK ↑(i1 A R S)
hIK' : hI.isDPMorphism hK' ↑(i1 A R S)
hJK : hJ.isDPMorphism hK ↑(i2 A R S)
hJK' : hJ.isDPMorphism hK' ↑(i2 A R S)
n : ℕ
x : R ⊗[A] S
hx : x ∈ K A I J
⊢ Ideal.map (i1 A R S) I ⊔ Ideal.map (i2 A R S) J ≤ hK.dpEqualizer hK'

State before:
case h_eq
A R S : Type u
inst✝⁴ : CommRing A
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal R
J : Ideal S
hI : DividedPowers I
hJ : DividedPowers J
hK hK' : DividedPowers (K A I J)
hIK : hI.isDPMorphism hK ↑(i1 A R S)
hIK' : hI.isDPMorphism hK' ↑(i1 A R S)
hJK : hJ.isDPMorphism hK ↑(i2 A R S)
hJK' : hJ.isDPMorphism hK' ↑(i2 A R S)
n : ℕ
x : R ⊗[A] S
hx : x ∈ K A I J
⊢ Ideal.map (i1 A R S) I ⊔ Ideal.map (i2 A R S) J ≤ hK.dpEqualizer hK'
Tactic:
rw [sup_le_iff]
State after:
case h_eq
A R S : Type u
inst✝⁴ : CommRing A
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal R
J : Ideal S
hI : DividedPowers I
hJ : DividedPowers J
hK hK' : DividedPowers (K A I J)
hIK : hI.isDPMorphism hK ↑(i1 A R S)
hIK' : hI.isDPMorphism hK' ↑(i1 A R S)
hJK : hJ.isDPMorphism hK ↑(i2 A R S)
hJK' : hJ.isDPMorphism hK' ↑(i2 A R S)
n : ℕ
x : R ⊗[A] S
hx : x ∈ K A I J
⊢ Ideal.map (i1 A R S) I ≤ hK.dpEqualizer hK' ∧ Ideal.map (i2 A R S) J ≤ hK.dpEqualizer hK'

State before:
case h_eq
A R S : Type u
inst✝⁴ : CommRing A
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal R
J : Ideal S
hI : DividedPowers I
hJ : DividedPowers J
hK hK' : DividedPowers (K A I J)
hIK : hI.isDPMorphism hK ↑(i1 A R S)
hIK' : hI.isDPMorphism hK' ↑(i1 A R S)
hJK : hJ.isDPMorphism hK ↑(i2 A R S)
hJK' : hJ.isDPMorphism hK' ↑(i2 A R S)
n : ℕ
x : R ⊗[A] S
hx : x ∈ K A I J
⊢ Ideal.map (i1 A R S) I ≤ hK.dpEqualizer hK' ∧ Ideal.map (i2 A R S) J ≤ hK.dpEqualizer hK'
Tactic:
constructor
State after:
case h_eq.left
A R S : Type u
inst✝⁴ : CommRing A
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal R
J : Ideal S
hI : DividedPowers I
hJ : DividedPowers J
hK hK' : DividedPowers (K A I J)
hIK : hI.isDPMorphism hK ↑(i1 A R S)
hIK' : hI.isDPMorphism hK' ↑(i1 A R S)
hJK : hJ.isDPMorphism hK ↑(i2 A R S)
hJK' : hJ.isDPMorphism hK' ↑(i2 A R S)
n : ℕ
x : R ⊗[A] S
hx : x ∈ K A I J
⊢ Ideal.map (i1 A R S) I ≤ hK.dpEqualizer hK'

case h_eq.right
A R S : Type u
inst✝⁴ : CommRing A
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal R
J : Ideal S
hI : DividedPowers I
hJ : DividedPowers J
hK hK' : DividedPowers (K A I J)
hIK : hI.isDPMorphism hK ↑(i1 A R S)
hIK' : hI.isDPMorphism hK' ↑(i1 A R S)
hJK : hJ.isDPMorphism hK ↑(i2 A R S)
hJK' : hJ.isDPMorphism hK' ↑(i2 A R S)
n : ℕ
x : R ⊗[A] S
hx : x ∈ K A I J
⊢ Ideal.map (i2 A R S) J ≤ hK.dpEqualizer hK'

State before:
case h_eq.left
A R S : Type u
inst✝⁴ : CommRing A
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal R
J : Ideal S
hI : DividedPowers I
hJ : DividedPowers J
hK hK' : DividedPowers (K A I J)
hIK : hI.isDPMorphism hK ↑(i1 A R S)
hIK' : hI.isDPMorphism hK' ↑(i1 A R S)
hJK : hJ.isDPMorphism hK ↑(i2 A R S)
hJK' : hJ.isDPMorphism hK' ↑(i2 A R S)
n : ℕ
x : R ⊗[A] S
hx : x ∈ K A I J
⊢ Ideal.map (i1 A R S) I ≤ hK.dpEqualizer hK'

case h_eq.right
A R S : Type u
inst✝⁴ : CommRing A
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal R
J : Ideal S
hI : DividedPowers I
hJ : DividedPowers J
hK hK' : DividedPowers (K A I J)
hIK : hI.isDPMorphism hK ↑(i1 A R S)
hIK' : hI.isDPMorphism hK' ↑(i1 A R S)
hJK : hJ.isDPMorphism hK ↑(i2 A R S)
hJK' : hJ.isDPMorphism hK' ↑(i2 A R S)
n : ℕ
x : R ⊗[A] S
hx : x ∈ K A I J
⊢ Ideal.map (i2 A R S) J ≤ hK.dpEqualizer hK'
Tactic:
apply le_equalizer_of_dp_morphism hI (i1 A R S).toRingHom le_sup_left hK hK' hIK hIK'
State after:
case h_eq.right
A R S : Type u
inst✝⁴ : CommRing A
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal R
J : Ideal S
hI : DividedPowers I
hJ : DividedPowers J
hK hK' : DividedPowers (K A I J)
hIK : hI.isDPMorphism hK ↑(i1 A R S)
hIK' : hI.isDPMorphism hK' ↑(i1 A R S)
hJK : hJ.isDPMorphism hK ↑(i2 A R S)
hJK' : hJ.isDPMorphism hK' ↑(i2 A R S)
n : ℕ
x : R ⊗[A] S
hx : x ∈ K A I J
⊢ Ideal.map (i2 A R S) J ≤ hK.dpEqualizer hK'

State before:
case h_eq.right
A R S : Type u
inst✝⁴ : CommRing A
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal R
J : Ideal S
hI : DividedPowers I
hJ : DividedPowers J
hK hK' : DividedPowers (K A I J)
hIK : hI.isDPMorphism hK ↑(i1 A R S)
hIK' : hI.isDPMorphism hK' ↑(i1 A R S)
hJK : hJ.isDPMorphism hK ↑(i2 A R S)
hJK' : hJ.isDPMorphism hK' ↑(i2 A R S)
n : ℕ
x : R ⊗[A] S
hx : x ∈ K A I J
⊢ Ideal.map (i2 A R S) J ≤ hK.dpEqualizer hK'
Tactic:
apply le_equalizer_of_dp_morphism hJ (i2 A R S).toRingHom le_sup_right hK hK' hJK hJK'
State after:
no goals

State before:
A R S : Type u
inst✝⁴ : CommRing A
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal R
J : Ideal S
hI : DividedPowers I
hJ : DividedPowers J
hK hK' : DividedPowers (K A I J)
hIK : hI.isDPMorphism hK ↑(i1 A R S)
hIK' : hI.isDPMorphism hK' ↑(i1 A R S)
hJK : hJ.isDPMorphism hK ↑(i2 A R S)
hJK' : hJ.isDPMorphism hK' ↑(i2 A R S)
n : ℕ
x : R ⊗[A] S
hx : x ∈ K A I J
this : x ∈ hK.dpEqualizer hK'
⊢ hK.dpow n x = hK'.dpow n x
Tactic:
exact ((mem_dpEqualizer_iff _ _).mp this).2 n
State after:
no goals

State before:
A R S : Type u
inst✝⁴ : CommRing A
inst✝³ : CommRing R
inst✝² : Algebra A R
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal R
J : Ideal S
hI : DividedPowers I
hJ : DividedPowers J
hK hK' : DividedPowers (K A I J)
hIK : hI.isDPMorphism hK ↑(i1 A R S)
hIK' : hI.isDPMorphism hK' ↑(i1 A R S)
hJK : hJ.isDPMorphism hK ↑(i2 A R S)
hJK' : hJ.isDPMorphism hK' ↑(i2 A R S)
n : ℕ
x : R ⊗[A] S
hx : x ∈ K A I J
h_ss : K A I J ≤ hK.dpEqualizer hK'
⊢ x ∈ hK.dpEqualizer hK'
Tactic:
exact h_ss hx
State after:
no goals