Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Smooth A B
P : Presentation A B (Fin (Presentation.ofFinitePresentationVars A B))
  (Fin (Presentation.ofFinitePresentationRels A B)) :=
  Presentation.ofFinitePresentation A B
f : P.Ring →ₐ[A] B := IsScalarTower.toAlgHom A P.Ring B
hkerf : RingHom.ker f = Ideal.span (Set.range P.relation)
σ : B →ₐ[A] MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A ⧸ RingHom.ker f ^ 2
hsig✝ : f.kerSquareLift.comp σ = AlgHom.id A B
h : Fin (Presentation.ofFinitePresentationVars A B) → MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A
hh :
  ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), (Ideal.Quotient.mk (RingHom.ker f ^ 2)) (h i) = σ (P.val i)
hdiag : (Ideal.Quotient.mkₐ A (RingHom.ker f ^ 2)).comp (aeval h) = σ.comp (aeval P.val)
p :
  Fin (Presentation.ofFinitePresentationRels A B) →
    MvPolynomial (Fin (Presentation.ofFinitePresentationRels A B))
      (MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A)
homog : ∀ (j : Fin (Presentation.ofFinitePresentationRels A B)), (p j).IsHomogeneous 2
hp : ∀ (j : Fin (Presentation.ofFinitePresentationRels A B)), (eval P.relation) (p j) = (aeval h) (P.relation j)
hsig : ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), f (h i) = P.val i
q :
  Fin (Presentation.ofFinitePresentationVars A B) →
    MvPolynomial (Fin (Presentation.ofFinitePresentationRels A B)) P.Ring
hqhom : ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), (q i).IsHomogeneous 1
hq : ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), (eval P.relation) (q i) = h i - X i
D : DescentAux A B :=
  { vars := Fin (Presentation.ofFinitePresentationVars A B), rels := Fin (Presentation.ofFinitePresentationRels A B),
    P := P, σ := σ, h := h, p := p, hphom := homog, hp := hp, q := q, hqhom := hqhom, hq := hq }
this : P.HasCoeffs ↥(DescentAux.subalgebra R D)
⊢ ∃ A₀ B₀ x x_1, A₀.FG ∧ Smooth (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)

Tactic:
obtain ⟨σ₀, hσ₀⟩ := D.exists_kerSquareLift_comp_eq_id R

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
A : Type u
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Smooth A B
P : Presentation A B (Fin (Presentation.ofFinitePresentationVars A B))
  (Fin (Presentation.ofFinitePresentationRels A B)) :=
  Presentation.ofFinitePresentation A B
f : P.Ring →ₐ[A] B := IsScalarTower.toAlgHom A P.Ring B
hkerf : RingHom.ker f = Ideal.span (Set.range P.relation)
σ : B →ₐ[A] MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A ⧸ RingHom.ker f ^ 2
hsig✝ : f.kerSquareLift.comp σ = AlgHom.id A B
h : Fin (Presentation.ofFinitePresentationVars A B) → MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A
hh :
  ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), (Ideal.Quotient.mk (RingHom.ker f ^ 2)) (h i) = σ (P.val i)
hdiag : (Ideal.Quotient.mkₐ A (RingHom.ker f ^ 2)).comp (aeval h) = σ.comp (aeval P.val)
p :
  Fin (Presentation.ofFinitePresentationRels A B) →
    MvPolynomial (Fin (Presentation.ofFinitePresentationRels A B))
      (MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A)
homog : ∀ (j : Fin (Presentation.ofFinitePresentationRels A B)), (p j).IsHomogeneous 2
hp : ∀ (j : Fin (Presentation.ofFinitePresentationRels A B)), (eval P.relation) (p j) = (aeval h) (P.relation j)
hsig : ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), f (h i) = P.val i
q :
  Fin (Presentation.ofFinitePresentationVars A B) →
    MvPolynomial (Fin (Presentation.ofFinitePresentationRels A B)) P.Ring
hqhom : ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), (q i).IsHomogeneous 1
hq : ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), (eval P.relation) (q i) = h i - X i
D : DescentAux A B :=
  { vars := Fin (Presentation.ofFinitePresentationVars A B), rels := Fin (Presentation.ofFinitePresentationRels A B),
    P := P, σ := σ, h := h, p := p, hphom := homog, hp := hp, q := q, hqhom := hqhom, hq := hq }
this : P.HasCoeffs ↥(DescentAux.subalgebra R D)
σ₀ :
  Presentation.ModelOfHasCoeffs ↥(DescentAux.subalgebra R D) →ₐ[↥(DescentAux.subalgebra R D)]
    MvPolynomial D.vars ↥(DescentAux.subalgebra R D) ⧸
      RingHom.ker
          (Ideal.Quotient.mkₐ (↥(DescentAux.subalgebra R D))
            (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(DescentAux.subalgebra R D))))) ^
        2
hσ₀ :
  (Ideal.Quotient.mkₐ (↥(DescentAux.subalgebra R D))
            (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(DescentAux.subalgebra R D))))).kerSquareLift.comp
      σ₀ =
    AlgHom.id (↥(DescentAux.subalgebra R D)) (Presentation.ModelOfHasCoeffs ↥(DescentAux.subalgebra R D))
⊢ ∃ A₀ B₀ x x_1, A₀.FG ∧ Smooth (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)