Theorem: kerφ_eq (DividedPowers/DPAlgebra/RobyLemma9.lean)

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
⊢ RingHom.ker (φ R S M N).toRingHom = kerφ R S M N
Tactic:
suffices h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom by
  rw [RingHom.ker_eq_ideal_iff]
  use h
  apply Function.HasLeftInverse.injective
  use ψ R S M N
  intro z
  obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective z
  simp only [AlgHom.toRingHom_eq_coe, Ideal.Quotient.lift_mk, AlgHom.coe_toRingHom]
  induction y using TensorProduct.induction_on with
  | zero => simp only [RingHom.map_zero, AlgHom.map_zero]
  | tmul m n => simp only [ψ_apply, φ_apply]
  | add x y hx hy =>
    simp only [RingHom.map_add, AlgHom.map_add, ← Ideal.Quotient.mkₐ_eq_mk, hx, hy]
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
⊢ kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom

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
⊢ kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
Tactic:
simp only [kerφ]
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
⊢ Ideal.span ((fun r => (r • 1) ⊗ₜ[R] 1 - 1 ⊗ₜ[R] (r • 1)) '' ⊤) ≤ RingHom.ker (φ R S M N).toRingHom

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
⊢ Ideal.span ((fun r => (r • 1) ⊗ₜ[R] 1 - 1 ⊗ₜ[R] (r • 1)) '' ⊤) ≤ RingHom.ker (φ R S M N).toRingHom
Tactic:
rw [Ideal.span_le]
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
⊢ (fun r => (r • 1) ⊗ₜ[R] 1 - 1 ⊗ₜ[R] (r • 1)) '' ⊤ ⊆ ↑(RingHom.ker (φ R S M N).toRingHom)

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
⊢ (fun r => (r • 1) ⊗ₜ[R] 1 - 1 ⊗ₜ[R] (r • 1)) '' ⊤ ⊆ ↑(RingHom.ker (φ R S M N).toRingHom)
Tactic:
intro z hz
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 ⊗[R] N
hz : z ∈ (fun r => (r • 1) ⊗ₜ[R] 1 - 1 ⊗ₜ[R] (r • 1)) '' ⊤
⊢ z ∈ ↑(RingHom.ker (φ R S M N).toRingHom)

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 ⊗[R] N
hz : z ∈ (fun r => (r • 1) ⊗ₜ[R] 1 - 1 ⊗ₜ[R] (r • 1)) '' ⊤
⊢ z ∈ ↑(RingHom.ker (φ R S M N).toRingHom)
Tactic:
simp only [Set.top_eq_univ, Set.image_univ, Set.mem_range] at hz
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 ⊗[R] N
hz : ∃ y, (y • 1) ⊗ₜ[R] 1 - 1 ⊗ₜ[R] (y • 1) = z
⊢ z ∈ ↑(RingHom.ker (φ R S M N).toRingHom)

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 ⊗[R] N
hz : ∃ y, (y • 1) ⊗ₜ[R] 1 - 1 ⊗ₜ[R] (y • 1) = z
⊢ z ∈ ↑(RingHom.ker (φ R S M N).toRingHom)
Tactic:
obtain ⟨r, rfl⟩ := hz
State after:
case intro
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
⊢ (r • 1) ⊗ₜ[R] 1 - 1 ⊗ₜ[R] (r • 1) ∈ ↑(RingHom.ker (φ R S M N).toRingHom)

State before:
case intro
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
⊢ (r • 1) ⊗ₜ[R] 1 - 1 ⊗ₜ[R] (r • 1) ∈ ↑(RingHom.ker (φ R S M N).toRingHom)
Tactic:
simp only [SetLike.mem_coe, RingHom.sub_mem_ker_iff,AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom,
  φ_apply, TensorProduct.tmul_smul]
State after:
case intro
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
⊢ (r • 1) ⊗ₜ[S] 1 = r • 1 ⊗ₜ[S] 1

State before:
case intro
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
⊢ (r • 1) ⊗ₜ[S] 1 = r • 1 ⊗ₜ[S] 1
Tactic:
rfl
State after:
no goals

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
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
⊢ RingHom.ker (φ R S M N).toRingHom = kerφ R S M N
Tactic:
rw [RingHom.ker_eq_ideal_iff]
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
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
⊢ ∃ (h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom),
    Function.Injective ⇑(Ideal.Quotient.lift (kerφ R S M N) (φ R S M N).toRingHom h)

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
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
⊢ ∃ (h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom),
    Function.Injective ⇑(Ideal.Quotient.lift (kerφ R S M N) (φ R S M N).toRingHom h)
