range_cotangentToQuotientSquare — Mathlib

English

The range of cotangentToQuotientSquare equals the cotangent ideal restricted to R, i.e., LinearMap.range I.cotangentToQuotientSquare = I.cotangentIdeal.restrictScalars R.

Русский

Образ I.cotangentToQuotientSquare равен I.cotangentIdeal.restrictScalars R.

LaTeX

$$$\\mathrm{range}\\, I.cotangentToQuotientSquare = I.cotangentIdeal.restrictScalars R$$$

Lean4

theorem range_cotangentToQuotientSquare :
    LinearMap.range I.cotangentToQuotientSquare = I.cotangentIdeal.restrictScalars R :=
  by
  trans LinearMap.range (I.cotangentToQuotientSquare.comp I.toCotangent)
  · rw [LinearMap.range_comp, I.toCotangent_range, Submodule.map_top]
  · rw [to_quotient_square_comp_toCotangent, LinearMap.range_comp, I.range_subtype]; ext; rfl

Похожие утверждения