[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ AddCommGroup (Cotangent I)
[PROOFSTEP]
delta Cotangent
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ AddCommGroup ({ x // x ∈ I } ⧸ I • ⊤)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ Module (R ⧸ I) (Cotangent I)
[PROOFSTEP]
delta Cotangent
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ Module (R ⧸ I) ({ x // x ∈ I } ⧸ I • ⊤)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ Submodule.map (Submodule.subtype I) (LinearMap.ker (toCotangent I)) = I ^ 2
[PROOFSTEP]
rw [Ideal.toCotangent, Submodule.ker_mkQ, pow_two, Submodule.map_smul'' I ⊤ (Submodule.subtype I),
  Algebra.id.smul_eq_mul, Submodule.map_subtype_top]
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : { x // x ∈ I }
⊢ x ∈ LinearMap.ker (toCotangent I) ↔ ↑x ∈ I ^ 2
[PROOFSTEP]
rw [← I.map_toCotangent_ker]
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : { x // x ∈ I }
⊢ x ∈ LinearMap.ker (toCotangent I) ↔ ↑x ∈ Submodule.map (Submodule.subtype I) (LinearMap.ker (toCotangent I))
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x y : { x // x ∈ I }
⊢ ↑(toCotangent I) x = ↑(toCotangent I) y ↔ ↑x - ↑y ∈ I ^ 2
[PROOFSTEP]
rw [← sub_eq_zero]
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x y : { x // x ∈ I }
⊢ ↑(toCotangent I) x - ↑(toCotangent I) y = 0 ↔ ↑x - ↑y ∈ I ^ 2
[PROOFSTEP]
exact I.mem_toCotangent_ker
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ Subsingleton (Cotangent I) ↔ IsIdempotentElem I
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ Subsingleton (Cotangent I) → IsIdempotentElem I
[PROOFSTEP]
intro H
[GOAL]
case mp
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
H : Subsingleton (Cotangent I)
⊢ IsIdempotentElem I
[PROOFSTEP]
refine' (pow_two I).symm.trans (le_antisymm (Ideal.pow_le_self two_ne_zero) _)
[GOAL]
case mp
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
H : Subsingleton (Cotangent I)
⊢ I ≤ I ^ 2
[PROOFSTEP]
exact fun x hx => (I.toCotangent_eq_zero ⟨x, hx⟩).mp (Subsingleton.elim _ _)
[GOAL]
case mpr
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ IsIdempotentElem I → Subsingleton (Cotangent I)
[PROOFSTEP]
exact fun e =>
  ⟨fun x y =>
    Quotient.inductionOn₂' x y fun x y => I.toCotangent_eq.mpr <| ((pow_two I).trans e).symm ▸ I.sub_mem x.prop y.prop⟩
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ I • ⊤ ≤ Submodule.comap (Submodule.subtype I) (I ^ 2)
[PROOFSTEP]
rw [← Submodule.map_le_iff_le_comap, Submodule.map_smul'', Submodule.map_top, Submodule.range_subtype, smul_eq_mul,
  pow_two]
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I✝ I : Ideal R
⊢ cotangentIdeal I ^ 2 = ⊥
[PROOFSTEP]
rw [eq_bot_iff, pow_two I.cotangentIdeal, ← smul_eq_mul]
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I✝ I : Ideal R
⊢ cotangentIdeal I • cotangentIdeal I ≤ ⊥
[PROOFSTEP]
intro x hx
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I✝ I : Ideal R
x : R ⧸ I ^ 2
hx : x ∈ cotangentIdeal I • cotangentIdeal I
⊢ x ∈ ⊥
[PROOFSTEP]
refine Submodule.smul_induction_on hx ?_ ?_
[GOAL]
case refine_1
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I✝ I : Ideal R
x : R ⧸ I ^ 2
hx : x ∈ cotangentIdeal I • cotangentIdeal I
⊢ ∀ (r : R ⧸ I ^ 2), r ∈ cotangentIdeal I → ∀ (n : R ⧸ I ^ 2), n ∈ cotangentIdeal I → r • n ∈ ⊥
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩
[GOAL]
case refine_1.intro.intro.intro.intro
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I✝ I : Ideal R
x✝ : R ⧸ I ^ 2
hx✝ : x✝ ∈ cotangentIdeal I • cotangentIdeal I
x : R
hx : x ∈ ↑I
y : R
hy : y ∈ ↑I
⊢ ↑(RingHom.toSemilinearMap (Quotient.mk (I ^ 2))) x • ↑(RingHom.toSemilinearMap (Quotient.mk (I ^ 2))) y ∈ ⊥
[PROOFSTEP]
apply (Submodule.Quotient.eq _).mpr _
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I✝ I : Ideal R
x✝ : R ⧸ I ^ 2
hx✝ : x✝ ∈ cotangentIdeal I • cotangentIdeal I
x : R
hx : x ∈ ↑I
y : R
hy : y ∈ ↑I
⊢ (fun x x_1 => x * x_1) x y - 0 ∈ I ^ 2
[PROOFSTEP]
rw [sub_zero, pow_two]
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I✝ I : Ideal R
x✝ : R ⧸ I ^ 2
hx✝ : x✝ ∈ cotangentIdeal I • cotangentIdeal I
x : R
hx : x ∈ ↑I
y : R
hy : y ∈ ↑I
⊢ (fun x x_1 => x * x_1) x y ∈ I * I
[PROOFSTEP]
exact Ideal.mul_mem_mul hx hy
[GOAL]
case refine_2
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I✝ I : Ideal R
x : R ⧸ I ^ 2
hx : x ∈ cotangentIdeal I • cotangentIdeal I
⊢ ∀ (x y : R ⧸ I ^ 2), x ∈ ⊥ → y ∈ ⊥ → x + y ∈ ⊥
[PROOFSTEP]
intro x y hx hy
[GOAL]
case refine_2
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I✝ I : Ideal R
x✝ : R ⧸ I ^ 2
hx✝ : x✝ ∈ cotangentIdeal I • cotangentIdeal I
x y : R ⧸ I ^ 2
hx : x ∈ ⊥
hy : y ∈ ⊥
⊢ x + y ∈ ⊥
[PROOFSTEP]
exact add_mem hx hy
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ LinearMap.range (cotangentToQuotientSquare I) = Submodule.restrictScalars R (cotangentIdeal I)
[PROOFSTEP]
trans LinearMap.range (I.cotangentToQuotientSquare.comp I.toCotangent)
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ LinearMap.range (cotangentToQuotientSquare I) =
    LinearMap.range (LinearMap.comp (cotangentToQuotientSquare I) (toCotangent I))
[PROOFSTEP]
rw [LinearMap.range_comp, I.toCotangent_range, Submodule.map_top]
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ LinearMap.range (LinearMap.comp (cotangentToQuotientSquare I) (toCotangent I)) =
    Submodule.restrictScalars R (cotangentIdeal I)
[PROOFSTEP]
rw [to_quotient_square_comp_toCotangent, LinearMap.range_comp, I.range_subtype]
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ Submodule.map (Submodule.mkQ (I ^ 2)) I = Submodule.restrictScalars R (cotangentIdeal I)
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x✝ : R ⧸ I ^ 2
⊢ x✝ ∈ Submodule.map (Submodule.mkQ (I ^ 2)) I ↔ x✝ ∈ Submodule.restrictScalars R (cotangentIdeal I)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ Cotangent I ≃ₗ[R] { x // x ∈ cotangentIdeal I }
[PROOFSTEP]
refine
  {
    LinearMap.codRestrict (I.cotangentIdeal.restrictScalars R) I.cotangentToQuotientSquare fun x => by
      {rw [← to_quotient_square_range]; exact LinearMap.mem_range_self _ _
    },
    Equiv.ofBijective _ ⟨?_, ?_⟩ with }
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : Cotangent I
⊢ ↑(cotangentToQuotientSquare I) x ∈ Submodule.restrictScalars R (cotangentIdeal I)
[PROOFSTEP]
{rw [← to_quotient_square_range]; exact LinearMap.mem_range_self _ _
}
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : Cotangent I
⊢ ↑(cotangentToQuotientSquare I) x ∈ Submodule.restrictScalars R (cotangentIdeal I)
[PROOFSTEP]
rw [← to_quotient_square_range]
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : Cotangent I
⊢ ↑(cotangentToQuotientSquare I) x ∈ LinearMap.range (cotangentToQuotientSquare I)
[PROOFSTEP]
exact LinearMap.mem_range_self _ _
[GOAL]
case refine_1
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
src✝ : Cotangent I →ₗ[R] { x // x ∈ Submodule.restrictScalars R (cotangentIdeal I) } :=
  LinearMap.codRestrict (Submodule.restrictScalars R (cotangentIdeal I)) (cotangentToQuotientSquare I)
    (_ : ∀ (x : Cotangent I), ↑(cotangentToQuotientSquare I) x ∈ Submodule.restrictScalars R (cotangentIdeal I))
⊢ Function.Injective fun c =>
    { val := ↑(cotangentToQuotientSquare I) c,
      property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) }
[PROOFSTEP]
rintro x y e
[GOAL]
case refine_1
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
src✝ : Cotangent I →ₗ[R] { x // x ∈ Submodule.restrictScalars R (cotangentIdeal I) } :=
  LinearMap.codRestrict (Submodule.restrictScalars R (cotangentIdeal I)) (cotangentToQuotientSquare I)
    (_ : ∀ (x : Cotangent I), ↑(cotangentToQuotientSquare I) x ∈ Submodule.restrictScalars R (cotangentIdeal I))
x y : Cotangent I
e :
  (fun c =>
        { val := ↑(cotangentToQuotientSquare I) c,
          property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) })
      x =
    (fun c =>
        { val := ↑(cotangentToQuotientSquare I) c,
          property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) })
      y
⊢ x = y
[PROOFSTEP]
replace e := congr_arg Subtype.val e
[GOAL]
case refine_1
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
src✝ : Cotangent I →ₗ[R] { x // x ∈ Submodule.restrictScalars R (cotangentIdeal I) } :=
  LinearMap.codRestrict (Submodule.restrictScalars R (cotangentIdeal I)) (cotangentToQuotientSquare I)
    (_ : ∀ (x : Cotangent I), ↑(cotangentToQuotientSquare I) x ∈ Submodule.restrictScalars R (cotangentIdeal I))
x y : Cotangent I
e :
  ↑((fun c =>
          { val := ↑(cotangentToQuotientSquare I) c,
            property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) })
        x) =
    ↑((fun c =>
          { val := ↑(cotangentToQuotientSquare I) c,
            property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) })
        y)
⊢ x = y
[PROOFSTEP]
obtain ⟨x, rfl⟩ := I.toCotangent_surjective x
[GOAL]
case refine_1.intro
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
src✝ : Cotangent I →ₗ[R] { x // x ∈ Submodule.restrictScalars R (cotangentIdeal I) } :=
  LinearMap.codRestrict (Submodule.restrictScalars R (cotangentIdeal I)) (cotangentToQuotientSquare I)
    (_ : ∀ (x : Cotangent I), ↑(cotangentToQuotientSquare I) x ∈ Submodule.restrictScalars R (cotangentIdeal I))
y : Cotangent I
x : { x // x ∈ I }
e :
  ↑((fun c =>
          { val := ↑(cotangentToQuotientSquare I) c,
            property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) })
        (↑(toCotangent I) x)) =
    ↑((fun c =>
          { val := ↑(cotangentToQuotientSquare I) c,
            property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) })
        y)
⊢ ↑(toCotangent I) x = y
[PROOFSTEP]
obtain ⟨y, rfl⟩ := I.toCotangent_surjective y
[GOAL]
case refine_1.intro.intro
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
src✝ : Cotangent I →ₗ[R] { x // x ∈ Submodule.restrictScalars R (cotangentIdeal I) } :=
  LinearMap.codRestrict (Submodule.restrictScalars R (cotangentIdeal I)) (cotangentToQuotientSquare I)
    (_ : ∀ (x : Cotangent I), ↑(cotangentToQuotientSquare I) x ∈ Submodule.restrictScalars R (cotangentIdeal I))
x y : { x // x ∈ I }
e :
  ↑((fun c =>
          { val := ↑(cotangentToQuotientSquare I) c,
            property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) })
        (↑(toCotangent I) x)) =
    ↑((fun c =>
          { val := ↑(cotangentToQuotientSquare I) c,
            property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) })
        (↑(toCotangent I) y))
⊢ ↑(toCotangent I) x = ↑(toCotangent I) y
[PROOFSTEP]
rw [I.toCotangent_eq]
[GOAL]
case refine_1.intro.intro
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
src✝ : Cotangent I →ₗ[R] { x // x ∈ Submodule.restrictScalars R (cotangentIdeal I) } :=
  LinearMap.codRestrict (Submodule.restrictScalars R (cotangentIdeal I)) (cotangentToQuotientSquare I)
    (_ : ∀ (x : Cotangent I), ↑(cotangentToQuotientSquare I) x ∈ Submodule.restrictScalars R (cotangentIdeal I))
x y : { x // x ∈ I }
e :
  ↑((fun c =>
          { val := ↑(cotangentToQuotientSquare I) c,
            property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) })
        (↑(toCotangent I) x)) =
    ↑((fun c =>
          { val := ↑(cotangentToQuotientSquare I) c,
            property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) })
        (↑(toCotangent I) y))
⊢ ↑x - ↑y ∈ I ^ 2
[PROOFSTEP]
dsimp only [toCotangent_to_quotient_square, Submodule.mkQ_apply] at e 
[GOAL]
case refine_1.intro.intro
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
src✝ : Cotangent I →ₗ[R] { x // x ∈ Submodule.restrictScalars R (cotangentIdeal I) } :=
  LinearMap.codRestrict (Submodule.restrictScalars R (cotangentIdeal I)) (cotangentToQuotientSquare I)
    (_ : ∀ (x : Cotangent I), ↑(cotangentToQuotientSquare I) x ∈ Submodule.restrictScalars R (cotangentIdeal I))
x y : { x // x ∈ I }
e : Submodule.Quotient.mk ↑x = Submodule.Quotient.mk ↑y
⊢ ↑x - ↑y ∈ I ^ 2
[PROOFSTEP]
rwa [Submodule.Quotient.eq] at e 
[GOAL]
case refine_2
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
src✝ : Cotangent I →ₗ[R] { x // x ∈ Submodule.restrictScalars R (cotangentIdeal I) } :=
  LinearMap.codRestrict (Submodule.restrictScalars R (cotangentIdeal I)) (cotangentToQuotientSquare I)
    (_ : ∀ (x : Cotangent I), ↑(cotangentToQuotientSquare I) x ∈ Submodule.restrictScalars R (cotangentIdeal I))
⊢ Function.Surjective fun c =>
    { val := ↑(cotangentToQuotientSquare I) c,
      property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) }
[PROOFSTEP]
rintro ⟨_, x, hx, rfl⟩
[GOAL]
case refine_2.mk.intro.intro
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
src✝ : Cotangent I →ₗ[R] { x // x ∈ Submodule.restrictScalars R (cotangentIdeal I) } :=
  LinearMap.codRestrict (Submodule.restrictScalars R (cotangentIdeal I)) (cotangentToQuotientSquare I)
    (_ : ∀ (x : Cotangent I), ↑(cotangentToQuotientSquare I) x ∈ Submodule.restrictScalars R (cotangentIdeal I))
x : R
hx : x ∈ ↑I
⊢ ∃ a,
    (fun c =>
          { val := ↑(cotangentToQuotientSquare I) c,
            property := (_ : ↑(cotangentToQuotientSquare I) c ∈ Submodule.restrictScalars R (cotangentIdeal I)) })
        a =
      { val := ↑(RingHom.toSemilinearMap (Quotient.mk (I ^ 2))) x,
        property :=
          (_ :
            ∃ a,
              a ∈ ↑I ∧
                ↑(RingHom.toSemilinearMap (Quotient.mk (I ^ 2))) a =
                  ↑(RingHom.toSemilinearMap (Quotient.mk (I ^ 2))) x) }
[PROOFSTEP]
exact ⟨I.toCotangent ⟨x, hx⟩, Subtype.ext rfl⟩
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : R
hx : x ∈ I
⊢ ↑(LinearEquiv.symm (cotangentEquivIdeal I))
      { val := ↑(Submodule.mkQ (I ^ 2)) x,
        property := (_ : ↑(Submodule.mkQ (I ^ 2)) x ∈ Submodule.map (Submodule.mkQ (I ^ 2)) I) } =
    ↑(toCotangent I) { val := x, property := hx }
[PROOFSTEP]
apply I.cotangentEquivIdeal.injective
[GOAL]
case a
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : R
hx : x ∈ I
⊢ ↑(cotangentEquivIdeal I)
      (↑(LinearEquiv.symm (cotangentEquivIdeal I))
        { val := ↑(Submodule.mkQ (I ^ 2)) x,
          property := (_ : ↑(Submodule.mkQ (I ^ 2)) x ∈ Submodule.map (Submodule.mkQ (I ^ 2)) I) }) =
    ↑(cotangentEquivIdeal I) (↑(toCotangent I) { val := x, property := hx })
[PROOFSTEP]
rw [I.cotangentEquivIdeal.apply_symm_apply]
[GOAL]
case a
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : R
hx : x ∈ I
⊢ { val := ↑(Submodule.mkQ (I ^ 2)) x,
      property := (_ : ↑(Submodule.mkQ (I ^ 2)) x ∈ Submodule.map (Submodule.mkQ (I ^ 2)) I) } =
    ↑(cotangentEquivIdeal I) (↑(toCotangent I) { val := x, property := hx })
[PROOFSTEP]
ext
[GOAL]
case a.a
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : R
hx : x ∈ I
⊢ ↑{ val := ↑(Submodule.mkQ (I ^ 2)) x,
        property := (_ : ↑(Submodule.mkQ (I ^ 2)) x ∈ Submodule.map (Submodule.mkQ (I ^ 2)) I) } =
    ↑(↑(cotangentEquivIdeal I) (↑(toCotangent I) { val := x, property := hx }))
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ A ⧸ RingHom.ker ↑f ^ 2 →ₐ[R] B
[PROOFSTEP]
refine { Ideal.Quotient.lift (RingHom.ker f.toRingHom ^ 2) f.toRingHom ?_ with commutes' := ?_ }
[GOAL]
case refine_1
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ ∀ (a : A), a ∈ RingHom.ker ↑f ^ 2 → ↑↑f a = 0
[PROOFSTEP]
intro a ha
[GOAL]
case refine_1
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
a : A
ha : a ∈ RingHom.ker ↑f ^ 2
⊢ ↑↑f a = 0
[PROOFSTEP]
exact Ideal.pow_le_self two_ne_zero ha
[GOAL]
case refine_2
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
src✝ : A ⧸ RingHom.ker ↑f ^ 2 →+* B :=
  Quotient.lift (RingHom.ker ↑f ^ 2) ↑f (_ : ∀ (a : A), a ∈ RingHom.ker ↑f ^ 2 → a ∈ RingHom.ker ↑f)
⊢ ∀ (r : R),
    OneHom.toFun
        (↑↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
              map_add' :=
                (_ :
                  ∀ (x y : A ⧸ RingHom.ker ↑f ^ 2),
                    OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) })
        (↑(algebraMap R (A ⧸ RingHom.ker ↑f ^ 2)) r) =
      ↑(algebraMap R B) r
[PROOFSTEP]
intro r
[GOAL]
case refine_2
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
src✝ : A ⧸ RingHom.ker ↑f ^ 2 →+* B :=
  Quotient.lift (RingHom.ker ↑f ^ 2) ↑f (_ : ∀ (a : A), a ∈ RingHom.ker ↑f ^ 2 → a ∈ RingHom.ker ↑f)
r : R
⊢ OneHom.toFun
      (↑↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ :
                ∀ (x y : A ⧸ RingHom.ker ↑f ^ 2),
                  OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) })
      (↑(algebraMap R (A ⧸ RingHom.ker ↑f ^ 2)) r) =
    ↑(algebraMap R B) r
[PROOFSTEP]
rw [IsScalarTower.algebraMap_apply R A, RingHom.toFun_eq_coe, Ideal.Quotient.algebraMap_eq, Ideal.Quotient.lift_mk]
[GOAL]
case refine_2
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
src✝ : A ⧸ RingHom.ker ↑f ^ 2 →+* B :=
  Quotient.lift (RingHom.ker ↑f ^ 2) ↑f (_ : ∀ (a : A), a ∈ RingHom.ker ↑f ^ 2 → a ∈ RingHom.ker ↑f)
r : R
⊢ ↑↑f (↑(algebraMap R A) r) = ↑(algebraMap R B) r
[PROOFSTEP]
exact f.map_algebraMap r
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ RingHom.ker ↑(AlgHom.kerSquareLift f) = cotangentIdeal (RingHom.ker ↑f)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ RingHom.ker ↑(AlgHom.kerSquareLift f) ≤ cotangentIdeal (RingHom.ker ↑f)
[PROOFSTEP]
intro x hx
[GOAL]
case a
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
x : A ⧸ RingHom.ker ↑f ^ 2
hx : x ∈ RingHom.ker ↑(AlgHom.kerSquareLift f)
⊢ x ∈ cotangentIdeal (RingHom.ker ↑f)
[PROOFSTEP]
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
[GOAL]
case a.intro
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
x : A
hx : ↑(Quotient.mk (RingHom.ker ↑f ^ 2)) x ∈ RingHom.ker ↑(AlgHom.kerSquareLift f)
⊢ ↑(Quotient.mk (RingHom.ker ↑f ^ 2)) x ∈ cotangentIdeal (RingHom.ker ↑f)
[PROOFSTEP]
exact ⟨x, hx, rfl⟩
[GOAL]
case a
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ cotangentIdeal (RingHom.ker ↑f) ≤ RingHom.ker ↑(AlgHom.kerSquareLift f)
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩
[GOAL]
case a.intro.intro
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
x : A
hx : x ∈ ↑(RingHom.ker ↑f)
⊢ ↑(RingHom.toSemilinearMap (Quotient.mk (RingHom.ker ↑f ^ 2))) x ∈ RingHom.ker ↑(AlgHom.kerSquareLift f)
[PROOFSTEP]
exact hx
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ (R ⧸ I ^ 2) ⧸ cotangentIdeal I ≃+* R ⧸ I
[PROOFSTEP]
refine (Ideal.quotEquivOfEq (Ideal.map_eq_submodule_map _ _).symm).trans ?_
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ (R ⧸ I ^ 2) ⧸ map (Quotient.mk (I ^ 2)) I ≃+* R ⧸ I
[PROOFSTEP]
refine (DoubleQuot.quotQuotEquivQuotSup _ _).trans ?_
[GOAL]
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ R ⧸ I ^ 2 ⊔ I ≃+* R ⧸ I
[PROOFSTEP]
exact Ideal.quotEquivOfEq (sup_eq_right.mpr <| Ideal.pow_le_self two_ne_zero)
