Affine equivalences #
In this file we define AffineEquiv k P₁ P₂
(notation: P₁ ≃ᵃ[k] P₂
) to be the type of affine
equivalences between P₁
and P₂
, i.e., equivalences such that both forward and inverse maps are
affine maps.
We define the following equivalences:
AffineEquiv.refl k P
: the identity map as anAffineEquiv
;e.symm
: the inverse map of anAffineEquiv
as anAffineEquiv
;e.trans e'
: composition of twoAffineEquiv
s; note that the order followsmathlib
'sCategoryTheory
convention (applye
, thene'
), not the convention used in function composition and compositions of bundled morphisms.
We equip AffineEquiv k P P
with a Group
structure with multiplication corresponding to
composition in AffineEquiv.group
.
Tags #
affine space, affine equivalence
An affine equivalence, denoted P₁ ≃ᵃ[k] P₂
, is an equivalence between affine spaces
such that both forward and inverse maps are affine.
We define it using an Equiv
for the map and a LinearEquiv
for the linear part in order
to allow affine equivalences with good definitional equalities.
- toFun : P₁ → P₂
- invFun : P₂ → P₁
- left_inv : Function.LeftInverse self.invFun self.toFun
- right_inv : Function.RightInverse self.invFun self.toFun
Instances For
An affine equivalence, denoted P₁ ≃ᵃ[k] P₂
, is an equivalence between affine spaces
such that both forward and inverse maps are affine.
We define it using an Equiv
for the map and a LinearEquiv
for the linear part in order
to allow affine equivalences with good definitional equalities.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Reinterpret an AffineEquiv
as an AffineMap
.
Equations
- ↑e = { toFun := e.toFun, linear := ↑e.linear, map_vadd' := ⋯ }
Instances For
Equations
- AffineEquiv.instCoeFunForall = DFunLike.hasCoeToFun
Equations
- AffineEquiv.instCoeOutEquiv = { coe := AffineEquiv.toEquiv }
Equations
- AffineEquiv.instCoeAffineMap = { coe := AffineEquiv.toAffineMap }
Construct an affine equivalence by verifying the relation between the map and its linear part at
one base point. Namely, this function takes a map e : P₁ → P₂
, a linear equivalence
e' : V₁ ≃ₗ[k] V₂
, and a point p
such that for any other point p'
we have
e p' = e' (p' -ᵥ p) +ᵥ e p
.
Equations
- AffineEquiv.mk' e e' p h = { toFun := e, invFun := fun (q' : P₂) => e'.symm (q' -ᵥ e p) +ᵥ p, left_inv := ⋯, right_inv := ⋯, linear := e', map_vadd' := ⋯ }
Instances For
Inverse of an affine equivalence as an affine equivalence.
Equations
- e.symm = { toEquiv := e.symm, linear := e.linear.symm, map_vadd' := ⋯ }
Instances For
See Note [custom simps projection]
Equations
- AffineEquiv.Simps.apply e = ⇑e
Instances For
See Note [custom simps projection]
Equations
- AffineEquiv.Simps.symm_apply e = ⇑e.symm
Instances For
Bijective affine maps are affine isomorphisms.
Equations
- AffineEquiv.ofBijective hφ = { toEquiv := Equiv.ofBijective (⇑φ) hφ, linear := LinearEquiv.ofBijective φ.linear ⋯, map_vadd' := ⋯ }
Instances For
Identity map as an AffineEquiv
.
Equations
- AffineEquiv.refl k P₁ = { toEquiv := Equiv.refl P₁, linear := LinearEquiv.refl k V₁, map_vadd' := ⋯ }
Instances For
Composition of two AffineEquiv
alences, applied left to right.
Equations
- e.trans e' = { toEquiv := e.trans e'.toEquiv, linear := e.linear.trans e'.linear, map_vadd' := ⋯ }
Instances For
AffineEquiv.linear
on automorphisms is a MonoidHom
.
Equations
- AffineEquiv.linearHom = { toFun := AffineEquiv.linear, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The group of AffineEquiv
s are equivalent to the group of units of AffineMap
.
This is the affine version of LinearMap.GeneralLinearGroup.generalLinearEquiv
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The map v ↦ v +ᵥ b
as an affine equivalence between a module V
and an affine space P
with
tangent space V
.
Equations
- AffineEquiv.vaddConst k b = { toEquiv := Equiv.vaddConst b, linear := LinearEquiv.refl k V₁, map_vadd' := ⋯ }
Instances For
p' ↦ p -ᵥ p'
as an equivalence.
Equations
- AffineEquiv.constVSub k p = { toEquiv := Equiv.constVSub p, linear := LinearEquiv.neg k, map_vadd' := ⋯ }
Instances For
The map p ↦ v +ᵥ p
as an affine automorphism of an affine space.
Note that there is no need for an AffineMap.constVAdd
as it is always an equivalence.
This is roughly to DistribMulAction.toLinearEquiv
as +ᵥ
is to •
.
Equations
- AffineEquiv.constVAdd k P₁ v = { toEquiv := Equiv.constVAdd P₁ v, linear := LinearEquiv.refl k V₁, map_vadd' := ⋯ }
Instances For
A more bundled version of AffineEquiv.constVAdd
.
Equations
- AffineEquiv.constVAddHom k P₁ = { toFun := fun (v : Multiplicative V₁) => AffineEquiv.constVAdd k P₁ (Multiplicative.toAdd v), map_one' := ⋯, map_mul' := ⋯ }
Instances For
Fixing a point in affine space, homothety about this point gives a group homomorphism from (the centre of) the units of the scalars into the group of affine equivalences.
Equations
- AffineEquiv.homothetyUnitsMulHom p = AffineEquiv.equivUnitsAffineMap.symm.toMonoidHom.comp (Units.map (AffineMap.homothetyHom p))
Instances For
Point reflection in x
as a permutation.
Equations
- AffineEquiv.pointReflection k x = (AffineEquiv.constVSub k x).trans (AffineEquiv.vaddConst k x)
Instances For
x
is the only fixed point of pointReflection 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.
Interpret a linear equivalence between modules as an affine equivalence.
Equations
- e.toAffineEquiv = { toEquiv := e.toEquiv, linear := e, map_vadd' := ⋯ }