Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommRing R
S : Type u_2
inst✝¹⁰ : CommRing S
R' : Type u_3
S' : Type u_4
inst✝⁹ : CommRing R'
inst✝⁸ : CommRing S'
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R R'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S'
inst✝² : IsScalarTower R S S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : Module.Flat R S
surj : Function.Surjective ⇑(algebraMap R R')
surjS : Function.Surjective ⇑(algebraMap S S')
eqmap : RingHom.ker (algebraMap S S') = Ideal.map (algebraMap R S) (RingHom.ker (algebraMap R R'))
sq0 : RingHom.ker (algebraMap R R') ^ 2 = ⊥
smoothq : FormallySmooth R' S'
P : Extension R S := (Generators.self R S).toExtension
this✝³ : FormallySmooth R P.Ring := instFormallySmoothMvPolynomial S
IP✝ : Ideal P.Ring := Ideal.map (algebraMap R P.Ring) (RingHom.ker (algebraMap R R'))
Gen : Generators R' S' S :=
  { val := ⇑(algebraMap S S'), σ' := fun s' ↦ MvPolynomial.X (Classical.choose ⋯), aeval_val_σ' := ⋯,
    algebraMap_eq := ⋯ }
P' : Extension R' S' := Gen.toExtension
this✝² : FormallySmooth R' P'.Ring := instFormallySmoothMvPolynomial S
this✝¹ : Algebra P.Ring P'.Ring := MvPolynomial.algebraMvPolynomial
this✝ : IsScalarTower R P.Ring P'.Ring :=
  IsScalarTower.of_algebraMap_eq fun x ↦ Eq.symm (MvPolynomial.map_C (algebraMap R R') x)
algInst✝ : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
scalarTowerInst✝ : IsScalarTower P.Ring S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap P.Ring S'))
this : IsScalarTower P.Ring P'.Ring S'
J : Ideal P.Ring := RingHom.ker (algebraMap P.Ring S)
J' : Ideal P'.Ring := RingHom.ker (algebraMap P'.Ring S')
I : Ideal R := RingHom.ker (algebraMap R R')
IS : Ideal S := Ideal.map (algebraMap R S) I
kerS : RingHom.ker (algebraMap S S') = IS
IP : Ideal P.Ring := Ideal.map (algebraMap R P.Ring) I
kerP : RingHom.ker (algebraMap P.Ring P'.Ring) = IP
surjPP' : Function.Surjective ⇑(algebraMap P.Ring P'.Ring)
ISeq : IS = Ideal.map (algebraMap P.Ring S) IP
surjP : Function.Surjective ⇑(algebraMap P.Ring S)
surjP' : Function.Surjective ⇑(algebraMap P'.Ring S')
σ : TensorProduct P'.Ring S' Ω[P'.Ring⁄R'] →ₗ[P'.Ring] (RingHom.ker (algebraMap P'.Ring S')).Cotangent
hσ : σ ∘ₗ KaehlerDifferential.kerCotangentToTensor R' P'.Ring S' = LinearMap.id
infeq : IP ⊓ J = IP * J
h : Ideal.comap (algebraMap P.Ring P'.Ring) J' = RingHom.ker (algebraMap P.Ring P'.Ring) ⊔ J
Jle : J ≤ Ideal.comap (algebraMap P.Ring P'.Ring) J'
mapcot : J.Cotangent →ₗ[P.Ring] J'.Cotangent := J.mapCotangent J' (ofId P.Ring P'.Ring) Jle
cotsurj : Function.Surjective ⇑mapcot
cotker : mapcot.ker = Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (IP * J))
cottoTen : (RingHom.ker (algebraMap P.Ring S)).Cotangent →ₗ[P.Ring] TensorProduct P.Ring S Ω[P.Ring⁄R] :=
  KaehlerDifferential.kerCotangentToTensor R P.Ring S
cottoTen' : (RingHom.ker (algebraMap P'.Ring S')).Cotangent →ₗ[P'.Ring] TensorProduct P'.Ring S' Ω[P'.Ring⁄R'] :=
  KaehlerDifferential.kerCotangentToTensor R' P'.Ring S'
mapTen : TensorProduct P.Ring S Ω[P.Ring⁄R] →ₗ[P.Ring] TensorProduct P'.Ring S' Ω[P'.Ring⁄R'] :=
  _root_.TensorProduct.lift
    ((LinearMap.restrictScalars₁₂ P.Ring P.Ring (TensorProduct.mk P'.Ring S' Ω[P'.Ring⁄R'])).compl₂
        (KaehlerDifferential.map R R' P.Ring P'.Ring) ∘ₗ
      (IsScalarTower.toAlgHom P.Ring S S').toLinearMap)
⊢ ∃ l, l ∘ₗ KaehlerDifferential.kerCotangentToTensor R P.Ring S = LinearMap.id

Tactic:
have comm : (cottoTen'.restrictScalars P.Ring).comp mapcot = mapTen.comp cottoTen := by
    ext x
    rcases Ideal.toCotangent_surjective _ x with ⟨y, rfl⟩
    have : (KaehlerDifferential.kerToTensor R' P'.Ring S')
      ⟨(algebraMap P.Ring P'.Ring) y.1, Jle y.2⟩ =
      mapTen ((KaehlerDifferential.kerToTensor R P.Ring S) y) := by
      simp [KaehlerDifferential.kerToTensor, mapTen]
    simpa [mapcot] using! this

Goal state after:
R : Type u_1
inst✝¹¹ : CommRing R
S : Type u_2
inst✝¹⁰ : CommRing S
R' : Type u_3
S' : Type u_4
inst✝⁹ : CommRing R'
inst✝⁸ : CommRing S'
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R R'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S'
inst✝² : IsScalarTower R S S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : Module.Flat R S
surj : Function.Surjective ⇑(algebraMap R R')
surjS : Function.Surjective ⇑(algebraMap S S')
eqmap : RingHom.ker (algebraMap S S') = Ideal.map (algebraMap R S) (RingHom.ker (algebraMap R R'))
sq0 : RingHom.ker (algebraMap R R') ^ 2 = ⊥
smoothq : FormallySmooth R' S'
P : Extension R S := (Generators.self R S).toExtension
this✝³ : FormallySmooth R P.Ring := instFormallySmoothMvPolynomial S
IP✝ : Ideal P.Ring := Ideal.map (algebraMap R P.Ring) (RingHom.ker (algebraMap R R'))
Gen : Generators R' S' S :=
  { val := ⇑(algebraMap S S'), σ' := fun s' ↦ MvPolynomial.X (Classical.choose ⋯), aeval_val_σ' := ⋯,
    algebraMap_eq := ⋯ }
P' : Extension R' S' := Gen.toExtension
this✝² : FormallySmooth R' P'.Ring := instFormallySmoothMvPolynomial S
this✝¹ : Algebra P.Ring P'.Ring := MvPolynomial.algebraMvPolynomial
this✝ : IsScalarTower R P.Ring P'.Ring :=
  IsScalarTower.of_algebraMap_eq fun x ↦ Eq.symm (MvPolynomial.map_C (algebraMap R R') x)
algInst✝ : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
scalarTowerInst✝ : IsScalarTower P.Ring S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap P.Ring S'))
this : IsScalarTower P.Ring P'.Ring S'
J : Ideal P.Ring := RingHom.ker (algebraMap P.Ring S)
J' : Ideal P'.Ring := RingHom.ker (algebraMap P'.Ring S')
I : Ideal R := RingHom.ker (algebraMap R R')
IS : Ideal S := Ideal.map (algebraMap R S) I
kerS : RingHom.ker (algebraMap S S') = IS
IP : Ideal P.Ring := Ideal.map (algebraMap R P.Ring) I
kerP : RingHom.ker (algebraMap P.Ring P'.Ring) = IP
surjPP' : Function.Surjective ⇑(algebraMap P.Ring P'.Ring)
ISeq : IS = Ideal.map (algebraMap P.Ring S) IP
surjP : Function.Surjective ⇑(algebraMap P.Ring S)
surjP' : Function.Surjective ⇑(algebraMap P'.Ring S')
σ : TensorProduct P'.Ring S' Ω[P'.Ring⁄R'] →ₗ[P'.Ring] (RingHom.ker (algebraMap P'.Ring S')).Cotangent
hσ : σ ∘ₗ KaehlerDifferential.kerCotangentToTensor R' P'.Ring S' = LinearMap.id
infeq : IP ⊓ J = IP * J
h : Ideal.comap (algebraMap P.Ring P'.Ring) J' = RingHom.ker (algebraMap P.Ring P'.Ring) ⊔ J
Jle : J ≤ Ideal.comap (algebraMap P.Ring P'.Ring) J'
mapcot : J.Cotangent →ₗ[P.Ring] J'.Cotangent := J.mapCotangent J' (ofId P.Ring P'.Ring) Jle
cotsurj : Function.Surjective ⇑mapcot
cotker : mapcot.ker = Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (IP * J))
cottoTen : (RingHom.ker (algebraMap P.Ring S)).Cotangent →ₗ[P.Ring] TensorProduct P.Ring S Ω[P.Ring⁄R] :=
  KaehlerDifferential.kerCotangentToTensor R P.Ring S
cottoTen' : (RingHom.ker (algebraMap P'.Ring S')).Cotangent →ₗ[P'.Ring] TensorProduct P'.Ring S' Ω[P'.Ring⁄R'] :=
  KaehlerDifferential.kerCotangentToTensor R' P'.Ring S'
mapTen : TensorProduct P.Ring S Ω[P.Ring⁄R] →ₗ[P.Ring] TensorProduct P'.Ring S' Ω[P'.Ring⁄R'] :=
  _root_.TensorProduct.lift
    ((LinearMap.restrictScalars₁₂ P.Ring P.Ring (TensorProduct.mk P'.Ring S' Ω[P'.Ring⁄R'])).compl₂
        (KaehlerDifferential.map R R' P.Ring P'.Ring) ∘ₗ
      (IsScalarTower.toAlgHom P.Ring S S').toLinearMap)
comm : ↑P.Ring cottoTen' ∘ₗ mapcot = mapTen ∘ₗ cottoTen
⊢ ∃ l, l ∘ₗ KaehlerDifferential.kerCotangentToTensor R P.Ring S = LinearMap.id