Tactic:
use h
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
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
⊢ Function.Injective ⇑(Ideal.Quotient.lift (kerφ R S M N) (φ R S M N).toRingHom h)

State before:
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
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
⊢ Function.Injective ⇑(Ideal.Quotient.lift (kerφ R S M N) (φ R S M N).toRingHom h)
Tactic:
apply Function.HasLeftInverse.injective
State after:
case h.a
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
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
⊢ Function.HasLeftInverse ⇑(Ideal.Quotient.lift (kerφ R S M N) (φ R S M N).toRingHom h)

State before:
case h.a
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
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
⊢ Function.HasLeftInverse ⇑(Ideal.Quotient.lift (kerφ R S M N) (φ R S M N).toRingHom h)
Tactic:
use ψ R S M N
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
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
⊢ Function.LeftInverse ⇑(ψ R S M N) ⇑(Ideal.Quotient.lift (kerφ R S M N) (φ R S M N).toRingHom h)

State before:
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
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
⊢ Function.LeftInverse ⇑(ψ R S M N) ⇑(Ideal.Quotient.lift (kerφ R S M N) (φ R S M N).toRingHom h)
Tactic:
intro z
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
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
z : M ⊗[R] N ⧸ kerφ R S M N
⊢ (ψ R S M N) ((Ideal.Quotient.lift (kerφ R S M N) (φ R S M N).toRingHom h) z) = z

State before:
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
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
z : M ⊗[R] N ⧸ kerφ R S M N
⊢ (ψ R S M N) ((Ideal.Quotient.lift (kerφ R S M N) (φ R S M N).toRingHom h) z) = z
Tactic:
obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective z
State after:
case h.intro
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
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
y : M ⊗[R] N
⊢ (ψ R S M N) ((Ideal.Quotient.lift (kerφ R S M N) (φ R S M N).toRingHom h) ((Ideal.Quotient.mk (kerφ R S M N)) y)) =
    (Ideal.Quotient.mk (kerφ R S M N)) y

State before:
case h.intro
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
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
y : M ⊗[R] N
⊢ (ψ R S M N) ((Ideal.Quotient.lift (kerφ R S M N) (φ R S M N).toRingHom h) ((Ideal.Quotient.mk (kerφ R S M N)) y)) =
    (Ideal.Quotient.mk (kerφ R S M N)) y
Tactic:
simp only [AlgHom.toRingHom_eq_coe, Ideal.Quotient.lift_mk, AlgHom.coe_toRingHom]
State after:
case h.intro
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
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
y : M ⊗[R] N
⊢ (ψ R S M N) ((φ R S M N) y) = (Ideal.Quotient.mk (kerφ R S M N)) y

State before:
case h.intro
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
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
y : M ⊗[R] N
⊢ (ψ R S M N) ((φ R S M N) y) = (Ideal.Quotient.mk (kerφ R S M N)) y
Tactic:
induction y using TensorProduct.induction_on with
| zero => simp only [RingHom.map_zero, AlgHom.map_zero]
| tmul m n => simp only [ψ_apply, φ_apply]
| add x y hx hy =>
  simp only [RingHom.map_add, AlgHom.map_add, ← Ideal.Quotient.mkₐ_eq_mk, hx, hy]
State after:
no goals

State before:
case h.intro.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
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
⊢ (ψ R S M N) ((φ R S M N) 0) = (Ideal.Quotient.mk (kerφ R S M N)) 0
Tactic:
simp only [RingHom.map_zero, AlgHom.map_zero]
State after:
no goals

State before:
case h.intro.tmul
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
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
m : M
n : N
⊢ (ψ R S M N) ((φ R S M N) (m ⊗ₜ[R] n)) = (Ideal.Quotient.mk (kerφ R S M N)) (m ⊗ₜ[R] n)
Tactic:
simp only [ψ_apply, φ_apply]
State after:
no goals

State before:
case h.intro.add
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
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
x y : M ⊗[R] N
hx : (ψ R S M N) ((φ R S M N) x) = (Ideal.Quotient.mk (kerφ R S M N)) x
hy : (ψ R S M N) ((φ R S M N) y) = (Ideal.Quotient.mk (kerφ R S M N)) y
⊢ (ψ R S M N) ((φ R S M N) (x + y)) = (Ideal.Quotient.mk (kerφ R S M N)) (x + y)
Tactic:
simp only [RingHom.map_add, AlgHom.map_add, ← Ideal.Quotient.mkₐ_eq_mk, hx, hy]
State after:
no goals