I'm a mathematician from México.
I've been meaning to have a blog which I can update from my
computer locally. 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): Ernesto suggested the possibility of also editing the website from my phone using github, which was the only disadvantage of migrating to the neocities+github workflow I could think of. After testing a bit here and there, I found that github's editor is not very good, but at least it works and is reliable. 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)