[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ f : R →+* S
a✝ b✝ : R ⧸ ker f
a b : R
h : ↑f a = ↑f b
⊢ a - b ∈ ker f
[PROOFSTEP]
rw [mem_ker, map_sub, h, sub_self]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hI : ker f ≤ I
⊢ Function.Injective ↑(Ideal.Quotient.lift I f H)
[PROOFSTEP]
rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hI : ker f ≤ I
⊢ ∀ (x : R ⧸ I), ↑(Ideal.Quotient.lift I f H) x = 0 → x = 0
[PROOFSTEP]
intro u hu
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hI : ker f ≤ I
u : R ⧸ I
hu : ↑(Ideal.Quotient.lift I f H) u = 0
⊢ u = 0
[PROOFSTEP]
obtain ⟨v, rfl⟩ := Ideal.Quotient.mk_surjective u
[GOAL]
case intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hI : ker f ≤ I
v : R
hu : ↑(Ideal.Quotient.lift I f H) (↑(Ideal.Quotient.mk I) v) = 0
⊢ ↑(Ideal.Quotient.mk I) v = 0
[PROOFSTEP]
rw [Ideal.Quotient.lift_mk] at hu 
[GOAL]
case intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hI : ker f ≤ I
v : R
hu : ↑f v = 0
⊢ ↑(Ideal.Quotient.mk I) v = 0
[PROOFSTEP]
rw [Ideal.Quotient.eq_zero_iff_mem]
[GOAL]
case intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hI : ker f ≤ I
v : R
hu : ↑f v = 0
⊢ v ∈ I
[PROOFSTEP]
exact hI ((RingHom.mem_ker f).mpr hu)
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
g : S → R
hf : Function.RightInverse g ↑f
src✝ : R ⧸ ker f →+* S := kerLift f
⊢ Function.LeftInverse (↑(Ideal.Quotient.mk (ker f)) ∘ g) ↑(kerLift f)
[PROOFSTEP]
rintro ⟨x⟩
[GOAL]
case mk
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
g : S → R
hf : Function.RightInverse g ↑f
src✝ : R ⧸ ker f →+* S := kerLift f
x✝ : R ⧸ ker f
x : R
⊢ (↑(Ideal.Quotient.mk (ker f)) ∘ g) (↑(kerLift f) (Quot.mk Setoid.r x)) = Quot.mk Setoid.r x
[PROOFSTEP]
apply kerLift_injective
[GOAL]
case mk.a
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
g : S → R
hf : Function.RightInverse g ↑f
src✝ : R ⧸ ker f →+* S := kerLift f
x✝ : R ⧸ ker f
x : R
⊢ ↑(kerLift f) ((↑(Ideal.Quotient.mk (ker f)) ∘ g) (↑(kerLift f) (Quot.mk Setoid.r x))) =
    ↑(kerLift f) (Quot.mk Setoid.r x)
[PROOFSTEP]
simp only [Submodule.Quotient.quot_mk_eq_mk, Ideal.Quotient.mk_eq_mk, kerLift_mk, Function.comp_apply, hf (f x)]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
⊢ RingHom.ker (Quotient.mk I) = I
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
x✝ : R
⊢ x✝ ∈ RingHom.ker (Quotient.mk I) ↔ x✝ ∈ I
[PROOFSTEP]
rw [RingHom.ker, mem_comap, @Submodule.mem_bot _ _ _ _ Semiring.toModule _, Quotient.eq_zero_iff_mem]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
h : I ≤ J
⊢ map (Quotient.mk J) I = ⊥
[PROOFSTEP]
rw [map_eq_bot_iff_le_ker, mk_ker]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
h : I ≤ J
⊢ I ≤ J
[PROOFSTEP]
exact h
[GOAL]
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
⊢ RingHom.ker (Quotient.lift I f H) = map (Quotient.mk I) (RingHom.ker f)
[PROOFSTEP]
apply Ideal.ext
[GOAL]
case h
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
⊢ ∀ (x : R ⧸ I), x ∈ RingHom.ker (Quotient.lift I f H) ↔ x ∈ map (Quotient.mk I) (RingHom.ker f)
[PROOFSTEP]
intro x
[GOAL]
case h
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
⊢ x ∈ RingHom.ker (Quotient.lift I f H) ↔ x ∈ map (Quotient.mk I) (RingHom.ker f)
[PROOFSTEP]
constructor
[GOAL]
case h.mp
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
⊢ x ∈ RingHom.ker (Quotient.lift I f H) → x ∈ map (Quotient.mk I) (RingHom.ker f)
[PROOFSTEP]
intro hx
[GOAL]
case h.mp
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
hx : x ∈ RingHom.ker (Quotient.lift I f H)
⊢ x ∈ map (Quotient.mk I) (RingHom.ker f)
[PROOFSTEP]
obtain ⟨y, hy⟩ := Quotient.mk_surjective x
[GOAL]
case h.mp.intro
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
hx : x ∈ RingHom.ker (Quotient.lift I f H)
y : R
hy : ↑(Quotient.mk I) y = x
⊢ x ∈ map (Quotient.mk I) (RingHom.ker f)
[PROOFSTEP]
rw [RingHom.mem_ker, ← hy, Ideal.Quotient.lift_mk, ← RingHom.mem_ker] at hx 
[GOAL]
case h.mp.intro
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
y : R
hx : y ∈ RingHom.ker f
hy : ↑(Quotient.mk I) y = x
⊢ x ∈ map (Quotient.mk I) (RingHom.ker f)
[PROOFSTEP]
rw [← hy, mem_map_iff_of_surjective (Quotient.mk I) Quotient.mk_surjective]
[GOAL]
case h.mp.intro
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
y : R
hx : y ∈ RingHom.ker f
hy : ↑(Quotient.mk I) y = x
⊢ ∃ x, x ∈ RingHom.ker f ∧ ↑(Quotient.mk I) x = ↑(Quotient.mk I) y
[PROOFSTEP]
exact ⟨y, hx, rfl⟩
[GOAL]
case h.mpr
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
⊢ x ∈ map (Quotient.mk I) (RingHom.ker f) → x ∈ RingHom.ker (Quotient.lift I f H)
[PROOFSTEP]
intro hx
[GOAL]
case h.mpr
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
hx : x ∈ map (Quotient.mk I) (RingHom.ker f)
⊢ x ∈ RingHom.ker (Quotient.lift I f H)
[PROOFSTEP]
rw [mem_map_iff_of_surjective (Quotient.mk I) Quotient.mk_surjective] at hx 
[GOAL]
case h.mpr
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
hx : ∃ x_1, x_1 ∈ RingHom.ker f ∧ ↑(Quotient.mk I) x_1 = x
⊢ x ∈ RingHom.ker (Quotient.lift I f H)
[PROOFSTEP]
obtain ⟨y, hy⟩ := hx
[GOAL]
case h.mpr.intro
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
y : R
hy : y ∈ RingHom.ker f ∧ ↑(Quotient.mk I) y = x
⊢ x ∈ RingHom.ker (Quotient.lift I f H)
[PROOFSTEP]
rw [RingHom.mem_ker, ← hy.right, Ideal.Quotient.lift_mk]
[GOAL]
case h.mpr.intro
R : Type u
S✝ : Type v
F : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S✝
S : Type v
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : I ≤ RingHom.ker f
x : R ⧸ I
y : R
hy : y ∈ RingHom.ker f ∧ ↑(Quotient.mk I) y = x
⊢ ↑f y = 0
[PROOFSTEP]
exact hy.left
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : IsMaximal I
⊢ IsMaximal ⊥
[PROOFSTEP]
skip
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : IsMaximal I
⊢ IsMaximal ⊥
[PROOFSTEP]
letI := Quotient.field I
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : IsMaximal I
this : Field (R ⧸ I) := Quotient.field I
⊢ IsMaximal ⊥
[PROOFSTEP]
exact bot_isMaximal
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
x : R
⊢ ↑(Quotient.mk I) x ∈ map (Quotient.mk I) J ↔ x ∈ J ⊔ I
[PROOFSTEP]
rw [← mem_comap, comap_map_of_surjective (Quotient.mk I) Quotient.mk_surjective, ← RingHom.ker_eq_comap_bot, mk_ker]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝¹ : CommRing R
inst✝ : CommRing S
I J : Ideal R
hIJ : I ≤ J
x : R
⊢ ↑(Quotient.mk I) x ∈ map (Quotient.mk I) J ↔ x ∈ J
[PROOFSTEP]
rw [mem_quotient_iff_mem_sup, sup_eq_left.mpr hIJ]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R₁
inst✝⁷ : CommSemiring R₂
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
inst✝² : Algebra R₁ B
inst✝¹ : SMul R₁ R₂
inst✝ : IsScalarTower R₁ R₂ A
I : Ideal A
⊢ IsScalarTower R₁ R₂ (A ⧸ I)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal A
f : A →ₐ[R₁] B
hI : ∀ (a : A), a ∈ I → ↑f a = 0
src✝ : A ⧸ I →+* B := lift I (↑f) hI
r : R₁
⊢ OneHom.toFun
      (↑↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ :
                ∀ (x y : A ⧸ I), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) })
      (↑(algebraMap R₁ (A ⧸ I)) r) =
    ↑(algebraMap R₁ B) r
