English
If x = a + r y with a ∈ (extensionOfMax i f).domain and r ∈ R, then extensionToFun(i,f,h)(x) equals (extensionOfMax i f).toLinearPMap(a) + extendIdealTo(i,f,h,y)(r). This is a well-defined behavior under the relation a + r y.
Русский
Если x = a + r y с a ∈ домена extensionOfMax и r ∈ R, то extensionToFun(i,f,h)(x) = (extensionOfMax i f).toLinearPMap(a) + extendIdealTo(i,f,h,y)(r). Это согласованное поведение относительно представления x.
LaTeX
$$$ ExtensionToFun\_wd(i,f,h)(x) = (extensionOfMax(i,f)).toLinearPMap(ExtensionOfMaxAdjoin.fst(i,x)) + ExtendIdealTo(i,f,h,y)(ExtensionOfMaxAdjoin.snd(i,x)) $$$
Lean4
theorem extensionToFun_wd (h : Module.Baer R Q) {y : N} (x : supExtensionOfMaxSingleton i f y)
(a : (extensionOfMax i f).domain) (r : R) (eq1 : ↑x = ↑a + r • y) :
ExtensionOfMaxAdjoin.extensionToFun i f h x =
(extensionOfMax i f).toLinearPMap a + ExtensionOfMaxAdjoin.extendIdealTo i f h y r :=
by
obtain ⟨a, ha⟩ := a
have eq2 : (ExtensionOfMaxAdjoin.fst i x - a : N) = (r - ExtensionOfMaxAdjoin.snd i x) • y :=
by
change x = a + r • y at eq1
rwa [ExtensionOfMaxAdjoin.eqn, ← sub_eq_zero, ← sub_sub_sub_eq, sub_eq_zero, ← sub_smul] at eq1
have eq3 :=
ExtensionOfMaxAdjoin.extendIdealTo_eq i f h (r - ExtensionOfMaxAdjoin.snd i x)
(by rw [← eq2]; exact Submodule.sub_mem _ (ExtensionOfMaxAdjoin.fst i x).2 ha)
simp only [map_sub, sub_smul, sub_eq_iff_eq_add] at eq3
unfold ExtensionOfMaxAdjoin.extensionToFun
rw [eq3, ← add_assoc, ← (extensionOfMax i f).toLinearPMap.map_add, AddMemClass.mk_add_mk]
congr
ext
dsimp
rw [Subtype.coe_mk, add_sub, ← eq1]
exact eq_sub_of_add_eq (ExtensionOfMaxAdjoin.eqn i x).symm
