internlm/Lean-Github huggingface dataset:
Theorem: DividedPowers.RatAlgebra.dpow_eq_inv_fact_smul
Proof state before:
case e_a.h
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
⊢ ↑n ! ≠ 0
Tactic:
rw [← cast_zero, ne_eq]
Proof state after:
case e_a.h
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
⊢ ¬↑n ! = ↑0
Theorem: DividedPowers.RatAlgebra.dpow_eq_inv_fact_smul
Proof state before:
case e_a.h
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
⊢ ¬↑n ! = ↑0
Tactic:
simp only [cast_zero, cast_eq_zero]
Proof state after:
case e_a.h
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
⊢ ¬n ! = 0
Theorem: DividedPowers.RatAlgebra.dpow_eq_inv_fact_smul
Proof state before:
case e_a.h
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
⊢ ¬n ! = 0
Tactic:
apply Nat.factorial_ne_zero
Proof state after:
no goals
Theorem: DividedPowers.RatAlgebra.dpow_eq_inv_fact_smul
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ ↑n ! = ↑n ! • 1
Tactic:
rw [← nsmul_eq_smul_cast, nsmul_eq_mul, mul_one]
Proof state after:
no goals
Theorem: DividedPowers.RatAlgebra.dpow_eq_inv_fact_smul
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
this : (↑n !)⁻¹ * ↑n ! = 1
⊢ 1 = ((↑n !)⁻¹ * ↑n !) • 1
Tactic:
rw [this, one_smul]
Proof state after:
no goals
Theorem: DividedPowers.RatAlgebra.dividedPowers_unique
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
⊢ hI = dividedPowers I
Tactic:
apply eq_of_eq_on_ideal
Proof state after:
case h_eq
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
⊢ ∀ (n : ℕ) {x : R}, x ∈ I → hI.dpow n x = (dividedPowers I).dpow n x
Theorem: DividedPowers.RatAlgebra.dividedPowers_unique
Proof state before:
case h_eq
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
⊢ ∀ (n : ℕ) {x : R}, x ∈ I → hI.dpow n x = (dividedPowers I).dpow n x
Tactic:
intro n x hx
Proof state after:
case h_eq
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = (dividedPowers I).dpow n x
Theorem: DividedPowers.RatAlgebra.dividedPowers_unique
Proof state before:
case h_eq
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = (dividedPowers I).dpow n x
Tactic:
have hn : IsUnit (n.factorial : R) := Factorial.isUnit n
Proof state after:
case h_eq
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
hn : IsUnit ↑n !
⊢ hI.dpow n x = (dividedPowers I).dpow n x
Theorem: DividedPowers.RatAlgebra.dividedPowers_unique
Proof state before:
case h_eq
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
hn : IsUnit ↑n !
⊢ hI.dpow n x = (dividedPowers I).dpow n x
Tactic:
rw [dividedPowers_dpow_apply, dpow_eq_of_mem n hx, eq_comm, Ring.inverse_mul_eq_iff_eq_mul _ _ _ hn,
  factorial_mul_dpow_eq_pow _ _ _ hx]
Proof state after:
no goals
Theorem: RingHom.ker_eq_ideal_iff
Proof state before:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
⊢ ker f = I ↔ ∃ (h : I ≤ ker f), Function.Injective ⇑(Ideal.Quotient.lift I f h)
Tactic:
constructor
Proof state after:
case mp
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
⊢ ker f = I → ∃ (h : I ≤ ker f), Function.Injective ⇑(Ideal.Quotient.lift I f h)

