Affine equivalences #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we define affine_equiv 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:
-
affine_equiv.refl k P: the identity map as anaffine_equiv; -
e.symm: the inverse map of anaffine_equivas anaffine_equiv; -
e.trans e': composition of twoaffine_equivs; note that the order followsmathlib'scategory_theoryconvention (applye, thene'), not the convention used in function composition and compositions of bundled morphisms.
We equip affine_equiv k P P with a group structure with multiplication corresponding to
composition in affine_equiv.group.
Tags #
affine space, affine equivalence
@[nolint]
structure
affine_equiv
(k : Type u_1)
(P₁ : Type u_2)
(P₂ : Type u_3)
{V₁ : Type u_4}
{V₂ : Type u_5}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂] :
Type (max u_2 u_3 u_4 u_5)
- to_equiv : P₁ ≃ P₂
- linear : V₁ ≃ₗ[k] V₂
- map_vadd' : ∀ (p : P₁) (v : V₁), ⇑(self.to_equiv) (v +ᵥ p) = ⇑(self.linear) v +ᵥ ⇑(self.to_equiv) p
An affine equivalence 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 linear_equiv for the linear part in order
to allow affine equivalences with good definitional equalities.
Instances for affine_equiv
- affine_equiv.has_sizeof_inst
- affine_equiv.equiv_like
- affine_equiv.has_coe_to_fun
- affine_equiv.equiv.has_coe
- affine_equiv.affine_map.has_coe
- affine_equiv.group
def
affine_equiv.to_affine_map
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂) :
Reinterpret an affine_equiv as an affine_map.
@[simp]
theorem
affine_equiv.to_affine_map_mk
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(f : P₁ ≃ P₂)
(f' : V₁ ≃ₗ[k] V₂)
(h : ∀ (p : P₁) (v : V₁), ⇑f (v +ᵥ p) = ⇑f' v +ᵥ ⇑f p) :
@[simp]
theorem
affine_equiv.linear_to_affine_map
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂) :
e.to_affine_map.linear = ↑(e.linear)
theorem
affine_equiv.to_affine_map_injective
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂] :
@[simp]
theorem
affine_equiv.to_affine_map_inj
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
{e e' : P₁ ≃ᵃ[k] P₂} :
e.to_affine_map = e'.to_affine_map ↔ e = e'
@[protected, instance]
def
affine_equiv.equiv_like
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂] :
equiv_like (P₁ ≃ᵃ[k] P₂) P₁ P₂
@[protected, instance]
def
affine_equiv.has_coe_to_fun
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂] :
@[protected, instance]
def
affine_equiv.equiv.has_coe
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂] :
Equations
- affine_equiv.equiv.has_coe = {coe := affine_equiv.to_equiv _inst_7}
@[simp]
theorem
affine_equiv.map_vadd
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂)
(p : P₁)
(v : V₁) :
@[simp]
theorem
affine_equiv.coe_to_equiv
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂) :
@[protected, instance]
def
affine_equiv.affine_map.has_coe
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂] :
Equations
@[simp]
theorem
affine_equiv.coe_to_affine_map
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂) :
⇑(e.to_affine_map) = ⇑e
@[simp, norm_cast]
theorem
affine_equiv.coe_coe
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂) :
@[simp]
theorem
affine_equiv.coe_linear
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂) :
@[ext]
theorem
affine_equiv.ext
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
{e e' : P₁ ≃ᵃ[k] P₂}
(h : ∀ (x : P₁), ⇑e x = ⇑e' x) :
e = e'
theorem
affine_equiv.coe_fn_injective
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂] :
@[simp, norm_cast]
theorem
affine_equiv.coe_fn_inj
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
{e e' : P₁ ≃ᵃ[k] P₂} :
theorem
affine_equiv.to_equiv_injective
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂] :
@[simp]
theorem
affine_equiv.to_equiv_inj
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
{e e' : P₁ ≃ᵃ[k] P₂} :
@[simp]
theorem
affine_equiv.coe_mk
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ P₂)
(e' : V₁ ≃ₗ[k] V₂)
(h : ∀ (p : P₁) (v : V₁), ⇑e (v +ᵥ p) = ⇑e' v +ᵥ ⇑e p) :
def
affine_equiv.mk'
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ → P₂)
(e' : V₁ ≃ₗ[k] V₂)
(p : P₁)
(h : ∀ (p' : P₁), e p' = ⇑e' (p' -ᵥ p) +ᵥ e p) :
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.
@[simp]
theorem
affine_equiv.coe_mk'
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ P₂)
(e' : V₁ ≃ₗ[k] V₂)
(p : P₁)
(h : ∀ (p' : P₁), ⇑e p' = ⇑e' (p' -ᵥ p) +ᵥ ⇑e p) :
⇑(affine_equiv.mk' ⇑e e' p h) = ⇑e
@[simp]
theorem
affine_equiv.linear_mk'
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ P₂)
(e' : V₁ ≃ₗ[k] V₂)
(p : P₁)
(h : ∀ (p' : P₁), ⇑e p' = ⇑e' (p' -ᵥ p) +ᵥ ⇑e p) :
(affine_equiv.mk' ⇑e e' p h).linear = e'
@[symm]
def
affine_equiv.symm
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂) :
Inverse of an affine equivalence as an affine equivalence.
@[simp]
theorem
affine_equiv.symm_to_equiv
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂) :
@[simp]
theorem
affine_equiv.symm_linear
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂) :
def
affine_equiv.simps.apply
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂) :
P₁ → P₂
See Note [custom simps projection]
Equations
def
affine_equiv.simps.symm_apply
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂) :
P₂ → P₁
See Note [custom simps projection]
Equations
@[protected]
theorem
affine_equiv.bijective
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂) :
@[protected]
theorem
affine_equiv.surjective
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂) :
@[protected]
theorem
affine_equiv.injective
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂) :
@[simp]
theorem
affine_equiv.of_bijective_symm_apply
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
{φ : P₁ →ᵃ[k] P₂}
(hφ : function.bijective ⇑φ)
(ᾰ : P₂) :
⇑((affine_equiv.of_bijective hφ).symm) ᾰ = (equiv.of_bijective ⇑φ hφ).inv_fun ᾰ
@[simp]
theorem
affine_equiv.of_bijective_apply
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
{φ : P₁ →ᵃ[k] P₂}
(hφ : function.bijective ⇑φ)
(ᾰ : P₁) :
⇑(affine_equiv.of_bijective hφ) ᾰ = (equiv.of_bijective ⇑φ hφ).to_fun ᾰ
noncomputable
def
affine_equiv.of_bijective
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
{φ : P₁ →ᵃ[k] P₂}
(hφ : function.bijective ⇑φ) :
Bijective affine maps are affine isomorphisms.
Equations
- affine_equiv.of_bijective hφ = {to_equiv := {to_fun := (equiv.of_bijective ⇑φ hφ).to_fun, inv_fun := (equiv.of_bijective ⇑φ hφ).inv_fun, left_inv := _, right_inv := _}, linear := linear_equiv.of_bijective φ.linear _, map_vadd' := _}
@[simp]
theorem
affine_equiv.linear_of_bijective
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
{φ : P₁ →ᵃ[k] P₂}
(hφ : function.bijective ⇑φ) :
theorem
affine_equiv.of_bijective.symm_eq
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
{φ : P₁ →ᵃ[k] P₂}
(hφ : function.bijective ⇑φ) :
(affine_equiv.of_bijective hφ).symm.to_equiv = (equiv.of_bijective ⇑φ hφ).symm
@[simp]
theorem
affine_equiv.range_eq
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂) :
@[simp]
theorem
affine_equiv.apply_symm_apply
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂)
(p : P₂) :
@[simp]
theorem
affine_equiv.symm_apply_apply
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂)
(p : P₁) :
theorem
affine_equiv.apply_eq_iff_eq_symm_apply
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂)
{p₁ : P₁}
{p₂ : P₂} :
@[simp]
theorem
affine_equiv.apply_eq_iff_eq
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂)
{p₁ p₂ : P₁} :
@[simp]
theorem
affine_equiv.image_symm
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(f : P₁ ≃ᵃ[k] P₂)
(s : set P₂) :
@[simp]
theorem
affine_equiv.preimage_symm
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(f : P₁ ≃ᵃ[k] P₂)
(s : set P₁) :
@[refl]
def
affine_equiv.refl
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁] :
Identity map as an affine_equiv.
Equations
- affine_equiv.refl k P₁ = {to_equiv := equiv.refl P₁, linear := linear_equiv.refl k V₁ _inst_3, map_vadd' := _}
@[simp]
theorem
affine_equiv.coe_refl
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁] :
⇑(affine_equiv.refl k P₁) = id
@[simp]
theorem
affine_equiv.coe_refl_to_affine_map
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁] :
↑(affine_equiv.refl k P₁) = affine_map.id k P₁
@[simp]
theorem
affine_equiv.refl_apply
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(x : P₁) :
⇑(affine_equiv.refl k P₁) x = x
@[simp]
theorem
affine_equiv.to_equiv_refl
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁] :
(affine_equiv.refl k P₁).to_equiv = equiv.refl P₁
@[simp]
theorem
affine_equiv.linear_refl
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁] :
(affine_equiv.refl k P₁).linear = linear_equiv.refl k V₁
@[simp]
theorem
affine_equiv.symm_refl
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁] :
(affine_equiv.refl k P₁).symm = affine_equiv.refl k P₁
@[trans]
def
affine_equiv.trans
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{P₃ : Type u_4}
{V₁ : Type u_6}
{V₂ : Type u_7}
{V₃ : Type u_8}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
[add_comm_group V₃]
[module k V₃]
[add_torsor V₃ P₃]
(e : P₁ ≃ᵃ[k] P₂)
(e' : P₂ ≃ᵃ[k] P₃) :
Composition of two affine_equivalences, applied left to right.
@[simp]
theorem
affine_equiv.coe_trans
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{P₃ : Type u_4}
{V₁ : Type u_6}
{V₂ : Type u_7}
{V₃ : Type u_8}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
[add_comm_group V₃]
[module k V₃]
[add_torsor V₃ P₃]
(e : P₁ ≃ᵃ[k] P₂)
(e' : P₂ ≃ᵃ[k] P₃) :
@[simp]
theorem
affine_equiv.coe_trans_to_affine_map
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{P₃ : Type u_4}
{V₁ : Type u_6}
{V₂ : Type u_7}
{V₃ : Type u_8}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
[add_comm_group V₃]
[module k V₃]
[add_torsor V₃ P₃]
(e : P₁ ≃ᵃ[k] P₂)
(e' : P₂ ≃ᵃ[k] P₃) :
@[simp]
theorem
affine_equiv.trans_apply
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{P₃ : Type u_4}
{V₁ : Type u_6}
{V₂ : Type u_7}
{V₃ : Type u_8}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
[add_comm_group V₃]
[module k V₃]
[add_torsor V₃ P₃]
(e : P₁ ≃ᵃ[k] P₂)
(e' : P₂ ≃ᵃ[k] P₃)
(p : P₁) :
theorem
affine_equiv.trans_assoc
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{P₃ : Type u_4}
{P₄ : Type u_5}
{V₁ : Type u_6}
{V₂ : Type u_7}
{V₃ : Type u_8}
{V₄ : Type u_9}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
[add_comm_group V₃]
[module k V₃]
[add_torsor V₃ P₃]
[add_comm_group V₄]
[module k V₄]
[add_torsor V₄ P₄]
(e₁ : P₁ ≃ᵃ[k] P₂)
(e₂ : P₂ ≃ᵃ[k] P₃)
(e₃ : P₃ ≃ᵃ[k] P₄) :
@[simp]
theorem
affine_equiv.trans_refl
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂) :
e.trans (affine_equiv.refl k P₂) = e
@[simp]
theorem
affine_equiv.refl_trans
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂) :
(affine_equiv.refl k P₁).trans e = e
@[simp]
theorem
affine_equiv.self_trans_symm
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂) :
e.trans e.symm = affine_equiv.refl k P₁
@[simp]
theorem
affine_equiv.symm_trans_self
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂) :
e.symm.trans e = affine_equiv.refl k P₂
@[simp]
theorem
affine_equiv.apply_line_map
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[add_comm_group V₂]
[module k V₂]
[add_torsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂)
(a b : P₁)
(c : k) :
⇑e (⇑(affine_map.line_map a b) c) = ⇑(affine_map.line_map (⇑e a) (⇑e b)) c
@[protected, instance]
def
affine_equiv.group
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁] :
Equations
- affine_equiv.group = {mul := λ (e e' : P₁ ≃ᵃ[k] P₁), e'.trans e, mul_assoc := _, one := affine_equiv.refl k P₁ _inst_4, one_mul := _, mul_one := _, npow := div_inv_monoid.npow._default (affine_equiv.refl k P₁) (λ (e e' : P₁ ≃ᵃ[k] P₁), e'.trans e) affine_equiv.trans_refl affine_equiv.refl_trans, npow_zero' := _, npow_succ' := _, inv := affine_equiv.symm _inst_4, div := div_inv_monoid.div._default (λ (e e' : P₁ ≃ᵃ[k] P₁), e'.trans e) affine_equiv.group._proof_4 (affine_equiv.refl k P₁) affine_equiv.trans_refl affine_equiv.refl_trans (div_inv_monoid.npow._default (affine_equiv.refl k P₁) (λ (e e' : P₁ ≃ᵃ[k] P₁), e'.trans e) affine_equiv.trans_refl affine_equiv.refl_trans) affine_equiv.group._proof_5 affine_equiv.group._proof_6 affine_equiv.symm, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default (λ (e e' : P₁ ≃ᵃ[k] P₁), e'.trans e) affine_equiv.group._proof_8 (affine_equiv.refl k P₁) affine_equiv.trans_refl affine_equiv.refl_trans (div_inv_monoid.npow._default (affine_equiv.refl k P₁) (λ (e e' : P₁ ≃ᵃ[k] P₁), e'.trans e) affine_equiv.trans_refl affine_equiv.refl_trans) affine_equiv.group._proof_9 affine_equiv.group._proof_10 affine_equiv.symm, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
theorem
affine_equiv.one_def
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁] :
1 = affine_equiv.refl k P₁
@[simp]
theorem
affine_equiv.coe_one
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁] :
theorem
affine_equiv.mul_def
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(e e' : P₁ ≃ᵃ[k] P₁) :
theorem
affine_equiv.inv_def
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(e : P₁ ≃ᵃ[k] P₁) :
def
affine_equiv.linear_hom
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁] :
affine_equiv.linear on automorphisms is a monoid_hom.
Equations
- affine_equiv.linear_hom = {to_fun := affine_equiv.linear _inst_4, map_one' := _, map_mul' := _}
@[simp]
theorem
affine_equiv.linear_hom_apply
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(self : P₁ ≃ᵃ[k] P₁) :
⇑affine_equiv.linear_hom self = self.linear
@[simp]
theorem
affine_equiv.coe_equiv_units_affine_map_apply
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(e : P₁ ≃ᵃ[k] P₁) :
def
affine_equiv.equiv_units_affine_map
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁] :
The group of affine_equivs are equivalent to the group of units of affine_map.
This is the affine version of linear_map.general_linear_group.general_linear_equiv.
Equations
- affine_equiv.equiv_units_affine_map = {to_fun := λ (e : P₁ ≃ᵃ[k] P₁), {val := ↑e, inv := ↑(e.symm), val_inv := _, inv_val := _}, inv_fun := λ (u : (P₁ →ᵃ[k] P₁)ˣ), {to_equiv := {to_fun := ⇑↑u, inv_fun := ⇑↑u⁻¹, left_inv := _, right_inv := _}, linear := ⇑(linear_map.general_linear_group.general_linear_equiv k V₁) (⇑(units.map affine_map.linear_hom) u), map_vadd' := _}, left_inv := _, right_inv := _, map_mul' := _}
@[simp]
theorem
affine_equiv.equiv_units_affine_map_symm_apply_apply
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(u : (P₁ →ᵃ[k] P₁)ˣ)
(ᾰ : P₁) :
@[simp]
theorem
affine_equiv.linear_equiv_units_affine_map_symm_apply
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(u : (P₁ →ᵃ[k] P₁)ˣ) :
@[simp]
theorem
affine_equiv.coe_inv_equiv_units_affine_map_apply
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(e : P₁ ≃ᵃ[k] P₁) :
@[simp]
theorem
affine_equiv.vadd_const_symm_apply
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(b p' : P₁) :
⇑((affine_equiv.vadd_const k b).symm) p' = p' -ᵥ b
def
affine_equiv.vadd_const
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(b : P₁) :
The map v ↦ v +ᵥ b as an affine equivalence between a module V and an affine space P with
tangent space V.
Equations
- affine_equiv.vadd_const k b = {to_equiv := equiv.vadd_const b, linear := linear_equiv.refl k V₁ _inst_3, map_vadd' := _}
@[simp]
theorem
affine_equiv.vadd_const_apply
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(b : P₁)
(v : V₁) :
⇑(affine_equiv.vadd_const k b) v = v +ᵥ b
@[simp]
theorem
affine_equiv.linear_vadd_const
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(b : P₁) :
(affine_equiv.vadd_const k b).linear = linear_equiv.refl k V₁
def
affine_equiv.const_vsub
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(p : P₁) :
p' ↦ p -ᵥ p' as an equivalence.
Equations
- affine_equiv.const_vsub k p = {to_equiv := equiv.const_vsub p, linear := linear_equiv.neg k _inst_3, map_vadd' := _}
@[simp]
theorem
affine_equiv.coe_const_vsub
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(p : P₁) :
⇑(affine_equiv.const_vsub k p) = has_vsub.vsub p
@[simp]
theorem
affine_equiv.coe_const_vsub_symm
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(p : P₁) :
@[simp]
theorem
affine_equiv.const_vadd_apply
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(v : V₁)
(ᾰ : P₁) :
⇑(affine_equiv.const_vadd k P₁ v) ᾰ = v +ᵥ ᾰ
def
affine_equiv.const_vadd
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(v : V₁) :
The map p ↦ v +ᵥ p as an affine automorphism of an affine space.
Note that there is no need for an affine_map.const_vadd as it is always an equivalence.
This is roughly to distrib_mul_action.to_linear_equiv as +ᵥ is to •.
Equations
- affine_equiv.const_vadd k P₁ v = {to_equiv := equiv.const_vadd P₁ v, linear := linear_equiv.refl k V₁ _inst_3, map_vadd' := _}
@[simp]
theorem
affine_equiv.linear_const_vadd
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(v : V₁) :
(affine_equiv.const_vadd k P₁ v).linear = linear_equiv.refl k V₁
@[simp]
theorem
affine_equiv.const_vadd_zero
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁] :
affine_equiv.const_vadd k P₁ 0 = affine_equiv.refl k P₁
@[simp]
theorem
affine_equiv.const_vadd_add
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(v w : V₁) :
affine_equiv.const_vadd k P₁ (v + w) = (affine_equiv.const_vadd k P₁ w).trans (affine_equiv.const_vadd k P₁ v)
@[simp]
theorem
affine_equiv.const_vadd_symm
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(v : V₁) :
(affine_equiv.const_vadd k P₁ v).symm = affine_equiv.const_vadd k P₁ (-v)
@[simp]
theorem
affine_equiv.const_vadd_hom_apply
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(v : multiplicative V₁) :
⇑(affine_equiv.const_vadd_hom k P₁) v = affine_equiv.const_vadd k P₁ (⇑multiplicative.to_add v)
def
affine_equiv.const_vadd_hom
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁] :
multiplicative V₁ →* P₁ ≃ᵃ[k] P₁
A more bundled version of affine_equiv.const_vadd.
Equations
- affine_equiv.const_vadd_hom k P₁ = {to_fun := λ (v : multiplicative V₁), affine_equiv.const_vadd k P₁ (⇑multiplicative.to_add v), map_one' := _, map_mul' := _}
theorem
affine_equiv.const_vadd_nsmul
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(n : ℕ)
(v : V₁) :
affine_equiv.const_vadd k P₁ (n • v) = affine_equiv.const_vadd k P₁ v ^ n
theorem
affine_equiv.const_vadd_zsmul
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(z : ℤ)
(v : V₁) :
affine_equiv.const_vadd k P₁ (z • v) = affine_equiv.const_vadd k P₁ v ^ z
def
affine_equiv.homothety_units_mul_hom
{R : Type u_10}
{V : Type u_11}
{P : Type u_12}
[comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
(p : P) :
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.
@[simp]
theorem
affine_equiv.coe_homothety_units_mul_hom_apply
{R : Type u_10}
{V : Type u_11}
{P : Type u_12}
[comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
(p : P)
(t : Rˣ) :
⇑(⇑(affine_equiv.homothety_units_mul_hom p) t) = ⇑(affine_map.homothety p ↑t)
@[simp]
theorem
affine_equiv.coe_homothety_units_mul_hom_apply_symm
{R : Type u_10}
{V : Type u_11}
{P : Type u_12}
[comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
(p : P)
(t : Rˣ) :
⇑((⇑(affine_equiv.homothety_units_mul_hom p) t).symm) = ⇑(affine_map.homothety p ↑t⁻¹)
@[simp]
theorem
affine_equiv.coe_homothety_units_mul_hom_eq_homothety_hom_coe
{R : Type u_10}
{V : Type u_11}
{P : Type u_12}
[comm_ring R]
[add_comm_group V]
[module R V]
[add_torsor V P]
(p : P) :
def
affine_equiv.point_reflection
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(x : P₁) :
Point reflection in x as a permutation.
Equations
theorem
affine_equiv.point_reflection_apply
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(x y : P₁) :
⇑(affine_equiv.point_reflection k x) y = x -ᵥ y +ᵥ x
@[simp]
theorem
affine_equiv.point_reflection_symm
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(x : P₁) :
@[simp]
theorem
affine_equiv.to_equiv_point_reflection
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(x : P₁) :
@[simp]
theorem
affine_equiv.point_reflection_self
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(x : P₁) :
⇑(affine_equiv.point_reflection k x) x = x
theorem
affine_equiv.point_reflection_involutive
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(x : P₁) :
theorem
affine_equiv.point_reflection_fixed_iff_of_injective_bit0
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
{x y : P₁}
(h : function.injective bit0) :
⇑(affine_equiv.point_reflection k x) y = y ↔ y = x
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.
theorem
affine_equiv.injective_point_reflection_left_of_injective_bit0
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(h : function.injective bit0)
(y : P₁) :
function.injective (λ (x : P₁), ⇑(affine_equiv.point_reflection k x) y)
theorem
affine_equiv.injective_point_reflection_left_of_module
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[invertible 2]
(y : P₁) :
function.injective (λ (x : P₁), ⇑(affine_equiv.point_reflection k x) y)
theorem
affine_equiv.point_reflection_fixed_iff_of_module
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
[invertible 2]
{x y : P₁} :
⇑(affine_equiv.point_reflection k x) y = y ↔ y = x
def
linear_equiv.to_affine_equiv
{k : Type u_1}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_comm_group V₂]
[module k V₂]
(e : V₁ ≃ₗ[k] V₂) :
Interpret a linear equivalence between modules as an affine equivalence.
@[simp]
theorem
linear_equiv.coe_to_affine_equiv
{k : Type u_1}
{V₁ : Type u_6}
{V₂ : Type u_7}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_comm_group V₂]
[module k V₂]
(e : V₁ ≃ₗ[k] V₂) :
⇑(e.to_affine_equiv) = ⇑e
theorem
affine_map.line_map_vadd
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(v v' : V₁)
(p : P₁)
(c : k) :
⇑(affine_map.line_map v v') c +ᵥ p = ⇑(affine_map.line_map (v +ᵥ p) (v' +ᵥ p)) c
theorem
affine_map.line_map_vsub
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(p₁ p₂ p₃ : P₁)
(c : k) :
⇑(affine_map.line_map p₁ p₂) c -ᵥ p₃ = ⇑(affine_map.line_map (p₁ -ᵥ p₃) (p₂ -ᵥ p₃)) c
theorem
affine_map.vsub_line_map
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(p₁ p₂ p₃ : P₁)
(c : k) :
p₁ -ᵥ ⇑(affine_map.line_map p₂ p₃) c = ⇑(affine_map.line_map (p₁ -ᵥ p₂) (p₁ -ᵥ p₃)) c
theorem
affine_map.vadd_line_map
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[ring k]
[add_comm_group V₁]
[module k V₁]
[add_torsor V₁ P₁]
(v : V₁)
(p₁ p₂ : P₁)
(c : k) :
v +ᵥ ⇑(affine_map.line_map p₁ p₂) c = ⇑(affine_map.line_map (v +ᵥ p₁) (v +ᵥ p₂)) c
theorem
affine_map.homothety_neg_one_apply
{P₁ : Type u_2}
{V₁ : Type u_6}
[add_comm_group V₁]
[add_torsor V₁ P₁]
{R' : Type u_10}
[comm_ring R']
[module R' V₁]
(c p : P₁) :
⇑(affine_map.homothety c (-1)) p = ⇑(affine_equiv.point_reflection R' c) p