English
Let F be a multivariate polynomial functor with fixed point Cofix F. The map on Cofix F is compatible with the MvQPF quotient, i.e., if two elements aa1 and aa2 are identified by the congruence Mcongr, then applying the map g lifts them to the same quotient.
Русский
Пусть F — мультивекторный полиномиальный функтор с фиксацией Cofix F. Отображение Cofix F совместимо с эквивалентностью Mcongr: если aa1 и aa2 идентифицируются конгруэнцией, то применение отображения g сохраняет эквивалентность под частной дробью.
LaTeX
$$$\\forall \\alpha \\beta, \\forall g:\\alpha\\Rightarrow\\beta, \\forall aa_1, aa_2:\\left(q.P F\\right).M\\alpha,\\; MvQPF.Mcongr\\ aa_1\\ aa_2 \\Rightarrow \\\\quad \\operatorname{Quot.mk} MvQPF.Mcongr\\left( (q.P F).mvfunctorM.map\\; g\\; aa_1\\right) = \\\\quad \\operatorname{Quot.mk} MvQPF.Mcongr\\left( (q.P F).mvfunctorM.map\\; g\\; aa_2\\right).$$
Lean4
/-- the map function for the functor `Cofix F` -/
def map {α β : TypeVec n} (g : α ⟹ β) : Cofix F α → Cofix F β :=
Quot.lift (fun x : q.P.M α => Quot.mk Mcongr (g <$$> x))
(by
rintro aa₁ aa₂ ⟨r, pr, ra₁a₂⟩; apply Quot.sound
let r' b₁ b₂ := ∃ a₁ a₂ : q.P.M α, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
use r'; constructor
· show IsPrecongr r'
rintro b₁ b₂ ⟨a₁, a₂, ra₁a₂, b₁eq, b₂eq⟩
let u : Quot r → Quot r' :=
Quot.lift (fun x : q.P.M α => Quot.mk r' (g <$$> x))
(by
intro a₁ a₂ ra₁a₂
apply Quot.sound
exact ⟨a₁, a₂, ra₁a₂, rfl, rfl⟩)
have hu : (Quot.mk r' ∘ fun x : q.P.M α => g <$$> x) = u ∘ Quot.mk r :=
by
ext x
rfl
rw [b₁eq, b₂eq, M.dest_map, M.dest_map, ← q.P.comp_map, ← q.P.comp_map]
rw [← appendFun_comp, id_comp, hu, ← comp_id g, appendFun_comp]
rw [q.P.comp_map, q.P.comp_map, abs_map, pr ra₁a₂, ← abs_map]
show r' (g <$$> aa₁) (g <$$> aa₂); exact ⟨aa₁, aa₂, ra₁a₂, rfl, rfl⟩)
