English
There is a multiplicative equivalence between the group of units in Unitization with fst=1 and the group of units of PreQuasiregular A.
Русский
Существует мультипликативное эквивалентностное отображение между группой единиц Unitization с fst=1 и группой единиц PreQuasiregular A.
LaTeX
$$$$ unitsFstOne\ R\ A \simeq^* (PreQuasiregular\ A)^{\times} $$$$
Lean4
/-- If `A` is a non-unital `R`-algebra, then the subgroup of units of `Unitization R A` whose
scalar part is `1 : R` (i.e., `Unitization.unitsFstOne`) is isomorphic to the group of units of
`PreQuasiregular A`. -/
@[simps]
def unitsFstOne_mulEquiv_quasiregular : unitsFstOne R A ≃* (PreQuasiregular A)ˣ
where
toFun
x :=
{ val := equiv x.val.val.snd
inv := equiv x⁻¹.val.val.snd
val_inv := equiv.symm.injective <| by simpa [-Units.mul_inv] using congr(snd $(x.val.mul_inv))
inv_val := equiv.symm.injective <| by simpa [-Units.inv_mul] using congr(snd $(x.val.inv_mul)) }
invFun
x :=
{ val :=
{ val := 1 + equiv.symm x.val
inv := 1 + equiv.symm x⁻¹.val
val_inv := by
convert congr((1 + $(inv_add_add_mul_eq_zero x) : Unitization R A)) using 1
· simp only [mul_one, equiv_symm_apply, one_mul, mul_add, add_mul, inr_add, inr_mul]
abel
· simp only [inr_zero, add_zero]
inv_val := by
convert congr((1 + $(add_inv_add_mul_eq_zero x) : Unitization R A)) using 1
· simp only [mul_one, equiv_symm_apply, one_mul, mul_add, add_mul, inr_add, inr_mul]
abel
· simp only [inr_zero, add_zero] }
property := by simp }
left_inv x := Subtype.ext <| Units.ext <| by simpa using x.val.val.inl_fst_add_inr_snd_eq
right_inv x := Units.ext <| by simp [-equiv_symm_apply]
map_mul' x y := Units.ext <| equiv.symm.injective <| by simp
