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,
my friend 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.
On the one hand, Grothendieck proudly describes his extension of the Riemann–Roch Theorem as a highly non-trivial and famous result whose proof requires hundreds of pages. On the other hand, he despises it, or (institutional) mathematics in general. The reason is that he believed that the wars at that time and environmental destruction were much more important and urgent topics. In fact, one reason for Grothendieck leaving the IHES were their military fundings.
For more details, I highly recommend to read a biography of Grothendieck. The short article Who is Grothendieck by W. Scharlau is a good start.
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)