[PROOFSTEP]
have : algebraMap R₁ (A ⧸ I) r = algebraMap A (A ⧸ I) (algebraMap R₁ A r) := by
  simp_rw [Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal A
f : A →ₐ[R₁] B
hI : ∀ (a : A), a ∈ I → ↑f a = 0
src✝ : A ⧸ I →+* B := lift I (↑f) hI
r : R₁
⊢ ↑(algebraMap R₁ (A ⧸ I)) r = ↑(algebraMap A (A ⧸ I)) (↑(algebraMap R₁ A) r)
[PROOFSTEP]
simp_rw [Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal A
f : A →ₐ[R₁] B
hI : ∀ (a : A), a ∈ I → ↑f a = 0
src✝ : A ⧸ I →+* B := lift I (↑f) hI
r : R₁
this : ↑(algebraMap R₁ (A ⧸ I)) r = ↑(algebraMap A (A ⧸ I)) (↑(algebraMap R₁ A) r)
⊢ OneHom.toFun
      (↑↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ :
                ∀ (x y : A ⧸ I), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) })
      (↑(algebraMap R₁ (A ⧸ I)) r) =
    ↑(algebraMap R₁ B) r
[PROOFSTEP]
rw [this, Ideal.Quotient.algebraMap_eq, RingHom.toFun_eq_coe, Ideal.Quotient.lift_mk, AlgHom.coe_toRingHom,
  Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, map_smul, map_one]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