case mpr
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
⊢ (∃ (h : I ≤ ker f), Function.Injective ⇑(Ideal.Quotient.lift I f h)) → ker f = I
Theorem: RingHom.ker_eq_ideal_iff
Proof state before:
case mp
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
⊢ ker f = I → ∃ (h : I ≤ ker f), Function.Injective ⇑(Ideal.Quotient.lift I f h)
Tactic:
intro hI
Proof state after:
case mp
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
hI : ker f = I
⊢ ∃ (h : I ≤ ker f), Function.Injective ⇑(Ideal.Quotient.lift I f h)
Theorem: RingHom.ker_eq_ideal_iff
Proof state before:
case mp
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
hI : ker f = I
⊢ ∃ (h : I ≤ ker f), Function.Injective ⇑(Ideal.Quotient.lift I f h)
Tactic:
use le_of_eq hI.symm
Proof state after:
case h
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
hI : ker f = I
⊢ Function.Injective ⇑(Ideal.Quotient.lift I f ⋯)
Theorem: RingHom.ker_eq_ideal_iff
Proof state before:
case h
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
hI : ker f = I
⊢ Function.Injective ⇑(Ideal.Quotient.lift I f ⋯)
Tactic:
apply RingHom.lift_injective_of_ker_le_ideal
Proof state after:
case h.hI
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
hI : ker f = I
⊢ ker f ≤ I
Theorem: RingHom.ker_eq_ideal_iff
Proof state before:
case h.hI
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
hI : ker f = I
⊢ ker f ≤ I
Tactic:
simp only [hI, le_refl]
Proof state after:
no goals
Theorem: RingHom.ker_eq_ideal_iff
Proof state before:
case mpr
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
⊢ (∃ (h : I ≤ ker f), Function.Injective ⇑(Ideal.Quotient.lift I f h)) → ker f = I
Tactic:
rintro ⟨hI, h⟩
Proof state after:
case mpr.intro
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
hI : I ≤ ker f
h : Function.Injective ⇑(Ideal.Quotient.lift I f hI)
⊢ ker f = I
Theorem: RingHom.ker_eq_ideal_iff
Proof state before:
case mpr.intro
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
hI : I ≤ ker f
h : Function.Injective ⇑(Ideal.Quotient.lift I f hI)
⊢ ker f = I
Tactic:
simp only [RingHom.injective_iff_ker_eq_bot, Ideal.ker_quotient_lift f hI,
  Ideal.map_eq_bot_iff_le_ker, Ideal.mk_ker] at h
Proof state after:
case mpr.intro
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
hI : I ≤ ker f
h : ker f ≤ I
⊢ ker f = I
Theorem: RingHom.ker_eq_ideal_iff
Proof state before:
case mpr.intro
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
I : Ideal A
hI : I ≤ ker f
h : ker f ≤ I
⊢ ker f = I
Tactic:
exact le_antisymm h hI
Proof state after:
no goals
Theorem: AlgHom.ker_eq_ideal_iff
Proof state before:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
⊢ RingHom.ker f = I ↔ ∃ (h : I ≤ RingHom.ker f), Function.Injective ⇑(Ideal.Quotient.liftₐ I f h)
Tactic:
have : RingHom.ker f = RingHom.ker f.toRingHom := rfl
Proof state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
⊢ RingHom.ker f = I ↔ ∃ (h : I ≤ RingHom.ker f), Function.Injective ⇑(Ideal.Quotient.liftₐ I f h)
Theorem: AlgHom.ker_eq_ideal_iff
Proof state before:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
⊢ RingHom.ker f = I ↔ ∃ (h : I ≤ RingHom.ker f), Function.Injective ⇑(Ideal.Quotient.liftₐ I f h)
Tactic:
constructor
Proof state after:
case mp
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
⊢ RingHom.ker f = I → ∃ (h : I ≤ RingHom.ker f), Function.Injective ⇑(Ideal.Quotient.liftₐ I f h)

