internlm/Lean-Github huggingface dataset:
Theorem: PowerSeries.scale_map_eq_map_scale'
Proof state before:
A : Type u_1
inst✝¹⁷ : CommRing A
R : Type u_2
inst✝¹⁶ : CommRing R
inst✝¹⁵ : Algebra A R
τ : Type u_3
inst✝¹⁴ : DecidableEq τ
S : Type u_4
inst✝¹³ : CommRing S
inst✝¹² : Algebra A S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : IsScalarTower A R S
υ✝ : Type u_5
inst✝⁹ : DecidableEq υ✝
T✝ : Type u_6
inst✝⁸ : CommRing T✝
inst✝⁷ : Algebra R T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R S T✝
a✝¹ : MvPowerSeries τ S
ha✝ : SubstDomain a✝¹
υ : Type u_7
inst✝⁴ : DecidableEq υ
T : Type u_8
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a✝ : S⟦X⟧
ha : SubstDomain a✝
b : MvPowerSeries υ T
hb : SubstDomain b
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
φ : R →+* S
a : A
f : R⟦X⟧
⊢ scale (φ ((algebraMap A R) a)) ((map φ) f) = (map φ) (scale a f)
Tactic:
ext n
Proof state after:
case h
A : Type u_1
inst✝¹⁷ : CommRing A
R : Type u_2
inst✝¹⁶ : CommRing R
inst✝¹⁵ : Algebra A R
τ : Type u_3
inst✝¹⁴ : DecidableEq τ
S : Type u_4
inst✝¹³ : CommRing S
inst✝¹² : Algebra A S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : IsScalarTower A R S
υ✝ : Type u_5
inst✝⁹ : DecidableEq υ✝
T✝ : Type u_6
inst✝⁸ : CommRing T✝
inst✝⁷ : Algebra R T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R S T✝
a✝¹ : MvPowerSeries τ S
ha✝ : SubstDomain a✝¹
υ : Type u_7
inst✝⁴ : DecidableEq υ
T : Type u_8
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a✝ : S⟦X⟧
ha : SubstDomain a✝
b : MvPowerSeries υ T
hb : SubstDomain b
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
φ : R →+* S
a : A
f : R⟦X⟧
n : ℕ
⊢ (coeff S n) (scale (φ ((algebraMap A R) a)) ((map φ) f)) = (coeff S n) ((map φ) (scale a f))
Theorem: PowerSeries.scale_map_eq_map_scale'
Proof state before:
case h
A : Type u_1
inst✝¹⁷ : CommRing A
R : Type u_2
inst✝¹⁶ : CommRing R
inst✝¹⁵ : Algebra A R
τ : Type u_3
inst✝¹⁴ : DecidableEq τ
S : Type u_4
inst✝¹³ : CommRing S
inst✝¹² : Algebra A S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : IsScalarTower A R S
υ✝ : Type u_5
inst✝⁹ : DecidableEq υ✝
T✝ : Type u_6
inst✝⁸ : CommRing T✝
inst✝⁷ : Algebra R T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R S T✝
a✝¹ : MvPowerSeries τ S
ha✝ : SubstDomain a✝¹
υ : Type u_7
inst✝⁴ : DecidableEq υ
T : Type u_8
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a✝ : S⟦X⟧
ha : SubstDomain a✝
b : MvPowerSeries υ T
hb : SubstDomain b
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
φ : R →+* S
a : A
f : R⟦X⟧
n : ℕ
⊢ (coeff S n) (scale (φ ((algebraMap A R) a)) ((map φ) f)) = (coeff S n) ((map φ) (scale a f))
Tactic:
simp only [coeff_scale, coeff_map,
  algebra_compatible_smul S (a ^ n), algebra_compatible_smul R (a ^ n),
  smul_eq_mul, smul_eq_mul, map_mul, map_pow]
