range_dualMap_eq_dualAnnihilator_ker_of_subtype_range_surjective

English

Under subtype range surjectivity, the same dual range- annihilator relation holds, expressed via composition with quotient restrictions.

Русский

При суперпозиции диапазона через подтип сохраняется та же связь между образами дуального отображения и двойственным аннигилятором.

LaTeX

$$range f.dualMap = (ker f).dualAnnihilator$$

Lean4

theorem range_dualMap_eq_dualAnnihilator_ker_of_subtype_range_surjective (f : M →ₗ[R] M')
    (hf : Function.Surjective (range f).subtype.dualMap) : LinearMap.range f.dualMap = (ker f).dualAnnihilator :=
  by
  have rr_surj : Function.Surjective f.rangeRestrict := by rw [← range_eq_top, range_rangeRestrict]
  have := range_dualMap_eq_dualAnnihilator_ker_of_surjective f.rangeRestrict rr_surj
  convert this using 1
  · calc
      _ = range ((range f).subtype.comp f.rangeRestrict).dualMap := by simp
      _ = _ := ?_
    rw [← dualMap_comp_dualMap, range_comp_of_range_eq_top]
    rwa [range_eq_top]
  · apply congr_arg
    exact (ker_rangeRestrict f).symm

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