case mpr
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
⊢ (∃ (h : I ≤ RingHom.ker f), Function.Injective ⇑(Ideal.Quotient.liftₐ I f h)) → RingHom.ker f = I
Theorem: AlgHom.ker_eq_ideal_iff
Proof state before:
case mp
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
⊢ RingHom.ker f = I → ∃ (h : I ≤ RingHom.ker f), Function.Injective ⇑(Ideal.Quotient.liftₐ I f h)
Tactic:
intro hI
Proof state after:
case mp
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI : RingHom.ker f = I
⊢ ∃ (h : I ≤ RingHom.ker f), Function.Injective ⇑(Ideal.Quotient.liftₐ I f h)
Theorem: AlgHom.ker_eq_ideal_iff
Proof state before:
case mp
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI : RingHom.ker f = I
⊢ ∃ (h : I ≤ RingHom.ker f), Function.Injective ⇑(Ideal.Quotient.liftₐ I f h)
Tactic:
use le_of_eq hI.symm
Proof state after:
case h
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI : RingHom.ker f = I
⊢ Function.Injective ⇑(Ideal.Quotient.liftₐ I f ⋯)
Theorem: AlgHom.ker_eq_ideal_iff
Proof state before:
case h
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI : RingHom.ker f = I
⊢ Function.Injective ⇑(Ideal.Quotient.liftₐ I f ⋯)
Tactic:
suffices h : Function.Injective (Ideal.Quotient.lift I f.toRingHom (le_of_eq hI.symm)) by
  intro x y hxy; apply h
  simpa only [Ideal.Quotient.liftₐ_apply] using hxy
