feat(algebraic_topology): basics on simplicial sets and singular chain complex by jcommelin · Pull Request #144 · leanprover-community/mathlib3

jcommelin · 2018-05-28T13:00:57Z

I have tried to follow the style guides. However, the proofs are probably not up to par. I have no idea how to improve them. All help appreciated.

…eneral

put simplex_category into its own file in algebraic_topology

…n complex

spl · 2018-05-28T13:05:27Z

You should check all your files for commented code that is no longer needed and remove it.

jcommelin · 2018-05-28T13:17:31Z

Well, there is some commented code, but that are short hints on how would have liked to improve the code. Maybe I could have been a bit more explicit about that...
Of course I will remove it once the code is ready for merging. But that seems unlikely atm...

johoelzl · 2018-05-28T13:44:06Z

algebraic_topology/simplex_category.lean

+
+lemma δ_monotone (i : [n+1]) : monotone (δ i) :=
+begin
+unfold monotone,


the part between begin and end is always indented by 2 spaces.

johoelzl · 2018-05-28T13:48:54Z

order/fixed_points.lean

  le_refl      := λ x, le_refl x,
  le_trans     := λ x y z, le_trans,
-  le_antisymm  := λ x y hx hy, subtype.eq $ le_antisymm hx hy,
+  le_antisymm  := λ x y hx hy, .eq $ le_antisymm hx hy,


I guess this doesn't compile?

Huh, how did that end up happening? I don't recall ever opening that file...

johoelzl · 2018-05-28T13:56:11Z

algebraic_topology/simplex_category.lean

