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 anAffineEquivas anAffineEquiv;e.trans e': composition of twoAffineEquivs; note that the order followsmathlib'sCategoryTheoryconvention (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
structure
AffineEquiv
(k : Type u_1)
(P₁ : Type u_2)
(P₂ : Type u_3)
{V₁ : Type u_4}
{V₂ : Type u_5}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
extends P₁ ≃ P₂ :
Type (max (max (max u_2 u_3) u_4) u_5)
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.
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.
Instances For
def
AffineEquiv.toAffineMap
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂)
:
Reinterpret an AffineEquiv as an AffineMap.
Instances For
@[simp]
theorem
AffineEquiv.toAffineMap_mk
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
(f : P₁ ≃ P₂)
(f' : V₁ ≃ₗ[k] V₂)
(h : ∀ (p : P₁) (v : V₁), f (v +ᵥ p) = f' v +ᵥ f p)
:
@[simp]
theorem
AffineEquiv.toAffineMap_injective
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
:
Function.Injective toAffineMap
@[simp]
theorem
AffineEquiv.toAffineMap_inj
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
{e e' : P₁ ≃ᵃ[k] P₂}
:
↑e = ↑e' ↔ e = e'
@[implicit_reducible]
@[implicit_reducible]
@[simp]
@[simp]
@[implicit_reducible]
@[simp]
theorem
AffineEquiv.coe_toAffineMap
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂)
:
⇑↑e = ⇑e
@[simp]
theorem
AffineEquiv.coe_coe
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂)
:
⇑↑e = ⇑e
@[simp]
theorem
AffineEquiv.ext_iff
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
{e e' : P₁ ≃ᵃ[k] P₂}
:
e = e' ↔ ∀ (x : P₁), e x = e' x
theorem
AffineEquiv.coeFn_injective
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
:
Function.Injective DFunLike.coe
theorem
AffineEquiv.coeFn_inj
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
{e e' : P₁ ≃ᵃ[k] P₂}
:
⇑e = ⇑e' ↔ e = e'
theorem
AffineEquiv.toEquiv_injective
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
:
Function.Injective toEquiv
@[simp]
@[simp]
theorem
AffineEquiv.coe_mk
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
(e : P₁ ≃ P₂)
(e' : V₁ ≃ₗ[k] V₂)
(h : ∀ (p : P₁) (v : V₁), e (v +ᵥ p) = e' v +ᵥ e p)
:
def
AffineEquiv.mk'
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor 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.
Instances For
@[simp]
theorem
AffineEquiv.coe_mk'
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
(e : P₁ ≃ P₂)
(e' : V₁ ≃ₗ[k] V₂)
(p : P₁)
(h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p)
:
⇑(mk' (⇑e) e' p h) = ⇑e
@[simp]
theorem
AffineEquiv.linear_mk'
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
(e : P₁ ≃ P₂)
(e' : V₁ ≃ₗ[k] V₂)
(p : P₁)
(h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p)
:
def
AffineEquiv.symm
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂)
:
Inverse of an affine equivalence as an affine equivalence.
Instances For
@[simp]
@[simp]
def
AffineEquiv.Simps.apply
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂)
:
P₁ → P₂
See Note [custom simps projection]
Instances For
def
AffineEquiv.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]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂)
:
P₂ → P₁
See Note [custom simps projection]
Instances For
theorem
AffineEquiv.bijective
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂)
:
theorem
AffineEquiv.surjective
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂)
:
Function.Surjective ⇑e
theorem
AffineEquiv.injective
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂)
:
Function.Injective ⇑e
noncomputable def
AffineEquiv.ofBijective
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
{φ : P₁ →ᵃ[k] P₂}
(hφ : Function.Bijective ⇑φ)
:
Bijective affine maps are affine isomorphisms.
Instances For
@[simp]
theorem
AffineEquiv.linear_ofBijective
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
{φ : P₁ →ᵃ[k] P₂}
(hφ : Function.Bijective ⇑φ)
:
(ofBijective hφ).linear = LinearEquiv.ofBijective φ.linear ⋯
@[simp]
theorem
AffineEquiv.ofBijective_apply
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
{φ : P₁ →ᵃ[k] P₂}
(hφ : Function.Bijective ⇑φ)
(a : P₁)
:
(ofBijective hφ) a = φ a
theorem
AffineEquiv.ofBijective.symm_eq
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
{φ : P₁ →ᵃ[k] P₂}
(hφ : Function.Bijective ⇑φ)
:
(ofBijective hφ).symm.toEquiv = (Equiv.ofBijective (⇑φ) hφ).symm
@[simp]
@[simp]
theorem
AffineEquiv.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]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂)
{p₁ : P₁}
{p₂ : P₂}
:
e p₁ = p₂ ↔ p₁ = e.symm p₂
theorem
AffineEquiv.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]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂)
{p₁ p₂ : P₁}
:
e p₁ = e p₂ ↔ p₁ = p₂
@[simp]
@[simp]
def
AffineEquiv.refl
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
:
Identity map as an AffineEquiv.
Instances For
@[simp]
theorem
AffineEquiv.coe_refl
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
:
⇑(refl k P₁) = id
@[simp]
theorem
AffineEquiv.coe_refl_to_affineMap
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
:
↑(refl k P₁) = AffineMap.id k P₁
@[simp]
theorem
AffineEquiv.refl_apply
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
(x : P₁)
:
(refl k P₁) x = x
@[simp]
theorem
AffineEquiv.toEquiv_refl
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
:
(refl k P₁).toEquiv = Equiv.refl P₁
@[simp]
theorem
AffineEquiv.linear_refl
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
:
(refl k P₁).linear = LinearEquiv.refl k V₁
@[simp]
def
AffineEquiv.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]
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[Module k V₁]
[Module k V₂]
[Module k V₃]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
[AddTorsor V₃ P₃]
(e : P₁ ≃ᵃ[k] P₂)
(e' : P₂ ≃ᵃ[k] P₃)
:
Composition of two AffineEquivalences, applied left to right.
Instances For
@[simp]
theorem
AffineEquiv.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]
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[Module k V₁]
[Module k V₂]
[Module k V₃]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
[AddTorsor V₃ P₃]
(e : P₁ ≃ᵃ[k] P₂)
(e' : P₂ ≃ᵃ[k] P₃)
:
⇑(e.trans e') = ⇑e' ∘ ⇑e
@[simp]
theorem
AffineEquiv.coe_trans_to_affineMap
{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]
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[Module k V₁]
[Module k V₂]
[Module k V₃]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
[AddTorsor V₃ P₃]
(e : P₁ ≃ᵃ[k] P₂)
(e' : P₂ ≃ᵃ[k] P₃)
:
@[simp]
theorem
AffineEquiv.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]
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[Module k V₁]
[Module k V₂]
[Module k V₃]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
[AddTorsor V₃ P₃]
(e : P₁ ≃ᵃ[k] P₂)
(e' : P₂ ≃ᵃ[k] P₃)
(p : P₁)
:
(e.trans e') p = e' (e p)
theorem
AffineEquiv.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]
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[AddCommGroup V₄]
[Module k V₁]
[Module k V₂]
[Module k V₃]
[Module k V₄]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
[AddTorsor V₃ P₃]
[AddTorsor V₄ P₄]
(e₁ : P₁ ≃ᵃ[k] P₂)
(e₂ : P₂ ≃ᵃ[k] P₃)
(e₃ : P₃ ≃ᵃ[k] P₄)
:
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
AffineEquiv.apply_lineMap
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
(e : P₁ ≃ᵃ[k] P₂)
(a b : P₁)
(c : k)
:
e ((AffineMap.lineMap a b) c) = (AffineMap.lineMap (e a) (e b)) c
@[implicit_reducible]
theorem
AffineEquiv.one_def
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
:
1 = refl k P₁
@[simp]
theorem
AffineEquiv.coe_one
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
:
⇑1 = id
@[simp]
theorem
AffineEquiv.coe_mul
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
(e e' : P₁ ≃ᵃ[k] P₁)
:
⇑(e * e') = ⇑e ∘ ⇑e'
def
AffineEquiv.linearHom
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
:
AffineEquiv.linear on automorphisms is a MonoidHom.
Instances For
@[simp]
def
AffineEquiv.equivUnitsAffineMap
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
:
The group of AffineEquivs are equivalent to the group of units of AffineMap.
This is the affine version of LinearMap.GeneralLinearGroup.generalLinearEquiv.
Instances For
@[simp]
theorem
AffineEquiv.equivUnitsAffineMap_symm_apply_apply
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
(u : (P₁ →ᵃ[k] P₁)ˣ)
(a : P₁)
:
(equivUnitsAffineMap.symm u) a = ↑u a
@[simp]
theorem
AffineEquiv.equivUnitsAffineMap_symm_apply_invFun
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
(u : (P₁ →ᵃ[k] P₁)ˣ)
(a : P₁)
:
(equivUnitsAffineMap.symm u).invFun a = ↑u⁻¹ a
@[simp]
theorem
AffineEquiv.equivUnitsAffineMap_symm_apply_toFun
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
(u : (P₁ →ᵃ[k] P₁)ˣ)
(a : P₁)
:
(equivUnitsAffineMap.symm u) a = ↑u a
@[simp]
theorem
AffineEquiv.val_equivUnitsAffineMap_apply
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
(e : P₁ ≃ᵃ[k] P₁)
:
↑(equivUnitsAffineMap e) = ↑e
@[simp]
theorem
AffineEquiv.equivUnitsAffineMap_symm_apply_symm_apply
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
(u : (P₁ →ᵃ[k] P₁)ˣ)
(a : P₁)
:
(equivUnitsAffineMap.symm u).symm a = ↑u⁻¹ a
@[simp]
theorem
AffineEquiv.val_inv_equivUnitsAffineMap_apply
{k : Type u_1}
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
(e : P₁ ≃ᵃ[k] P₁)
:
↑(equivUnitsAffineMap e)⁻¹ = ↑e.symm
def
AffineEquiv.prodCongr
{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]
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[AddCommGroup V₄]
[Module k V₁]
[Module k V₂]
[Module k V₃]
[Module k V₄]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
[AddTorsor V₃ P₃]
[AddTorsor V₄ P₄]
(e₁ : P₁ ≃ᵃ[k] P₂)
(e₂ : P₃ ≃ᵃ[k] P₄)
:
Product of two affine equivalences. The map comes from Equiv.prodCongr
Instances For
@[simp]
theorem
AffineEquiv.linear_prodCongr
{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]
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[AddCommGroup V₄]
[Module k V₁]
[Module k V₂]
[Module k V₃]
[Module k V₄]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
[AddTorsor V₃ P₃]
[AddTorsor V₄ P₄]
(e₁ : P₁ ≃ᵃ[k] P₂)
(e₂ : P₃ ≃ᵃ[k] P₄)
:
@[simp]
theorem
AffineEquiv.prodCongr_symm
{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]
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[AddCommGroup V₄]
[Module k V₁]
[Module k V₂]
[Module k V₃]
[Module k V₄]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
[AddTorsor V₃ P₃]
[AddTorsor V₄ P₄]
(e₁ : P₁ ≃ᵃ[k] P₂)
(e₂ : P₃ ≃ᵃ[k] P₄)
:
@[simp]
theorem
AffineEquiv.prodCongr_apply
{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]
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[AddCommGroup V₄]
[Module k V₁]
[Module k V₂]
[Module k V₃]
[Module k V₄]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
[AddTorsor V₃ P₃]
[AddTorsor V₄ P₄]
(e₁ : P₁ ≃ᵃ[k] P₂)
(e₂ : P₃ ≃ᵃ[k] P₄)
(p : P₁ × P₃)
:
(e₁.prodCongr e₂) p = (e₁ p.1, e₂ p.2)
@[simp]
theorem
AffineEquiv.coe_prodCongr
{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]
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[AddCommGroup V₄]
[Module k V₁]
[Module k V₂]
[Module k V₃]
[Module k V₄]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
[AddTorsor V₃ P₃]
[AddTorsor V₄ P₄]
(e₁ : P₁ ≃ᵃ[k] P₂)
(e₂ : P₃ ≃ᵃ[k] P₄)
:
def
AffineEquiv.prodComm
(k : Type u_1)
(P₁ : Type u_2)
(P₂ : Type u_3)
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
:
Product of affine spaces is commutative up to affine isomorphism.
Instances For
@[simp]
theorem
AffineEquiv.linear_prodComm
(k : Type u_1)
(P₁ : Type u_2)
(P₂ : Type u_3)
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
:
(prodComm k P₁ P₂).linear = LinearEquiv.prodComm k V₁ V₂
@[simp]
theorem
AffineEquiv.prodComm_apply
(k : Type u_1)
(P₁ : Type u_2)
(P₂ : Type u_3)
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
(a✝ : P₁ × P₂)
:
(prodComm k P₁ P₂) a✝ = a✝.swap
@[simp]
def
AffineEquiv.prodAssoc
(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]
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[Module k V₁]
[Module k V₂]
[Module k V₃]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
[AddTorsor V₃ P₃]
:
Product of affine spaces is associative up to affine isomorphism.
Instances For
@[simp]
theorem
AffineEquiv.prodAssoc_symm_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]
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[Module k V₁]
[Module k V₂]
[Module k V₃]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
[AddTorsor V₃ P₃]
(p : P₁ × P₂ × P₃)
:
@[simp]
theorem
AffineEquiv.linear_prodAssoc
(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]
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[Module k V₁]
[Module k V₂]
[Module k V₃]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
[AddTorsor V₃ P₃]
:
(prodAssoc k P₁ P₂ P₃).linear = LinearEquiv.prodAssoc k V₁ V₂ V₃
@[simp]
theorem
AffineEquiv.prodAssoc_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]
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[Module k V₁]
[Module k V₂]
[Module k V₃]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
[AddTorsor V₃ P₃]
(p : (P₁ × P₂) × P₃)
:
(prodAssoc k P₁ P₂ P₃) p = (p.1.1, p.1.2, p.2)
def
AffineEquiv.vaddConst
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor 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.
Instances For
@[simp]
theorem
AffineEquiv.vaddConst_apply
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
(b : P₁)
(v : V₁)
:
@[simp]
theorem
AffineEquiv.linear_vaddConst
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
(b : P₁)
:
(vaddConst k b).linear = LinearEquiv.refl k V₁
@[simp]
def
AffineEquiv.constVSub
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
(p : P₁)
:
p' ↦ p -ᵥ p' as an equivalence.
Instances For
@[simp]
theorem
AffineEquiv.coe_constVSub
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
(p : P₁)
:
@[simp]
def
AffineEquiv.constVAdd
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor 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 AffineMap.constVAdd as it is always an equivalence.
This is roughly to DistribMulAction.toLinearEquiv as +ᵥ is to •.
Instances For
@[simp]
theorem
AffineEquiv.constVAdd_apply
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
(v : V₁)
(x✝ : P₁)
:
@[simp]
theorem
AffineEquiv.linear_constVAdd
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
(v : V₁)
:
(constVAdd k P₁ v).linear = LinearEquiv.refl k V₁
@[simp]
theorem
AffineEquiv.constVAdd_zero
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
:
@[simp]
@[simp]
def
AffineEquiv.constVAddHom
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
:
A more bundled version of AffineEquiv.constVAdd.
Instances For
@[simp]
theorem
AffineEquiv.constVAddHom_apply
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
(v : Multiplicative V₁)
:
(constVAddHom k P₁) v = constVAdd k P₁ (Multiplicative.toAdd v)
theorem
AffineEquiv.constVAdd_nsmul
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
(n : ℕ)
(v : V₁)
:
theorem
AffineEquiv.constVAdd_zsmul
(k : Type u_1)
(P₁ : Type u_2)
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
(z : ℤ)
(v : V₁)
:
def
AffineEquiv.homothetyUnitsMulHom
{R : Type u_10}
{V : Type u_11}
{P : Type u_12}
[CommRing R]
[AddCommGroup V]
[Module R V]
[AddTorsor 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.
Instances For
@[simp]
theorem
AffineEquiv.coe_homothetyUnitsMulHom_apply
{R : Type u_10}
{V : Type u_11}
{P : Type u_12}
[CommRing R]
[AddCommGroup V]
[Module R V]
[AddTorsor V P]
(p : P)
(t : Rˣ)
:
⇑((homothetyUnitsMulHom p) t) = ⇑(AffineMap.homothety p ↑t)
@[simp]
theorem
AffineEquiv.coe_homothetyUnitsMulHom_apply_symm
{R : Type u_10}
{V : Type u_11}
{P : Type u_12}
[CommRing R]
[AddCommGroup V]
[Module R V]
[AddTorsor V P]
(p : P)
(t : Rˣ)
:
⇑((homothetyUnitsMulHom p) t).symm = ⇑(AffineMap.homothety p ↑t⁻¹)
@[simp]
theorem
AffineEquiv.coe_homothetyUnitsMulHom_eq_homothetyHom_coe
{R : Type u_10}
{V : Type u_11}
{P : Type u_12}
[CommRing R]
[AddCommGroup V]
[Module R V]
[AddTorsor V P]
(p : P)
:
toAffineMap ∘ ⇑(homothetyUnitsMulHom p) = ⇑(AffineMap.homothetyHom p) ∘ Units.val
def
AffineEquiv.pointReflection
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
(x : P₁)
:
Point reflection in x as a permutation.
Instances For
@[simp]
theorem
AffineEquiv.pointReflection_apply_eq_equivPointReflection_apply
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
(x y : P₁)
:
(pointReflection k x) y = (Equiv.pointReflection x) y
theorem
AffineEquiv.pointReflection_apply
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
(x y : P₁)
:
(pointReflection k x) y = (x -ᵥ y) +ᵥ x
@[simp]
theorem
AffineEquiv.pointReflection_symm
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
(x : P₁)
:
(pointReflection k x).symm = pointReflection k x
@[simp]
theorem
AffineEquiv.toEquiv_pointReflection
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
(x : P₁)
:
(pointReflection k x).toEquiv = Equiv.pointReflection x
theorem
AffineEquiv.pointReflection_self
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
(x : P₁)
:
(pointReflection k x) x = x
theorem
AffineEquiv.pointReflection_involutive
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
(x : P₁)
:
theorem
AffineEquiv.pointReflection_fixed_iff_of_injective_two_nsmul
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
{x y : P₁}
(h : Function.Injective fun (x : V₁) => 2 • x)
:
(pointReflection k x) y = y ↔ y = x
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.
theorem
AffineEquiv.injective_pointReflection_left_of_injective_two_nsmul
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
(h : Function.Injective fun (x : V₁) => 2 • x)
(y : P₁)
:
Function.Injective fun (x : P₁) => (pointReflection k x) y
theorem
AffineEquiv.injective_pointReflection_left_of_module
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
[Invertible 2]
(y : P₁)
:
Function.Injective fun (x : P₁) => (pointReflection k x) y
theorem
AffineEquiv.pointReflection_fixed_iff_of_module
(k : Type u_1)
{P₁ : Type u_2}
{V₁ : Type u_6}
[Ring k]
[AddCommGroup V₁]
[Module k V₁]
[AddTorsor V₁ P₁]
[Invertible 2]
{x y : P₁}
:
(pointReflection k x) y = y ↔ y = x
def
LinearEquiv.toAffineEquiv
{k : Type u_1}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
(e : V₁ ≃ₗ[k] V₂)
:
Interpret a linear equivalence between modules as an affine equivalence.
Instances For
@[simp]
theorem
LinearEquiv.coe_toAffineEquiv
{k : Type u_1}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
(e : V₁ ≃ₗ[k] V₂)
:
⇑e.toAffineEquiv = ⇑e
def
AffineEquiv.ofLinearEquiv
{k : Type u_10}
{V : Type u_11}
{P : Type u_12}
[Ring k]
[AddCommGroup V]
[Module k V]
[AddTorsor V P]
(A : V ≃ₗ[k] V)
(p₀ p₁ : P)
:
Construct an affine equivalence from a linear equivalence and two base points.
Given a linear equivalence A : V ≃ₗ[k] V and base points p₀ p₁ : P, this constructs
the affine equivalence T x = A (x -ᵥ p₀) +ᵥ p₁. This is the standard way to convert
a linear automorphism into an affine automorphism with specified base point mapping.
Instances For
@[simp]
theorem
AffineEquiv.ofLinearEquiv_apply
{k : Type u_10}
{V : Type u_11}
{P : Type u_12}
[Ring k]
[AddCommGroup V]
[Module k V]
[AddTorsor V P]
(A : V ≃ₗ[k] V)
(p₀ p₁ x : P)
:
(ofLinearEquiv A p₀ p₁) x = A (x -ᵥ p₀) +ᵥ p₁
@[simp]
theorem
AffineEquiv.linear_ofLinearEquiv
{k : Type u_10}
{V : Type u_11}
{P : Type u_12}
[Ring k]
[AddCommGroup V]
[Module k V]
[AddTorsor V P]
(A : V ≃ₗ[k] V)
(p₀ p₁ : P)
:
(ofLinearEquiv A p₀ p₁).linear = A
@[simp]
theorem
AffineEquiv.ofLinearEquiv_refl
{k : Type u_10}
{V : Type u_11}
{P : Type u_12}
[Ring k]
[AddCommGroup V]
[Module k V]
[AddTorsor V P]
(p : P)
:
ofLinearEquiv (LinearEquiv.refl k V) p p = refl k P
@[simp]
theorem
AffineEquiv.ofLinearEquiv_trans_ofLinearEquiv
{k : Type u_10}
{V : Type u_11}
{P : Type u_12}
[Ring k]
[AddCommGroup V]
[Module k V]
[AddTorsor V P]
(A B : V ≃ₗ[k] V)
(p₀ p₁ p₂ : P)
:
(ofLinearEquiv A p₀ p₁).trans (ofLinearEquiv B p₁ p₂) = ofLinearEquiv (A ≪≫ₗ B) p₀ p₂
def
AffineEquiv.arrowCongrEquiv
{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]
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[AddCommGroup V₄]
[Module k V₁]
[Module k V₂]
[Module k V₃]
[Module k V₄]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
[AddTorsor V₃ P₃]
[AddTorsor V₄ P₄]
(e₁ : P₁ ≃ᵃ[k] P₂)
(e₂ : P₃ ≃ᵃ[k] P₄)
:
Affine isomorphisms between the domains and codomains of two spaces of affine maps give a bijection between the two function spaces.
See AffineEquiv.arrowCongr and AffineEquiv.arrowCongrₗ for the affine and linear versions of
this bijection.
Instances For
@[simp]
theorem
AffineEquiv.arrowCongrEquiv_apply
{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]
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[AddCommGroup V₄]
[Module k V₁]
[Module k V₂]
[Module k V₃]
[Module k V₄]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
[AddTorsor V₃ P₃]
[AddTorsor V₄ P₄]
(e₁ : P₁ ≃ᵃ[k] P₂)
(e₂ : P₃ ≃ᵃ[k] P₄)
(f : P₁ →ᵃ[k] P₃)
(x : P₂)
:
((e₁.arrowCongrEquiv e₂) f) x = e₂ (f (e₁.symm x))
@[simp]
theorem
AffineEquiv.arrowCongrEquiv_symm_apply
{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]
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[AddCommGroup V₄]
[Module k V₁]
[Module k V₂]
[Module k V₃]
[Module k V₄]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
[AddTorsor V₃ P₃]
[AddTorsor V₄ P₄]
(e₁ : P₁ ≃ᵃ[k] P₂)
(e₂ : P₃ ≃ᵃ[k] P₄)
(f : P₂ →ᵃ[k] P₄)
(x : P₁)
:
((e₁.arrowCongrEquiv e₂).symm f) x = e₂.symm (f (e₁ x))
def
AffineEquiv.arrowCongrₗ
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
{V₃ : Type u_8}
{V₄ : Type u_9}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[AddCommGroup V₄]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
{R : Type u_10}
[CommRing R]
[Module R V₁]
[Module R V₂]
[Module R V₃]
[Module R V₄]
(e₁ : P₁ ≃ᵃ[R] P₂)
(e₂ : V₃ ≃ₗ[R] V₄)
:
An affine isomorphism between the domains and a linear isomorphism between the codomains of two spaces of affine maps give a linear isomorphism between the two function spaces.
See also AffineEquiv.arrowCongrEquiv and AffineEquiv.arrowCongr.
Instances For
@[simp]
theorem
AffineEquiv.arrowCongrₗ_apply
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
{V₃ : Type u_8}
{V₄ : Type u_9}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[AddCommGroup V₄]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
{R : Type u_10}
[CommRing R]
[Module R V₁]
[Module R V₂]
[Module R V₃]
[Module R V₄]
(e₁ : P₁ ≃ᵃ[R] P₂)
(e₂ : V₃ ≃ₗ[R] V₄)
(f : P₁ →ᵃ[R] V₃)
(x : P₂)
:
((e₁.arrowCongrₗ e₂) f) x = e₂ (f (e₁.symm x))
@[simp]
theorem
AffineEquiv.arrowCongrₗ_symm_apply
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
{V₃ : Type u_8}
{V₄ : Type u_9}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[AddCommGroup V₄]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
{R : Type u_10}
[CommRing R]
[Module R V₁]
[Module R V₂]
[Module R V₃]
[Module R V₄]
(e₁ : P₁ ≃ᵃ[R] P₂)
(e₂ : V₃ ≃ₗ[R] V₄)
(f : P₂ →ᵃ[R] V₄)
(x : P₁)
:
((e₁.arrowCongrₗ e₂).symm f) x = e₂.symm (f (e₁ x))
def
AffineEquiv.arrowCongr
{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}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[AddCommGroup V₄]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
[AddTorsor V₃ P₃]
[AddTorsor V₄ P₄]
{R : Type u_10}
[CommRing R]
[Module R V₁]
[Module R V₂]
[Module R V₃]
[Module R V₄]
(e₁ : P₁ ≃ᵃ[R] P₂)
(e₂ : P₃ ≃ᵃ[R] P₄)
:
Affine isomorphisms between the domains and codomains of two spaces of affine maps give an affine isomorphism between the two function spaces.
See also AffineEquiv.arrowCongrEquiv and AffineEquiv.arrowCongrₗ.
Instances For
@[simp]
theorem
AffineEquiv.linear_arrowCongr
{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}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[AddCommGroup V₄]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
[AddTorsor V₃ P₃]
[AddTorsor V₄ P₄]
{R : Type u_10}
[CommRing R]
[Module R V₁]
[Module R V₂]
[Module R V₃]
[Module R V₄]
(e₁ : P₁ ≃ᵃ[R] P₂)
(e₂ : P₃ ≃ᵃ[R] P₄)
:
(e₁.arrowCongr e₂).linear = e₁.arrowCongrₗ e₂.linear
@[simp]
theorem
AffineEquiv.arrowCongr_apply
{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}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[AddCommGroup V₄]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
[AddTorsor V₃ P₃]
[AddTorsor V₄ P₄]
{R : Type u_10}
[CommRing R]
[Module R V₁]
[Module R V₂]
[Module R V₃]
[Module R V₄]
(e₁ : P₁ ≃ᵃ[R] P₂)
(e₂ : P₃ ≃ᵃ[R] P₄)
(f : P₁ →ᵃ[R] P₃)
(x : P₂)
:
((e₁.arrowCongr e₂) f) x = e₂ (f (e₁.symm x))
@[simp]
theorem
AffineEquiv.arrowCongr_symm_apply
{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}
[AddCommGroup V₁]
[AddCommGroup V₂]
[AddCommGroup V₃]
[AddCommGroup V₄]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
[AddTorsor V₃ P₃]
[AddTorsor V₄ P₄]
{R : Type u_10}
[CommRing R]
[Module R V₁]
[Module R V₂]
[Module R V₃]
[Module R V₄]
(e₁ : P₁ ≃ᵃ[R] P₂)
(e₂ : P₃ ≃ᵃ[R] P₄)
(f : P₂ →ᵃ[R] P₄)
(x : P₁)
:
((e₁.arrowCongr e₂).symm f) x = e₂.symm (f (e₁ x))
def
AffineEquiv.congrLeftₗ
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
(R : Type u_10)
(W : Type u_11)
[Ring R]
[AddCommGroup W]
[Module k W]
[Module R W]
[SMulCommClass k R W]
(e : P₁ ≃ᵃ[k] P₂)
:
An affine isomorphism between the domains of affine spaces induces a linear isomorphism over another ring between the two function spaces.
Instances For
@[simp]
theorem
AffineEquiv.congrLeftₗ_apply
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
(R : Type u_10)
(W : Type u_11)
[Ring R]
[AddCommGroup W]
[Module k W]
[Module R W]
[SMulCommClass k R W]
(e : P₁ ≃ᵃ[k] P₂)
(f : P₁ →ᵃ[k] W)
(x : P₂)
:
((congrLeftₗ R W e) f) x = f (e.symm x)
@[simp]
theorem
AffineEquiv.congrLeftₗ_symm_apply
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
(R : Type u_10)
(W : Type u_11)
[Ring R]
[AddCommGroup W]
[Module k W]
[Module R W]
[SMulCommClass k R W]
(e : P₁ ≃ᵃ[k] P₂)
(f : P₂ →ᵃ[k] W)
(x : P₁)
:
((congrLeftₗ R W e).symm f) x = f (e x)
def
AffineEquiv.congrLeft
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
(R : Type u_10)
{W : Type u_11}
[Ring R]
[AddCommGroup W]
[Module k W]
[Module R W]
[SMulCommClass k R W]
(e : P₁ ≃ᵃ[k] P₂)
(Q : Type u_12)
[AddTorsor W Q]
:
An affine isomorphism between the domains of affine spaces induces an affine isomorphism over another ring between the two function spaces.
Instances For
@[simp]
theorem
AffineEquiv.congrLeft_apply
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
(R : Type u_10)
{W : Type u_11}
[Ring R]
[AddCommGroup W]
[Module k W]
[Module R W]
[SMulCommClass k R W]
(e : P₁ ≃ᵃ[k] P₂)
(Q : Type u_12)
[AddTorsor W Q]
(f : P₁ →ᵃ[k] Q)
(x : P₂)
:
@[simp]
theorem
AffineEquiv.congrLeft_symm_apply
{k : Type u_1}
{P₁ : Type u_2}
{P₂ : Type u_3}
{V₁ : Type u_6}
{V₂ : Type u_7}
[Ring k]
[AddCommGroup V₁]
[AddCommGroup V₂]
[Module k V₁]
[Module k V₂]
[AddTorsor V₁ P₁]
[AddTorsor V₂ P₂]
(R : Type u_10)
{W : Type u_11}
[Ring R]
[AddCommGroup W]
[Module k W]
[Module R W]
[SMulCommClass k R W]
(e : P₁ ≃ᵃ[k] P₂)
(Q : Type u_12)
[AddTorsor W Q]
(f : P₂ →ᵃ[k] Q)
(x : P₁)
:
theorem
AffineMap.homothety_neg_one_apply
{P₁ : Type u_2}
{V₁ : Type u_6}
[AddCommGroup V₁]
[AddTorsor V₁ P₁]
{R' : Type u_10}
[CommRing R']
[Module R' V₁]
(c p : P₁)
:
(homothety c (-1)) p = (AffineEquiv.pointReflection R' c) p