Proof state after:
case h
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI : RingHom.ker f = I
⊢ Function.Injective ⇑(Ideal.Quotient.lift I f.toRingHom ⋯)
Theorem: AlgHom.ker_eq_ideal_iff
Proof state before:
case h
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI : RingHom.ker f = I
⊢ Function.Injective ⇑(Ideal.Quotient.lift I f.toRingHom ⋯)
Tactic:
apply RingHom.lift_injective_of_ker_le_ideal
Proof state after:
case h.hI
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI : RingHom.ker f = I
⊢ RingHom.ker f.toRingHom ≤ I
Theorem: AlgHom.ker_eq_ideal_iff
Proof state before:
case h.hI
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI : RingHom.ker f = I
⊢ RingHom.ker f.toRingHom ≤ I
Tactic:
rw [← hI, ← this]
Proof state after:
no goals
Theorem: AlgHom.ker_eq_ideal_iff
Proof state before:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI : RingHom.ker f = I
h : Function.Injective ⇑(Ideal.Quotient.lift I f.toRingHom ⋯)
⊢ Function.Injective ⇑(Ideal.Quotient.liftₐ I f ⋯)
Tactic:
intro x y hxy
Proof state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI : RingHom.ker f = I
h : Function.Injective ⇑(Ideal.Quotient.lift I f.toRingHom ⋯)
x y : A ⧸ I
hxy : (Ideal.Quotient.liftₐ I f ⋯) x = (Ideal.Quotient.liftₐ I f ⋯) y
⊢ x = y
Theorem: AlgHom.ker_eq_ideal_iff
Proof state before:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI : RingHom.ker f = I
h : Function.Injective ⇑(Ideal.Quotient.lift I f.toRingHom ⋯)
x y : A ⧸ I
hxy : (Ideal.Quotient.liftₐ I f ⋯) x = (Ideal.Quotient.liftₐ I f ⋯) y
⊢ x = y
Tactic:
apply h
Proof state after:
case a
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI : RingHom.ker f = I
h : Function.Injective ⇑(Ideal.Quotient.lift I f.toRingHom ⋯)
x y : A ⧸ I
hxy : (Ideal.Quotient.liftₐ I f ⋯) x = (Ideal.Quotient.liftₐ I f ⋯) y
⊢ (Ideal.Quotient.lift I f.toRingHom ⋯) x = (Ideal.Quotient.lift I f.toRingHom ⋯) y
Theorem: AlgHom.ker_eq_ideal_iff
Proof state before:
case a
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI : RingHom.ker f = I
h : Function.Injective ⇑(Ideal.Quotient.lift I f.toRingHom ⋯)
x y : A ⧸ I
hxy : (Ideal.Quotient.liftₐ I f ⋯) x = (Ideal.Quotient.liftₐ I f ⋯) y
⊢ (Ideal.Quotient.lift I f.toRingHom ⋯) x = (Ideal.Quotient.lift I f.toRingHom ⋯) y
Tactic:
simpa only [Ideal.Quotient.liftₐ_apply] using hxy
Proof state after:
no goals
Theorem: AlgHom.ker_eq_ideal_iff
Proof state before:
case mpr
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
⊢ (∃ (h : I ≤ RingHom.ker f), Function.Injective ⇑(Ideal.Quotient.liftₐ I f h)) → RingHom.ker f = I
Tactic:
rintro ⟨hI, h⟩
Proof state after:
case mpr.intro
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI : I ≤ RingHom.ker f
h : Function.Injective ⇑(Ideal.Quotient.liftₐ I f hI)
⊢ RingHom.ker f = I
Theorem: AlgHom.ker_eq_ideal_iff
Proof state before:
case mpr.intro
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI : I ≤ RingHom.ker f
h : Function.Injective ⇑(Ideal.Quotient.liftₐ I f hI)
⊢ RingHom.ker f = I
Tactic:
rw [this]
Proof state after:
case mpr.intro
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI : I ≤ RingHom.ker f
h : Function.Injective ⇑(Ideal.Quotient.liftₐ I f hI)
⊢ RingHom.ker f.toRingHom = I
Theorem: AlgHom.ker_eq_ideal_iff
Proof state before:
case mpr.intro
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI : I ≤ RingHom.ker f
h : Function.Injective ⇑(Ideal.Quotient.liftₐ I f hI)
⊢ RingHom.ker f.toRingHom = I
Tactic:
rw [RingHom.ker_eq_ideal_iff]
Proof state after:
case mpr.intro
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI : I ≤ RingHom.ker f
h : Function.Injective ⇑(Ideal.Quotient.liftₐ I f hI)
⊢ ∃ (h : I ≤ RingHom.ker f.toRingHom), Function.Injective ⇑(Ideal.Quotient.lift I f.toRingHom h)
Theorem: AlgHom.ker_eq_ideal_iff
Proof state before:
case mpr.intro
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI : I ≤ RingHom.ker f
h : Function.Injective ⇑(Ideal.Quotient.liftₐ I f hI)
⊢ ∃ (h : I ≤ RingHom.ker f.toRingHom), Function.Injective ⇑(Ideal.Quotient.lift I f.toRingHom h)
Tactic:
rw [this] at hI
Proof state after:
case mpr.intro
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI✝ : I ≤ RingHom.ker f
hI : I ≤ RingHom.ker f.toRingHom
h : Function.Injective ⇑(Ideal.Quotient.liftₐ I f hI✝)
⊢ ∃ (h : I ≤ RingHom.ker f.toRingHom), Function.Injective ⇑(Ideal.Quotient.lift I f.toRingHom h)
Theorem: AlgHom.ker_eq_ideal_iff
Proof state before:
case mpr.intro
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI✝ : I ≤ RingHom.ker f
hI : I ≤ RingHom.ker f.toRingHom
h : Function.Injective ⇑(Ideal.Quotient.liftₐ I f hI✝)
⊢ ∃ (h : I ≤ RingHom.ker f.toRingHom), Function.Injective ⇑(Ideal.Quotient.lift I f.toRingHom h)
Tactic:
use hI
Proof state after:
case h
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI✝ : I ≤ RingHom.ker f
hI : I ≤ RingHom.ker f.toRingHom
h : Function.Injective ⇑(Ideal.Quotient.liftₐ I f hI✝)
⊢ Function.Injective ⇑(Ideal.Quotient.lift I f.toRingHom hI)
Theorem: AlgHom.ker_eq_ideal_iff
Proof state before:
case h
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI✝ : I ≤ RingHom.ker f
hI : I ≤ RingHom.ker f.toRingHom
h : Function.Injective ⇑(Ideal.Quotient.liftₐ I f hI✝)
⊢ Function.Injective ⇑(Ideal.Quotient.lift I f.toRingHom hI)
Tactic:
intro x y hxy
Proof state after:
case h
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI✝ : I ≤ RingHom.ker f
hI : I ≤ RingHom.ker f.toRingHom
h : Function.Injective ⇑(Ideal.Quotient.liftₐ I f hI✝)
x y : A ⧸ I
hxy : (Ideal.Quotient.lift I f.toRingHom hI) x = (Ideal.Quotient.lift I f.toRingHom hI) y
⊢ x = y
Theorem: AlgHom.ker_eq_ideal_iff
Proof state before:
case h
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI✝ : I ≤ RingHom.ker f
hI : I ≤ RingHom.ker f.toRingHom
h : Function.Injective ⇑(Ideal.Quotient.liftₐ I f hI✝)
x y : A ⧸ I
hxy : (Ideal.Quotient.lift I f.toRingHom hI) x = (Ideal.Quotient.lift I f.toRingHom hI) y
⊢ x = y
Tactic:
apply h
Proof state after:
case h.a
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI✝ : I ≤ RingHom.ker f
hI : I ≤ RingHom.ker f.toRingHom
h : Function.Injective ⇑(Ideal.Quotient.liftₐ I f hI✝)
x y : A ⧸ I
hxy : (Ideal.Quotient.lift I f.toRingHom hI) x = (Ideal.Quotient.lift I f.toRingHom hI) y
⊢ (Ideal.Quotient.liftₐ I f hI✝) x = (Ideal.Quotient.liftₐ I f hI✝) y
Theorem: AlgHom.ker_eq_ideal_iff
Proof state before:
case h.a
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
I : Ideal A
this : RingHom.ker f = RingHom.ker f.toRingHom
hI✝ : I ≤ RingHom.ker f
hI : I ≤ RingHom.ker f.toRingHom
h : Function.Injective ⇑(Ideal.Quotient.liftₐ I f hI✝)
x y : A ⧸ I
hxy : (Ideal.Quotient.lift I f.toRingHom hI) x = (Ideal.Quotient.lift I f.toRingHom hI) y
⊢ (Ideal.Quotient.liftₐ I f hI✝) x = (Ideal.Quotient.liftₐ I f hI✝) y
Tactic:
simpa only [Ideal.Quotient.liftₐ_apply] using hxy
Proof state after:
no goals
Theorem: φ_apply
Proof state before:
R : Type u_4
inst✝¹⁰ : CommRing R
S : Type u_3
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
m : M
n : N
⊢ (φ R S M N) (m ⊗ₜ[R] n) = m ⊗ₜ[S] n
Tactic:
simp only [φ, productMap_apply_tmul, AlgHom.coe_restrictScalars', includeLeft_apply,
  includeRight_apply, tmul_mul_tmul, _root_.mul_one, _root_.one_mul]
Proof state after:
no goals
Theorem: φ_surjective
Proof state before:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
⊢ Function.Surjective ⇑(φ R S M N)
Tactic:
intro z
Proof state after:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
z : M ⊗[S] N
⊢ ∃ a, (φ R S M N) a = z
Theorem: φ_surjective
Proof state before:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
z : M ⊗[S] N
⊢ ∃ a, (φ R S M N) a = z
Tactic:
induction z using TensorProduct.induction_on with
| zero => use 0; simp only [map_zero]
| tmul m n => use m ⊗ₜ n; simp only [φ_apply]
| add x y hx hy =>
    obtain ⟨a, rfl⟩ := hx
    obtain ⟨b, rfl⟩ := hy
    exact ⟨a + b, map_add _ _ _⟩
Proof state after:
no goals
Theorem: φ_surjective
Proof state before:
case zero
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
⊢ ∃ a, (φ R S M N) a = 0
Tactic:
use 0
Proof state after:
case h
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
⊢ (φ R S M N) 0 = 0