f : A →ₐ[R₁] B
r : R₁
x : A ⧸ RingHom.ker ↑f
⊢ ↑(RingHom.kerLift ↑f) (r • x) = r • ↑(RingHom.kerLift ↑f) x
[PROOFSTEP]
obtain ⟨a, rfl⟩ := Quotient.mkₐ_surjective R₁ _ x
[GOAL]
case intro
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
f : A →ₐ[R₁] B
r : R₁
a : A
⊢ ↑(RingHom.kerLift ↑f) (r • ↑(Quotient.mkₐ R₁ (RingHom.ker ↑f)) a) =
    r • ↑(RingHom.kerLift ↑f) (↑(Quotient.mkₐ R₁ (RingHom.ker ↑f)) a)
[PROOFSTEP]
exact f.map_smul _ _
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
f : A →ₐ[R₁] B
a : A
⊢ ↑(kerLiftAlg f) (↑(Quotient.mk (RingHom.ker f)) a) = ↑f a
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal R
J : Ideal S
f : R →+* S
hIJ : I ≤ comap f J
x✝ : R
ha : x✝ ∈ I
⊢ ↑(RingHom.comp (Quotient.mk J) f) x✝ = 0
[PROOFSTEP]
simpa [Function.comp_apply, RingHom.coe_comp, Quotient.eq_zero_iff_mem] using hIJ ha
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
J : Ideal R
I : Ideal S
f : R →+* S
H : J ≤ comap f I
x : R
⊢ ↑(RingHom.comp (quotientMap I f H) (Quotient.mk J)) x = ↑(RingHom.comp (Quotient.mk I) f) x
[PROOFSTEP]
simp only [Function.comp_apply, RingHom.coe_comp, Ideal.quotientMap_mk]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal R
J : Ideal S
f : R ≃+* S
hIJ : J = map (↑f) I
⊢ I ≤ comap (↑f) J
[PROOFSTEP]
rw [hIJ]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal R
J : Ideal S
f : R ≃+* S
hIJ : J = map (↑f) I
⊢ I ≤ comap (↑f) (map (↑f) I)
[PROOFSTEP]
exact @le_comap_map _ S _ _ _ _ _ _
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal R
J : Ideal S
f : R ≃+* S
hIJ : J = map (↑f) I
src✝ : R ⧸ I →+* S ⧸ J := quotientMap J ↑f (_ : I ≤ comap (↑f) J)
⊢ J ≤ comap (↑(RingEquiv.symm f)) I
[PROOFSTEP]
rw [hIJ]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal R
J : Ideal S
f : R ≃+* S
hIJ : J = map (↑f) I
src✝ : R ⧸ I →+* S ⧸ J := quotientMap J ↑f (_ : I ≤ comap (↑f) J)
⊢ map (↑f) I ≤ comap (↑(RingEquiv.symm f)) I
[PROOFSTEP]
exact le_of_eq (map_comap_of_equiv I f)
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal R
J : Ideal S
f : R ≃+* S
hIJ : J = map (↑f) I
src✝ : R ⧸ I →+* S ⧸ J := quotientMap J ↑f (_ : I ≤ comap (↑f) J)
⊢ Function.LeftInverse (↑(quotientMap I ↑(RingEquiv.symm f) (_ : J ≤ comap (↑(RingEquiv.symm f)) I))) src✝.toFun
[PROOFSTEP]
rintro ⟨r⟩
[GOAL]
case mk
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal R
J : Ideal S
f : R ≃+* S
hIJ : J = map (↑f) I
src✝ : R ⧸ I →+* S ⧸ J := quotientMap J ↑f (_ : I ≤ comap (↑f) J)
x✝ : R ⧸ I
r : R
⊢ ↑(quotientMap I ↑(RingEquiv.symm f) (_ : J ≤ comap (↑(RingEquiv.symm f)) I))
      (OneHom.toFun (↑↑src✝) (Quot.mk Setoid.r r)) =
    Quot.mk Setoid.r r
