[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type u
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
I : Ideal B
⊢ FormallyEtale R A ↔ FormallyUnramified R A ∧ FormallySmooth R A
[PROOFSTEP]
rw [FormallyUnramified_iff, FormallySmooth_iff, FormallyEtale_iff]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type u
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
I : Ideal B
⊢ (∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
      I ^ 2 = ⊥ → Function.Bijective (AlgHom.comp (Ideal.Quotient.mkₐ R I))) ↔
    (∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
        I ^ 2 = ⊥ → Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R I))) ∧
      ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
        I ^ 2 = ⊥ → Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
[PROOFSTEP]
simp_rw [← forall_and]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type u
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
I : Ideal B
⊢ (∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
      I ^ 2 = ⊥ → Function.Bijective (AlgHom.comp (Ideal.Quotient.mkₐ R I))) ↔
    ∀ (x : Type u) (x_1 : CommRing x) (x_2 : Algebra R x) (x_3 : Ideal x),
      x_3 ^ 2 = ⊥ →
        Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R x_3)) ∧
          Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R x_3))
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
A : Type u
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B✝ : Type u
inst✝³ : CommRing B✝
inst✝² : Algebra R B✝
I✝ : Ideal B✝
B : Type u
inst✝¹ : CommRing B
_RB : Algebra R B
inst✝ : FormallyUnramified R A
I : Ideal B
hI : IsNilpotent I
g₁ g₂ : A →ₐ[R] B
h : AlgHom.comp (Ideal.Quotient.mkₐ R I) g₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) g₂
⊢ g₁ = g₂
[PROOFSTEP]
revert g₁ g₂
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
A : Type u
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B✝ : Type u
inst✝³ : CommRing B✝
inst✝² : Algebra R B✝
I✝ : Ideal B✝
B : Type u
inst✝¹ : CommRing B
_RB : Algebra R B
inst✝ : FormallyUnramified R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ (g₁ g₂ : A →ₐ[R] B), AlgHom.comp (Ideal.Quotient.mkₐ R I) g₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) g₂ → g₁ = g₂
[PROOFSTEP]
change Function.Injective (Ideal.Quotient.mkₐ R I).comp
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
A : Type u
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B✝ : Type u
inst✝³ : CommRing B✝
inst✝² : Algebra R B✝
I✝ : Ideal B✝
B : Type u
inst✝¹ : CommRing B
_RB : Algebra R B
inst✝ : FormallyUnramified R A
I : Ideal B
hI : IsNilpotent I
⊢ Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
[PROOFSTEP]
revert _RB
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
A : Type u
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B✝ : Type u
inst✝³ : CommRing B✝
inst✝² : Algebra R B✝
I✝ : Ideal B✝
B : Type u
inst✝¹ : CommRing B
inst✝ : FormallyUnramified R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ [_RB : Algebra R B], Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
[PROOFSTEP]
apply Ideal.IsNilpotent.induction_on (R := B) I hI
[GOAL]
case h₁
R : Type u
inst✝⁶ : CommSemiring R
A : Type u
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B✝ : Type u
inst✝³ : CommRing B✝
inst✝² : Algebra R B✝
I✝ : Ideal B✝
B : Type u
inst✝¹ : CommRing B
inst✝ : FormallyUnramified R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ ⦃S : Type u⦄ [inst : CommRing S] (I : Ideal S),
    I ^ 2 = ⊥ → ∀ [_RB : Algebra R S], Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
[PROOFSTEP]
intro B _ I hI _
[GOAL]
case h₁
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B✝¹ : Type u
inst✝⁴ : CommRing B✝¹
inst✝³ : Algebra R B✝¹
I✝¹ : Ideal B✝¹
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallyUnramified R A
I✝ : Ideal B✝
hI✝ : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I : Ideal B
hI : I ^ 2 = ⊥
_RB✝ : Algebra R B
⊢ Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
[PROOFSTEP]
exact FormallyUnramified.comp_injective I hI
[GOAL]
case h₂
R : Type u
inst✝⁶ : CommSemiring R
A : Type u
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B✝ : Type u
inst✝³ : CommRing B✝
inst✝² : Algebra R B✝
I✝ : Ideal B✝
B : Type u
inst✝¹ : CommRing B
inst✝ : FormallyUnramified R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ ⦃S : Type u⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ [_RB : Algebra R S], Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R I))) →
        (∀ [_RB : Algebra R (S ⧸ I)],
            Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)))) →
          ∀ [_RB : Algebra R S], Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R J))
[PROOFSTEP]
intro B _ I J hIJ h₁ h₂ _ g₁ g₂ e
[GOAL]
case h₂
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B✝¹ : Type u
inst✝⁴ : CommRing B✝¹
inst✝³ : Algebra R B✝¹
I✝¹ : Ideal B✝¹
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallyUnramified R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [_RB : Algebra R B], Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [_RB : Algebra R (B ⧸ I)],
    Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)))
_RB✝ : Algebra R B
g₁ g₂ : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R J) g₁ = AlgHom.comp (Ideal.Quotient.mkₐ R J) g₂
⊢ g₁ = g₂
[PROOFSTEP]
apply h₁
[GOAL]
case h₂.a
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B✝¹ : Type u
inst✝⁴ : CommRing B✝¹
inst✝³ : Algebra R B✝¹
I✝¹ : Ideal B✝¹
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallyUnramified R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [_RB : Algebra R B], Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [_RB : Algebra R (B ⧸ I)],
    Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)))
_RB✝ : Algebra R B
g₁ g₂ : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R J) g₁ = AlgHom.comp (Ideal.Quotient.mkₐ R J) g₂
⊢ AlgHom.comp (Ideal.Quotient.mkₐ R I) g₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) g₂
[PROOFSTEP]
apply h₂
[GOAL]
case h₂.a.a
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B✝¹ : Type u
inst✝⁴ : CommRing B✝¹
inst✝³ : Algebra R B✝¹
I✝¹ : Ideal B✝¹
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallyUnramified R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [_RB : Algebra R B], Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [_RB : Algebra R (B ⧸ I)],
    Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)))
_RB✝ : Algebra R B
g₁ g₂ : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R J) g₁ = AlgHom.comp (Ideal.Quotient.mkₐ R J) g₂
⊢ AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₁) =
    AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₂)
[PROOFSTEP]
ext x
[GOAL]
case h₂.a.a.H
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B✝¹ : Type u
inst✝⁴ : CommRing B✝¹
inst✝³ : Algebra R B✝¹
I✝¹ : Ideal B✝¹
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallyUnramified R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [_RB : Algebra R B], Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [_RB : Algebra R (B ⧸ I)],
    Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)))
_RB✝ : Algebra R B
g₁ g₂ : A →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R J) g₁ = AlgHom.comp (Ideal.Quotient.mkₐ R J) g₂
x : A
⊢ ↑(AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₁))
      x =
    ↑(AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₂))
      x
[PROOFSTEP]
replace e := AlgHom.congr_fun e x
[GOAL]
case h₂.a.a.H
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B✝¹ : Type u
inst✝⁴ : CommRing B✝¹
inst✝³ : Algebra R B✝¹
I✝¹ : Ideal B✝¹
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallyUnramified R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [_RB : Algebra R B], Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [_RB : Algebra R (B ⧸ I)],
    Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)))
_RB✝ : Algebra R B
g₁ g₂ : A →ₐ[R] B
x : A
e : ↑(AlgHom.comp (Ideal.Quotient.mkₐ R J) g₁) x = ↑(AlgHom.comp (Ideal.Quotient.mkₐ R J) g₂) x
⊢ ↑(AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₁))
      x =
    ↑(AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₂))
      x
[PROOFSTEP]
dsimp only [AlgHom.comp_apply, Ideal.Quotient.mkₐ_eq_mk] at e ⊢
[GOAL]
case h₂.a.a.H
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B✝¹ : Type u
inst✝⁴ : CommRing B✝¹
inst✝³ : Algebra R B✝¹
I✝¹ : Ideal B✝¹
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallyUnramified R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [_RB : Algebra R B], Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [_RB : Algebra R (B ⧸ I)],
    Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)))
_RB✝ : Algebra R B
g₁ g₂ : A →ₐ[R] B
x : A
e : ↑(Ideal.Quotient.mk J) (↑g₁ x) = ↑(Ideal.Quotient.mk J) (↑g₂ x)
⊢ ↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) (↑(Ideal.Quotient.mk I) (↑g₁ x)) =
    ↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) (↑(Ideal.Quotient.mk I) (↑g₂ x))
[PROOFSTEP]
rwa [Ideal.Quotient.eq, ← map_sub, Ideal.mem_quotient_iff_mem hIJ, ← Ideal.Quotient.eq]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
A : Type u
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B : Type u
inst✝³ : CommRing B
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : FormallyUnramified R A
C : Type u
inst✝ : CommRing C
f : B →+* C
hf : IsNilpotent (RingHom.ker f)
g₁ g₂ : A →ₐ[R] B
h : RingHom.comp f ↑g₁ = RingHom.comp f ↑g₂
⊢ AlgHom.comp (Ideal.Quotient.mkₐ R (RingHom.ker f)) g₁ = AlgHom.comp (Ideal.Quotient.mkₐ R (RingHom.ker f)) g₂
[PROOFSTEP]
ext x
[GOAL]
case H
R : Type u
inst✝⁶ : CommSemiring R
A : Type u
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B : Type u
inst✝³ : CommRing B
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : FormallyUnramified R A
C : Type u
inst✝ : CommRing C
f : B →+* C
hf : IsNilpotent (RingHom.ker f)
g₁ g₂ : A →ₐ[R] B
h : RingHom.comp f ↑g₁ = RingHom.comp f ↑g₂
x : A
⊢ ↑(AlgHom.comp (Ideal.Quotient.mkₐ R (RingHom.ker f)) g₁) x =
    ↑(AlgHom.comp (Ideal.Quotient.mkₐ R (RingHom.ker f)) g₂) x
[PROOFSTEP]
have := RingHom.congr_fun h x
[GOAL]
case H
R : Type u
inst✝⁶ : CommSemiring R
A : Type u
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B : Type u
inst✝³ : CommRing B
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : FormallyUnramified R A
C : Type u
inst✝ : CommRing C
f : B →+* C
hf : IsNilpotent (RingHom.ker f)
g₁ g₂ : A →ₐ[R] B
h : RingHom.comp f ↑g₁ = RingHom.comp f ↑g₂
x : A
this : ↑(RingHom.comp f ↑g₁) x = ↑(RingHom.comp f ↑g₂) x
⊢ ↑(AlgHom.comp (Ideal.Quotient.mkₐ R (RingHom.ker f)) g₁) x =
    ↑(AlgHom.comp (Ideal.Quotient.mkₐ R (RingHom.ker f)) g₂) x
[PROOFSTEP]
simpa only [Ideal.Quotient.eq, Function.comp_apply, AlgHom.coe_comp, Ideal.Quotient.mkₐ_eq_mk, RingHom.mem_ker, map_sub,
  sub_eq_zero]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
A : Type u
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B✝ : Type u
inst✝³ : CommRing B✝
inst✝² : Algebra R B✝
I✝ : Ideal B✝
B : Type u
inst✝¹ : CommRing B
_RB : Algebra R B
inst✝ : FormallySmooth R A
I : Ideal B
hI : IsNilpotent I
g : A →ₐ[R] B ⧸ I
⊢ ∃ f, AlgHom.comp (Ideal.Quotient.mkₐ R I) f = g
[PROOFSTEP]
revert g
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
A : Type u
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B✝ : Type u
inst✝³ : CommRing B✝
inst✝² : Algebra R B✝
I✝ : Ideal B✝
B : Type u
inst✝¹ : CommRing B
_RB : Algebra R B
inst✝ : FormallySmooth R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ (g : A →ₐ[R] B ⧸ I), ∃ f, AlgHom.comp (Ideal.Quotient.mkₐ R I) f = g
[PROOFSTEP]
change Function.Surjective (Ideal.Quotient.mkₐ R I).comp
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
A : Type u
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B✝ : Type u
inst✝³ : CommRing B✝
inst✝² : Algebra R B✝
I✝ : Ideal B✝
B : Type u
inst✝¹ : CommRing B
_RB : Algebra R B
inst✝ : FormallySmooth R A
I : Ideal B
hI : IsNilpotent I
⊢ Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
[PROOFSTEP]
revert _RB
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
A : Type u
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B✝ : Type u
inst✝³ : CommRing B✝
inst✝² : Algebra R B✝
I✝ : Ideal B✝
B : Type u
inst✝¹ : CommRing B
inst✝ : FormallySmooth R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ [_RB : Algebra R B], Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
[PROOFSTEP]
apply Ideal.IsNilpotent.induction_on (R := B) I hI
[GOAL]
case h₁
R : Type u
inst✝⁶ : CommSemiring R
A : Type u
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B✝ : Type u
inst✝³ : CommRing B✝
inst✝² : Algebra R B✝
I✝ : Ideal B✝
B : Type u
inst✝¹ : CommRing B
inst✝ : FormallySmooth R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ ⦃S : Type u⦄ [inst : CommRing S] (I : Ideal S),
    I ^ 2 = ⊥ → ∀ [_RB : Algebra R S], Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
[PROOFSTEP]
intro B _ I hI _
[GOAL]
case h₁
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B✝¹ : Type u
inst✝⁴ : CommRing B✝¹
inst✝³ : Algebra R B✝¹
I✝¹ : Ideal B✝¹
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I✝ : Ideal B✝
hI✝ : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I : Ideal B
hI : I ^ 2 = ⊥
_RB✝ : Algebra R B
⊢ Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
[PROOFSTEP]
exact FormallySmooth.comp_surjective I hI
[GOAL]
case h₂
R : Type u
inst✝⁶ : CommSemiring R
A : Type u
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B✝ : Type u
inst✝³ : CommRing B✝
inst✝² : Algebra R B✝
I✝ : Ideal B✝
B : Type u
inst✝¹ : CommRing B
inst✝ : FormallySmooth R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ ⦃S : Type u⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ [_RB : Algebra R S], Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R I))) →
        (∀ [_RB : Algebra R (S ⧸ I)],
            Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)))) →
          ∀ [_RB : Algebra R S], Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R J))
[PROOFSTEP]
intro B _ I J hIJ h₁ h₂ _ g
[GOAL]
case h₂
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B✝¹ : Type u
inst✝⁴ : CommRing B✝¹
inst✝³ : Algebra R B✝¹
I✝¹ : Ideal B✝¹
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [_RB : Algebra R B], Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [_RB : Algebra R (B ⧸ I)],
    Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)))
_RB✝ : Algebra R B
g : A →ₐ[R] B ⧸ J
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ R J) a = g
[PROOFSTEP]
let this : ((B ⧸ I) ⧸ J.map (Ideal.Quotient.mk I)) ≃ₐ[R] B ⧸ J :=
  { (DoubleQuot.quotQuotEquivQuotSup I J).trans (Ideal.quotEquivOfEq (sup_eq_right.mpr hIJ)) with
    commutes' := fun x => rfl }
[GOAL]
case h₂
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B✝¹ : Type u
inst✝⁴ : CommRing B✝¹
inst✝³ : Algebra R B✝¹
I✝¹ : Ideal B✝¹
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [_RB : Algebra R B], Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [_RB : Algebra R (B ⧸ I)],
    Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)))
