Collinear set

Stream: new members

[Maxime Darrin]

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 !

[Adam Topaz]

#backticks

[Heather Macbeth]

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]

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]

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]

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

[Adam Topaz]

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

[Damiano Testa]

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]

but anyway, the example of the projection breaks this

[Adam Topaz]

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

[Damiano Testa]

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]

Wait, aren't two points always colinear?

[Adam Topaz]

They are with the usual math definition

[Adam Topaz]

We even have docs#collinear_insert_singleton

[Adam Topaz]

Ah but maybe Heather's formulation is correct

[Adam Topaz]

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]

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

[Damiano Testa]

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]

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