[PROOFSTEP]
simp only [Submodule.Quotient.quot_mk_eq_mk, Quotient.mk_eq_mk, RingHom.toFun_eq_coe, quotientMap_mk,
  RingEquiv.coe_toRingHom, RingEquiv.symm_apply_apply]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal R
J : Ideal S
f : R ≃+* S
hIJ : J = map (↑f) I
src✝ : R ⧸ I →+* S ⧸ J := quotientMap J ↑f (_ : I ≤ comap (↑f) J)
⊢ Function.RightInverse (↑(quotientMap I ↑(RingEquiv.symm f) (_ : J ≤ comap (↑(RingEquiv.symm f)) I))) src✝.toFun
[PROOFSTEP]
rintro ⟨s⟩
[GOAL]
case mk
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal R
J : Ideal S
f : R ≃+* S
hIJ : J = map (↑f) I
src✝ : R ⧸ I →+* S ⧸ J := quotientMap J ↑f (_ : I ≤ comap (↑f) J)
x✝ : S ⧸ J
s : S
⊢ OneHom.toFun (↑↑src✝)
      (↑(quotientMap I ↑(RingEquiv.symm f) (_ : J ≤ comap (↑(RingEquiv.symm f)) I)) (Quot.mk Setoid.r s)) =
    Quot.mk Setoid.r s
[PROOFSTEP]
simp only [Submodule.Quotient.quot_mk_eq_mk, Quotient.mk_eq_mk, RingHom.toFun_eq_coe, quotientMap_mk,
  RingEquiv.coe_toRingHom, RingEquiv.apply_symm_apply]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