_RB✝ : Algebra R B
g : A →ₐ[R] B ⧸ J
this : ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J) ≃ₐ[R] B ⧸ J :=
  let src := RingEquiv.trans (DoubleQuot.quotQuotEquivQuotSup I J) (Ideal.quotEquivOfEq (_ : I ⊔ J = J));
  { toEquiv := src.toEquiv,
    map_mul' :=
      (_ :
        ∀ (x y : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J),
          Equiv.toFun src.toEquiv (x * y) = Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
    map_add' :=
      (_ :
        ∀ (x y : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J),
          Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
    commutes' :=
      (_ :
        ∀ (x : R),
          Equiv.toFun src.toEquiv (↑(algebraMap R ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x) =
            Equiv.toFun src.toEquiv (↑(algebraMap R ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x)) }
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ R J) a = g
[PROOFSTEP]
obtain ⟨g', e⟩ := h₂ (this.symm.toAlgHom.comp g)
[GOAL]
case h₂.intro
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B✝¹ : Type u
inst✝⁴ : CommRing B✝¹
inst✝³ : Algebra R B✝¹
I✝¹ : Ideal B✝¹
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [_RB : Algebra R B], Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [_RB : Algebra R (B ⧸ I)],
    Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)))
_RB✝ : Algebra R B
g : A →ₐ[R] B ⧸ J
this : ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J) ≃ₐ[R] B ⧸ J :=
  let src := RingEquiv.trans (DoubleQuot.quotQuotEquivQuotSup I J) (Ideal.quotEquivOfEq (_ : I ⊔ J = J));
  { toEquiv := src.toEquiv,
    map_mul' :=
      (_ :
        ∀ (x y : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J),
          Equiv.toFun src.toEquiv (x * y) = Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
    map_add' :=
      (_ :
        ∀ (x y : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J),
          Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
    commutes' :=
      (_ :
        ∀ (x : R),
          Equiv.toFun src.toEquiv (↑(algebraMap R ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x) =
            Equiv.toFun src.toEquiv (↑(algebraMap R ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x)) }
g' : A →ₐ[R] B ⧸ I
e : AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)) g' = AlgHom.comp (↑(AlgEquiv.symm this)) g
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ R J) a = g
[PROOFSTEP]
obtain ⟨g', rfl⟩ := h₁ g'
[GOAL]
case h₂.intro.intro
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B✝¹ : Type u
inst✝⁴ : CommRing B✝¹
inst✝³ : Algebra R B✝¹
I✝¹ : Ideal B✝¹
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [_RB : Algebra R B], Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [_RB : Algebra R (B ⧸ I)],
    Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)))
_RB✝ : Algebra R B
g : A →ₐ[R] B ⧸ J
this : ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J) ≃ₐ[R] B ⧸ J :=
  let src := RingEquiv.trans (DoubleQuot.quotQuotEquivQuotSup I J) (Ideal.quotEquivOfEq (_ : I ⊔ J = J));
  { toEquiv := src.toEquiv,
    map_mul' :=
      (_ :
        ∀ (x y : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J),
          Equiv.toFun src.toEquiv (x * y) = Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
    map_add' :=
      (_ :
        ∀ (x y : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J),
          Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
    commutes' :=
      (_ :
        ∀ (x : R),
          Equiv.toFun src.toEquiv (↑(algebraMap R ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x) =
            Equiv.toFun src.toEquiv (↑(algebraMap R ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x)) }
g' : A →ₐ[R] B
e :
  AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) g') =
    AlgHom.comp (↑(AlgEquiv.symm this)) g
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ R J) a = g
[PROOFSTEP]
replace e := congr_arg this.toAlgHom.comp e
[GOAL]
case h₂.intro.intro
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B✝¹ : Type u
inst✝⁴ : CommRing B✝¹
inst✝³ : Algebra R B✝¹
I✝¹ : Ideal B✝¹
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [_RB : Algebra R B], Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [_RB : Algebra R (B ⧸ I)],
    Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)))
_RB✝ : Algebra R B
g : A →ₐ[R] B ⧸ J
this : ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J) ≃ₐ[R] B ⧸ J :=
  let src := RingEquiv.trans (DoubleQuot.quotQuotEquivQuotSup I J) (Ideal.quotEquivOfEq (_ : I ⊔ J = J));
  { toEquiv := src.toEquiv,
    map_mul' :=
      (_ :
        ∀ (x y : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J),
          Equiv.toFun src.toEquiv (x * y) = Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
    map_add' :=
      (_ :
        ∀ (x y : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J),
          Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
    commutes' :=
      (_ :
        ∀ (x : R),
          Equiv.toFun src.toEquiv (↑(algebraMap R ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x) =
            Equiv.toFun src.toEquiv (↑(algebraMap R ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x)) }
g' : A →ₐ[R] B
e :
  AlgHom.comp (↑this)
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J))
        (AlgHom.comp (Ideal.Quotient.mkₐ R I) g')) =
    AlgHom.comp (↑this) (AlgHom.comp (↑(AlgEquiv.symm this)) g)
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ R J) a = g
[PROOFSTEP]
conv_rhs at e =>
  rw [← AlgHom.comp_assoc, AlgEquiv.toAlgHom_eq_coe, AlgEquiv.toAlgHom_eq_coe, AlgEquiv.comp_symm, AlgHom.id_comp]
[GOAL]
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B✝¹ : Type u
inst✝⁴ : CommRing B✝¹
inst✝³ : Algebra R B✝¹
I✝¹ : Ideal B✝¹
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [_RB : Algebra R B], Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [_RB : Algebra R (B ⧸ I)],
    Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)))
_RB✝ : Algebra R B
g : A →ₐ[R] B ⧸ J
this : ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J) ≃ₐ[R] B ⧸ J :=
  let src := RingEquiv.trans (DoubleQuot.quotQuotEquivQuotSup I J) (Ideal.quotEquivOfEq (_ : I ⊔ J = J));
  { toEquiv := src.toEquiv,
    map_mul' :=
      (_ :
        ∀ (x y : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J),
          Equiv.toFun src.toEquiv (x * y) = Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
    map_add' :=
      (_ :
        ∀ (x y : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J),
          Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
    commutes' :=
      (_ :
        ∀ (x : R),
          Equiv.toFun src.toEquiv (↑(algebraMap R ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x) =
            Equiv.toFun src.toEquiv (↑(algebraMap R ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x)) }
g' : A →ₐ[R] B
e :
  AlgHom.comp (↑this)
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J))
        (AlgHom.comp (Ideal.Quotient.mkₐ R I) g')) =
    AlgHom.comp (↑this) (AlgHom.comp (↑(AlgEquiv.symm this)) g)
| AlgHom.comp (↑this) (AlgHom.comp (↑(AlgEquiv.symm this)) g)
[PROOFSTEP]
rw [← AlgHom.comp_assoc, AlgEquiv.toAlgHom_eq_coe, AlgEquiv.toAlgHom_eq_coe, AlgEquiv.comp_symm, AlgHom.id_comp]
[GOAL]
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B✝¹ : Type u
inst✝⁴ : CommRing B✝¹
inst✝³ : Algebra R B✝¹
I✝¹ : Ideal B✝¹
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [_RB : Algebra R B], Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [_RB : Algebra R (B ⧸ I)],
    Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)))
_RB✝ : Algebra R B
g : A →ₐ[R] B ⧸ J
this : ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J) ≃ₐ[R] B ⧸ J :=
  let src := RingEquiv.trans (DoubleQuot.quotQuotEquivQuotSup I J) (Ideal.quotEquivOfEq (_ : I ⊔ J = J));
  { toEquiv := src.toEquiv,
    map_mul' :=
      (_ :
        ∀ (x y : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J),
          Equiv.toFun src.toEquiv (x * y) = Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
    map_add' :=
      (_ :
        ∀ (x y : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J),
          Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
    commutes' :=
      (_ :
        ∀ (x : R),
          Equiv.toFun src.toEquiv (↑(algebraMap R ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x) =
            Equiv.toFun src.toEquiv (↑(algebraMap R ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x)) }
g' : A →ₐ[R] B
e :
  AlgHom.comp (↑this)
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J))
        (AlgHom.comp (Ideal.Quotient.mkₐ R I) g')) =
    AlgHom.comp (↑this) (AlgHom.comp (↑(AlgEquiv.symm this)) g)
| AlgHom.comp (↑this) (AlgHom.comp (↑(AlgEquiv.symm this)) g)
[PROOFSTEP]
rw [← AlgHom.comp_assoc, AlgEquiv.toAlgHom_eq_coe, AlgEquiv.toAlgHom_eq_coe, AlgEquiv.comp_symm, AlgHom.id_comp]
[GOAL]
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B✝¹ : Type u
inst✝⁴ : CommRing B✝¹
inst✝³ : Algebra R B✝¹
I✝¹ : Ideal B✝¹
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [_RB : Algebra R B], Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [_RB : Algebra R (B ⧸ I)],
    Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)))
_RB✝ : Algebra R B
g : A →ₐ[R] B ⧸ J
this : ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J) ≃ₐ[R] B ⧸ J :=
  let src := RingEquiv.trans (DoubleQuot.quotQuotEquivQuotSup I J) (Ideal.quotEquivOfEq (_ : I ⊔ J = J));
  { toEquiv := src.toEquiv,
    map_mul' :=
      (_ :
        ∀ (x y : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J),
          Equiv.toFun src.toEquiv (x * y) = Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
    map_add' :=
      (_ :
        ∀ (x y : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J),
          Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
    commutes' :=
      (_ :
        ∀ (x : R),
          Equiv.toFun src.toEquiv (↑(algebraMap R ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x) =
            Equiv.toFun src.toEquiv (↑(algebraMap R ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x)) }
g' : A →ₐ[R] B
e :
  AlgHom.comp (↑this)
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J))
        (AlgHom.comp (Ideal.Quotient.mkₐ R I) g')) =
    AlgHom.comp (↑this) (AlgHom.comp (↑(AlgEquiv.symm this)) g)
| AlgHom.comp (↑this) (AlgHom.comp (↑(AlgEquiv.symm this)) g)
[PROOFSTEP]
rw [← AlgHom.comp_assoc, AlgEquiv.toAlgHom_eq_coe, AlgEquiv.toAlgHom_eq_coe, AlgEquiv.comp_symm, AlgHom.id_comp]
[GOAL]
case h₂.intro.intro
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B✝¹ : Type u
inst✝⁴ : CommRing B✝¹
inst✝³ : Algebra R B✝¹
I✝¹ : Ideal B✝¹
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [_RB : Algebra R B], Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [_RB : Algebra R (B ⧸ I)],
    Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)))
