Topology of affine subspaces.

This file defines the embedding map from an affine subspace to the ambient space as a continuous affine map.

Main definitions

• AffineSubspace.subtypeA is AffineSubspace.subtype as a ContinuousAffineMap.

def AffineSubspace.subtypeA {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] (s : AffineSubspace R P) [Nonempty ↥s] : ↥s →ᴬ[R] P

Embedding of an affine subspace to the ambient space, as a continuous affine map.

Equations

• s.subtypeA = { toAffineMap := s.subtype, cont := ⋯ }

@[simp]

theorem AffineSubspace.coe_subtypeA {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] (s : AffineSubspace R P) [Nonempty ↥s] : ⇑s.subtypeA = Subtype.val

@[simp]

theorem AffineSubspace.subtypeA_toAffineMap {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] (s : AffineSubspace R P) [Nonempty ↥s] : ↑s.subtypeA = s.subtype

noncomputable def AffineSubspace.ofEq {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] {s t : AffineSubspace R P} [Nonempty ↥s] [Nonempty ↥t] (h : s = t) : ↥s ≃ᴬ[R] ↥t

AffineEquiv.ofEq as a continuous affine equivalence.

Equations

• AffineSubspace.ofEq h = { toAffineEquiv := AffineEquiv.ofEq s t h, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem AffineSubspace.coe_ofEq_apply {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] {s t : AffineSubspace R P} [Nonempty ↥s] [Nonempty ↥t] (h : s = t) (x : ↥s) : ↑((ofEq h) x) = ↑x

noncomputable def ContinuousAffineEquiv.affineSubspaceMap {R : Type u_1} {V : Type u_2} {P : Type u_3} {W : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] (e : P ≃ᴬ[R] Q) (s : AffineSubspace R P) [Nonempty ↥s] : ↥s ≃ᴬ[R] ↥(AffineSubspace.map (↑↑e) s)

A continuous affine equivalence restricts to a continuous affine equivalence between an affine subspace and its image.

This is the continuous affine version of AffineEquiv.affineSubspaceMap.

Equations

• e.affineSubspaceMap s = { toAffineEquiv := (↑e).affineSubspaceMap s, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousAffineEquiv.affineSubspaceMap_apply {R : Type u_1} {V : Type u_2} {P : Type u_3} {W : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] (e : P ≃ᴬ[R] Q) (s : AffineSubspace R P) [Nonempty ↥s] (x : ↥s) : ↑((e.affineSubspaceMap s) x) = e ↑x

@[simp]

theorem ContinuousAffineEquiv.affineSubspaceMap_apply_symm_apply {R : Type u_1} {V : Type u_2} {P : Type u_3} {W : Type u_4} {Q : Type u_5} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [AddCommGroup W] [Module R W] [TopologicalSpace Q] [AddTorsor W Q] (e : P ≃ᴬ[R] Q) (s : AffineSubspace R P) [Nonempty ↥s] (x : ↥(AffineSubspace.map (↑↑e) s)) : e ↑((e.affineSubspaceMap s).symm x) = ↑x

instance AffineSubspace.instIsTopologicalAddTorsorSubtypeMemSubmoduleDirection {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [TopologicalSpace V] [IsTopologicalAddTorsor P] {s : AffineSubspace R P} [Nonempty ↥s] : IsTopologicalAddTorsor ↥s

theorem AffineSubspace.isClosed_direction_iff {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup V] [Module R V] [TopologicalSpace P] [AddTorsor V P] [TopologicalSpace V] [IsTopologicalAddTorsor P] [T1Space V] (s : AffineSubspace R P) : IsClosed ↑s.direction ↔ IsClosed ↑s