English
There is a key relation in the localization setting showing that a certain combination of the renamed generator and the X-variable equals one, which becomes zero after applying compLocalizationAwayAlgHom.
Русский
Существует фундаментальное соотношение в локализации, в котором сочетание переименованного генератора и переменной X образуют единицу, и после применения compLocalizationAwayAlgHom это соотношение обращается в ноль.
LaTeX
$$compLocalizationAwayAlgHom (rename Sum.inr (P.σ g) * X (Sum.inl ()) - 1) = 0$$
Lean4
theorem compLocalizationAwayAlgHom_relation_eq_zero :
compLocalizationAwayAlgHom T g P (rename Sum.inr (P.σ g) * X (Sum.inl ()) - 1) = 0 :=
by
rw [map_sub, map_one, map_mul, ← toComp_toAlgHom (Generators.localizationAway T g) P]
change (compLocalizationAwayAlgHom T g P) (((localizationAway T g).toComp P).toAlgHom _) * _ - _ = _
rw [compLocalizationAwayAlgHom_toAlgHom_toComp, compLocalizationAwayAlgHom_X_inl,
IsScalarTower.algebraMap_apply P.Ring (P.Ring ⧸ P.ker ^ 2) (Localization.Away _)]
simp