_RB✝ : Algebra R B
g : A →ₐ[R] B ⧸ J
this : ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J) ≃ₐ[R] B ⧸ J :=
  let src := RingEquiv.trans (DoubleQuot.quotQuotEquivQuotSup I J) (Ideal.quotEquivOfEq (_ : I ⊔ J = J));
  { toEquiv := src.toEquiv,
    map_mul' :=
      (_ :
        ∀ (x y : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J),
          Equiv.toFun src.toEquiv (x * y) = Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y),
    map_add' :=
      (_ :
        ∀ (x y : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J),
          Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y),
    commutes' :=
      (_ :
        ∀ (x : R),
          Equiv.toFun src.toEquiv (↑(algebraMap R ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x) =
            Equiv.toFun src.toEquiv (↑(algebraMap R ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x)) }
g' : A →ₐ[R] B
e :
  AlgHom.comp (↑this)
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J))
        (AlgHom.comp (Ideal.Quotient.mkₐ R I) g')) =
    g
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ R J) a = g
[PROOFSTEP]
exact ⟨g', e⟩
[GOAL]
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
I : Ideal B
C : Type u
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ↑g
hg' : IsNilpotent (RingHom.ker ↑g)
x : A
⊢ ↑g (↑(liftOfSurjective f g hg hg') x) = ↑f x
[PROOFSTEP]
apply (Ideal.quotientKerAlgEquivOfSurjective hg).symm.injective
[GOAL]
case a
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
I : Ideal B
C : Type u
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ↑g
hg' : IsNilpotent (RingHom.ker ↑g)
x : A
⊢ ↑(AlgEquiv.symm (Ideal.quotientKerAlgEquivOfSurjective hg)) (↑g (↑(liftOfSurjective f g hg hg') x)) =
    ↑(AlgEquiv.symm (Ideal.quotientKerAlgEquivOfSurjective hg)) (↑f x)
[PROOFSTEP]
change _ = ((Ideal.quotientKerAlgEquivOfSurjective hg).symm.toAlgHom.comp f) x
[GOAL]
case a
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
I : Ideal B
C : Type u
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ↑g
hg' : IsNilpotent (RingHom.ker ↑g)
x : A
⊢ ↑(AlgEquiv.symm (Ideal.quotientKerAlgEquivOfSurjective hg)) (↑g (↑(liftOfSurjective f g hg hg') x)) =
    ↑(AlgHom.comp (↑(AlgEquiv.symm (Ideal.quotientKerAlgEquivOfSurjective hg))) f) x
[PROOFSTEP]
rw [← FormallySmooth.mk_lift _ hg' ((Ideal.quotientKerAlgEquivOfSurjective hg).symm.toAlgHom.comp f)]
[GOAL]
case a
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
I : Ideal B
C : Type u
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ↑g
hg' : IsNilpotent (RingHom.ker ↑g)
x : A
⊢ ↑(AlgEquiv.symm (Ideal.quotientKerAlgEquivOfSurjective hg)) (↑g (↑(liftOfSurjective f g hg hg') x)) =
    ↑(Ideal.Quotient.mk (RingHom.ker ↑g))
      (↑(lift (RingHom.ker ↑g) hg' (AlgHom.comp (↑(AlgEquiv.symm (Ideal.quotientKerAlgEquivOfSurjective hg))) f)) x)
[PROOFSTEP]
apply (Ideal.quotientKerAlgEquivOfSurjective hg).injective
[GOAL]
case a.a
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
I : Ideal B
C : Type u
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ↑g
hg' : IsNilpotent (RingHom.ker ↑g)
x : A
⊢ ↑(Ideal.quotientKerAlgEquivOfSurjective hg)
      (↑(AlgEquiv.symm (Ideal.quotientKerAlgEquivOfSurjective hg)) (↑g (↑(liftOfSurjective f g hg hg') x))) =
    ↑(Ideal.quotientKerAlgEquivOfSurjective hg)
      (↑(Ideal.Quotient.mk (RingHom.ker ↑g))
        (↑(lift (RingHom.ker ↑g) hg' (AlgHom.comp (↑(AlgEquiv.symm (Ideal.quotientKerAlgEquivOfSurjective hg))) f)) x))
[PROOFSTEP]
rw [AlgEquiv.apply_symm_apply, Ideal.quotientKerAlgEquivOfSurjective, Ideal.quotientKerAlgEquivOfRightInverse.apply]
[GOAL]
case a.a
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
I : Ideal B
C : Type u
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ↑g
hg' : IsNilpotent (RingHom.ker ↑g)
x : A
⊢ ↑g (↑(liftOfSurjective f g hg hg') x) =
    ↑(Ideal.kerLiftAlg g)
      (↑(Ideal.Quotient.mk (RingHom.ker ↑g))
        (↑(lift (RingHom.ker ↑g) hg'
              (AlgHom.comp
                (↑(AlgEquiv.symm
                    (Ideal.quotientKerAlgEquivOfRightInverse
                      (_ : Function.RightInverse (Classical.choose (_ : Function.HasRightInverse ↑g)) ↑g))))
                f))
          x))
[PROOFSTEP]
exact (Ideal.kerLiftAlg_mk _ _).symm
[GOAL]
R : Type u
inst✝⁵ : CommSemiring R
A B : Type u
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
e : A ≃ₐ[R] B
⊢ FormallySmooth R B
[PROOFSTEP]
constructor
[GOAL]
case comp_surjective
R : Type u
inst✝⁵ : CommSemiring R
A B : Type u
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
e : A ≃ₐ[R] B
⊢ ∀ ⦃B_1 : Type u⦄ [inst : CommRing B_1] [inst_1 : Algebra R B_1] (I : Ideal B_1),
    I ^ 2 = ⊥ → Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
[PROOFSTEP]
intro C _ _ I hI f
[GOAL]
case comp_surjective
R : Type u
inst✝⁷ : CommSemiring R
A B : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : FormallySmooth R A
e : A ≃ₐ[R] B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[R] C ⧸ I
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
[PROOFSTEP]
use(FormallySmooth.lift I ⟨2, hI⟩ (f.comp e : A →ₐ[R] C ⧸ I)).comp e.symm
[GOAL]
case h
R : Type u
inst✝⁷ : CommSemiring R
A B : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : FormallySmooth R A
e : A ≃ₐ[R] B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[R] C ⧸ I
⊢ AlgHom.comp (Ideal.Quotient.mkₐ R I)
      (AlgHom.comp (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp f ↑e)) ↑(AlgEquiv.symm e)) =
    f
[PROOFSTEP]
rw [← AlgHom.comp_assoc, FormallySmooth.comp_lift, AlgHom.comp_assoc, AlgEquiv.comp_symm, AlgHom.comp_id]
[GOAL]
R : Type u
inst✝⁵ : CommSemiring R
A B : Type u
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : FormallyUnramified R A
e : A ≃ₐ[R] B
⊢ FormallyUnramified R B
[PROOFSTEP]
constructor
[GOAL]
case comp_injective
R : Type u
inst✝⁵ : CommSemiring R
A B : Type u
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : FormallyUnramified R A
e : A ≃ₐ[R] B
⊢ ∀ ⦃B_1 : Type u⦄ [inst : CommRing B_1] [inst_1 : Algebra R B_1] (I : Ideal B_1),
    I ^ 2 = ⊥ → Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
[PROOFSTEP]
intro C _ _ I hI f₁ f₂ e'
[GOAL]
case comp_injective
R : Type u
inst✝⁷ : CommSemiring R
A B : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
e : A ≃ₐ[R] B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e' : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂
⊢ f₁ = f₂
[PROOFSTEP]
rw [← f₁.comp_id, ← f₂.comp_id, ← e.comp_symm, ← AlgHom.comp_assoc, ← AlgHom.comp_assoc]
[GOAL]
case comp_injective
R : Type u
inst✝⁷ : CommSemiring R
A B : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
e : A ≃ₐ[R] B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e' : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂
⊢ AlgHom.comp (AlgHom.comp f₁ ↑e) ↑(AlgEquiv.symm e) = AlgHom.comp (AlgHom.comp f₂ ↑e) ↑(AlgEquiv.symm e)
[PROOFSTEP]
congr 1
[GOAL]
case comp_injective.e_φ₁
R : Type u
inst✝⁷ : CommSemiring R
A B : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
e : A ≃ₐ[R] B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e' : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂
⊢ AlgHom.comp f₁ ↑e = AlgHom.comp f₂ ↑e
[PROOFSTEP]
refine' FormallyUnramified.comp_injective I hI _
[GOAL]
case comp_injective.e_φ₁
R : Type u
inst✝⁷ : CommSemiring R
A B : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
e : A ≃ₐ[R] B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e' : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂
⊢ AlgHom.comp (Ideal.Quotient.mkₐ R I) (AlgHom.comp f₁ ↑e) = AlgHom.comp (Ideal.Quotient.mkₐ R I) (AlgHom.comp f₂ ↑e)
[PROOFSTEP]
rw [← AlgHom.comp_assoc, e', AlgHom.comp_assoc]
[GOAL]
R : Type u
inst✝ : CommSemiring R
σ : Type u
⊢ FormallySmooth R (MvPolynomial σ R)
[PROOFSTEP]
constructor
[GOAL]
case comp_surjective
R : Type u
inst✝ : CommSemiring R
σ : Type u
⊢ ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
[PROOFSTEP]
intro C _ _ I _ f
[GOAL]
case comp_surjective
R : Type u
inst✝² : CommSemiring R
σ C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
x✝ : I ^ 2 = ⊥
f : MvPolynomial σ R →ₐ[R] C ⧸ I
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
[PROOFSTEP]
have : ∀ s : σ, ∃ c : C, Ideal.Quotient.mk I c = f (MvPolynomial.X s) := fun s => Ideal.Quotient.mk_surjective _
[GOAL]
case comp_surjective
R : Type u
inst✝² : CommSemiring R
σ C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
x✝ : I ^ 2 = ⊥
f : MvPolynomial σ R →ₐ[R] C ⧸ I
this : ∀ (s : σ), ∃ c, ↑(Ideal.Quotient.mk I) c = ↑f (MvPolynomial.X s)
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
[PROOFSTEP]
choose g hg using this
[GOAL]
case comp_surjective
R : Type u
inst✝² : CommSemiring R
σ C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
x✝ : I ^ 2 = ⊥
f : MvPolynomial σ R →ₐ[R] C ⧸ I
g : σ → C
hg : ∀ (s : σ), ↑(Ideal.Quotient.mk I) (g s) = ↑f (MvPolynomial.X s)
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
[PROOFSTEP]
refine' ⟨MvPolynomial.aeval g, _⟩
[GOAL]
case comp_surjective
R : Type u
inst✝² : CommSemiring R
σ C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
x✝ : I ^ 2 = ⊥
f : MvPolynomial σ R →ₐ[R] C ⧸ I
g : σ → C
hg : ∀ (s : σ), ↑(Ideal.Quotient.mk I) (g s) = ↑f (MvPolynomial.X s)
⊢ AlgHom.comp (Ideal.Quotient.mkₐ R I) (MvPolynomial.aeval g) = f
[PROOFSTEP]
ext s
[GOAL]
case comp_surjective.hf
R : Type u
inst✝² : CommSemiring R
σ C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
x✝ : I ^ 2 = ⊥
f : MvPolynomial σ R →ₐ[R] C ⧸ I
g : σ → C
hg : ∀ (s : σ), ↑(Ideal.Quotient.mk I) (g s) = ↑f (MvPolynomial.X s)
s : σ
⊢ ↑(AlgHom.comp (Ideal.Quotient.mkₐ R I) (MvPolynomial.aeval g)) (MvPolynomial.X s) = ↑f (MvPolynomial.X s)
[PROOFSTEP]
rw [← hg, AlgHom.comp_apply, MvPolynomial.aeval_X]
[GOAL]
case comp_surjective.hf
R : Type u
inst✝² : CommSemiring R
σ C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
x✝ : I ^ 2 = ⊥
f : MvPolynomial σ R →ₐ[R] C ⧸ I
g : σ → C
hg : ∀ (s : σ), ↑(Ideal.Quotient.mk I) (g s) = ↑f (MvPolynomial.X s)
s : σ
⊢ ↑(Ideal.Quotient.mkₐ R I) (g s) = ↑(Ideal.Quotient.mk I) (g s)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝⁸ : CommSemiring R
A : Type u
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
B : Type u
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FormallySmooth R A
inst✝ : FormallySmooth A B
⊢ FormallySmooth R B
[PROOFSTEP]
constructor
[GOAL]
case comp_surjective
R : Type u
inst✝⁸ : CommSemiring R
A : Type u
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
B : Type u
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FormallySmooth R A
inst✝ : FormallySmooth A B
⊢ ∀ ⦃B_1 : Type u⦄ [inst : CommRing B_1] [inst_1 : Algebra R B_1] (I : Ideal B_1),
    I ^ 2 = ⊥ → Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
[PROOFSTEP]
intro C _ _ I hI f
[GOAL]
case comp_surjective
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type u
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
B : Type u
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallySmooth R A
inst✝² : FormallySmooth A B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[R] C ⧸ I
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
[PROOFSTEP]
obtain ⟨f', e⟩ := FormallySmooth.comp_surjective I hI (f.comp (IsScalarTower.toAlgHom R A B))
[GOAL]
case comp_surjective.intro
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type u
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
B : Type u
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallySmooth R A
inst✝² : FormallySmooth A B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[R] C ⧸ I
f' : A →ₐ[R] C
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f' = AlgHom.comp f (IsScalarTower.toAlgHom R A B)
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
[PROOFSTEP]
letI := f'.toRingHom.toAlgebra
[GOAL]
case comp_surjective.intro
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type u
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
B : Type u
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallySmooth R A
inst✝² : FormallySmooth A B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[R] C ⧸ I
f' : A →ₐ[R] C
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f' = AlgHom.comp f (IsScalarTower.toAlgHom R A B)
this : Algebra A C := RingHom.toAlgebra ↑f'
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
[PROOFSTEP]
obtain ⟨f'', e'⟩ := FormallySmooth.comp_surjective I hI { f.toRingHom with commutes' := AlgHom.congr_fun e.symm }
[GOAL]
case comp_surjective.intro.intro
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type u
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
B : Type u
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallySmooth R A
inst✝² : FormallySmooth A B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[R] C ⧸ I
f' : A →ₐ[R] C
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f' = AlgHom.comp f (IsScalarTower.toAlgHom R A B)
this : Algebra A C := RingHom.toAlgebra ↑f'
f'' : B →ₐ[A] C
e' :
  AlgHom.comp (Ideal.Quotient.mkₐ A I) f'' =
    let src := ↑f;
    {
      toRingHom :=
        { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
          map_add' :=
            (_ : ∀ (x y : B), OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
      commutes' :=
        (_ :
          ∀ (x : A), ↑(AlgHom.comp f (IsScalarTower.toAlgHom R A B)) x = ↑(AlgHom.comp (Ideal.Quotient.mkₐ R I) f') x) }
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
[PROOFSTEP]
apply_fun AlgHom.restrictScalars R at e' 
[GOAL]
case comp_surjective.intro.intro
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type u
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
B : Type u
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallySmooth R A
inst✝² : FormallySmooth A B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[R] C ⧸ I
f' : A →ₐ[R] C
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f' = AlgHom.comp f (IsScalarTower.toAlgHom R A B)
this : Algebra A C := RingHom.toAlgebra ↑f'
f'' : B →ₐ[A] C
e' :
  AlgHom.restrictScalars R (AlgHom.comp (Ideal.Quotient.mkₐ A I) f'') =
    AlgHom.restrictScalars R
      (let src := ↑f;
      {
        toRingHom :=
          { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : B), OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
        commutes' :=
          (_ :
            ∀ (x : A),
              ↑(AlgHom.comp f (IsScalarTower.toAlgHom R A B)) x = ↑(AlgHom.comp (Ideal.Quotient.mkₐ R I) f') x) })
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
[PROOFSTEP]
exact ⟨f''.restrictScalars _, e'.trans (AlgHom.ext fun _ => rfl)⟩
[GOAL]
R : Type u
inst✝⁸ : CommSemiring R
A : Type u
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
B : Type u
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FormallyUnramified R A
inst✝ : FormallyUnramified A B
⊢ FormallyUnramified R B
[PROOFSTEP]
constructor
[GOAL]
case comp_injective
R : Type u
inst✝⁸ : CommSemiring R
A : Type u
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
B : Type u
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FormallyUnramified R A
inst✝ : FormallyUnramified A B
⊢ ∀ ⦃B_1 : Type u⦄ [inst : CommRing B_1] [inst_1 : Algebra R B_1] (I : Ideal B_1),
    I ^ 2 = ⊥ → Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
[PROOFSTEP]
intro C _ _ I hI f₁ f₂ e
[GOAL]
case comp_injective
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type u
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
B : Type u
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallyUnramified R A
inst✝² : FormallyUnramified A B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂
⊢ f₁ = f₂
[PROOFSTEP]
have e' :=
  FormallyUnramified.lift_unique I ⟨2, hI⟩ (f₁.comp <| IsScalarTower.toAlgHom R A B)
    (f₂.comp <| IsScalarTower.toAlgHom R A B) (by rw [← AlgHom.comp_assoc, e, AlgHom.comp_assoc])
[GOAL]
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type u
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
B : Type u
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallyUnramified R A
inst✝² : FormallyUnramified A B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂
⊢ AlgHom.comp (Ideal.Quotient.mkₐ R I) (AlgHom.comp f₁ (IsScalarTower.toAlgHom R A B)) =
    AlgHom.comp (Ideal.Quotient.mkₐ R I) (AlgHom.comp f₂ (IsScalarTower.toAlgHom R A B))
[PROOFSTEP]
rw [← AlgHom.comp_assoc, e, AlgHom.comp_assoc]
[GOAL]
case comp_injective
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type u
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
B : Type u
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallyUnramified R A
inst✝² : FormallyUnramified A B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂
e' : AlgHom.comp f₁ (IsScalarTower.toAlgHom R A B) = AlgHom.comp f₂ (IsScalarTower.toAlgHom R A B)
⊢ f₁ = f₂
[PROOFSTEP]
letI := (f₁.comp (IsScalarTower.toAlgHom R A B)).toRingHom.toAlgebra
[GOAL]
case comp_injective
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type u
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
B : Type u
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallyUnramified R A
inst✝² : FormallyUnramified A B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂
e' : AlgHom.comp f₁ (IsScalarTower.toAlgHom R A B) = AlgHom.comp f₂ (IsScalarTower.toAlgHom R A B)
this : Algebra A C := RingHom.toAlgebra ↑(AlgHom.comp f₁ (IsScalarTower.toAlgHom R A B))
⊢ f₁ = f₂
[PROOFSTEP]
let F₁ : B →ₐ[A] C := { f₁ with commutes' := fun r => rfl }
[GOAL]
case comp_injective
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type u
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
B : Type u
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallyUnramified R A
inst✝² : FormallyUnramified A B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂
e' : AlgHom.comp f₁ (IsScalarTower.toAlgHom R A B) = AlgHom.comp f₂ (IsScalarTower.toAlgHom R A B)
this : Algebra A C := RingHom.toAlgebra ↑(AlgHom.comp f₁ (IsScalarTower.toAlgHom R A B))
F₁ : B →ₐ[A] C :=
  { toRingHom := ↑f₁,
    commutes' :=
      (_ : ∀ (r : A), OneHom.toFun (↑↑↑f₁) (↑(algebraMap A B) r) = OneHom.toFun (↑↑↑f₁) (↑(algebraMap A B) r)) }
⊢ f₁ = f₂
[PROOFSTEP]
let F₂ : B →ₐ[A] C := { f₂ with commutes' := AlgHom.congr_fun e'.symm }
[GOAL]
case comp_injective
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type u
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
B : Type u
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallyUnramified R A
inst✝² : FormallyUnramified A B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂
e' : AlgHom.comp f₁ (IsScalarTower.toAlgHom R A B) = AlgHom.comp f₂ (IsScalarTower.toAlgHom R A B)
this : Algebra A C := RingHom.toAlgebra ↑(AlgHom.comp f₁ (IsScalarTower.toAlgHom R A B))
F₁ : B →ₐ[A] C :=
  { toRingHom := ↑f₁,
    commutes' :=
      (_ : ∀ (r : A), OneHom.toFun (↑↑↑f₁) (↑(algebraMap A B) r) = OneHom.toFun (↑↑↑f₁) (↑(algebraMap A B) r)) }
F₂ : B →ₐ[A] C :=
  { toRingHom := ↑f₂,
    commutes' :=
      (_ :
        ∀ (x : A),
          ↑(AlgHom.comp f₂ (IsScalarTower.toAlgHom R A B)) x = ↑(AlgHom.comp f₁ (IsScalarTower.toAlgHom R A B)) x) }
⊢ f₁ = f₂
[PROOFSTEP]
ext1 x
[GOAL]
case comp_injective.H
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type u
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
B : Type u
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallyUnramified R A
inst✝² : FormallyUnramified A B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂
e' : AlgHom.comp f₁ (IsScalarTower.toAlgHom R A B) = AlgHom.comp f₂ (IsScalarTower.toAlgHom R A B)
this : Algebra A C := RingHom.toAlgebra ↑(AlgHom.comp f₁ (IsScalarTower.toAlgHom R A B))
F₁ : B →ₐ[A] C :=
  { toRingHom := ↑f₁,
    commutes' :=
      (_ : ∀ (r : A), OneHom.toFun (↑↑↑f₁) (↑(algebraMap A B) r) = OneHom.toFun (↑↑↑f₁) (↑(algebraMap A B) r)) }
F₂ : B →ₐ[A] C :=
  { toRingHom := ↑f₂,
    commutes' :=
      (_ :
        ∀ (x : A),
          ↑(AlgHom.comp f₂ (IsScalarTower.toAlgHom R A B)) x = ↑(AlgHom.comp f₁ (IsScalarTower.toAlgHom R A B)) x) }
x : B
⊢ ↑f₁ x = ↑f₂ x
[PROOFSTEP]
change F₁ x = F₂ x
[GOAL]
case comp_injective.H
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type u
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
B : Type u
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallyUnramified R A
inst✝² : FormallyUnramified A B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂
e' : AlgHom.comp f₁ (IsScalarTower.toAlgHom R A B) = AlgHom.comp f₂ (IsScalarTower.toAlgHom R A B)
this : Algebra A C := RingHom.toAlgebra ↑(AlgHom.comp f₁ (IsScalarTower.toAlgHom R A B))
F₁ : B →ₐ[A] C :=
  { toRingHom := ↑f₁,
    commutes' :=
      (_ : ∀ (r : A), OneHom.toFun (↑↑↑f₁) (↑(algebraMap A B) r) = OneHom.toFun (↑↑↑f₁) (↑(algebraMap A B) r)) }
F₂ : B →ₐ[A] C :=
  { toRingHom := ↑f₂,
    commutes' :=
      (_ :
        ∀ (x : A),
          ↑(AlgHom.comp f₂ (IsScalarTower.toAlgHom R A B)) x = ↑(AlgHom.comp f₁ (IsScalarTower.toAlgHom R A B)) x) }
x : B
⊢ ↑F₁ x = ↑F₂ x
[PROOFSTEP]
congr
[GOAL]
case comp_injective.H.e_a
R : Type u
inst✝¹⁰ : CommSemiring R
A : Type u
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
B : Type u
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra A B
inst✝⁴ : IsScalarTower R A B
inst✝³ : FormallyUnramified R A
inst✝² : FormallyUnramified A B
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂
e' : AlgHom.comp f₁ (IsScalarTower.toAlgHom R A B) = AlgHom.comp f₂ (IsScalarTower.toAlgHom R A B)
this : Algebra A C := RingHom.toAlgebra ↑(AlgHom.comp f₁ (IsScalarTower.toAlgHom R A B))
F₁ : B →ₐ[A] C :=
  { toRingHom := ↑f₁,
    commutes' :=
      (_ : ∀ (r : A), OneHom.toFun (↑↑↑f₁) (↑(algebraMap A B) r) = OneHom.toFun (↑↑↑f₁) (↑(algebraMap A B) r)) }
F₂ : B →ₐ[A] C :=
  { toRingHom := ↑f₂,
    commutes' :=
      (_ :
        ∀ (x : A),
          ↑(AlgHom.comp f₂ (IsScalarTower.toAlgHom R A B)) x = ↑(AlgHom.comp f₁ (IsScalarTower.toAlgHom R A B)) x) }
x : B
⊢ F₁ = F₂
[PROOFSTEP]
exact FormallyUnramified.ext I ⟨2, hI⟩ (AlgHom.congr_fun e)
[GOAL]
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R A B
inst✝ : FormallyUnramified R B
⊢ FormallyUnramified A B
[PROOFSTEP]
constructor
[GOAL]
case comp_injective
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R A B
inst✝ : FormallyUnramified R B
⊢ ∀ ⦃B_1 : Type u⦄ [inst : CommRing B_1] [inst_1 : Algebra A B_1] (I : Ideal B_1),
    I ^ 2 = ⊥ → Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ A I))
[PROOFSTEP]
intro Q _ _ I e f₁ f₂ e'
[GOAL]
case comp_injective
R : Type u
inst✝⁹ : CommSemiring R
A : Type u
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
B : Type u
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R B
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra A Q
I : Ideal Q
e : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : AlgHom.comp (Ideal.Quotient.mkₐ A I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ A I) f₂
⊢ f₁ = f₂
[PROOFSTEP]
letI := ((algebraMap A Q).comp (algebraMap R A)).toAlgebra
[GOAL]
case comp_injective
R : Type u
inst✝⁹ : CommSemiring R
A : Type u
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
B : Type u
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R B
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra A Q
I : Ideal Q
e : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : AlgHom.comp (Ideal.Quotient.mkₐ A I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ A I) f₂
this : Algebra R Q := RingHom.toAlgebra (RingHom.comp (algebraMap A Q) (algebraMap R A))
⊢ f₁ = f₂
[PROOFSTEP]
letI : IsScalarTower R A Q := IsScalarTower.of_algebraMap_eq' rfl
[GOAL]
case comp_injective
R : Type u
inst✝⁹ : CommSemiring R
A : Type u
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
B : Type u
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R B
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra A Q
I : Ideal Q
e : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : AlgHom.comp (Ideal.Quotient.mkₐ A I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ A I) f₂
this✝ : Algebra R Q := RingHom.toAlgebra (RingHom.comp (algebraMap A Q) (algebraMap R A))
this : IsScalarTower R A Q := IsScalarTower.of_algebraMap_eq' rfl
⊢ f₁ = f₂
[PROOFSTEP]
refine' AlgHom.restrictScalars_injective R _
[GOAL]
case comp_injective
R : Type u
inst✝⁹ : CommSemiring R
A : Type u
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
B : Type u
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R B
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra A Q
I : Ideal Q
e : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : AlgHom.comp (Ideal.Quotient.mkₐ A I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ A I) f₂
this✝ : Algebra R Q := RingHom.toAlgebra (RingHom.comp (algebraMap A Q) (algebraMap R A))
this : IsScalarTower R A Q := IsScalarTower.of_algebraMap_eq' rfl
⊢ AlgHom.restrictScalars R f₁ = AlgHom.restrictScalars R f₂
[PROOFSTEP]
refine' FormallyUnramified.ext I ⟨2, e⟩ _
[GOAL]
case comp_injective
R : Type u
inst✝⁹ : CommSemiring R
A : Type u
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
B : Type u
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R B
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra A Q
I : Ideal Q
e : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : AlgHom.comp (Ideal.Quotient.mkₐ A I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ A I) f₂
this✝ : Algebra R Q := RingHom.toAlgebra (RingHom.comp (algebraMap A Q) (algebraMap R A))
this : IsScalarTower R A Q := IsScalarTower.of_algebraMap_eq' rfl
⊢ ∀ (x : B),
    ↑(Ideal.Quotient.mk I) (↑(AlgHom.restrictScalars R f₁) x) =
      ↑(Ideal.Quotient.mk I) (↑(AlgHom.restrictScalars R f₂) x)
[PROOFSTEP]
intro x
[GOAL]
case comp_injective
R : Type u
inst✝⁹ : CommSemiring R
A : Type u
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
B : Type u
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : FormallyUnramified R B
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra A Q
I : Ideal Q
e : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[A] Q
e' : AlgHom.comp (Ideal.Quotient.mkₐ A I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ A I) f₂
this✝ : Algebra R Q := RingHom.toAlgebra (RingHom.comp (algebraMap A Q) (algebraMap R A))
this : IsScalarTower R A Q := IsScalarTower.of_algebraMap_eq' rfl
x : B
⊢ ↑(Ideal.Quotient.mk I) (↑(AlgHom.restrictScalars R f₁) x) = ↑(Ideal.Quotient.mk I) (↑(AlgHom.restrictScalars R f₂) x)
[PROOFSTEP]
exact AlgHom.congr_fun e' x
[GOAL]
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
P A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing P
inst✝¹ : Algebra R P
I : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝ : FormallySmooth R P
g : A →ₐ[R] P ⧸ RingHom.ker ↑f ^ 2
hg : AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A
⊢ FormallySmooth R A
[PROOFSTEP]
constructor
[GOAL]
case comp_surjective
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
P A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing P
inst✝¹ : Algebra R P
I : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝ : FormallySmooth R P
g : A →ₐ[R] P ⧸ RingHom.ker ↑f ^ 2
hg : AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A
⊢ ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
[PROOFSTEP]
intro C _ _ I hI i
[GOAL]
case comp_surjective
R S : Type u
inst✝⁸ : CommRing R
inst✝⁷ : CommSemiring S
P A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
I✝ : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝² : FormallySmooth R P
g : A →ₐ[R] P ⧸ RingHom.ker ↑f ^ 2
hg : AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
i : A →ₐ[R] C ⧸ I
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ R I) a = i
[PROOFSTEP]
let l : P ⧸ (RingHom.ker f.toRingHom) ^ 2 →ₐ[R] C :=
  by
  refine' Ideal.Quotient.liftₐ _ (FormallySmooth.lift I ⟨2, hI⟩ (i.comp f)) _
  have : RingHom.ker f ≤ I.comap (FormallySmooth.lift I ⟨2, hI⟩ (i.comp f)) :=
    by
    rintro x (hx : f x = 0)
    have : _ = i (f x) := (FormallySmooth.mk_lift I ⟨2, hI⟩ (i.comp f) x : _)
    rwa [hx, map_zero, ← Ideal.Quotient.mk_eq_mk, Submodule.Quotient.mk_eq_zero] at this 
  intro x hx
  have := (Ideal.pow_mono this 2).trans (Ideal.le_comap_pow _ 2) hx
  rwa [hI] at this 
[GOAL]
R S : Type u
inst✝⁸ : CommRing R
inst✝⁷ : CommSemiring S
P A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
I✝ : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝² : FormallySmooth R P
g : A →ₐ[R] P ⧸ RingHom.ker ↑f ^ 2
hg : AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
i : A →ₐ[R] C ⧸ I
⊢ P ⧸ RingHom.ker ↑f ^ 2 →ₐ[R] C
[PROOFSTEP]
refine' Ideal.Quotient.liftₐ _ (FormallySmooth.lift I ⟨2, hI⟩ (i.comp f)) _
[GOAL]
R S : Type u
inst✝⁸ : CommRing R
inst✝⁷ : CommSemiring S
P A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
I✝ : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝² : FormallySmooth R P
g : A →ₐ[R] P ⧸ RingHom.ker ↑f ^ 2
hg : AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
i : A →ₐ[R] C ⧸ I
⊢ ∀ (a : P), a ∈ RingHom.ker ↑f ^ 2 → ↑(lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f)) a = 0
[PROOFSTEP]
have : RingHom.ker f ≤ I.comap (FormallySmooth.lift I ⟨2, hI⟩ (i.comp f)) :=
  by
  rintro x (hx : f x = 0)
  have : _ = i (f x) := (FormallySmooth.mk_lift I ⟨2, hI⟩ (i.comp f) x : _)
  rwa [hx, map_zero, ← Ideal.Quotient.mk_eq_mk, Submodule.Quotient.mk_eq_zero] at this 
[GOAL]
R S : Type u
inst✝⁸ : CommRing R
inst✝⁷ : CommSemiring S
P A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
I✝ : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝² : FormallySmooth R P
g : A →ₐ[R] P ⧸ RingHom.ker ↑f ^ 2
hg : AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
i : A →ₐ[R] C ⧸ I
⊢ RingHom.ker f ≤ Ideal.comap (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f)) I
[PROOFSTEP]
rintro x (hx : f x = 0)
[GOAL]
R S : Type u
inst✝⁸ : CommRing R
inst✝⁷ : CommSemiring S
P A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
I✝ : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝² : FormallySmooth R P
g : A →ₐ[R] P ⧸ RingHom.ker ↑f ^ 2
hg : AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
i : A →ₐ[R] C ⧸ I
x : P
hx : ↑f x = 0
⊢ x ∈ Ideal.comap (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f)) I
[PROOFSTEP]
have : _ = i (f x) := (FormallySmooth.mk_lift I ⟨2, hI⟩ (i.comp f) x : _)
[GOAL]
R S : Type u
inst✝⁸ : CommRing R
inst✝⁷ : CommSemiring S
P A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
I✝ : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝² : FormallySmooth R P
g : A →ₐ[R] P ⧸ RingHom.ker ↑f ^ 2
hg : AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
i : A →ₐ[R] C ⧸ I
x : P
hx : ↑f x = 0
this : ↑(Ideal.Quotient.mk I) (↑(lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f)) x) = ↑i (↑f x)
⊢ x ∈ Ideal.comap (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f)) I
[PROOFSTEP]
rwa [hx, map_zero, ← Ideal.Quotient.mk_eq_mk, Submodule.Quotient.mk_eq_zero] at this 
[GOAL]
R S : Type u
inst✝⁸ : CommRing R
inst✝⁷ : CommSemiring S
P A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
I✝ : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝² : FormallySmooth R P
g : A →ₐ[R] P ⧸ RingHom.ker ↑f ^ 2
hg : AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
i : A →ₐ[R] C ⧸ I
this : RingHom.ker f ≤ Ideal.comap (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f)) I
⊢ ∀ (a : P), a ∈ RingHom.ker ↑f ^ 2 → ↑(lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f)) a = 0
[PROOFSTEP]
intro x hx
[GOAL]
R S : Type u
inst✝⁸ : CommRing R
inst✝⁷ : CommSemiring S
P A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
I✝ : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝² : FormallySmooth R P
g : A →ₐ[R] P ⧸ RingHom.ker ↑f ^ 2
hg : AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
i : A →ₐ[R] C ⧸ I
this : RingHom.ker f ≤ Ideal.comap (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f)) I
x : P
hx : x ∈ RingHom.ker ↑f ^ 2
⊢ ↑(lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f)) x = 0
[PROOFSTEP]
have := (Ideal.pow_mono this 2).trans (Ideal.le_comap_pow _ 2) hx
[GOAL]
R S : Type u
inst✝⁸ : CommRing R
inst✝⁷ : CommSemiring S
P A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
I✝ : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝² : FormallySmooth R P
g : A →ₐ[R] P ⧸ RingHom.ker ↑f ^ 2
hg : AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
i : A →ₐ[R] C ⧸ I
this✝ : RingHom.ker f ≤ Ideal.comap (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f)) I
x : P
hx : x ∈ RingHom.ker ↑f ^ 2
this : x ∈ Ideal.comap (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f)) (I ^ 2)
⊢ ↑(lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f)) x = 0
[PROOFSTEP]
rwa [hI] at this 
[GOAL]
case comp_surjective
R S : Type u
inst✝⁸ : CommRing R
inst✝⁷ : CommSemiring S
P A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
I✝ : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝² : FormallySmooth R P
g : A →ₐ[R] P ⧸ RingHom.ker ↑f ^ 2
hg : AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
i : A →ₐ[R] C ⧸ I
l : P ⧸ RingHom.ker ↑f ^ 2 →ₐ[R] C :=
  Ideal.Quotient.liftₐ (RingHom.ker ↑f ^ 2) (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f))
    (_ : ∀ (x : P), x ∈ RingHom.ker ↑f ^ 2 → x ∈ Ideal.comap (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f)) ⊥)
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ R I) a = i
[PROOFSTEP]
have : i.comp f.kerSquareLift = (Ideal.Quotient.mkₐ R _).comp l :=
  by
  apply AlgHom.coe_ringHom_injective
  apply Ideal.Quotient.ringHom_ext
  ext x
  exact (FormallySmooth.mk_lift I ⟨2, hI⟩ (i.comp f) x).symm
[GOAL]
R S : Type u
inst✝⁸ : CommRing R
inst✝⁷ : CommSemiring S
P A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
I✝ : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝² : FormallySmooth R P
g : A →ₐ[R] P ⧸ RingHom.ker ↑f ^ 2
hg : AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
i : A →ₐ[R] C ⧸ I
l : P ⧸ RingHom.ker ↑f ^ 2 →ₐ[R] C :=
  Ideal.Quotient.liftₐ (RingHom.ker ↑f ^ 2) (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f))
    (_ : ∀ (x : P), x ∈ RingHom.ker ↑f ^ 2 → x ∈ Ideal.comap (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f)) ⊥)
⊢ AlgHom.comp i (AlgHom.kerSquareLift f) = AlgHom.comp (Ideal.Quotient.mkₐ R I) l
[PROOFSTEP]
apply AlgHom.coe_ringHom_injective
[GOAL]
case a
R S : Type u
inst✝⁸ : CommRing R
inst✝⁷ : CommSemiring S
P A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
I✝ : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝² : FormallySmooth R P
g : A →ₐ[R] P ⧸ RingHom.ker ↑f ^ 2
hg : AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
i : A →ₐ[R] C ⧸ I
l : P ⧸ RingHom.ker ↑f ^ 2 →ₐ[R] C :=
  Ideal.Quotient.liftₐ (RingHom.ker ↑f ^ 2) (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f))
    (_ : ∀ (x : P), x ∈ RingHom.ker ↑f ^ 2 → x ∈ Ideal.comap (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f)) ⊥)
⊢ ↑(AlgHom.comp i (AlgHom.kerSquareLift f)) = ↑(AlgHom.comp (Ideal.Quotient.mkₐ R I) l)
[PROOFSTEP]
apply Ideal.Quotient.ringHom_ext
[GOAL]
case a.h
R S : Type u
inst✝⁸ : CommRing R
inst✝⁷ : CommSemiring S
P A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
I✝ : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝² : FormallySmooth R P
g : A →ₐ[R] P ⧸ RingHom.ker ↑f ^ 2
hg : AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
i : A →ₐ[R] C ⧸ I
l : P ⧸ RingHom.ker ↑f ^ 2 →ₐ[R] C :=
  Ideal.Quotient.liftₐ (RingHom.ker ↑f ^ 2) (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f))
    (_ : ∀ (x : P), x ∈ RingHom.ker ↑f ^ 2 → x ∈ Ideal.comap (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f)) ⊥)
⊢ RingHom.comp (↑(AlgHom.comp i (AlgHom.kerSquareLift f))) (Ideal.Quotient.mk (RingHom.ker ↑f ^ 2)) =
    RingHom.comp (↑(AlgHom.comp (Ideal.Quotient.mkₐ R I) l)) (Ideal.Quotient.mk (RingHom.ker ↑f ^ 2))
[PROOFSTEP]
ext x
[GOAL]
case a.h.a
R S : Type u
inst✝⁸ : CommRing R
inst✝⁷ : CommSemiring S
P A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
I✝ : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝² : FormallySmooth R P
g : A →ₐ[R] P ⧸ RingHom.ker ↑f ^ 2
hg : AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
i : A →ₐ[R] C ⧸ I
l : P ⧸ RingHom.ker ↑f ^ 2 →ₐ[R] C :=
  Ideal.Quotient.liftₐ (RingHom.ker ↑f ^ 2) (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f))
    (_ : ∀ (x : P), x ∈ RingHom.ker ↑f ^ 2 → x ∈ Ideal.comap (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f)) ⊥)
x : P
⊢ ↑(RingHom.comp (↑(AlgHom.comp i (AlgHom.kerSquareLift f))) (Ideal.Quotient.mk (RingHom.ker ↑f ^ 2))) x =
    ↑(RingHom.comp (↑(AlgHom.comp (Ideal.Quotient.mkₐ R I) l)) (Ideal.Quotient.mk (RingHom.ker ↑f ^ 2))) x
[PROOFSTEP]
exact (FormallySmooth.mk_lift I ⟨2, hI⟩ (i.comp f) x).symm
[GOAL]
case comp_surjective
R S : Type u
inst✝⁸ : CommRing R
inst✝⁷ : CommSemiring S
P A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
I✝ : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝² : FormallySmooth R P
g : A →ₐ[R] P ⧸ RingHom.ker ↑f ^ 2
hg : AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
i : A →ₐ[R] C ⧸ I
l : P ⧸ RingHom.ker ↑f ^ 2 →ₐ[R] C :=
  Ideal.Quotient.liftₐ (RingHom.ker ↑f ^ 2) (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f))
    (_ : ∀ (x : P), x ∈ RingHom.ker ↑f ^ 2 → x ∈ Ideal.comap (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f)) ⊥)
this : AlgHom.comp i (AlgHom.kerSquareLift f) = AlgHom.comp (Ideal.Quotient.mkₐ R I) l
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ R I) a = i
[PROOFSTEP]
exact ⟨l.comp g, by rw [← AlgHom.comp_assoc, ← this, AlgHom.comp_assoc, hg, AlgHom.comp_id]⟩
[GOAL]
R S : Type u
inst✝⁸ : CommRing R
inst✝⁷ : CommSemiring S
P A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
I✝ : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝² : FormallySmooth R P
g : A →ₐ[R] P ⧸ RingHom.ker ↑f ^ 2
hg : AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
i : A →ₐ[R] C ⧸ I
l : P ⧸ RingHom.ker ↑f ^ 2 →ₐ[R] C :=
  Ideal.Quotient.liftₐ (RingHom.ker ↑f ^ 2) (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f))
    (_ : ∀ (x : P), x ∈ RingHom.ker ↑f ^ 2 → x ∈ Ideal.comap (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp i f)) ⊥)
this : AlgHom.comp i (AlgHom.kerSquareLift f) = AlgHom.comp (Ideal.Quotient.mkₐ R I) l
⊢ AlgHom.comp (Ideal.Quotient.mkₐ R I) (AlgHom.comp l g) = i
[PROOFSTEP]
rw [← AlgHom.comp_assoc, ← this, AlgHom.comp_assoc, hg, AlgHom.comp_id]
[GOAL]
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
P A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing P
inst✝¹ : Algebra R P
I : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝ : FormallySmooth R P
⊢ FormallySmooth R A ↔ ∃ g, AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A
[PROOFSTEP]
constructor
[GOAL]
case mp
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
P A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing P
inst✝¹ : Algebra R P
I : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝ : FormallySmooth R P
⊢ FormallySmooth R A → ∃ g, AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A
[PROOFSTEP]
intro
[GOAL]
case mp
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
P A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing P
inst✝¹ : Algebra R P
I : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝ : FormallySmooth R P
a✝ : FormallySmooth R A
⊢ ∃ g, AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A
[PROOFSTEP]
have surj : Function.Surjective f.kerSquareLift := fun x => ⟨Submodule.Quotient.mk (hf x).choose, (hf x).choose_spec⟩
[GOAL]
case mp
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
P A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing P
inst✝¹ : Algebra R P
I : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝ : FormallySmooth R P
a✝ : FormallySmooth R A
surj : Function.Surjective ↑(AlgHom.kerSquareLift f)
⊢ ∃ g, AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A
[PROOFSTEP]
have sqz : RingHom.ker f.kerSquareLift.toRingHom ^ 2 = 0 := by
  rw [AlgHom.ker_kerSquareLift, Ideal.cotangentIdeal_square, Ideal.zero_eq_bot]
[GOAL]
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
P A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing P
inst✝¹ : Algebra R P
I : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝ : FormallySmooth R P
a✝ : FormallySmooth R A
surj : Function.Surjective ↑(AlgHom.kerSquareLift f)
⊢ RingHom.ker ↑(AlgHom.kerSquareLift f) ^ 2 = 0
[PROOFSTEP]
rw [AlgHom.ker_kerSquareLift, Ideal.cotangentIdeal_square, Ideal.zero_eq_bot]
[GOAL]
case mp
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
P A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing P
inst✝¹ : Algebra R P
I : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝ : FormallySmooth R P
a✝ : FormallySmooth R A
surj : Function.Surjective ↑(AlgHom.kerSquareLift f)
sqz : RingHom.ker ↑(AlgHom.kerSquareLift f) ^ 2 = 0
⊢ ∃ g, AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A
[PROOFSTEP]
refine' ⟨FormallySmooth.lift _ ⟨2, sqz⟩ (Ideal.quotientKerAlgEquivOfSurjective surj).symm.toAlgHom, _⟩
[GOAL]
case mp
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
P A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing P
inst✝¹ : Algebra R P
I : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝ : FormallySmooth R P
a✝ : FormallySmooth R A
surj : Function.Surjective ↑(AlgHom.kerSquareLift f)
sqz : RingHom.ker ↑(AlgHom.kerSquareLift f) ^ 2 = 0
⊢ AlgHom.comp (AlgHom.kerSquareLift f)
      (lift (RingHom.ker ↑(AlgHom.kerSquareLift f)) (_ : ∃ n, RingHom.ker ↑(AlgHom.kerSquareLift f) ^ n = 0)
        ↑(AlgEquiv.symm (Ideal.quotientKerAlgEquivOfSurjective surj))) =
    AlgHom.id R A
[PROOFSTEP]
ext x
[GOAL]
case mp.H
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
P A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing P
inst✝¹ : Algebra R P
I : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝ : FormallySmooth R P
a✝ : FormallySmooth R A
surj : Function.Surjective ↑(AlgHom.kerSquareLift f)
sqz : RingHom.ker ↑(AlgHom.kerSquareLift f) ^ 2 = 0
x : A
⊢ ↑(AlgHom.comp (AlgHom.kerSquareLift f)
          (lift (RingHom.ker ↑(AlgHom.kerSquareLift f)) (_ : ∃ n, RingHom.ker ↑(AlgHom.kerSquareLift f) ^ n = 0)
            ↑(AlgEquiv.symm (Ideal.quotientKerAlgEquivOfSurjective surj))))
      x =
    ↑(AlgHom.id R A) x
[PROOFSTEP]
have :=
  (Ideal.quotientKerAlgEquivOfSurjective surj).toAlgHom.congr_arg
    (FormallySmooth.mk_lift _ ⟨2, sqz⟩ (Ideal.quotientKerAlgEquivOfSurjective surj).symm.toAlgHom x)
      -- Porting note: was
          -- dsimp at this
          -- rw [AlgEquiv.apply_symm_apply] at this
[GOAL]
case mp.H
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
P A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing P
inst✝¹ : Algebra R P
I : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝ : FormallySmooth R P
a✝ : FormallySmooth R A
surj : Function.Surjective ↑(AlgHom.kerSquareLift f)
sqz : RingHom.ker ↑(AlgHom.kerSquareLift f) ^ 2 = 0
x : A
this :
  ↑↑(Ideal.quotientKerAlgEquivOfSurjective surj)
      (↑(Ideal.Quotient.mk (RingHom.ker ↑(AlgHom.kerSquareLift f)))
        (↑(lift (RingHom.ker ↑(AlgHom.kerSquareLift f)) (_ : ∃ n, RingHom.ker ↑(AlgHom.kerSquareLift f) ^ n = 0)
              ↑(AlgEquiv.symm (Ideal.quotientKerAlgEquivOfSurjective surj)))
          x)) =
    ↑↑(Ideal.quotientKerAlgEquivOfSurjective surj) (↑↑(AlgEquiv.symm (Ideal.quotientKerAlgEquivOfSurjective surj)) x)
⊢ ↑(AlgHom.comp (AlgHom.kerSquareLift f)
          (lift (RingHom.ker ↑(AlgHom.kerSquareLift f)) (_ : ∃ n, RingHom.ker ↑(AlgHom.kerSquareLift f) ^ n = 0)
            ↑(AlgEquiv.symm (Ideal.quotientKerAlgEquivOfSurjective surj))))
      x =
    ↑(AlgHom.id R A) x
[PROOFSTEP]
erw [AlgEquiv.apply_symm_apply] at this 
[GOAL]
case mp.H
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
P A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing P
inst✝¹ : Algebra R P
I : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝ : FormallySmooth R P
a✝ : FormallySmooth R A
surj : Function.Surjective ↑(AlgHom.kerSquareLift f)
sqz : RingHom.ker ↑(AlgHom.kerSquareLift f) ^ 2 = 0
x : A
this :
  ↑↑(Ideal.quotientKerAlgEquivOfSurjective surj)
      (↑(Ideal.Quotient.mk (RingHom.ker ↑(AlgHom.kerSquareLift f)))
        (↑(lift (RingHom.ker ↑(AlgHom.kerSquareLift f)) (_ : ∃ n, RingHom.ker ↑(AlgHom.kerSquareLift f) ^ n = 0)
              ↑(AlgEquiv.symm (Ideal.quotientKerAlgEquivOfSurjective surj)))
          x)) =
    x
⊢ ↑(AlgHom.comp (AlgHom.kerSquareLift f)
          (lift (RingHom.ker ↑(AlgHom.kerSquareLift f)) (_ : ∃ n, RingHom.ker ↑(AlgHom.kerSquareLift f) ^ n = 0)
            ↑(AlgEquiv.symm (Ideal.quotientKerAlgEquivOfSurjective surj))))
      x =
    ↑(AlgHom.id R A) x
[PROOFSTEP]
conv_rhs =>
  rw [← this, AlgHom.id_apply]
    -- Porting note: lean3 was not finished here:
        -- obtain ⟨y, e⟩ :=
        --   Ideal.Quotient.mk_surjective
        --     (FormallySmooth.lift _ ⟨2, sqz⟩
        --       (Ideal.quotientKerAlgEquivOfSurjective surj).symm.toAlgHom
        --       x)
        -- dsimp at e ⊢
        -- rw [← e]
        -- rfl
[GOAL]
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
P A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing P
inst✝¹ : Algebra R P
I : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝ : FormallySmooth R P
a✝ : FormallySmooth R A
surj : Function.Surjective ↑(AlgHom.kerSquareLift f)
sqz : RingHom.ker ↑(AlgHom.kerSquareLift f) ^ 2 = 0
x : A
this :
  ↑↑(Ideal.quotientKerAlgEquivOfSurjective surj)
      (↑(Ideal.Quotient.mk (RingHom.ker ↑(AlgHom.kerSquareLift f)))
        (↑(lift (RingHom.ker ↑(AlgHom.kerSquareLift f)) (_ : ∃ n, RingHom.ker ↑(AlgHom.kerSquareLift f) ^ n = 0)
              ↑(AlgEquiv.symm (Ideal.quotientKerAlgEquivOfSurjective surj)))
          x)) =
    x
| ↑(AlgHom.id R A) x
[PROOFSTEP]
rw [← this, AlgHom.id_apply]
    -- Porting note: lean3 was not finished here:
        -- obtain ⟨y, e⟩ :=
        --   Ideal.Quotient.mk_surjective
        --     (FormallySmooth.lift _ ⟨2, sqz⟩
        --       (Ideal.quotientKerAlgEquivOfSurjective surj).symm.toAlgHom
        --       x)
        -- dsimp at e ⊢
        -- rw [← e]
        -- rfl
[GOAL]
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
P A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing P
inst✝¹ : Algebra R P
I : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝ : FormallySmooth R P
a✝ : FormallySmooth R A
surj : Function.Surjective ↑(AlgHom.kerSquareLift f)
sqz : RingHom.ker ↑(AlgHom.kerSquareLift f) ^ 2 = 0
x : A
this :
  ↑↑(Ideal.quotientKerAlgEquivOfSurjective surj)
      (↑(Ideal.Quotient.mk (RingHom.ker ↑(AlgHom.kerSquareLift f)))
        (↑(lift (RingHom.ker ↑(AlgHom.kerSquareLift f)) (_ : ∃ n, RingHom.ker ↑(AlgHom.kerSquareLift f) ^ n = 0)
              ↑(AlgEquiv.symm (Ideal.quotientKerAlgEquivOfSurjective surj)))
          x)) =
    x
| ↑(AlgHom.id R A) x
[PROOFSTEP]
rw [← this, AlgHom.id_apply]
    -- Porting note: lean3 was not finished here:
        -- obtain ⟨y, e⟩ :=
        --   Ideal.Quotient.mk_surjective
        --     (FormallySmooth.lift _ ⟨2, sqz⟩
        --       (Ideal.quotientKerAlgEquivOfSurjective surj).symm.toAlgHom
        --       x)
        -- dsimp at e ⊢
        -- rw [← e]
        -- rfl
[GOAL]
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
P A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing P
inst✝¹ : Algebra R P
I : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝ : FormallySmooth R P
a✝ : FormallySmooth R A
surj : Function.Surjective ↑(AlgHom.kerSquareLift f)
sqz : RingHom.ker ↑(AlgHom.kerSquareLift f) ^ 2 = 0
x : A
this :
  ↑↑(Ideal.quotientKerAlgEquivOfSurjective surj)
      (↑(Ideal.Quotient.mk (RingHom.ker ↑(AlgHom.kerSquareLift f)))
        (↑(lift (RingHom.ker ↑(AlgHom.kerSquareLift f)) (_ : ∃ n, RingHom.ker ↑(AlgHom.kerSquareLift f) ^ n = 0)
              ↑(AlgEquiv.symm (Ideal.quotientKerAlgEquivOfSurjective surj)))
          x)) =
    x
| ↑(AlgHom.id R A) x
[PROOFSTEP]
rw [← this, AlgHom.id_apply]
  -- Porting note: lean3 was not finished here:
      -- obtain ⟨y, e⟩ :=
      --   Ideal.Quotient.mk_surjective
      --     (FormallySmooth.lift _ ⟨2, sqz⟩
      --       (Ideal.quotientKerAlgEquivOfSurjective surj).symm.toAlgHom
      --       x)
      -- dsimp at e ⊢
      -- rw [← e]
      -- rfl
[GOAL]
case mpr
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
P A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing P
inst✝¹ : Algebra R P
I : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝ : FormallySmooth R P
⊢ (∃ g, AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A) → FormallySmooth R A
[PROOFSTEP]
rintro ⟨g, hg⟩
[GOAL]
case mpr.intro
R S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
P A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing P
inst✝¹ : Algebra R P
I : Ideal P
f : P →ₐ[R] A
hf : Function.Surjective ↑f
inst✝ : FormallySmooth R P
g : A →ₐ[R] P ⧸ RingHom.ker ↑f ^ 2
hg : AlgHom.comp (AlgHom.kerSquareLift f) g = AlgHom.id R A
⊢ FormallySmooth R A
[PROOFSTEP]
exact FormallySmooth.of_split f g hg
[GOAL]
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FormallyUnramified R S
⊢ Subsingleton (Ω[S⁄R])
[PROOFSTEP]
rw [← not_nontrivial_iff_subsingleton]
[GOAL]
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FormallyUnramified R S
⊢ ¬Nontrivial (Ω[S⁄R])
[PROOFSTEP]
intro h
[GOAL]
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FormallyUnramified R S
h : Nontrivial (Ω[S⁄R])
⊢ False
[PROOFSTEP]
obtain ⟨f₁, f₂, e⟩ := (KaehlerDifferential.endEquiv R S).injective.nontrivial
[GOAL]
case mk.intro.intro
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FormallyUnramified R S
h : Nontrivial (Ω[S⁄R])
f₁ f₂ : { f // AlgHom.comp (AlgHom.kerSquareLift (TensorProduct.lmul' R)) f = AlgHom.id R S }
e : f₁ ≠ f₂
⊢ False
[PROOFSTEP]
apply e
[GOAL]
case mk.intro.intro
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FormallyUnramified R S
h : Nontrivial (Ω[S⁄R])
f₁ f₂ : { f // AlgHom.comp (AlgHom.kerSquareLift (TensorProduct.lmul' R)) f = AlgHom.id R S }
e : f₁ ≠ f₂
⊢ f₁ = f₂
[PROOFSTEP]
ext1
[GOAL]
case mk.intro.intro.a
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FormallyUnramified R S
h : Nontrivial (Ω[S⁄R])
f₁ f₂ : { f // AlgHom.comp (AlgHom.kerSquareLift (TensorProduct.lmul' R)) f = AlgHom.id R S }
e : f₁ ≠ f₂
⊢ ↑f₁ = ↑f₂
[PROOFSTEP]
apply FormallyUnramified.lift_unique' _ _ _ _ (f₁.2.trans f₂.2.symm)
[GOAL]
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FormallyUnramified R S
h : Nontrivial (Ω[S⁄R])
f₁ f₂ : { f // AlgHom.comp (AlgHom.kerSquareLift (TensorProduct.lmul' R)) f = AlgHom.id R S }
e : f₁ ≠ f₂
⊢ IsNilpotent (RingHom.ker ↑(AlgHom.kerSquareLift (TensorProduct.lmul' R)))
[PROOFSTEP]
rw [← AlgHom.toRingHom_eq_coe, AlgHom.ker_kerSquareLift]
[GOAL]
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FormallyUnramified R S
h : Nontrivial (Ω[S⁄R])
f₁ f₂ : { f // AlgHom.comp (AlgHom.kerSquareLift (TensorProduct.lmul' R)) f = AlgHom.id R S }
e : f₁ ≠ f₂
⊢ IsNilpotent (Ideal.cotangentIdeal (RingHom.ker ↑(TensorProduct.lmul' R)))
[PROOFSTEP]
exact ⟨_, Ideal.cotangentIdeal_square _⟩
[GOAL]
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ FormallyUnramified R S ↔ Subsingleton (Ω[S⁄R])
[PROOFSTEP]
constructor
[GOAL]
case mp
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ FormallyUnramified R S → Subsingleton (Ω[S⁄R])
[PROOFSTEP]
intros
[GOAL]
case mp
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
a✝ : FormallyUnramified R S
⊢ Subsingleton (Ω[S⁄R])
[PROOFSTEP]
infer_instance
[GOAL]
case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Subsingleton (Ω[S⁄R]) → FormallyUnramified R S
[PROOFSTEP]
intro H
[GOAL]
case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : Subsingleton (Ω[S⁄R])
⊢ FormallyUnramified R S
[PROOFSTEP]
constructor
[GOAL]
case mpr.comp_injective
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : Subsingleton (Ω[S⁄R])
⊢ ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
[PROOFSTEP]
intro B _ _ I hI f₁ f₂ e
[GOAL]
case mpr.comp_injective
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
H : Subsingleton (Ω[S⁄R])
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
f₁ f₂ : S →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂
⊢ f₁ = f₂
[PROOFSTEP]
letI := f₁.toRingHom.toAlgebra
[GOAL]
case mpr.comp_injective
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
H : Subsingleton (Ω[S⁄R])
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
f₁ f₂ : S →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂
this : Algebra S B := RingHom.toAlgebra ↑f₁
⊢ f₁ = f₂
[PROOFSTEP]
haveI := IsScalarTower.of_algebraMap_eq' f₁.comp_algebraMap.symm
[GOAL]
case mpr.comp_injective
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
H : Subsingleton (Ω[S⁄R])
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
f₁ f₂ : S →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂
this✝ : Algebra S B := RingHom.toAlgebra ↑f₁
this : IsScalarTower R S B
⊢ f₁ = f₂
[PROOFSTEP]
have :=
  ((KaehlerDifferential.linearMapEquivDerivation R S).toEquiv.trans
      (derivationToSquareZeroEquivLift I hI)).surjective.subsingleton
[GOAL]
case mpr.comp_injective
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
H : Subsingleton (Ω[S⁄R])
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
f₁ f₂ : S →ₐ[R] B
e : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂
this✝¹ : Algebra S B := RingHom.toAlgebra ↑f₁
this✝ : IsScalarTower R S B
this : Subsingleton { f // AlgHom.comp (Ideal.Quotient.mkₐ R I) f = IsScalarTower.toAlgHom R S (B ⧸ I) }
⊢ f₁ = f₂
[PROOFSTEP]
exact Subtype.ext_iff.mp (@Subsingleton.elim _ this ⟨f₁, rfl⟩ ⟨f₂, e.symm⟩)
[GOAL]
R : Type u
inst✝⁵ : CommSemiring R
A : Type u
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : FormallyUnramified R A
⊢ FormallyUnramified B (B ⊗[R] A)
[PROOFSTEP]
constructor
[GOAL]
case comp_injective
R : Type u
inst✝⁵ : CommSemiring R
A : Type u
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : FormallyUnramified R A
⊢ ∀ ⦃B_1 : Type u⦄ [inst : CommRing B_1] [inst_1 : Algebra B B_1] (I : Ideal B_1),
    I ^ 2 = ⊥ → Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ B I))
[PROOFSTEP]
intro C _ _ I hI f₁ f₂ e
[GOAL]
case comp_injective
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B ⊗[R] A →ₐ[B] C
e : AlgHom.comp (Ideal.Quotient.mkₐ B I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ B I) f₂
⊢ f₁ = f₂
[PROOFSTEP]
letI := ((algebraMap B C).comp (algebraMap R B)).toAlgebra
[GOAL]
case comp_injective
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B ⊗[R] A →ₐ[B] C
e : AlgHom.comp (Ideal.Quotient.mkₐ B I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ B I) f₂
this : Algebra R C := RingHom.toAlgebra (RingHom.comp (algebraMap B C) (algebraMap R B))
⊢ f₁ = f₂
[PROOFSTEP]
haveI : IsScalarTower R B C := IsScalarTower.of_algebraMap_eq' rfl
[GOAL]
case comp_injective
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B ⊗[R] A →ₐ[B] C
e : AlgHom.comp (Ideal.Quotient.mkₐ B I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ B I) f₂
this✝ : Algebra R C := RingHom.toAlgebra (RingHom.comp (algebraMap B C) (algebraMap R B))
this : IsScalarTower R B C
⊢ f₁ = f₂
[PROOFSTEP]
ext : 1
[GOAL]
case comp_injective.ha
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B ⊗[R] A →ₐ[B] C
e : AlgHom.comp (Ideal.Quotient.mkₐ B I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ B I) f₂
this✝ : Algebra R C := RingHom.toAlgebra (RingHom.comp (algebraMap B C) (algebraMap R B))
this : IsScalarTower R B C
⊢ AlgHom.comp f₁ TensorProduct.includeLeft = AlgHom.comp f₂ TensorProduct.includeLeft
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
case comp_injective.hb
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B ⊗[R] A →ₐ[B] C
e : AlgHom.comp (Ideal.Quotient.mkₐ B I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ B I) f₂
this✝ : Algebra R C := RingHom.toAlgebra (RingHom.comp (algebraMap B C) (algebraMap R B))
this : IsScalarTower R B C
⊢ AlgHom.comp (AlgHom.restrictScalars R f₁) TensorProduct.includeRight =
    AlgHom.comp (AlgHom.restrictScalars R f₂) TensorProduct.includeRight
[PROOFSTEP]
exact FormallyUnramified.ext I ⟨2, hI⟩ fun x => AlgHom.congr_fun e (1 ⊗ₜ x)
[GOAL]
R : Type u
inst✝⁵ : CommSemiring R
A : Type u
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
⊢ FormallySmooth B (B ⊗[R] A)
[PROOFSTEP]
constructor
[GOAL]
case comp_surjective
R : Type u
inst✝⁵ : CommSemiring R
A : Type u
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
⊢ ∀ ⦃B_1 : Type u⦄ [inst : CommRing B_1] [inst_1 : Algebra B B_1] (I : Ideal B_1),
    I ^ 2 = ⊥ → Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ B I))
[PROOFSTEP]
intro C _ _ I hI f
[GOAL]
case comp_surjective
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R B
inst✝² : FormallySmooth R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ B I) a = f
[PROOFSTEP]
letI := ((algebraMap B C).comp (algebraMap R B)).toAlgebra
[GOAL]
case comp_surjective
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R B
inst✝² : FormallySmooth R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this : Algebra R C := RingHom.toAlgebra (RingHom.comp (algebraMap B C) (algebraMap R B))
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ B I) a = f
[PROOFSTEP]
haveI : IsScalarTower R B C := IsScalarTower.of_algebraMap_eq' rfl
[GOAL]
case comp_surjective
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R B
inst✝² : FormallySmooth R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this✝ : Algebra R C := RingHom.toAlgebra (RingHom.comp (algebraMap B C) (algebraMap R B))
this : IsScalarTower R B C
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ B I) a = f
[PROOFSTEP]
refine' ⟨TensorProduct.productLeftAlgHom (Algebra.ofId B C) _, _⟩
[GOAL]
case comp_surjective.refine'_1
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R B
inst✝² : FormallySmooth R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this✝ : Algebra R C := RingHom.toAlgebra (RingHom.comp (algebraMap B C) (algebraMap R B))
this : IsScalarTower R B C
⊢ A →ₐ[R] C
[PROOFSTEP]
exact FormallySmooth.lift I ⟨2, hI⟩ ((f.restrictScalars R).comp TensorProduct.includeRight)
[GOAL]
case comp_surjective.refine'_2
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R B
inst✝² : FormallySmooth R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this✝ : Algebra R C := RingHom.toAlgebra (RingHom.comp (algebraMap B C) (algebraMap R B))
this : IsScalarTower R B C
⊢ AlgHom.comp (Ideal.Quotient.mkₐ B I)
      (TensorProduct.productLeftAlgHom (ofId B C)
        (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp (AlgHom.restrictScalars R f) TensorProduct.includeRight))) =
    f
[PROOFSTEP]
apply AlgHom.restrictScalars_injective R
[GOAL]
case comp_surjective.refine'_2.a
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R B
inst✝² : FormallySmooth R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this✝ : Algebra R C := RingHom.toAlgebra (RingHom.comp (algebraMap B C) (algebraMap R B))
this : IsScalarTower R B C
⊢ AlgHom.restrictScalars R
      (AlgHom.comp (Ideal.Quotient.mkₐ B I)
        (TensorProduct.productLeftAlgHom (ofId B C)
          (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp (AlgHom.restrictScalars R f) TensorProduct.includeRight)))) =
    AlgHom.restrictScalars R f
[PROOFSTEP]
apply TensorProduct.ext'
[GOAL]
case comp_surjective.refine'_2.a.H
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R B
inst✝² : FormallySmooth R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this✝ : Algebra R C := RingHom.toAlgebra (RingHom.comp (algebraMap B C) (algebraMap R B))
this : IsScalarTower R B C
⊢ ∀ (a : B) (b : A),
    ↑(AlgHom.restrictScalars R
            (AlgHom.comp (Ideal.Quotient.mkₐ B I)
              (TensorProduct.productLeftAlgHom (ofId B C)
                (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp (AlgHom.restrictScalars R f) TensorProduct.includeRight)))))
        (a ⊗ₜ[R] b) =
      ↑(AlgHom.restrictScalars R f) (a ⊗ₜ[R] b)
[PROOFSTEP]
intro b a
[GOAL]
case comp_surjective.refine'_2.a.H
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R B
inst✝² : FormallySmooth R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this✝ : Algebra R C := RingHom.toAlgebra (RingHom.comp (algebraMap B C) (algebraMap R B))
this : IsScalarTower R B C
b : B
a : A
⊢ ↑(AlgHom.restrictScalars R
          (AlgHom.comp (Ideal.Quotient.mkₐ B I)
            (TensorProduct.productLeftAlgHom (ofId B C)
              (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp (AlgHom.restrictScalars R f) TensorProduct.includeRight)))))
      (b ⊗ₜ[R] a) =
    ↑(AlgHom.restrictScalars R f) (b ⊗ₜ[R] a)
[PROOFSTEP]
suffices algebraMap B _ b * f (1 ⊗ₜ[R] a) = f (b ⊗ₜ[R] a) by simpa [Algebra.ofId_apply]
[GOAL]
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R B
inst✝² : FormallySmooth R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this✝¹ : Algebra R C := RingHom.toAlgebra (RingHom.comp (algebraMap B C) (algebraMap R B))
this✝ : IsScalarTower R B C
b : B
a : A
this : ↑(algebraMap B (C ⧸ I)) b * ↑f (1 ⊗ₜ[R] a) = ↑f (b ⊗ₜ[R] a)
⊢ ↑(AlgHom.restrictScalars R
          (AlgHom.comp (Ideal.Quotient.mkₐ B I)
            (TensorProduct.productLeftAlgHom (ofId B C)
              (lift I (_ : ∃ n, I ^ n = 0) (AlgHom.comp (AlgHom.restrictScalars R f) TensorProduct.includeRight)))))
      (b ⊗ₜ[R] a) =
    ↑(AlgHom.restrictScalars R f) (b ⊗ₜ[R] a)
[PROOFSTEP]
simpa [Algebra.ofId_apply]
[GOAL]
case comp_surjective.refine'_2.a.H
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R B
inst✝² : FormallySmooth R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this✝ : Algebra R C := RingHom.toAlgebra (RingHom.comp (algebraMap B C) (algebraMap R B))
this : IsScalarTower R B C
b : B
a : A
⊢ ↑(algebraMap B (C ⧸ I)) b * ↑f (1 ⊗ₜ[R] a) = ↑f (b ⊗ₜ[R] a)
[PROOFSTEP]
rw [← Algebra.smul_def, ← map_smul, TensorProduct.smul_tmul', smul_eq_mul, mul_one]
[GOAL]
R S Rₘ Sₘ : Type u
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₘ
inst✝⁹ : CommRing Sₘ
M : Submonoid R
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : Algebra Rₘ Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
⊢ FormallySmooth R Rₘ
[PROOFSTEP]
constructor
[GOAL]
case comp_surjective
R S Rₘ Sₘ : Type u
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₘ
inst✝⁹ : CommRing Sₘ
M : Submonoid R
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : Algebra Rₘ Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
⊢ ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
[PROOFSTEP]
intro Q _ _ I e f
[GOAL]
case comp_surjective
R S Rₘ Sₘ : Type u
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₘ
inst✝¹¹ : CommRing Sₘ
M : Submonoid R
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Sₘ
inst✝⁸ : Algebra S Sₘ
inst✝⁷ : Algebra R Rₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : IsScalarTower R Rₘ Sₘ
inst✝⁴ : IsScalarTower R S Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
[PROOFSTEP]
have : ∀ x : M, IsUnit (algebraMap R Q x) := by
  intro x
  apply (IsNilpotent.isUnit_quotient_mk_iff ⟨2, e⟩).mp
  convert (IsLocalization.map_units Rₘ x).map f
  simp only [Ideal.Quotient.mk_algebraMap, AlgHom.commutes]
[GOAL]
R S Rₘ Sₘ : Type u
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₘ
inst✝¹¹ : CommRing Sₘ
M : Submonoid R
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Sₘ
inst✝⁸ : Algebra S Sₘ
inst✝⁷ : Algebra R Rₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : IsScalarTower R Rₘ Sₘ
inst✝⁴ : IsScalarTower R S Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
⊢ ∀ (x : { x // x ∈ M }), IsUnit (↑(algebraMap R Q) ↑x)
[PROOFSTEP]
intro x
[GOAL]
R S Rₘ Sₘ : Type u
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₘ
inst✝¹¹ : CommRing Sₘ
M : Submonoid R
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Sₘ
inst✝⁸ : Algebra S Sₘ
inst✝⁷ : Algebra R Rₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : IsScalarTower R Rₘ Sₘ
inst✝⁴ : IsScalarTower R S Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
x : { x // x ∈ M }
⊢ IsUnit (↑(algebraMap R Q) ↑x)
[PROOFSTEP]
apply (IsNilpotent.isUnit_quotient_mk_iff ⟨2, e⟩).mp
[GOAL]
R S Rₘ Sₘ : Type u
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₘ
inst✝¹¹ : CommRing Sₘ
M : Submonoid R
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Sₘ
inst✝⁸ : Algebra S Sₘ
inst✝⁷ : Algebra R Rₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : IsScalarTower R Rₘ Sₘ
inst✝⁴ : IsScalarTower R S Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
x : { x // x ∈ M }
⊢ IsUnit (↑(Ideal.Quotient.mk I) (↑(algebraMap R Q) ↑x))
[PROOFSTEP]
convert (IsLocalization.map_units Rₘ x).map f
[GOAL]
case h.e'_3
R S Rₘ Sₘ : Type u
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₘ
inst✝¹¹ : CommRing Sₘ
M : Submonoid R
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Sₘ
inst✝⁸ : Algebra S Sₘ
inst✝⁷ : Algebra R Rₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : IsScalarTower R Rₘ Sₘ
inst✝⁴ : IsScalarTower R S Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
x : { x // x ∈ M }
⊢ ↑(Ideal.Quotient.mk I) (↑(algebraMap R Q) ↑x) = ↑f (↑(algebraMap R Rₘ) ↑x)
[PROOFSTEP]
simp only [Ideal.Quotient.mk_algebraMap, AlgHom.commutes]
[GOAL]
case comp_surjective
R S Rₘ Sₘ : Type u
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₘ
inst✝¹¹ : CommRing Sₘ
M : Submonoid R
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Sₘ
inst✝⁸ : Algebra S Sₘ
inst✝⁷ : Algebra R Rₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : IsScalarTower R Rₘ Sₘ
inst✝⁴ : IsScalarTower R S Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this : ∀ (x : { x // x ∈ M }), IsUnit (↑(algebraMap R Q) ↑x)
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
[PROOFSTEP]
let this : Rₘ →ₐ[R] Q := { IsLocalization.lift this with commutes' := IsLocalization.lift_eq this }
[GOAL]
case comp_surjective
R S Rₘ Sₘ : Type u
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₘ
inst✝¹¹ : CommRing Sₘ
M : Submonoid R
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Sₘ
inst✝⁸ : Algebra S Sₘ
inst✝⁷ : Algebra R Rₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : IsScalarTower R Rₘ Sₘ
inst✝⁴ : IsScalarTower R S Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this✝ : ∀ (x : { x // x ∈ M }), IsUnit (↑(algebraMap R Q) ↑x)
this : Rₘ →ₐ[R] Q :=
  let src := IsLocalization.lift this✝;
  {
    toRingHom :=
      { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
        map_add' :=
          (_ : ∀ (x y : Rₘ), OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
    commutes' := (_ : ∀ (x : R), ↑(IsLocalization.lift this✝) (↑(algebraMap R Rₘ) x) = ↑(algebraMap R Q) x) }
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
[PROOFSTEP]
use this
[GOAL]
case h
R S Rₘ Sₘ : Type u
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₘ
inst✝¹¹ : CommRing Sₘ
M : Submonoid R
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Sₘ
inst✝⁸ : Algebra S Sₘ
inst✝⁷ : Algebra R Rₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : IsScalarTower R Rₘ Sₘ
inst✝⁴ : IsScalarTower R S Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this✝ : ∀ (x : { x // x ∈ M }), IsUnit (↑(algebraMap R Q) ↑x)
this : Rₘ →ₐ[R] Q :=
  let src := IsLocalization.lift this✝;
  {
    toRingHom :=
      { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
        map_add' :=
          (_ : ∀ (x y : Rₘ), OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
    commutes' := (_ : ∀ (x : R), ↑(IsLocalization.lift this✝) (↑(algebraMap R Rₘ) x) = ↑(algebraMap R Q) x) }
⊢ AlgHom.comp (Ideal.Quotient.mkₐ R I) this = f
[PROOFSTEP]
apply AlgHom.coe_ringHom_injective
[GOAL]
case h.a
R S Rₘ Sₘ : Type u
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₘ
inst✝¹¹ : CommRing Sₘ
M : Submonoid R
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Sₘ
inst✝⁸ : Algebra S Sₘ
inst✝⁷ : Algebra R Rₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : IsScalarTower R Rₘ Sₘ
inst✝⁴ : IsScalarTower R S Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this✝ : ∀ (x : { x // x ∈ M }), IsUnit (↑(algebraMap R Q) ↑x)
this : Rₘ →ₐ[R] Q :=
  let src := IsLocalization.lift this✝;
  {
    toRingHom :=
      { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
        map_add' :=
          (_ : ∀ (x y : Rₘ), OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
    commutes' := (_ : ∀ (x : R), ↑(IsLocalization.lift this✝) (↑(algebraMap R Rₘ) x) = ↑(algebraMap R Q) x) }
⊢ ↑(AlgHom.comp (Ideal.Quotient.mkₐ R I) this) = ↑f
[PROOFSTEP]
refine' IsLocalization.ringHom_ext M _
[GOAL]
case h.a
R S Rₘ Sₘ : Type u
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₘ
inst✝¹¹ : CommRing Sₘ
M : Submonoid R
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Sₘ
inst✝⁸ : Algebra S Sₘ
inst✝⁷ : Algebra R Rₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : IsScalarTower R Rₘ Sₘ
inst✝⁴ : IsScalarTower R S Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this✝ : ∀ (x : { x // x ∈ M }), IsUnit (↑(algebraMap R Q) ↑x)
this : Rₘ →ₐ[R] Q :=
  let src := IsLocalization.lift this✝;
  {
    toRingHom :=
      { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
        map_add' :=
          (_ : ∀ (x y : Rₘ), OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
    commutes' := (_ : ∀ (x : R), ↑(IsLocalization.lift this✝) (↑(algebraMap R Rₘ) x) = ↑(algebraMap R Q) x) }
⊢ RingHom.comp (↑(AlgHom.comp (Ideal.Quotient.mkₐ R I) this)) (algebraMap R Rₘ) = RingHom.comp (↑f) (algebraMap R Rₘ)
[PROOFSTEP]
ext
[GOAL]
case h.a.a
R S Rₘ Sₘ : Type u
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₘ
inst✝¹¹ : CommRing Sₘ
M : Submonoid R
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Sₘ
inst✝⁸ : Algebra S Sₘ
inst✝⁷ : Algebra R Rₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : IsScalarTower R Rₘ Sₘ
inst✝⁴ : IsScalarTower R S Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this✝ : ∀ (x : { x // x ∈ M }), IsUnit (↑(algebraMap R Q) ↑x)
this : Rₘ →ₐ[R] Q :=
  let src := IsLocalization.lift this✝;
  {
    toRingHom :=
      { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
        map_add' :=
          (_ : ∀ (x y : Rₘ), OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
    commutes' := (_ : ∀ (x : R), ↑(IsLocalization.lift this✝) (↑(algebraMap R Rₘ) x) = ↑(algebraMap R Q) x) }
x✝ : R
⊢ ↑(RingHom.comp (↑(AlgHom.comp (Ideal.Quotient.mkₐ R I) this)) (algebraMap R Rₘ)) x✝ =
    ↑(RingHom.comp (↑f) (algebraMap R Rₘ)) x✝
[PROOFSTEP]
simp
[GOAL]
R S Rₘ Sₘ : Type u
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₘ
inst✝⁹ : CommRing Sₘ
M : Submonoid R
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : Algebra Rₘ Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
⊢ FormallyUnramified R Rₘ
[PROOFSTEP]
constructor
[GOAL]
case comp_injective
R S Rₘ Sₘ : Type u
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₘ
inst✝⁹ : CommRing Sₘ
M : Submonoid R
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : Algebra Rₘ Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
⊢ ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (AlgHom.comp (Ideal.Quotient.mkₐ R I))
[PROOFSTEP]
intro Q _ _ I _ f₁ f₂ _
[GOAL]
case comp_injective
R S Rₘ Sₘ : Type u
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₘ
inst✝¹¹ : CommRing Sₘ
M : Submonoid R
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Sₘ
inst✝⁸ : Algebra S Sₘ
inst✝⁷ : Algebra R Rₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : IsScalarTower R Rₘ Sₘ
inst✝⁴ : IsScalarTower R S Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
x✝ : I ^ 2 = ⊥
f₁ f₂ : Rₘ →ₐ[R] Q
a✝ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂
⊢ f₁ = f₂
[PROOFSTEP]
apply AlgHom.coe_ringHom_injective
[GOAL]
case comp_injective.a
R S Rₘ Sₘ : Type u
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₘ
inst✝¹¹ : CommRing Sₘ
M : Submonoid R
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Sₘ
inst✝⁸ : Algebra S Sₘ
inst✝⁷ : Algebra R Rₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : IsScalarTower R Rₘ Sₘ
inst✝⁴ : IsScalarTower R S Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
x✝ : I ^ 2 = ⊥
f₁ f₂ : Rₘ →ₐ[R] Q
a✝ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂
⊢ ↑f₁ = ↑f₂
[PROOFSTEP]
refine' IsLocalization.ringHom_ext M _
[GOAL]
case comp_injective.a
R S Rₘ Sₘ : Type u
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₘ
inst✝¹¹ : CommRing Sₘ
M : Submonoid R
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Sₘ
inst✝⁸ : Algebra S Sₘ
inst✝⁷ : Algebra R Rₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : IsScalarTower R Rₘ Sₘ
inst✝⁴ : IsScalarTower R S Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
x✝ : I ^ 2 = ⊥
f₁ f₂ : Rₘ →ₐ[R] Q
a✝ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂
⊢ RingHom.comp (↑f₁) (algebraMap R Rₘ) = RingHom.comp (↑f₂) (algebraMap R Rₘ)
[PROOFSTEP]
ext
[GOAL]
case comp_injective.a.a
R S Rₘ Sₘ : Type u
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₘ
inst✝¹¹ : CommRing Sₘ
M : Submonoid R
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Sₘ
inst✝⁸ : Algebra S Sₘ
inst✝⁷ : Algebra R Rₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : IsScalarTower R Rₘ Sₘ
inst✝⁴ : IsScalarTower R S Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
x✝¹ : I ^ 2 = ⊥
f₁ f₂ : Rₘ →ₐ[R] Q
a✝ : AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁ = AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂
x✝ : R
⊢ ↑(RingHom.comp (↑f₁) (algebraMap R Rₘ)) x✝ = ↑(RingHom.comp (↑f₂) (algebraMap R Rₘ)) x✝
[PROOFSTEP]
simp
[GOAL]
R S Rₘ Sₘ : Type u
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallySmooth R Sₘ
⊢ FormallySmooth Rₘ Sₘ
[PROOFSTEP]
constructor
[GOAL]
case comp_surjective
R S Rₘ Sₘ : Type u
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallySmooth R Sₘ
⊢ ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra Rₘ B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Surjective (AlgHom.comp (Ideal.Quotient.mkₐ Rₘ I))
[PROOFSTEP]
intro Q _ _ I e f
[GOAL]
case comp_surjective
R S Rₘ Sₘ : Type u
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : CommRing Rₘ
inst✝¹² : CommRing Sₘ
M : Submonoid R
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R Sₘ
inst✝⁹ : Algebra S Sₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : Algebra Rₘ Sₘ
inst✝⁶ : IsScalarTower R Rₘ Sₘ
inst✝⁵ : IsScalarTower R S Sₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝² : FormallySmooth R Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ Rₘ I) a = f
[PROOFSTEP]
letI := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra
[GOAL]
case comp_surjective
R S Rₘ Sₘ : Type u
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : CommRing Rₘ
inst✝¹² : CommRing Sₘ
M : Submonoid R
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R Sₘ
inst✝⁹ : Algebra S Sₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : Algebra Rₘ Sₘ
inst✝⁶ : IsScalarTower R Rₘ Sₘ
inst✝⁵ : IsScalarTower R S Sₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝² : FormallySmooth R Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this : Algebra R Q := RingHom.toAlgebra (RingHom.comp (algebraMap Rₘ Q) (algebraMap R Rₘ))
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ Rₘ I) a = f
[PROOFSTEP]
letI : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
[GOAL]
case comp_surjective
R S Rₘ Sₘ : Type u
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : CommRing Rₘ
inst✝¹² : CommRing Sₘ
M : Submonoid R
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R Sₘ
inst✝⁹ : Algebra S Sₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : Algebra Rₘ Sₘ
inst✝⁶ : IsScalarTower R Rₘ Sₘ
inst✝⁵ : IsScalarTower R S Sₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝² : FormallySmooth R Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := RingHom.toAlgebra (RingHom.comp (algebraMap Rₘ Q) (algebraMap R Rₘ))
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ Rₘ I) a = f
[PROOFSTEP]
let f : Sₘ →ₐ[Rₘ] Q :=
  by
  refine' { FormallySmooth.lift I ⟨2, e⟩ (f.restrictScalars R) with commutes' := _ }
  intro r
  change
    (RingHom.comp (FormallySmooth.lift I ⟨2, e⟩ (f.restrictScalars R) : Sₘ →+* Q) (algebraMap _ _)) r = algebraMap _ _ r
  congr 1
  refine' IsLocalization.ringHom_ext M _
  rw [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq, AlgHom.comp_algebraMap]
[GOAL]
R S Rₘ Sₘ : Type u
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : CommRing Rₘ
inst✝¹² : CommRing Sₘ
M : Submonoid R
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R Sₘ
inst✝⁹ : Algebra S Sₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : Algebra Rₘ Sₘ
inst✝⁶ : IsScalarTower R Rₘ Sₘ
inst✝⁵ : IsScalarTower R S Sₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝² : FormallySmooth R Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := RingHom.toAlgebra (RingHom.comp (algebraMap Rₘ Q) (algebraMap R Rₘ))
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
⊢ Sₘ →ₐ[Rₘ] Q
[PROOFSTEP]
refine' { FormallySmooth.lift I ⟨2, e⟩ (f.restrictScalars R) with commutes' := _ }
[GOAL]
R S Rₘ Sₘ : Type u
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : CommRing Rₘ
inst✝¹² : CommRing Sₘ
M : Submonoid R
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R Sₘ
inst✝⁹ : Algebra S Sₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : Algebra Rₘ Sₘ
inst✝⁶ : IsScalarTower R Rₘ Sₘ
inst✝⁵ : IsScalarTower R S Sₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝² : FormallySmooth R Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := RingHom.toAlgebra (RingHom.comp (algebraMap Rₘ Q) (algebraMap R Rₘ))
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
src✝ : Sₘ →ₐ[R] Q := lift I (_ : ∃ n, I ^ n = 0) (AlgHom.restrictScalars R f)
⊢ ∀ (r : Rₘ), OneHom.toFun (↑↑↑src✝) (↑(algebraMap Rₘ Sₘ) r) = ↑(algebraMap Rₘ Q) r
[PROOFSTEP]
intro r
[GOAL]
R S Rₘ Sₘ : Type u
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : CommRing Rₘ
inst✝¹² : CommRing Sₘ
M : Submonoid R
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R Sₘ
inst✝⁹ : Algebra S Sₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : Algebra Rₘ Sₘ
inst✝⁶ : IsScalarTower R Rₘ Sₘ
inst✝⁵ : IsScalarTower R S Sₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝² : FormallySmooth R Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := RingHom.toAlgebra (RingHom.comp (algebraMap Rₘ Q) (algebraMap R Rₘ))
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
src✝ : Sₘ →ₐ[R] Q := lift I (_ : ∃ n, I ^ n = 0) (AlgHom.restrictScalars R f)
r : Rₘ
⊢ OneHom.toFun (↑↑↑src✝) (↑(algebraMap Rₘ Sₘ) r) = ↑(algebraMap Rₘ Q) r
[PROOFSTEP]
change
  (RingHom.comp (FormallySmooth.lift I ⟨2, e⟩ (f.restrictScalars R) : Sₘ →+* Q) (algebraMap _ _)) r = algebraMap _ _ r
[GOAL]
R S Rₘ Sₘ : Type u
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : CommRing Rₘ
inst✝¹² : CommRing Sₘ
M : Submonoid R
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R Sₘ
inst✝⁹ : Algebra S Sₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : Algebra Rₘ Sₘ
inst✝⁶ : IsScalarTower R Rₘ Sₘ
inst✝⁵ : IsScalarTower R S Sₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝² : FormallySmooth R Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := RingHom.toAlgebra (RingHom.comp (algebraMap Rₘ Q) (algebraMap R Rₘ))
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
src✝ : Sₘ →ₐ[R] Q := lift I (_ : ∃ n, I ^ n = 0) (AlgHom.restrictScalars R f)
r : Rₘ
⊢ ↑(RingHom.comp (↑(lift I (_ : ∃ n, I ^ n = 0) (AlgHom.restrictScalars R f))) (algebraMap Rₘ Sₘ)) r =
    ↑(algebraMap Rₘ Q) r
[PROOFSTEP]
congr 1
[GOAL]
case e_a
R S Rₘ Sₘ : Type u
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : CommRing Rₘ
inst✝¹² : CommRing Sₘ
M : Submonoid R
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R Sₘ
inst✝⁹ : Algebra S Sₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : Algebra Rₘ Sₘ
inst✝⁶ : IsScalarTower R Rₘ Sₘ
inst✝⁵ : IsScalarTower R S Sₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝² : FormallySmooth R Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := RingHom.toAlgebra (RingHom.comp (algebraMap Rₘ Q) (algebraMap R Rₘ))
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
src✝ : Sₘ →ₐ[R] Q := lift I (_ : ∃ n, I ^ n = 0) (AlgHom.restrictScalars R f)
r : Rₘ
⊢ RingHom.comp (↑(lift I (_ : ∃ n, I ^ n = 0) (AlgHom.restrictScalars R f))) (algebraMap Rₘ Sₘ) = algebraMap Rₘ Q
[PROOFSTEP]
refine' IsLocalization.ringHom_ext M _
[GOAL]
case e_a
R S Rₘ Sₘ : Type u
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : CommRing Rₘ
inst✝¹² : CommRing Sₘ
M : Submonoid R
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R Sₘ
inst✝⁹ : Algebra S Sₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : Algebra Rₘ Sₘ
inst✝⁶ : IsScalarTower R Rₘ Sₘ
inst✝⁵ : IsScalarTower R S Sₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝² : FormallySmooth R Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := RingHom.toAlgebra (RingHom.comp (algebraMap Rₘ Q) (algebraMap R Rₘ))
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
src✝ : Sₘ →ₐ[R] Q := lift I (_ : ∃ n, I ^ n = 0) (AlgHom.restrictScalars R f)
r : Rₘ
⊢ RingHom.comp (RingHom.comp (↑(lift I (_ : ∃ n, I ^ n = 0) (AlgHom.restrictScalars R f))) (algebraMap Rₘ Sₘ))
      (algebraMap R Rₘ) =
    RingHom.comp (algebraMap Rₘ Q) (algebraMap R Rₘ)
[PROOFSTEP]
rw [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq, AlgHom.comp_algebraMap]
[GOAL]
case comp_surjective
R S Rₘ Sₘ : Type u
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : CommRing Rₘ
inst✝¹² : CommRing Sₘ
M : Submonoid R
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R Sₘ
inst✝⁹ : Algebra S Sₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : Algebra Rₘ Sₘ
inst✝⁶ : IsScalarTower R Rₘ Sₘ
inst✝⁵ : IsScalarTower R S Sₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝² : FormallySmooth R Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f✝ : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := RingHom.toAlgebra (RingHom.comp (algebraMap Rₘ Q) (algebraMap R Rₘ))
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
f : Sₘ →ₐ[Rₘ] Q :=
  let src := lift I (_ : ∃ n, I ^ n = 0) (AlgHom.restrictScalars R f✝);
  { toRingHom := ↑src,
    commutes' :=
      (_ :
        ∀ (r : Rₘ),
          ↑(RingHom.comp (↑(lift I (_ : ∃ n, I ^ n = 0) (AlgHom.restrictScalars R f✝))) (algebraMap Rₘ Sₘ)) r =
            ↑(algebraMap Rₘ Q) r) }
⊢ ∃ a, AlgHom.comp (Ideal.Quotient.mkₐ Rₘ I) a = f✝
[PROOFSTEP]
use f
[GOAL]
case h
R S Rₘ Sₘ : Type u
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : CommRing Rₘ
inst✝¹² : CommRing Sₘ
M : Submonoid R
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R Sₘ
inst✝⁹ : Algebra S Sₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : Algebra Rₘ Sₘ
inst✝⁶ : IsScalarTower R Rₘ Sₘ
inst✝⁵ : IsScalarTower R S Sₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝² : FormallySmooth R Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f✝ : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := RingHom.toAlgebra (RingHom.comp (algebraMap Rₘ Q) (algebraMap R Rₘ))
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
f : Sₘ →ₐ[Rₘ] Q :=
  let src := lift I (_ : ∃ n, I ^ n = 0) (AlgHom.restrictScalars R f✝);
  { toRingHom := ↑src,
    commutes' :=
      (_ :
        ∀ (r : Rₘ),
          ↑(RingHom.comp (↑(lift I (_ : ∃ n, I ^ n = 0) (AlgHom.restrictScalars R f✝))) (algebraMap Rₘ Sₘ)) r =
            ↑(algebraMap Rₘ Q) r) }
⊢ AlgHom.comp (Ideal.Quotient.mkₐ Rₘ I) f = f✝
[PROOFSTEP]
ext
[GOAL]
case h.H
R S Rₘ Sₘ : Type u
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : CommRing Rₘ
inst✝¹² : CommRing Sₘ
M : Submonoid R
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R Sₘ
inst✝⁹ : Algebra S Sₘ
inst✝⁸ : Algebra R Rₘ
inst✝⁷ : Algebra Rₘ Sₘ
inst✝⁶ : IsScalarTower R Rₘ Sₘ
inst✝⁵ : IsScalarTower R S Sₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝² : FormallySmooth R Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f✝ : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := RingHom.toAlgebra (RingHom.comp (algebraMap Rₘ Q) (algebraMap R Rₘ))
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
f : Sₘ →ₐ[Rₘ] Q :=
  let src := lift I (_ : ∃ n, I ^ n = 0) (AlgHom.restrictScalars R f✝);
  { toRingHom := ↑src,
    commutes' :=
      (_ :
        ∀ (r : Rₘ),
          ↑(RingHom.comp (↑(lift I (_ : ∃ n, I ^ n = 0) (AlgHom.restrictScalars R f✝))) (algebraMap Rₘ Sₘ)) r =
            ↑(algebraMap Rₘ Q) r) }
x✝ : Sₘ
⊢ ↑(AlgHom.comp (Ideal.Quotient.mkₐ Rₘ I) f) x✝ = ↑f✝ x✝
[PROOFSTEP]
simp
[GOAL]
R S Rₘ Sₘ : Type u
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallySmooth R S
⊢ FormallySmooth Rₘ Sₘ
[PROOFSTEP]
haveI : FormallySmooth S Sₘ := FormallySmooth.of_isLocalization (M.map (algebraMap R S))
[GOAL]
R S Rₘ Sₘ : Type u
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallySmooth R S
this : FormallySmooth S Sₘ
⊢ FormallySmooth Rₘ Sₘ
[PROOFSTEP]
haveI : FormallySmooth R Sₘ := FormallySmooth.comp R S Sₘ
[GOAL]
R S Rₘ Sₘ : Type u
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallySmooth R S
this✝ : FormallySmooth S Sₘ
this : FormallySmooth R Sₘ
⊢ FormallySmooth Rₘ Sₘ
[PROOFSTEP]
exact FormallySmooth.localization_base M
[GOAL]
R S Rₘ Sₘ : Type u
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallyUnramified R S
⊢ FormallyUnramified Rₘ Sₘ
[PROOFSTEP]
haveI : FormallyUnramified S Sₘ := FormallyUnramified.of_isLocalization (M.map (algebraMap R S))
[GOAL]
R S Rₘ Sₘ : Type u
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallyUnramified R S
this : FormallyUnramified S Sₘ
⊢ FormallyUnramified Rₘ Sₘ
[PROOFSTEP]
haveI : FormallyUnramified R Sₘ := FormallyUnramified.comp R S Sₘ
[GOAL]
R S Rₘ Sₘ : Type u
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallyUnramified R S
this✝ : FormallyUnramified S Sₘ
this : FormallyUnramified R Sₘ
⊢ FormallyUnramified Rₘ Sₘ
[PROOFSTEP]
exact FormallyUnramified.localization_base M
[GOAL]
R S Rₘ Sₘ : Type u
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallyEtale R S
⊢ FormallyEtale Rₘ Sₘ
[PROOFSTEP]
haveI : FormallyEtale S Sₘ := FormallyEtale.of_isLocalization (M.map (algebraMap R S))
[GOAL]
R S Rₘ Sₘ : Type u
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallyEtale R S
this : FormallyEtale S Sₘ
⊢ FormallyEtale Rₘ Sₘ
[PROOFSTEP]
haveI : FormallyEtale R Sₘ := FormallyEtale.comp R S Sₘ
[GOAL]
R S Rₘ Sₘ : Type u
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallyEtale R S
this✝ : FormallyEtale S Sₘ
this : FormallyEtale R Sₘ
⊢ FormallyEtale Rₘ Sₘ
[PROOFSTEP]
exact FormallyEtale.localization_base M
