Continuous affine equivalences #
In this file, we define continuous affine equivalences, affine equivalences which are continuous with continuous inverse.
Main definitions #
ContinuousAffineEquiv.refl k P
: the identity map as aContinuousAffineEquiv
;e.symm
: the inverse map of aContinuousAffineEquiv
as aContinuousAffineEquiv
;e.trans e'
: composition of twoContinuousAffineEquiv
s; note that the order followsmathlib
'sCategoryTheory
convention (applye
, thene'
), not the convention used in function composition and compositions of bundled morphisms.e.toHomeomorph
: the continuous affine equivalencee
as a homeomorphismContinuousLinearEquiv.toContinuousAffineEquiv
: a continuous linear equivalence as a continuous affine equivalenceContinuousAffineEquiv.constVAdd
:AffineEquiv.constVAdd
as a continuous affine equivalence
TODO #
- equip
ContinuousAffineEquiv k P P
with aGroup
structure, with multiplication corresponding to composition inAffineEquiv.group
.
A continuous affine equivalence, denoted P₁ ≃ᵃL[k] P₂
, between two affine topological spaces
is an affine equivalence such that forward and inverse maps are continuous.
- toFun : P₁ → P₂
- invFun : P₂ → P₁
- left_inv : Function.LeftInverse (↑self).invFun (↑self).toFun
- right_inv : Function.RightInverse (↑self).invFun (↑self).toFun
- continuous_toFun : Continuous (↑self).toFun
- continuous_invFun : Continuous (↑self).invFun
Instances For
A continuous affine equivalence, denoted P₁ ≃ᵃL[k] P₂
, between two affine topological spaces
is an affine equivalence such that forward and inverse maps are continuous.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A continuous affine equivalence is a homeomorphism.
Equations
- e.toHomeomorph = { toEquiv := (↑e).toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
Equations
- ContinuousAffineEquiv.instCoeFunForall = DFunLike.hasCoeToFun
Coerce continuous affine equivalences to affine equivalences.
Equations
- ContinuousAffineEquiv.coe = { coe := ContinuousAffineEquiv.toAffineEquiv }
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Equations
Instances For
See Note [custom simps projection].
Equations
Instances For
Identity map as a ContinuousAffineEquiv
.
Equations
- ContinuousAffineEquiv.refl k P₁ = { toEquiv := Equiv.refl P₁, linear := LinearEquiv.refl k V₁, map_vadd' := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
Inverse of a continuous affine equivalence as a continuous affine equivalence.
Equations
- e.symm = { toAffineEquiv := (↑e).symm, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
Composition of two ContinuousAffineEquiv
alences, applied left to right.
Equations
- e.trans e' = { toAffineEquiv := (↑e).trans ↑e', continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
Reinterpret a continuous linear equivalence between modules as a continuous affine equivalence.
Equations
- L.toContinuousAffineEquiv = { toAffineEquiv := L.toAffineEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
The map p ↦ v +ᵥ p
as a continuous affine automorphism of an affine space
on which addition is continuous.
Equations
- ContinuousAffineEquiv.constVAdd k P₁ v = { toAffineEquiv := AffineEquiv.constVAdd k P₁ v, continuous_toFun := ⋯, continuous_invFun := ⋯ }