## Stream: new members

### Topic: Collinear set

#### Maxime Darrin (Jun 01 2021 at 19:55):

Hi !
I'm trying to write the property \forall x, collinear {x, f(x)} -> f is an homothy but I did not manage to define the set {x, f(x)}
For the moment I have: (∀ x : E, collinear {x, f x} )-> ∃ c : E, ∃ s : R, (affine_map.homothety c s) = f
What should I do ?
Thanks !

#backticks

#### Heather Macbeth (Jun 01 2021 at 20:09):

It's useful to provide a #mwe so we can see what the variable names are supposed to represent. Anyway, I tried to guess; is this what you want to say?

import linear_algebra.affine_space.finite_dimensional

open_locale affine

variables (k : Type*) {V : Type*} {E : Type*} [field k] [add_comm_group V] [module k V]
[affine_space V E]

variables (f : E →ᵃ[k] E)

example :
collinear k {p : E × E | p.2 = f p.1}   c : E,  s : k, (affine_map.homothety c s) = f :=
sorry

#### Adam Topaz (Jun 01 2021 at 20:14):

I suppose what was meant is more like the following?

import linear_algebra.affine_space.finite_dimensional

open_locale affine

variables (k : Type*) {V : Type*} {E : Type*} [field k] [add_comm_group V] [module k V]
[affine_space V E]

variables (f : E →ᵃ[k] E)

example :
( x, collinear k ({x, f x} : set E))   c : E,  s : k, (affine_map.homothety c s) = f :=
sorry

#### Damiano Testa (Jun 01 2021 at 20:15):

Does homotethy allow for a projection? I would not call the map R^2 --> R^2 given by (x,y) |-> (x,0) a homotethy, though I think it satisfies the collinearity condition, right?

#### Adam Topaz (Jun 01 2021 at 20:16):

Yeah homothethy means scaling by a nonzero scalar (after choosing an origin in the affine space)

#### Adam Topaz (Jun 01 2021 at 20:16):

at least that's the definition I have in mind...

#### Damiano Testa (Jun 01 2021 at 20:17):

Me too, although I was not sure about non-zero. If so, then any linear map with a nontrivial kernel might fail the statement...

#### Adam Topaz (Jun 01 2021 at 20:17):

but anyway, the example of the projection breaks this

#### Adam Topaz (Jun 01 2021 at 20:18):

if you also assume f is bijective then it should be okay

#### Damiano Testa (Jun 01 2021 at 20:22):

I wonder about Q(✓2)^2 mapping to itself via a Galois conjugation on each component. Although I am on mobile and do not have paper to write either!

#### Adam Topaz (Jun 01 2021 at 20:28):

Wait, aren't two points always colinear?

#### Adam Topaz (Jun 01 2021 at 20:28):

They are with the usual math definition

#### Adam Topaz (Jun 01 2021 at 20:30):

We even have docs#collinear_insert_singleton

#### Adam Topaz (Jun 01 2021 at 20:32):

Ah but maybe Heather's formulation is correct

#### Adam Topaz (Jun 01 2021 at 20:45):

No, if f is the identity and E has dimension at least 2, then f is clearly a homothethy but the set in Heather's code is not colinear.

#### Eric Wieser (Jun 01 2021 at 21:43):

I've not seen :check_mark:️ used as square root before. Mobile input limitations make communication weird...

#### Damiano Testa (Jun 02 2021 at 04:20):

Ah, to be honest, I had not looked at the code, I simply assumed that the question was about a function mapping collinear sets to collinear sets.

Eric, when I saw the "square root symbol", I thought "it shows that people deciding which keys are easily accessible have a maths background". :rofl: :face_palm:

#### Maxime Darrin (Jun 05 2021 at 08:28):

Thank you! and sorry for the formating I'll make sure to do it right next time

Last updated: Dec 20 2023 at 11:08 UTC