J : Ideal R
I : Ideal S
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
⊢ Function.Injective ↑(quotientMap I f H)
[PROOFSTEP]
refine' (injective_iff_map_eq_zero (quotientMap I f H)).2 fun a ha => _
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
J : Ideal R
I : Ideal S
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
a : R ⧸ J
ha : ↑(quotientMap I f H) a = 0
⊢ a = 0
[PROOFSTEP]
obtain ⟨r, rfl⟩ := Quotient.mk_surjective a
[GOAL]
case intro
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
J : Ideal R
I : Ideal S
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
r : R
ha : ↑(quotientMap I f H) (↑(Quotient.mk J) r) = 0
⊢ ↑(Quotient.mk J) r = 0
[PROOFSTEP]
rw [quotientMap_mk, Quotient.eq_zero_iff_mem] at ha 
[GOAL]
case intro
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
J : Ideal R
I : Ideal S
f : R →+* S
H : J ≤ comap f I
h : comap f I ≤ J
r : R
ha : ↑f r ∈ I
⊢ ↑(Quotient.mk J) r = 0
[PROOFSTEP]
exact Quotient.eq_zero_iff_mem.mpr (h ha)
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
J : Ideal R
I : Ideal S
f : R →+* S
H : J ≤ comap f I
hf : Function.Surjective ↑f
x✝ : S ⧸ I
x : S
hx : ↑(Quotient.mk I) x = x✝
y : R
hy : ↑f y = x
⊢ ↑(quotientMap I f H) (↑(Quotient.mk J) y) = x✝
[PROOFSTEP]
simp [hx, hy]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R₁
inst✝⁷ : CommSemiring R₂
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
inst✝² : Algebra R₁ B
R' : Type u_5
S' : Type u_6
inst✝¹ : CommRing R'
inst✝ : CommRing S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : RingHom.comp f' g = RingHom.comp g' f
I : Ideal S'
⊢ let leq := (_ : comap f (comap g' I) ≤ comap g (comap f' I));
  RingHom.comp (quotientMap I g' (_ : comap g' I ≤ comap g' I))
      (quotientMap (comap g' I) f (_ : comap f (comap g' I) ≤ comap f (comap g' I))) =
    RingHom.comp (quotientMap I f' (_ : comap f' I ≤ comap f' I)) (quotientMap (comap f' I) g leq)
[PROOFSTEP]
refine RingHom.ext fun a => ?_
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R₁
inst✝⁷ : CommSemiring R₂
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
inst✝² : Algebra R₁ B
R' : Type u_5
S' : Type u_6
inst✝¹ : CommRing R'
inst✝ : CommRing S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : RingHom.comp f' g = RingHom.comp g' f
I : Ideal S'
a : R ⧸ comap f (comap g' I)
⊢ ↑(RingHom.comp (quotientMap I g' (_ : comap g' I ≤ comap g' I))
          (quotientMap (comap g' I) f (_ : comap f (comap g' I) ≤ comap f (comap g' I))))
      a =
    ↑(RingHom.comp (quotientMap I f' (_ : comap f' I ≤ comap f' I))
          (quotientMap (comap f' I) g (_ : comap f (comap g' I) ≤ comap g (comap f' I))))
      a
[PROOFSTEP]
obtain ⟨r, rfl⟩ := Quotient.mk_surjective a
[GOAL]
case intro
R : Type u
S : Type v
F : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R₁
inst✝⁷ : CommSemiring R₂
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
inst✝² : Algebra R₁ B
R' : Type u_5
S' : Type u_6
inst✝¹ : CommRing R'
inst✝ : CommRing S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : RingHom.comp f' g = RingHom.comp g' f
I : Ideal S'
r : R
⊢ ↑(RingHom.comp (quotientMap I g' (_ : comap g' I ≤ comap g' I))
          (quotientMap (comap g' I) f (_ : comap f (comap g' I) ≤ comap f (comap g' I))))
      (↑(Quotient.mk (comap f (comap g' I))) r) =
    ↑(RingHom.comp (quotientMap I f' (_ : comap f' I ≤ comap f' I))
          (quotientMap (comap f' I) g (_ : comap f (comap g' I) ≤ comap g (comap f' I))))
      (↑(Quotient.mk (comap f (comap g' I))) r)
[PROOFSTEP]
simp only [RingHom.comp_apply, quotientMap_mk]
[GOAL]
case intro
R : Type u
S : Type v
F : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R₁
inst✝⁷ : CommSemiring R₂
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
inst✝² : Algebra R₁ B
R' : Type u_5
S' : Type u_6
inst✝¹ : CommRing R'
inst✝ : CommRing S'
f : R →+* S
f' : R' →+* S'
g : R →+* R'
g' : S →+* S'
hfg : RingHom.comp f' g = RingHom.comp g' f
I : Ideal S'
r : R
⊢ ↑(Quotient.mk I) (↑g' (↑f r)) = ↑(Quotient.mk I) (↑f' (↑g r))
[PROOFSTEP]
exact congr_arg (Ideal.Quotient.mk I) (_root_.trans (g'.comp_apply f r).symm (hfg ▸ f'.comp_apply g r))
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal A
J : Ideal B
f : A →ₐ[R₁] B
hIJ : I ≤ comap f J
src✝ : A ⧸ I →+* B ⧸ J := quotientMap J (↑f) hIJ
r : R₁
⊢ OneHom.toFun
      (↑↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ :
                ∀ (x y : A ⧸ I), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) })
      (↑(algebraMap R₁ (A ⧸ I)) r) =
    ↑(algebraMap R₁ (B ⧸ J)) r
[PROOFSTEP]
simp only [RingHom.toFun_eq_coe, quotientMap_algebraMap, AlgHom.coe_toRingHom, AlgHom.commutes, Quotient.mk_algebraMap]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal A
J : Ideal B
f : A →ₐ[R₁] B
H : I ≤ comap f J
x : A
⊢ ↑(AlgHom.comp (quotientMapₐ J f H) (Quotient.mkₐ R₁ I)) x = ↑(AlgHom.comp (Quotient.mkₐ R₁ J) f) x
[PROOFSTEP]
simp only [quotient_map_mkₐ, Quotient.mkₐ_eq_mk, AlgHom.comp_apply]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal A
J : Ideal B
f : A ≃ₐ[R₁] B
hIJ : J = map (↑f) I
src✝ : A ⧸ I ≃+* B ⧸ J := quotientEquiv I J (↑f) hIJ
r : R₁
⊢ Equiv.toFun src✝.toEquiv (↑(algebraMap R₁ (A ⧸ I)) r) = ↑(algebraMap R₁ (B ⧸ J)) r
[PROOFSTEP]
have : ∀ (e : RingEquiv (A ⧸ I) (B ⧸ J)), Equiv.toFun e.toEquiv = FunLike.coe e := fun _ ↦ rfl
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal A
J : Ideal B
f : A ≃ₐ[R₁] B
hIJ : J = map (↑f) I
src✝ : A ⧸ I ≃+* B ⧸ J := quotientEquiv I J (↑f) hIJ
r : R₁
this : ∀ (e : A ⧸ I ≃+* B ⧸ J), e.toFun = ↑e
⊢ Equiv.toFun src✝.toEquiv (↑(algebraMap R₁ (A ⧸ I)) r) = ↑(algebraMap R₁ (B ⧸ J)) r
[PROOFSTEP]
rw [this]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I : Ideal A
J : Ideal B
f : A ≃ₐ[R₁] B
hIJ : J = map (↑f) I
src✝ : A ⧸ I ≃+* B ⧸ J := quotientEquiv I J (↑f) hIJ
r : R₁
this : ∀ (e : A ⧸ I ≃+* B ⧸ J), e.toFun = ↑e
⊢ ↑src✝ (↑(algebraMap R₁ (A ⧸ I)) r) = ↑(algebraMap R₁ (B ⧸ J)) r
[PROOFSTEP]
simp only [quotientEquiv_apply, RingHom.toFun_eq_coe, quotientMap_algebraMap, RingEquiv.coe_toRingHom,
  AlgEquiv.coe_ringEquiv, AlgEquiv.commutes, Quotient.mk_algebraMap]
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R₁ A
inst✝² : Algebra R₂ A
inst✝¹ : Algebra R₁ B
I : Ideal A
inst✝ : Algebra R A
⊢ Function.Injective ↑(algebraMap (R ⧸ comap (algebraMap R A) I) (A ⧸ I))
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩ hab
[GOAL]
case mk.mk
R : Type u
S : Type v
F : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R₁ A
inst✝² : Algebra R₂ A
inst✝¹ : Algebra R₁ B
I : Ideal A
inst✝ : Algebra R A
a₁✝ : R ⧸ comap (algebraMap R A) I
a : R
a₂✝ : R ⧸ comap (algebraMap R A) I
b : R
hab :
  ↑(algebraMap (R ⧸ comap (algebraMap R A) I) (A ⧸ I)) (Quot.mk Setoid.r a) =
    ↑(algebraMap (R ⧸ comap (algebraMap R A) I) (A ⧸ I)) (Quot.mk Setoid.r b)
⊢ Quot.mk Setoid.r a = Quot.mk Setoid.r b
[PROOFSTEP]
replace hab := Quotient.eq.mp hab
[GOAL]
case mk.mk
R : Type u
S : Type v
F : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R₁ A
inst✝² : Algebra R₂ A
inst✝¹ : Algebra R₁ B
I : Ideal A
inst✝ : Algebra R A
a₁✝ : R ⧸ comap (algebraMap R A) I
a : R
a₂✝ : R ⧸ comap (algebraMap R A) I
b : R
hab : ↑(algebraMap R A) a - ↑(algebraMap R A) b ∈ I
⊢ Quot.mk Setoid.r a = Quot.mk Setoid.r b
[PROOFSTEP]
rw [← RingHom.map_sub] at hab 
[GOAL]
case mk.mk
R : Type u
S : Type v
F : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R₁ A
inst✝² : Algebra R₂ A
inst✝¹ : Algebra R₁ B
I : Ideal A
inst✝ : Algebra R A
a₁✝ : R ⧸ comap (algebraMap R A) I
a : R
a₂✝ : R ⧸ comap (algebraMap R A) I
b : R
hab : ↑(algebraMap R A) (a - b) ∈ I
⊢ Quot.mk Setoid.r a = Quot.mk Setoid.r b
[PROOFSTEP]
exact Quotient.eq.mpr hab
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I J : Ideal A
h : I = J
⊢ AlgEquiv.symm (quotientEquivAlgOfEq R₁ h) = quotientEquivAlgOfEq R₁ (_ : J = I)
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I J : Ideal A
h : I = J
a✝ : A ⧸ J
⊢ ↑(AlgEquiv.symm (quotientEquivAlgOfEq R₁ h)) a✝ = ↑(quotientEquivAlgOfEq R₁ (_ : J = I)) a✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I J : Ideal R
h : I ≤ J
⊢ comap (Quotient.mk I) (map (Quotient.mk I) J) = J
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I J : Ideal R
h : I ≤ J
x✝ : R
⊢ x✝ ∈ comap (Quotient.mk I) (map (Quotient.mk I) J) ↔ x✝ ∈ J
[PROOFSTEP]
rw [← Ideal.mem_quotient_iff_mem h, Ideal.mem_comap]
[GOAL]
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingHom.ker (quotLeftToQuotSup I J) = map (Ideal.Quotient.mk I) J
[PROOFSTEP]
simp only [mk_ker, sup_idem, sup_comm, quotLeftToQuotSup, Quotient.factor, ker_quotient_lift,
  map_eq_iff_sup_ker_eq_of_surjective (Ideal.Quotient.mk I) Quotient.mk_surjective, ← sup_assoc]
[GOAL]
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingHom.ker (quotQuotMk I J) = I ⊔ J
[PROOFSTEP]
rw [RingHom.ker_eq_comap_bot, quotQuotMk, ← comap_comap, ← RingHom.ker, mk_ker,
  comap_map_of_surjective (Ideal.Quotient.mk I) Quotient.mk_surjective, ← RingHom.ker, mk_ker, sup_comm]
[GOAL]
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingHom.comp ↑(liftSupQuotQuotMk I J) ↑(quotQuotToQuotSup I J) = RingHom.id ((R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)
[PROOFSTEP]
repeat apply Ideal.Quotient.ringHom_ext
[GOAL]
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingHom.comp ↑(liftSupQuotQuotMk I J) ↑(quotQuotToQuotSup I J) = RingHom.id ((R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)
[PROOFSTEP]
apply Ideal.Quotient.ringHom_ext
[GOAL]
case h
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingHom.comp (RingHom.comp ↑(liftSupQuotQuotMk I J) ↑(quotQuotToQuotSup I J))
      (Ideal.Quotient.mk (map (Ideal.Quotient.mk I) J)) =
    RingHom.comp (RingHom.id ((R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)) (Ideal.Quotient.mk (map (Ideal.Quotient.mk I) J))
[PROOFSTEP]
apply Ideal.Quotient.ringHom_ext
[GOAL]
case h.h
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingHom.comp
      (RingHom.comp (RingHom.comp ↑(liftSupQuotQuotMk I J) ↑(quotQuotToQuotSup I J))
        (Ideal.Quotient.mk (map (Ideal.Quotient.mk I) J)))
      (Ideal.Quotient.mk I) =
    RingHom.comp
      (RingHom.comp (RingHom.id ((R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J))
        (Ideal.Quotient.mk (map (Ideal.Quotient.mk I) J)))
      (Ideal.Quotient.mk I)
[PROOFSTEP]
apply Ideal.Quotient.ringHom_ext
[GOAL]
case h.h
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingHom.comp
      (RingHom.comp (RingHom.comp ↑(liftSupQuotQuotMk I J) ↑(quotQuotToQuotSup I J))
        (Ideal.Quotient.mk (map (Ideal.Quotient.mk I) J)))
      (Ideal.Quotient.mk I) =
    RingHom.comp
      (RingHom.comp (RingHom.id ((R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J))
        (Ideal.Quotient.mk (map (Ideal.Quotient.mk I) J)))
      (Ideal.Quotient.mk I)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingHom.comp ↑(quotQuotToQuotSup I J) ↑(liftSupQuotQuotMk I J) = RingHom.id (R ⧸ I ⊔ J)
[PROOFSTEP]
repeat apply Ideal.Quotient.ringHom_ext
[GOAL]
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingHom.comp ↑(quotQuotToQuotSup I J) ↑(liftSupQuotQuotMk I J) = RingHom.id (R ⧸ I ⊔ J)
[PROOFSTEP]
apply Ideal.Quotient.ringHom_ext
[GOAL]
case h
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingHom.comp (RingHom.comp ↑(quotQuotToQuotSup I J) ↑(liftSupQuotQuotMk I J)) (Ideal.Quotient.mk (I ⊔ J)) =
    RingHom.comp (RingHom.id (R ⧸ I ⊔ J)) (Ideal.Quotient.mk (I ⊔ J))
[PROOFSTEP]
apply Ideal.Quotient.ringHom_ext
[GOAL]
case h
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingHom.comp (RingHom.comp ↑(quotQuotToQuotSup I J) ↑(liftSupQuotQuotMk I J)) (Ideal.Quotient.mk (I ⊔ J)) =
    RingHom.comp (RingHom.id (R ⧸ I ⊔ J)) (Ideal.Quotient.mk (I ⊔ J))
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingEquiv.symm (quotQuotEquivComm I J) = quotQuotEquivComm J I
[PROOFSTEP]
change
  (((quotQuotEquivQuotSup I J).trans (quotEquivOfEq (sup_comm))).trans (quotQuotEquivQuotSup J I).symm).symm =
    ((quotQuotEquivQuotSup J I).trans (quotEquivOfEq (sup_comm))).trans (quotQuotEquivQuotSup I J).symm
[GOAL]
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingEquiv.symm
      (RingEquiv.trans (RingEquiv.trans (quotQuotEquivQuotSup I J) (quotEquivOfEq (_ : I ⊔ J = J ⊔ I)))
        (RingEquiv.symm (quotQuotEquivQuotSup J I))) =
    RingEquiv.trans (RingEquiv.trans (quotQuotEquivQuotSup J I) (quotEquivOfEq (_ : J ⊔ I = I ⊔ J)))
      (RingEquiv.symm (quotQuotEquivQuotSup I J))
[PROOFSTEP]
ext r
[GOAL]
case h
R : Type u
inst✝ : CommRing R
I J : Ideal R
r : (R ⧸ J) ⧸ map (Ideal.Quotient.mk J) I
⊢ ↑(RingEquiv.symm
          (RingEquiv.trans (RingEquiv.trans (quotQuotEquivQuotSup I J) (quotEquivOfEq (_ : I ⊔ J = J ⊔ I)))
            (RingEquiv.symm (quotQuotEquivQuotSup J I))))
      r =
    ↑(RingEquiv.trans (RingEquiv.trans (quotQuotEquivQuotSup J I) (quotEquivOfEq (_ : J ⊔ I = I ⊔ J)))
          (RingEquiv.symm (quotQuotEquivQuotSup I J)))
      r
[PROOFSTEP]
dsimp
[GOAL]
case h
R : Type u
inst✝ : CommRing R
I J : Ideal R
r : (R ⧸ J) ⧸ map (Ideal.Quotient.mk J) I
⊢ ↑(RingEquiv.symm (quotQuotEquivQuotSup I J))
      (↑(RingEquiv.symm (quotEquivOfEq (_ : I ⊔ J = J ⊔ I)))
        (↑(RingEquiv.symm (RingEquiv.symm (quotQuotEquivQuotSup J I))) r)) =
    ↑(RingEquiv.symm (quotQuotEquivQuotSup I J)) (↑(quotEquivOfEq (_ : J ⊔ I = I ⊔ J)) (↑(quotQuotEquivQuotSup J I) r))
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
⊢ RingHom.comp (↑(quotQuotEquivQuotOfLE h)) (quotQuotMk I J) = Ideal.Quotient.mk J
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
x✝ : R
⊢ ↑(RingHom.comp (↑(quotQuotEquivQuotOfLE h)) (quotQuotMk I J)) x✝ = ↑(Ideal.Quotient.mk J) x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
⊢ RingHom.comp (↑(RingEquiv.symm (quotQuotEquivQuotOfLE h))) (Ideal.Quotient.mk J) = quotQuotMk I J
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
x✝ : R
⊢ ↑(RingHom.comp (↑(RingEquiv.symm (quotQuotEquivQuotOfLE h))) (Ideal.Quotient.mk J)) x✝ = ↑(quotQuotMk I J) x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
I J : Ideal A
⊢ AlgEquiv.symm (quotQuotEquivCommₐ R I J) = quotQuotEquivCommₐ R J I
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
I J : Ideal A
a✝ : (A ⧸ J) ⧸ map (Quotient.mkₐ R J) I
⊢ ↑(AlgEquiv.symm (quotQuotEquivCommₐ R I J)) a✝ = ↑(quotQuotEquivCommₐ R J I) a✝
[PROOFSTEP]
unfold quotQuotEquivCommₐ
[GOAL]
case h
R : Type u
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
I J : Ideal A
a✝ : (A ⧸ J) ⧸ map (Quotient.mkₐ R J) I
⊢ ↑(AlgEquiv.symm
          (AlgEquiv.ofRingEquiv
            (_ :
              ∀ (x : R),
                ↑(quotQuotEquivComm I J) (↑(algebraMap R ((A ⧸ I) ⧸ map (Quotient.mkₐ R I) J)) x) =
                  ↑(quotQuotEquivComm I J) (↑(algebraMap R ((A ⧸ I) ⧸ map (Quotient.mkₐ R I) J)) x))))
      a✝ =
    ↑(AlgEquiv.ofRingEquiv
          (_ :
            ∀ (x : R),
              ↑(quotQuotEquivComm J I) (↑(algebraMap R ((A ⧸ J) ⧸ map (Quotient.mkₐ R J) I)) x) =
                ↑(quotQuotEquivComm J I) (↑(algebraMap R ((A ⧸ J) ⧸ map (Quotient.mkₐ R J) I)) x)))
      a✝
[PROOFSTEP]
congr