+intros a b H,
+unfold δ,
+by_cases ha : (i.val ≤ a.val),
+{ rw [dif_pos ha],


You have a lot of by_cases and rw with if_pos or similar. You can use Gabriels new split_ifs tactic.

johoelzl · 2018-05-28T13:56:31Z

algebraic_topology/simplex_category.lean

+
+lemma σ_monotone (i : [n]) : monotone (σ i) :=
+begin
+unfold monotone,


You don't need to unfold monotone, intros will do it for you.

johoelzl · 2018-05-28T13:58:05Z

algebraic_topology/simplex_category.lean

+    have hia' : ((fin.raise i).val ≤ (fin.raise a).val) :=
+    begin
+      unfold fin.raise,
+      exact hia


Are you sure that unfold and then exact is necessary? The unfold looks unnecessary.

johoelzl · 2018-05-28T13:58:22Z

algebraic_topology/simplex_category.lean

+
+lemma simplicial_identity₁ {i j : [n+1]} (H : i ≤ j) : δ j.succ ∘ δ i = δ i.raise ∘ δ j :=
+begin
+apply funext,


funext a or ext a

Sorry, I don't understand this comment.

Instead of apply funext, intro a, ... you can use funext a, ... or ext a, ....
ext is a more general version which uses a database of extensionality theorems.

johoelzl · 2018-05-28T14:02:50Z

General comment on style:
The form for lemma and definition is:

lemma name (a : A) (b : B) : stmt :=
-- or
lemma name (a : A) (b : B) :
  stmt :=
-- or
lemma name
  (a : A)
  (b : B) :
  stmt :=
_

The : and := are at the end of the previous line. The statement is indented by 2 spaces, and when you need to add a line break for the parameters also indent them by 2 spaces.

johoelzl · 2018-05-28T14:09:34Z

For the proofs it gets harder.

I have a couple of ideas:

some of your statements might be easier to proof using an abstracted version instead of univ use a s : finset A (where A is a type). Some proofs get a lot easier.
When you have a long chain of rw A, rw B, rw C you can write it in one list rw [A, B, C] but even bettr: use the simplifer!
When you start adding rules to the simplifier it gets very powerful, but it needs guidance. One solution is to use a more declarative style. Instead of starting to just destruct your goal (using tactics like intros, unfold etc) you might tell him what you actually want. Use for example calc or have to state your intermediate steps.
Look at other proofs: e.g. topological_space.induced_comp, how are the other proofs done? Maybe you want to follow this style.

johoelzl · 2018-05-29T13:31:40Z

algebraic_topology/standard_topological_simplex.lean

+end typepown
+
+/-- The n-th standard topological simplex: Δ_n = { x ∈ ℝ^{n+1} | ∀ i, x_i ≥ 0, and ∑ x_i = 1 } -/
+definition standard_topological_simplex (n : ℕ) : set (ℝ≥0^(n+1)) :=


I added probability mass functions, you can use them instead of this construction.

A search in VScode didn't show up anything. Where did you define those?

Aah, sorry, I didn't read "I added ..." as something you did today. My bad I didn't check the latest commits.

@johoelzl I think I understand what those probability mass functions are doing. But I prefer to continue using fin n. Within this theory of simplicial sets etc, the simplex category plays quite an important role: you want to look at monotone functions fin m \to fin n. If I start using these probability mass functions, I fear losing access to those monotone functions. (Or at least their role in the theory it becomes a lot less apparent to me.)

I don't understand?! You still use fin n: you would use pmf (fin (n + 1)) to define standard_topological_simplex n. Then you use pmf.map to map your vertices.

Ok, then I didn't understand pmf correctly. Let me see again.

…implicial

rwbarton · 2018-06-01T13:29:10Z

analysis/topology/topological_space.lean

 ⟨assume ⟨t, ht, heq⟩, ⟨-t, by simp; assumption, by simp [preimage_compl, heq.symm]⟩,
  assume ⟨t, ht, heq⟩, ⟨-t, ht, by simp [preimage_compl, heq.symm]⟩⟩

+lemma induced_comp {α β γ : Type*} (f : α → β) (g : β → γ) :


Isn't this already induced_compose, up to minor details?

I guess it is. And in fact, I don't need this lemma anymore. So I will remove it. Thanks for spotting this!

kbuzzard · 2018-06-09T18:39:08Z

algebra/group.lean

+-- instance ring_hom_is_add_group_hom [ring α] [ring β] (f : α → β) [is_ring_hom f] : is_add_group_hom f :=
+-- ⟨λ _ _, is_ring_hom.map_add f⟩
+
+theorem zero {α β : Type*} [add_group α] [add_group β] (f : α → β) [hf : is_add_group_hom f] :


Should this be a simp lemma?

This can't be a simp lemma as the head of the left-hand side is just f which is a variable. The simplifier cannot work with such cases.

spl · 2018-06-19T12:31:36Z

analysis/topology/continuity.lean

 continuous_supr_rng $ assume i, continuous_induced_rng $ h i

-lemma continuous_apply [topological_space α] [∀i, topological_space (π i)] (i : ι) :
+lemma continuous_apply [∀i, topological_space (π i)] (i : ι) :


This was fixed in fba4d89 (#157). Can you rebase or merge in master?

rwbarton · 2018-09-30T11:55:07Z

Now that categories are in mathlib, we could consider splitting up this construction into smaller pieces, namely:

The simplex category, and simplicial sets as a category of presheaves.
The "standard topological simplices" as a functor from the simplex category to Top.
Using the previous item, obtain the Sing functor from Top to simplicial sets by a standard construction ("restricted Yoneda embedding"), though maybe it would be more natural to do it when we can also define the left adjoint (geometric realization) at the same time, using colimits.
If modules are in a good state, define the category of R-modules. If not yet, just define the category of abelian groups for now.
Define the "free R-module" (or "free abelian group") functor and apply it to Sing X to get the simplicial R-module of chains on X. (If/when we have adjunctions, prove that the free R-module functor is left adjoint to the forgetful functor.)
Define chain complexes (in R-modules for now, or abelian groups), the unnormalized chain complex functor from simplicial modules to chain complexes of modules, and the homology functors on chain complexes.

At least the first two items could be done right now, and none of the items are far from being doable in some version (depending on the status of modules and (co)limits).

PatrickMassot · 2018-09-30T19:47:32Z

This all sounds very nice. I think we should wait for the module refactor and some progress in the category theory PR, and then try to make one big push. This would be a really nice test for all those new features.

johoelzl · 2019-01-11T16:32:21Z

@jcommelin is it OK to close this PR?

jcommelin · 2019-01-12T12:22:03Z

Yes. Let's close this for now. I hope to return to it in the future!

jcommelin added 14 commits May 16, 2018 21:29

Put raise_fin in fin namespace; simp lemmas for fin

ea42f7d

Remove function

ace0a45

Merge branch 'simplicial' into fin

5f29649

A small start on simplicial sets

63f76eb

Face maps are continuous

fec9db2

More stuff on simplices

623f2e5

style(analysis/nnreal): move to correct directory; improve style in g…

840ef2d

…eneral

refactor: create directory algebraic_topology

95bb099

put simplex_category into its own file in algebraic_topology

feat(algebraic_topology): define the basics; some stuff is still broken

b3fdd15

Small steps

149e86b

The simplicial complex is a complex

7dd90bc

Removed final sorry, thanks to Patrick Massot

06469f0

feat(algebraic_topology): basics on simplicial sets and singular chai…

fda931f

…n complex

Merge upstream:master into feature branch

3fd7fae

johoelzl reviewed May 28, 2018

View reviewed changes

jcommelin added 4 commits May 28, 2018 16:32

Revert weird change

41480d3

cleanup of proofs; add condition on id to simplicial set

49a3ad3

Use results from continuity.lean, instead of rolling own

7e9c51f

Cleanup induced_comp in topological_space.lean

1855bd5

johoelzl reviewed May 29, 2018

View reviewed changes

Merge branch 'master' into simplicial

2ee8a07

jcommelin added 4 commits May 30, 2018 11:04

Use pmf for topological simplices

da1194e

Merge branch 'master' of https://github.com/leanprover/mathlib into s…

5b7f119

…implicial

Prove continuity with pmf

9214647

Break long lines

206608f

rwbarton reviewed Jun 1, 2018

View reviewed changes

Remove unnecessary lemma

fc34f8f

kbuzzard reviewed Jun 9, 2018

View reviewed changes

spl reviewed Jun 19, 2018

View reviewed changes

Merge branch 'master' into simplicial

ece70f3

johoelzl added the maybe-later label Aug 27, 2018

johoelzl closed this Jan 13, 2019

Conversation

jcommelin commented May 28, 2018

Uh oh!

spl commented May 28, 2018

Uh oh!

jcommelin commented May 28, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

johoelzl commented May 28, 2018

Uh oh!

johoelzl commented May 28, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jcommelin Jun 1, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

rwbarton commented Sep 30, 2018

Uh oh!

PatrickMassot commented Sep 30, 2018

Uh oh!

johoelzl commented Jan 11, 2019

Uh oh!

jcommelin commented Jan 12, 2019

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

jcommelin commented May 28, 2018 •

edited

Loading

jcommelin Jun 1, 2018 •

edited

Loading