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)
comm : ↑P.Ring cottoTen' ∘ₗ mapcot = mapTen ∘ₗ cottoTen
ediff : Ω[P.Ring⁄R] ≃ₗ[P.Ring] S →₀ P.Ring := KaehlerDifferential.mvPolynomialEquiv R S
eTen : TensorProduct P.Ring S Ω[P.Ring⁄R] ≃ₗ[P.Ring] S →₀ S :=
  LinearEquiv.lTensor S ediff ≪≫ₗ TensorProduct.finsuppRight P.Ring P.Ring S P.Ring S ≪≫ₗ
    Finsupp.mapRange.linearEquiv (_root_.TensorProduct.rid P.Ring S)
toJ'cot : (S →₀ S) →ₗ[P.Ring] J'.Cotangent := (↑P.Ring σ ∘ₗ mapTen) ∘ₗ ↑eTen.symm
eS : (P.Ring ⧸ J) ≃ₗ[P.Ring] S :=
  Submodule.quotEquivOfEq J J ⋯ ≪≫ₗ (Algebra.linearMap P.Ring S).quotKerEquivOfSurjective surjP
toJcot : (S →₀ S) →ₗ[P.Ring] J.Cotangent :=
  (Finsupp.lsum P.Ring) fun s ↦
    ↑P.Ring (LinearMap.toSpanSingleton (P.Ring ⧸ J) J.Cotangent (Classical.choose ⋯)) ∘ₗ ↑eS.symm
⊢ ∃ l, l ∘ₗ KaehlerDifferential.kerCotangentToTensor R P.Ring S = LinearMap.id

Tactic:
have toJcot_spec : mapcot.comp toJcot = toJ'cot := by
    ext i s
    simp only [LinearMap.comp_assoc, toJcot, Finsupp.lsum_comp_lsingle]
    rcases Ideal.Quotient.mk_surjective (eS.symm s) with ⟨p, hp⟩
    have (x : J.Cotangent) : mapcot (eS.symm s • x) = p • mapcot x := hp ▸ map_smul mapcot p x
    have psmul : p • 1 = s := by simpa [Algebra.smul_def, eS] using! eS.eq_symm_apply.mp hp
    simp [this, Classical.choose_spec (cotsurj (toJ'cot (Finsupp.single i 1))), ← map_smul, psmul]

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
ediff : Ω[P.Ring⁄R] ≃ₗ[P.Ring] S →₀ P.Ring := KaehlerDifferential.mvPolynomialEquiv R S
eTen : TensorProduct P.Ring S Ω[P.Ring⁄R] ≃ₗ[P.Ring] S →₀ S :=
  LinearEquiv.lTensor S ediff ≪≫ₗ TensorProduct.finsuppRight P.Ring P.Ring S P.Ring S ≪≫ₗ
    Finsupp.mapRange.linearEquiv (_root_.TensorProduct.rid P.Ring S)
toJ'cot : (S →₀ S) →ₗ[P.Ring] J'.Cotangent := (↑P.Ring σ ∘ₗ mapTen) ∘ₗ ↑eTen.symm
eS : (P.Ring ⧸ J) ≃ₗ[P.Ring] S :=
  Submodule.quotEquivOfEq J J ⋯ ≪≫ₗ (Algebra.linearMap P.Ring S).quotKerEquivOfSurjective surjP
toJcot : (S →₀ S) →ₗ[P.Ring] J.Cotangent :=
  (Finsupp.lsum P.Ring) fun s ↦
    ↑P.Ring (LinearMap.toSpanSingleton (P.Ring ⧸ J) J.Cotangent (Classical.choose ⋯)) ∘ₗ ↑eS.symm
toJcot_spec : mapcot ∘ₗ toJcot = toJ'cot
⊢ ∃ l, l ∘ₗ KaehlerDifferential.kerCotangentToTensor R P.Ring S = LinearMap.id