Все ли гомоморфизмы правильны? - PullRequest
Новая
       7

Все ли гомоморфизмы правильны?

2 голосов
/ 12 января 2020

Является ли гомоморфизм между двумя группами собственными? Вот мои определения групп и гомоморфизмов: 

Definition associative {ty : Type} (f : ty -> ty -> ty) (eq : ty -> ty -> Prop) := 
  forall a b c, eq (f (f a b) c) (f a (f b c)).

Definition identity {ty : Type} (f : ty -> ty -> ty) (eq : ty -> ty -> Prop) (e : ty) :=
  forall a, eq (f a e) a /\ eq (f e a) a.

Definition op_inverse {ty : Type} (f : ty -> ty -> ty) (eq : ty -> ty -> Prop) (e a a' : ty) :=
  eq (f a a') e /\ eq (f a' a) e.

Definition op_invertible {ty : Type} (f : ty -> ty -> ty) (eq : ty -> ty -> Prop) (e : ty) :=
  forall a, exists a', op_inverse f eq e a a'.

Record Group : Type := Group'
  { ty :> Type
  ; op : ty -> ty -> ty
  ; eqr : ty -> ty -> Prop
  ; e : ty
  ; eq_rel :> Equivalence eqr
  ; prop_op :> Proper (eqr ==> eqr ==> eqr) op
  ; assoc_op : associative op eqr
  ; id_op : identity op eqr e
  ; inv_op : op_invertible op eqr e
  }.

Notation "A <.> B" := ((op _) A B) (at level 50).
Notation "A =.= B" := ((eqr _) A B) (at level 50).

Definition homomorphism {G H : Group} (f : G -> H) := 
  forall x y, f (x <.> y) =.= (f x <.> f y).

Я хочу доказать: 

Lemma homo_is_proper : forall {G H : Group} (f : ty G -> ty H),
  homomorphism f -> Proper (eqr G ==> eqr H) f.

Обязательно ли это правда?

1 Ответ

2 голосов
/ 12 января 2020

Это не так.

Пусть H будет нетривиальной группой (например, Z/2Z), определите G как частное H при общем соотношении eqr := fun _ _ => True ( Таким образом, G изоморфно c тривиальной группе), а f : ty G -> ty H - единичная функция. f удовлетворяет homomorphism, но это не правильно.

В общем, для отражения обычной математической практики при работе с сетоидами правильность является основным c фактом, который должен быть доказан из первых принципов, и что остальная часть теории опирается на. Можно утверждать, что homo_is_proper не является естественным вопросом, потому что все теоремы и свойства (такие как homomorphism) должны действительно параметризоваться только собственными функциями.

...