In this file we define
affine_equiv k P₁ P₂ (notation:
P₁ ≃ᵃ[k] P₂) to be the type of affine
P₁ and `P₂, i.e., equivalences such that both forward and inverse maps are
We define the following equivalences:
e.trans e': composition of two
affine_equivs; note that the order follows
e'), not the convention used in function composition and compositions of bundled morphisms.
affine space, affine equivalence
- to_equiv : P₁ ≃ P₂
- linear : V₁ ≃ₗ[k] V₂
- map_vadd' : ∀ (p : P₁) (v : V₁), ⇑(c.to_equiv) (v +ᵥ p) = ⇑(c.linear) v +ᵥ ⇑(c.to_equiv) p
An affine equivalence is an equivalence between affine spaces such that both forward and inverse maps are affine.
Interpret a linear equivalence between modules as an affine equivalence.
Identity map as an
Construct an affine equivalence by verifying the relation between the map and its linear part at
one base point. Namely, this function takes an equivalence
e : P₁ ≃ P₂, a linear equivalece
e' : V₁ ≃ₗ[k] V₂, and a point
p such that for any other point
p' we have
e p' = e' (p' -ᵥ p) +ᵥ e p.
Inverse of an affine equivalence as an affine equivalence.
Composition of two
affine_equivalences, applied left to right.
v ↦ v +ᵥ b as an affine equivalence between a module
V and an affine space
p' ↦ p -ᵥ p' as an equivalence.
p ↦ v +ᵥ p as an affine automorphism of an affine space.
Point reflection in
x as a permutation.
x is the only fixed point of
point_reflection x. This lemma requires
x + x = y + y ↔ x = y. There is no typeclass to use here, so we add it as an explicit argument.