Proof state after:
no goals
Theorem: PowerSeries.scale_map_eq_map_scale
Proof state before:
A : Type u_1
inst✝¹⁷ : CommRing A
R : Type u_2
inst✝¹⁶ : CommRing R
inst✝¹⁵ : Algebra A R
τ : Type u_3
inst✝¹⁴ : DecidableEq τ
S : Type u_4
inst✝¹³ : CommRing S
inst✝¹² : Algebra A S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : IsScalarTower A R S
υ✝ : Type u_5
inst✝⁹ : DecidableEq υ✝
T✝ : Type u_6
inst✝⁸ : CommRing T✝
inst✝⁷ : Algebra R T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R S T✝
a✝¹ : MvPowerSeries τ S
ha✝ : SubstDomain a✝¹
υ : Type u_7
inst✝⁴ : DecidableEq υ
T : Type u_8
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a✝ : S⟦X⟧
ha : SubstDomain a✝
b : MvPowerSeries υ T
hb : SubstDomain b
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
φ : R →ₐ[A] S
a : A
f : R⟦X⟧
⊢ scale a ((map ↑φ) f) = (map ↑φ) (scale a f)
Tactic:
rw [← scale_map_eq_map_scale', ← scale_algebraMap, RingHom.coe_coe, AlgHom.commutes]
Proof state after:
no goals
Theorem: Submodule.mem_sup_iff_exists_add
Proof state before:
R : Type u_1
inst✝² : Semiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M₁ M₂ : Submodule R M
m : M
⊢ m ∈ M₁ ⊔ M₂ ↔ ∃ m₁ ∈ M₁, ∃ m₂ ∈ M₂, m₁ + m₂ = m
Tactic:
rw [← Submodule.mem_toAddSubmonoid (M₁ ⊔ M₂),
  Submodule.sup_toAddSubmonoid, AddSubmonoid.mem_sup]
Proof state after:
R : Type u_1
inst✝² : Semiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M₁ M₂ : Submodule R M
m : M
⊢ (∃ y ∈ M₁.toAddSubmonoid, ∃ z ∈ M₂.toAddSubmonoid, y + z = m) ↔ ∃ m₁ ∈ M₁, ∃ m₂ ∈ M₂, m₁ + m₂ = m
Theorem: Submodule.mem_sup_iff_exists_add
Proof state before:
R : Type u_1
inst✝² : Semiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M₁ M₂ : Submodule R M
m : M
⊢ (∃ y ∈ M₁.toAddSubmonoid, ∃ z ∈ M₂.toAddSubmonoid, y + z = m) ↔ ∃ m₁ ∈ M₁, ∃ m₂ ∈ M₂, m₁ + m₂ = m
Tactic:
simp only [Submodule.mem_toAddSubmonoid]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.on_dp_algebra_unique
Proof state before:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : DecidableEq R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : DecidableEq M
inst✝ : Module R M
x : M
n : ℕ
h h' : DividedPowers (augIdeal R M)
h1 : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
h1' : ∀ (n : ℕ) (x : M), h'.dpow n ((ι R M) x) = dp R n x
⊢ h = h'
Tactic:
apply DividedPowers.dp_uniqueness_self h' h (augIdeal_eq_span R M)
Proof state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : DecidableEq R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : DecidableEq M
inst✝ : Module R M
x : M
n : ℕ
h h' : DividedPowers (augIdeal R M)
h1 : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
h1' : ∀ (n : ℕ) (x : M), h'.dpow n ((ι R M) x) = dp R n x
⊢ ∀ (n : ℕ), ∀ a ∈ Set.image2 (dp R) {n | 0 < n} Set.univ, h'.dpow n a = h.dpow n a
Theorem: DividedPowerAlgebra.on_dp_algebra_unique
Proof state before:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : DecidableEq R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : DecidableEq M
inst✝ : Module R M
x : M
n : ℕ
h h' : DividedPowers (augIdeal R M)
h1 : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
h1' : ∀ (n : ℕ) (x : M), h'.dpow n ((ι R M) x) = dp R n x
⊢ ∀ (n : ℕ), ∀ a ∈ Set.image2 (dp R) {n | 0 < n} Set.univ, h'.dpow n a = h.dpow n a
Tactic:
rintro n f ⟨q, hq : 0 < q, m, _, rfl⟩
Proof state after:
case intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : DecidableEq R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : DecidableEq M
inst✝ : Module R M
x : M
n✝ : ℕ
h h' : DividedPowers (augIdeal R M)
h1 : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
h1' : ∀ (n : ℕ) (x : M), h'.dpow n ((ι R M) x) = dp R n x
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ h'.dpow n (dp R q m) = h.dpow n (dp R q m)
Theorem: DividedPowerAlgebra.on_dp_algebra_unique
Proof state before:
case intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : DecidableEq R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : DecidableEq M
inst✝ : Module R M
x : M
n✝ : ℕ
h h' : DividedPowers (augIdeal R M)
h1 : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
h1' : ∀ (n : ℕ) (x : M), h'.dpow n ((ι R M) x) = dp R n x
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ h'.dpow n (dp R q m) = h.dpow n (dp R q m)
Tactic:
nth_rw 1 [← h1' q m]
Proof state after:
case intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : DecidableEq R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : DecidableEq M
inst✝ : Module R M
x : M
n✝ : ℕ
h h' : DividedPowers (augIdeal R M)
h1 : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
h1' : ∀ (n : ℕ) (x : M), h'.dpow n ((ι R M) x) = dp R n x
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ h'.dpow n (h'.dpow q ((ι R M) m)) = h.dpow n (dp R q m)
Theorem: DividedPowerAlgebra.on_dp_algebra_unique
Proof state before:
case intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : DecidableEq R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : DecidableEq M
inst✝ : Module R M
x : M
n✝ : ℕ
h h' : DividedPowers (augIdeal R M)
h1 : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
h1' : ∀ (n : ℕ) (x : M), h'.dpow n ((ι R M) x) = dp R n x
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ h'.dpow n (h'.dpow q ((ι R M) m)) = h.dpow n (dp R q m)
Tactic:
rw [← h1 q m, h.dpow_comp n (ne_of_gt hq) (ι_mem_augIdeal R M m),
  h'.dpow_comp n (ne_of_gt hq) (ι_mem_augIdeal R M m), h1 _ m, h1' _ m]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.on_tensorProduct_unique
