oneofvalts

general recent conversations

$TeX - LaTeX$ TeX, LaTeX and Friends

\begin{chat}

oneofvalts

Jun 14 18:07

The book itself: unimath.github.io/SymmetryBook/book.pdf

oneofvalts

Jun 14 18:07

I like the look of this book: github.com/UniMath/SymmetryBook the source is there

oneofvalts

Jun 14 17:56

Hmm, \symit{f} works.

oneofvalts

Jun 14 17:48

\documentclass{memoir}

\usepackage{unicode-math}

\setmainfont{EB Garamond}
\setmathfont{Garamond-Math.otf}
\setmathfont[range="1D453]{Asana Math}

\begin{document}
\( \text{graph} (f) \).
\end{document}

oneofvalts

Jun 14 17:45

Let me post an mwe

oneofvalts

Jun 14 17:45

Hey, I am trying to get a single character, in fact mathematical small italic f, but why does this not work? \setmathfont[range="1D453]{Asana Math} ?

oneofvalts

May 20 11:51

@DavidCarlisle Ah yes, that way I don't have to calculate the decrement in the indentation every time, and I can have any number of diagonal lines. Now it's hardcoded to 6.

oneofvalts

May 20 11:48

(Not related to what you wrote, I was talking to myself)

oneofvalts

May 20 11:48

Or better still, I can set the diagonal line width dynamically with 1.4142\marginparwidth

oneofvalts

May 20 11:40

Thanks for the suggestions @David and @Skillmon. I think I achieved what I imagined with this:
\documentclass[10pt, a4paper, oneside]{memoir}

\usepackage{graphicx}
\usepackage{lipsum}

\usepackage[pass, showframe]{geometry}

\begin{document}
\marginpar{
\rotatebox{45}{%
\hspace{-60pt}
\begin{minipage}{1cm}
\parshape=6
60pt 89.0954pt
48pt 89.0954pt
36pt 89.0954pt
24pt 89.0954pt
12pt 89.0954pt
0pt 89.0954pt
\noindent
Lorem ipsum dolor sit amet, consectetur adipiscing elit. Sed do
eiusmod tempor incididunt ut labore et

oneofvalts

May 19 18:38

Hey, I searched on the site but apparently this is fairly esoteric that I could not found anything close. How can I typeset diagonal lines like in this image kislakcenter.github.io/islamicmss/assets/prose-layout.png

♦ $Mathematics$ Logic

This room is meant for discussion about logic, including found...

oneofvalts

Sep 9, 2024 18:13

So, while I will continue to formalize the framework in Lean, I want to investigate the pure logical side of this topic. The question that comes to my mind is "Where to go from here?"

As I am a very beginner in logic research and research in general, I wonder: Whould it be interesting to determine the minimal order system that expresses this framework layed out in the book?

oneofvalts

Sep 9, 2024 16:52

@user21820 I also didn't know this, and it is now very good to know.

oneofvalts

Sep 9, 2024 16:50

@user21820 You are right, and it is shame that I confused one with the other.

oneofvalts

Sep 7, 2024 16:40

Anyways, those are details, and I think it boils down to the following: The book's main desire is to create a framework around morphisms, and since there is no mention of the details of the foundational system, the foundationzl system was a secondary thing, just a tool to realize that framework and that type of expressing things in projective geometry.

oneofvalts

Sep 7, 2024 16:28

oneofvalts

Sep 7, 2024 16:27

And here I use Exists.choose_spec to access again the property the element satisfies: github.com/oneofvalts/desargues/blob/main/Basic.lean#L741

oneofvalts

Sep 7, 2024 16:26

Here: github.com/oneofvalts/desargues/blob/main/Basic.lean#L731

oneofvalts

Sep 7, 2024 16:24

Continuing on the book's foundational base... I don't know why I was unsure! In the proof of a theorem about central projection, I think the book freely uses ZFC in the background, specifically axiom of choice, since I had to use Exists.choose which extracts the element from an existential proposition.

oneofvalts

Sep 7, 2024 16:15

@user21820 And with this message, I realize my aim was not well-defined, but I didn't know it was not well-defined. Although, I formalized in Lean theorem prover fair bit of introductory properties and structures, and I now realize this has the problem that I didn't exactly know what I formalized. What I formalized seems to rely on ZFC.

oneofvalts

Sep 7, 2024 16:10

@user21820 I think I now realize the problem. I don't remember a careful specification of the foundational base in the book, so I presume the book chooses a position fairly closer to a working mathematician's one rather than a logician's. In that case, it seems plausible to me that the author implicitly presumed ZFC.

oneofvalts

Sep 4, 2024 11:00

@user21820 That's pretty much my organization. And to recapitulate, I think the additional theorems you asked reside in the definitions of "irreducible", "arguesian" and "morphism".

oneofvalts

Sep 4, 2024 10:57

oneofvalts

Sep 4, 2024 10:57

The axioms are given with musical notation which are defined as follows.

oneofvalts

Sep 4, 2024 10:57

oneofvalts

Sep 4, 2024 10:57

oneofvalts

Sep 4, 2024 10:57

And a homomorphism is a morphism plus two axioms:

oneofvalts

Sep 4, 2024 10:56

Being a subspace embedding is being a homomorphism with empty kernel.

oneofvalts

Sep 4, 2024 10:51

oneofvalts

Sep 4, 2024 10:51

So the goal is to determine all the dependencies of the following essential theorem.

oneofvalts

Sep 4, 2024 10:49

oneofvalts

Sep 4, 2024 10:48

The final theorem is 8.4.4, that is, "Projectivization is arguesian".

oneofvalts

Sep 4, 2024 10:47

oneofvalts

Sep 4, 2024 10:47

If you are familiar with org-roam-ui, that schema is visualized as follows.

oneofvalts

Sep 4, 2024 10:45

For my project, I am creating this schema of dependencies of the final theorem: github.com/oneofvalts/desargues-schema

oneofvalts

Sep 4, 2024 10:32

oneofvalts

Sep 4, 2024 10:32

oneofvalts

Sep 4, 2024 10:32

And an endomorphism is simply a morphism from $G$ to $G$. Their definition is as follows.

oneofvalts

Sep 4, 2024 10:28

oneofvalts

Sep 4, 2024 10:28

Now, for the third specialization, there is being "arguesian", and it is as follows.

oneofvalts

Sep 4, 2024 10:25

oneofvalts

Sep 4, 2024 10:25

As an example, it gives the projectivisation of a vector space.

oneofvalts

Sep 4, 2024 10:22

oneofvalts

Sep 4, 2024 10:20

For this, I will ask if the following helps us classify them accordingly.

oneofvalts

Sep 4, 2024 10:06

Let me start by acknowledging that L_1-L_3 should be called weak projective plane.

oneofvalts

Sep 4, 2024 10:05

I have been thinking about how I can organize my findings and understanding to effectively communicate them.

oneofvalts

Aug 31, 2024 17:18

Hey @user21820, I don't know I you remember me but we once talked abuot Desargues's theorem. Then it ended abrubtly, because there has been a misunderstanding by my side, but I want to state that my intention was not bad. If you are willing to continue to discuss, I have some news from my study.

$Mathematics$ Mathematics

Associated with Math.SE; for both general discussion & math qu...

oneofvalts

May 5, 2024 15:15

And hoping to get something from $h_1^{-1} n_2 h_2 \in N$.

oneofvalts

May 5, 2024 15:14

I was trying the path $h_1^{-1} n_1 h_1 = h_1^{-1} n_2 h_2$...

oneofvalts

May 5, 2024 15:13

I actually have been looking at it for a few hours (:facepalms:), but I focused to much on $N$ being normal, I think.

oneofvalts

TeX, LaTeX and Friends

♦ Logic

Mathematics

$TeX - LaTeX$ TeX, LaTeX and Friends

♦ $Mathematics$ Logic

$Mathematics$ Mathematics