Zulip Chat Archive

Stream: maths

Topic: category over and under


view this post on Zulip orlando (Apr 06 2020 at 08:37):

Hello,

A little question :

structure truc (R : Ring)(S : set R)(hyp : (1 : R)  ideal.span S) :=
(arrow : { f : under R |  s  S,  (f.hom) (1 : R) = (1 : f.left) })   --- stupid condition but don't work  :(
---- hum : f.hom  : R ⟶ A for some A true ?
---  How i can evaluate f.hom ?

view this post on Zulip orlando (Apr 06 2020 at 09:27):

In fact the problem is : if i have f : A ⟶ B and a : A , how can i evaluate f(a) f ( a) ? With A,BA,B CommRing and ff a morphism of commutative Ring ?

view this post on Zulip Kenny Lau (Apr 06 2020 at 09:27):

f a

view this post on Zulip orlando (Apr 06 2020 at 09:28):

it's doesn't work !!!

view this post on Zulip Kenny Lau (Apr 06 2020 at 09:28):

include all the imports

view this post on Zulip Kenny Lau (Apr 06 2020 at 09:28):

the W in MWE is important too

view this post on Zulip orlando (Apr 06 2020 at 09:31):

Sorry i don't understand ? What is MWE ?

view this post on Zulip Kenny Lau (Apr 06 2020 at 09:32):

minimal working example

view this post on Zulip Kenny Lau (Apr 06 2020 at 09:32):

it would be easier for us to help one if one posts MWEs instead of code snippets that can't be copied directly

view this post on Zulip Scott Morrison (Apr 06 2020 at 09:36):

(i.e. copy and paste your code into a new file, make sure it compiles with the error you expect, and that there is nothing in the file besides what is required to demonstrate the behaviour you want help with)

view this post on Zulip Scott Morrison (Apr 06 2020 at 09:36):

(sometimes it's onerous to do this; on the other hand at least half the time I set out to do this, attempting to construct the MWE reveals for me what the problem is)

view this post on Zulip orlando (Apr 06 2020 at 09:37):

Sorry !!! For example !

 import algebra.category.CommRing
structure truc (R :CommRing) :=
(A : CommRing)
(f : A  R)
(certif : f (1:A) = (1 : R))   --- problem ?

view this post on Zulip Scott Morrison (Apr 06 2020 at 09:37):

missing close parenthesis on the last line?

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 09:38):

function expected at
  f
term has type
  A ⟶ R

view this post on Zulip orlando (Apr 06 2020 at 09:38):

ok but it's not the problem

view this post on Zulip orlando (Apr 06 2020 at 09:38):

yes Kevin !

view this post on Zulip Scott Morrison (Apr 06 2020 at 09:38):

(It also helps if you include the text of the error message in the comment in the MWE, so people don't have to copy and paste themselves)

view this post on Zulip Scott Morrison (Apr 06 2020 at 09:38):

(Nevertheless, go edit the MWE now!)

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 09:39):

It would be nice to just be able to say "@lean_bot print_errors".

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 09:39):

import algebra.category.CommRing
structure truc (R :CommRing) :=
(A : CommRing)
(f : A  R)
(certif : (f : A  R) 1 = 1)

works

view this post on Zulip Johan Commelin (Apr 06 2020 at 09:39):

Does it help if you change CommRing to CommRing.{0}? (In both places.)

view this post on Zulip Scott Morrison (Apr 06 2020 at 09:40):

No...

view this post on Zulip Kenny Lau (Apr 06 2020 at 09:40):

Kenny Lau said:

it would be easier for us to help one if one posts MWEs instead of code snippets that can't be copied directly

and the proof is that immediately two people joined the discussion

view this post on Zulip Scott Morrison (Apr 06 2020 at 09:41):

import algebra.category.CommRing
structure truc (R : CommRing.{0}) :=
(A : CommRing.{0})
(f : A  R)
(certif : (f (1:A) : R) = 1)

view this post on Zulip Scott Morrison (Apr 06 2020 at 09:41):

do the coercion on the other side?

view this post on Zulip Scott Morrison (Apr 06 2020 at 09:42):

I think the problem is that when you write f (1 : A), Lean doesn't yet know the expected type of the whole term, so it can't find the coercion for f yet.

