English
The naive construction yields a presentation whose relation exactly matches the coefficients vector v.
Русский
Невая конструкция даёт презентацию, у которой отношение совпадает с коэффициентами v.
LaTeX
$$$\\mathrm{naive}\\; s\\; hs\\;.\\text{relation} = v$$$
Lean4
/-- Given a presentation `P` and equivalences `ι' ≃ ι` and
`σ' ≃ σ`, this is the induced presentation with variables indexed
by `ι'` and relations indexed by `σ'` -/
@[simps toGenerators]
noncomputable def reindex (P : Presentation R S ι σ) {ι' σ' : Type*} (e : ι' ≃ ι) (f : σ' ≃ σ) : Presentation R S ι' σ'
where
__ := P.toGenerators.reindex e
relation := rename e.symm ∘ P.relation ∘ f
span_range_relation_eq_ker :=
by
rw [Generators.ker_eq_ker_aeval_val, Generators.reindex_val, ← aeval_comp_rename, ← AlgHom.comap_ker, ←
P.ker_eq_ker_aeval_val, ← P.span_range_relation_eq_ker, Set.range_comp, Set.range_comp, Equiv.range_eq_univ,
Set.image_univ, ← Ideal.map_span (rename ⇑e.symm)]
have hf : Function.Bijective (MvPolynomial.rename e.symm) := (renameEquiv R e.symm).bijective
apply Ideal.comap_injective_of_surjective _ hf.2
simp_rw [Ideal.comap_comapₐ, rename_comp_rename, Equiv.self_comp_symm]
simp [Ideal.comap_map_of_bijective _ hf, rename_id]
