basis — Mathlib

English

modByMonicHom is a linear map sending the basis element to the corresponding polynomial representative modulo f.

Русский

modByMonicHom — линейное отображение, отправляющее базисный элемент в соответствующий представитель полинома по модулю f.

LaTeX

$$$ h.modByMonicHom \colon S \to_R R[X] $$$

Lean4

/-- The basis on `S` generated by powers of `h.root`.

Auxiliary definition for `IsAdjoinRootMonic.powerBasis`. -/
def basis : Basis (Fin (natDegree f)) R S :=
  Basis.ofRepr
    { toFun x := (h.modByMonicHom x).toFinsupp.comapDomain _ Fin.val_injective.injOn
      invFun g := h.map (ofFinsupp (g.mapDomain Fin.val))
      left_inv
        x := by
        nontriviality R using Algebra.subsingleton R S
        simp only
        rw [Finsupp.mapDomain_comapDomain, Polynomial.eta, h.map_modByMonicHom x]
        · exact Fin.val_injective
        intro i hi
        refine Set.mem_range.mpr ⟨⟨i, ?_⟩, rfl⟩
        contrapose! hi
        simp only [Polynomial.toFinsupp_apply, Classical.not_not, Finsupp.mem_support_iff, Ne, modByMonicHom,
          LinearMap.coe_mk, Finset.mem_coe]
        obtain rfl | hf := eq_or_ne f 1
        · simp
        · exact coeff_eq_zero_of_natDegree_lt <| (natDegree_modByMonic_lt _ h.monic hf).trans_le hi
      right_inv
        g := by
        nontriviality R
        ext i
        simp only [h.modByMonicHom_map, Finsupp.comapDomain_apply, Polynomial.toFinsupp_apply]
        rw [(Polynomial.modByMonic_eq_self_iff h.monic).mpr, Polynomial.coeff]
        · rw [Finsupp.mapDomain_apply Fin.val_injective]
        rw [degree_eq_natDegree h.monic.ne_zero, degree_lt_iff_coeff_zero]
        intro m hm
        rw [Polynomial.coeff]
        rw [Finsupp.mapDomain_notin_range]
        rw [Set.mem_range, not_exists]
        rintro i rfl
        exact i.prop.not_ge hm
      map_add' := by simp [Finsupp.comapDomain_add_of_injective Fin.val_injective]
      map_smul' := by simp [Finsupp.comapDomain_smul_of_injective Fin.val_injective] }

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