view this post on Zulip Kenny Lau (Apr 06 2020 at 09:42):

import algebra.category.CommRing

universes u

structure truc (R : CommRing.{u}) : Type (u+1) :=
(A : CommRing.{u})
(f : A  R)
(certif : (f 1 : R) = 1)

view this post on Zulip Johan Commelin (Apr 06 2020 at 09:43):

Scott Morrison said:

I think the problem is that when you write f (1 : A), Lean doesn't yet know the expected type of the whole term, so it can't find the coercion for f yet.

Note that this is because Lean 3 has a coercion system that isn't very smart. Lean 4 should make all of this look stupid.

view this post on Zulip Kenny Lau (Apr 06 2020 at 09:43):

specifying the type of the outer term is better than the inner term

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 09:43):

Why?

view this post on Zulip Kenny Lau (Apr 06 2020 at 09:43):

because Lean elaborates from left to right

view this post on Zulip Kenny Lau (Apr 06 2020 at 09:43):

if you specify the inner type then Lean has to backtrack

view this post on Zulip Kenny Lau (Apr 06 2020 at 09:44):

and of course, people who know what they're talking about can confirm/deny my speculations

view this post on Zulip orlando (Apr 06 2020 at 09:47):

ohhhh that work !

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 09:47):

I think all our suggestions work :-)

view this post on Zulip orlando (Apr 06 2020 at 09:50):

I don't tell you, how many time a spent with this problem :sweat_smile:

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 09:55):

Well I hope you learn from the MWE suggestion because it makes questions much easier to answer. I ignored your question initially precisely because it didn't compile.

view this post on Zulip orlando (Apr 06 2020 at 13:00):

Hello,

Another triviality problem !

My MWE :grinning_face_with_smiling_eyes:

Is there a unop for morphism ?

import category_theory.comma
import data.opposite
import algebra.category.CommRing
universe u
namespace category_theory
local notation `Ring` := CommRing.{u}
local notation `Set` :=  Type u



open category_theory
open opposite
lemma test (Aop Bop  : Ringᵒᵖ ) (f : Aop  Bop) (a b : unop Bop) : f (a * b) = f (a) * f(b) := begin
exact f.map_mul a b,    -- don't work ?
end
lemma test1 (A B : Ring)(f : B  A) (a b: B) : f(a*b) = f(a) * f(b) := begin
exact f.map_mul a b,   -- work !
 end
end category_theory

view this post on Zulip orlando (Apr 06 2020 at 13:00):

it's not minimal :upside_down:

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 13:01):

The main thing is that it works. end category_theory ;-)

view this post on Zulip orlando (Apr 06 2020 at 13:02):

I edit Kevin !

view this post on Zulip Johan Commelin (Apr 06 2020 at 13:02):

What happens if you Ctrl-click on unop

view this post on Zulip Johan Commelin (Apr 06 2020 at 13:02):

It will take you to a different file, and most likely somewhere nearby you will find unop for homs

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 13:03):

it's nothing to do with categories, where we end up :-(

view this post on Zulip Reid Barton (Apr 06 2020 at 13:04):

Right because opposite for categories was merged with something else. I still don't think it was necessarily a good idea.

view this post on Zulip Reid Barton (Apr 06 2020 at 13:04):

IIRC, you want f.unop for a hom

view this post on Zulip Reid Barton (Apr 06 2020 at 13:04):

but I probably don't

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 13:05):

confirmed: exact f.unop.map_mul a b, works

view this post on Zulip Reid Barton (Apr 06 2020 at 13:05):

I actually wonder whether we could get rid of the op/unop for homs. It doesn't seem as important as the one for objects

view this post on Zulip orlando (Apr 06 2020 at 13:07):

Ok f.unop i try unop f f^\unop :+1:

view this post on Zulip Johan Commelin (Apr 06 2020 at 13:07):

f.unop is hom.unop f

view this post on Zulip Johan Commelin (Apr 06 2020 at 13:07):

Or actually category_theory.category.hom.unop f

view this post on Zulip orlando (Apr 06 2020 at 13:16):

Ok i understand Johan, in fact there is two files opposite !

  1. in data/ opposite
  2. in category_theory/ opposites

And i just see the first :frown:


Last updated: May 14 2021 at 19:21 UTC