-- Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
/-- If `g` is surjective, then the kernel of `(id A) ⊗ g` is generated by the kernel of `g` -/
lemma Algebra.TensorProduct.lTensor_ker (hg : Function.Surjective g) :
    RingHom.ker (map (AlgHom.id R A) g) =
      (RingHom.ker g).map (Algebra.TensorProduct.includeRight : C →ₐ[R] A ⊗[R] C)

Proof state:
R : Type u_4
inst✝⁶ : CommRing R
A : Type u_5
C : Type u_7
D : Type u_8
inst✝⁵ : Ring A
inst✝⁴ : Ring C
inst✝³ : Ring D
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Algebra R D
g : C →ₐ[R] D
hg : Function.Surjective ⇑g
this :
  Submodule.restrictScalars R (RingHom.ker (map (AlgHom.id R A) g)) = LinearMap.ker (LinearMap.lTensor A g.toLinearMap)
⊢ LinearMap.ker (LinearMap.lTensor A g.toLinearMap) =
    LinearMap.range (LinearMap.lTensor A (Submodule.restrictScalars R (RingHom.ker g)).subtype)

Tactic:
rw [(lTensor_exact A g.toLinearMap.exact_subtype_ker_map hg).linearMap_ker_eq]

Result:
R : Type u_4
inst✝⁶ : CommRing R
A : Type u_5
C : Type u_7
D : Type u_8
inst✝⁵ : Ring A
inst✝⁴ : Ring C
inst✝³ : Ring D
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Algebra R D
g : C →ₐ[R] D
hg : Function.Surjective ⇑g
this :
  Submodule.restrictScalars R (RingHom.ker (map (AlgHom.id R A) g)) = LinearMap.ker (LinearMap.lTensor A g.toLinearMap)
⊢ LinearMap.range (LinearMap.lTensor A (LinearMap.ker g.toLinearMap).subtype) =
    LinearMap.range (LinearMap.lTensor A (Submodule.restrictScalars R (RingHom.ker g)).subtype)

Proof state:
R : Type u_4
inst✝⁶ : CommRing R
A : Type u_5
C : Type u_7
D : Type u_8
inst✝⁵ : Ring A
inst✝⁴ : Ring C
inst✝³ : Ring D
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Algebra R D
g : C →ₐ[R] D
hg : Function.Surjective ⇑g
this :
  Submodule.restrictScalars R (RingHom.ker (map (AlgHom.id R A) g)) = LinearMap.ker (LinearMap.lTensor A g.toLinearMap)
⊢ LinearMap.range (LinearMap.lTensor A (LinearMap.ker g.toLinearMap).subtype) =
    LinearMap.range (LinearMap.lTensor A (Submodule.restrictScalars R (RingHom.ker g)).subtype)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_4
inst✝⁶ : CommRing R
A : Type u_5
C : Type u_7
D : Type u_8
inst✝⁵ : Ring A
inst✝⁴ : Ring C
inst✝³ : Ring D
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Algebra R D
g : C →ₐ[R] D
hg : Function.Surjective ⇑g
⊢ RingHom.ker (map (AlgHom.id R A) g) = Ideal.map includeRight (RingHom.ker g)

Tactic:
rw [← Submodule.restrictScalars_inj R]

Result:
R : Type u_4
inst✝⁶ : CommRing R
A : Type u_5
C : Type u_7
D : Type u_8
inst✝⁵ : Ring A
inst✝⁴ : Ring C
inst✝³ : Ring D
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Algebra R D
g : C →ₐ[R] D
hg : Function.Surjective ⇑g
⊢ Submodule.restrictScalars R (RingHom.ker (map (AlgHom.id R A) g)) =
    Submodule.restrictScalars R (Ideal.map includeRight (RingHom.ker g))

Proof state:
R : Type u_4
inst✝⁶ : CommRing R
A : Type u_5
C : Type u_7
D : Type u_8
inst✝⁵ : Ring A
inst✝⁴ : Ring C
inst✝³ : Ring D
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Algebra R D
g : C →ₐ[R] D
hg : Function.Surjective ⇑g
⊢ Submodule.restrictScalars R (RingHom.ker (map (AlgHom.id R A) g)) =
    Submodule.restrictScalars R (Ideal.map includeRight (RingHom.ker g))

Tactic:
have : (RingHom.ker (map (AlgHom.id R A) g)).restrictScalars R =
  LinearMap.ker (LinearMap.lTensor A (AlgHom.toLinearMap g)) := rfl

Result:
R : Type u_4
inst✝⁶ : CommRing R
A : Type u_5
C : Type u_7
D : Type u_8
inst✝⁵ : Ring A
inst✝⁴ : Ring C
inst✝³ : Ring D
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Algebra R D
g : C →ₐ[R] D
hg : Function.Surjective ⇑g
this :
  Submodule.restrictScalars R (RingHom.ker (map (AlgHom.id R A) g)) = LinearMap.ker (LinearMap.lTensor A g.toLinearMap)
⊢ Submodule.restrictScalars R (RingHom.ker (map (AlgHom.id R A) g)) =
    Submodule.restrictScalars R (Ideal.map includeRight (RingHom.ker g))

Proof state:
R : Type u_4
inst✝⁶ : CommRing R
A : Type u_5
C : Type u_7
D : Type u_8
inst✝⁵ : Ring A
inst✝⁴ : Ring C
inst✝³ : Ring D
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Algebra R D
g : C →ₐ[R] D
hg : Function.Surjective ⇑g
this :
  Submodule.restrictScalars R (RingHom.ker (map (AlgHom.id R A) g)) = LinearMap.ker (LinearMap.lTensor A g.toLinearMap)
⊢ Submodule.restrictScalars R (RingHom.ker (map (AlgHom.id R A) g)) =
    Submodule.restrictScalars R (Ideal.map includeRight (RingHom.ker g))

Tactic:
rw [this, Ideal.map_includeRight_eq]

Result:
R : Type u_4
inst✝⁶ : CommRing R
A : Type u_5
C : Type u_7
D : Type u_8
inst✝⁵ : Ring A
inst✝⁴ : Ring C
inst✝³ : Ring D
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Algebra R D
g : C →ₐ[R] D
hg : Function.Surjective ⇑g
this :
  Submodule.restrictScalars R (RingHom.ker (map (AlgHom.id R A) g)) = LinearMap.ker (LinearMap.lTensor A g.toLinearMap)
⊢ LinearMap.ker (LinearMap.lTensor A g.toLinearMap) =
    LinearMap.range (LinearMap.lTensor A (Submodule.restrictScalars R (RingHom.ker g)).subtype)