I'm a mathematician from México.
For a long time I've had the intention of mantaining a blog but
I wanted to be able to update it both from my computer locally
and also from my phone.
If neocities works as I expect it to, making a
personal website here should be ok. I write in my computer and
push to
my github
where I created a workflow using
Liassica's instructions
.
Update (26 aug): in order to satisfy my need of editing this
website from my phone, Ernesto made me aware that github has a
mobile app. After testing it, I found that github's editor is
bad, but at least it is usable. Good.
The initial content of this site (18 and 19 August 2024) is a mixture of stuff I've been carrying throughout my life since approximately 2016, using the sticky notes app from windows 7 and later the Indicator stickynotes in Ubuntu, a variety of .txt files, my telegram chat with myself, a blog hosted in Blogger and another one in Wordpress. After all this time, yesterday I finally decided I would organize it all in a coherent (or at least centralized) way.
Sometimes I write in English and others on Spanish. If I get confidence with my Deutsch, I might even use it as well.
type * a; // declaración de un apuntador de tipo "type" type * a = &b; // declaración con asignación, donde b : type a = &c; // reasignación, donde c : type type & a = b; // declaración de una referencia que apunta a lo mismo que b : type *a // es el valor guardado en la dirección a &b // es la dirección del objeto b
-- import the definition of the category of modules over a ring import algebra.category.Module.basic -- let R be a commutative ring variables {R : Type} [comm_ring R] /-- dual_obj M is Hom(M,R). -/ def dual_obj (M : Module R) : Module R := Module.of R (M →ₗ[R] R) /-- If f : M → N is R-linear then dual_mor f : dual_obj N → dual_obj M is the obvious thing. -/ def dual_mor {M N : Module R} (f : M ⟶ N) : dual_obj N ⟶ dual_obj M := { to_fun := λ φ, { to_fun := λ m, φ.to_fun (f m), map_add' := λ x y, by simp, map_smul' := λ r x, by simp }, map_add' := λ φ ψ, by {ext, simp }, map_smul' := λ r φ, by {ext, simp } }. -- dual of identity is identity @[simp] lemma dual_mor_id {M : Module R} : dual_mor (𝟙 M) = 𝟙 _ := begin ext φ m, refl, end -- dual of composite is composite of duals @[simp] lemma dual_mor_comp {M N P : Module R} (f : M ⟶ N) (g : N ⟶ P) : dual_mor (f ≫ g) = dual_mor g ≫ dual_mor f := begin refl, end /-- Double dual functor, sending M to dual_obj (dual_obj M). -/ def double_dual : Module R ⥤ Module R := { obj := λ M, dual_obj (dual_obj M), map := λ M N f, dual_mor (dual_mor f), map_id' := by {intros, ext, simp}, map_comp' := by {intros, ext, simp } }. /-- If r : R then the map sending m : M to (the map sending φ to r * φ(m)) is a natural transformation. -/ def i_am_canonical (r : R) : (𝟭 (Module R) : Module R ⥤ Module R) ⟶ (double_dual : Module R ⥤ Module R) := { app := λ M, { to_fun := λ m, { to_fun := λ φ, r * φ.to_fun m, map_add' := by {intros, simp [mul_add], }, map_smul' := by {intros, simp [mul_left_comm], } }, map_add' := by {intros, ext, simp [mul_add], }, map_smul' := by {intros, ext, simp [mul_left_comm], } }, naturality' := by {intros, ext, simp, refl } }
\ / o\ / \ / o \ / \/(footer by Sami)