English
The product of two affine equivalences e1: P1 ≃ᵃ[k] P2 and e2: P3 ≃ᵃ[k] P4 yields an affine equivalence between the products: (P1×P3) ≃ᵃ[k] (P2×P4).
Русский
Произведение двух аффинных отображений даёт аффинное отображение между произведениями пространств: (P1×P3) ≃ᵃ[k] (P2×P4).
LaTeX
$$$\bigl(e_1 \times e_2\bigr) : P_1 \times P_3 \;\to\; P_2 \times P_4 \quad \text{является} \; \text{аффинным эквивалентом}$$$
Lean4
/-- The group of `AffineEquiv`s are equivalent to the group of units of `AffineMap`.
This is the affine version of `LinearMap.GeneralLinearGroup.generalLinearEquiv`. -/
@[simps]
def equivUnitsAffineMap : (P₁ ≃ᵃ[k] P₁) ≃* (P₁ →ᵃ[k] P₁)ˣ
where
toFun
e :=
{ val := e, inv := e.symm, val_inv := congr_arg toAffineMap e.symm_trans_self
inv_val := congr_arg toAffineMap e.self_trans_symm }
invFun
u :=
{ toFun := (u : P₁ →ᵃ[k] P₁)
invFun := (↑u⁻¹ : P₁ →ᵃ[k] P₁)
left_inv := AffineMap.congr_fun u.inv_mul
right_inv := AffineMap.congr_fun u.mul_inv
linear := LinearMap.GeneralLinearGroup.generalLinearEquiv _ _ <| Units.map AffineMap.linearHom u
map_vadd' := fun _ _ => (u : P₁ →ᵃ[k] P₁).map_vadd _ _ }
map_mul' _ _ := rfl
