English
Applying the calculus after precomposing with f' and then g equals applying the calculus to the composition with a predecessor computed from f, i.e., a functoriality with respect to composition.
Русский
Применение калькулятора после предварительной композиции f' и затем g эквивалентно применению калькулятора к композиции с предшественником, вычисленным по f.
LaTeX
$$$\mathrm{cfc}_nHa(g\circ f') = \mathrm{cfc}_n(Ha f)(g)$$$
Lean4
theorem cfcₙHom_comp [UniqueHom R A] (f : C(σₙ R a, R)₀) (f' : C(σₙ R a, σₙ R (cfcₙHom ha f))₀) (hff' : ∀ x, f x = f' x)
(g : C(σₙ R (cfcₙHom ha f), R)₀) : cfcₙHom ha (g.comp f') = cfcₙHom (cfcₙHom_predicate ha f) g :=
by
let ψ : C(σₙ R (cfcₙHom ha f), R)₀ →⋆ₙₐ[R] C(σₙ R a, R)₀ :=
{ toFun := (ContinuousMapZero.comp · f')
map_smul' := fun _ _ ↦ rfl
map_add' := fun _ _ ↦ rfl
map_mul' := fun _ _ ↦ rfl
map_zero' := rfl
map_star' := fun _ ↦ rfl }
let φ : C(σₙ R (cfcₙHom ha f), R)₀ →⋆ₙₐ[R] A := (cfcₙHom ha).comp ψ
suffices cfcₙHom (cfcₙHom_predicate ha f) = φ from DFunLike.congr_fun this.symm g
refine cfcₙHom_eq_of_continuous_of_map_id (cfcₙHom_predicate ha f) φ ?_ ?_
· refine (cfcₙHom_isClosedEmbedding ha).continuous.comp <| continuous_induced_rng.mpr ?_
exact f'.toContinuousMap.continuous_precomp.comp continuous_induced_dom
· simp only [φ, ψ, NonUnitalStarAlgHom.comp_apply, NonUnitalStarAlgHom.coe_mk', NonUnitalAlgHom.coe_mk]
congr
ext x
simp [hff']