Proof 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
Proof 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
Theorem: DividedPowerAlgebra.on_tensorProduct_unique
Proof 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
Proof 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
Theorem: DividedPowerAlgebra.on_tensorProduct_unique
Proof 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
Proof 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'
Theorem: DividedPowerAlgebra.on_tensorProduct_unique
Proof 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
Proof 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'
Theorem: DividedPowerAlgebra.on_tensorProduct_unique
Proof 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]
Proof 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'
Theorem: DividedPowerAlgebra.on_tensorProduct_unique
Proof 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]
Proof 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'
Theorem: DividedPowerAlgebra.on_tensorProduct_unique
Proof 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
Proof 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'
Theorem: DividedPowerAlgebra.on_tensorProduct_unique
Proof 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'
Proof 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'
Theorem: DividedPowerAlgebra.on_tensorProduct_unique
Proof 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'
Proof state after:
no goals
Theorem: DividedPowerAlgebra.on_tensorProduct_unique
Proof 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
Proof state after:
no goals
Theorem: DividedPowerAlgebra.on_tensorProduct_unique
Proof 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
Proof state after:
no goals
Theorem: DividedPowerAlgebra.cond_D_uniqueness
Proof state before:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
⊢ h.isDPMorphism hJ ↑(lift hJ f hf)
Tactic:
constructor
Proof state after:
case left
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
⊢ Ideal.map (↑(lift hJ f hf)) (augIdeal R M) ≤ J

case right
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
⊢ ∀ (n : ℕ), ∀ a ∈ augIdeal R M, hJ.dpow n (↑(lift hJ f hf) a) = ↑(lift hJ f hf) (h.dpow n a)
Theorem: DividedPowerAlgebra.cond_D_uniqueness
Proof state before:
case left
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
⊢ Ideal.map (↑(lift hJ f hf)) (augIdeal R M) ≤ J
Tactic:
rw [augIdeal_eq_span]
Proof state after:
case left
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
⊢ Ideal.map (↑(lift hJ f hf)) (span (Set.image2 (dp R) {n | 0 < n} Set.univ)) ≤ J
Theorem: DividedPowerAlgebra.cond_D_uniqueness
Proof state before:
case left
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
⊢ Ideal.map (↑(lift hJ f hf)) (span (Set.image2 (dp R) {n | 0 < n} Set.univ)) ≤ J
Tactic:
rw [Ideal.map_span]
Proof state after:
case left
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
⊢ span (⇑↑(lift hJ f hf) '' Set.image2 (dp R) {n | 0 < n} Set.univ) ≤ J
Theorem: DividedPowerAlgebra.cond_D_uniqueness
Proof state before:
case left
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
⊢ span (⇑↑(lift hJ f hf) '' Set.image2 (dp R) {n | 0 < n} Set.univ) ≤ J
Tactic:
rw [Ideal.span_le]
Proof state after:
case left
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
⊢ ⇑↑(lift hJ f hf) '' Set.image2 (dp R) {n | 0 < n} Set.univ ⊆ ↑J
Theorem: DividedPowerAlgebra.cond_D_uniqueness
Proof state before:
case left
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
⊢ ⇑↑(lift hJ f hf) '' Set.image2 (dp R) {n | 0 < n} Set.univ ⊆ ↑J
Tactic:
intro s
Proof state after:
case left
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
s : S
⊢ s ∈ ⇑↑(lift hJ f hf) '' Set.image2 (dp R) {n | 0 < n} Set.univ → s ∈ ↑J