Theorem: AlgHom.ker_eq_ideal_iff (DividedPowers/DPAlgebra/RobyLemma9.lean)

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
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)

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
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

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
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)

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
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 ⋯)

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
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 ⋯)

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
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

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]
State after:
no goals

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
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

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
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

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
State after:
no goals

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⟩
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

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]
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

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]
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)

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
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)

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
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)

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
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

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
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

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
State after:
no goals