## Stream: maths

### Topic: category over and under

#### 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 ?

#### 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)$ ? With $A,B$ CommRing and $f$ a morphism of commutative Ring ?

f a

#### orlando (Apr 06 2020 at 09:28):

it's doesn't work !!!

#### Kenny Lau (Apr 06 2020 at 09:28):

include all the imports

#### Kenny Lau (Apr 06 2020 at 09:28):

the W in MWE is important too

#### orlando (Apr 06 2020 at 09:31):

Sorry i don't understand ? What is MWE ?

#### Kenny Lau (Apr 06 2020 at 09:32):

minimal working example

#### 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

#### 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)

#### 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)

#### 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 ?

#### Scott Morrison (Apr 06 2020 at 09:37):

missing close parenthesis on the last line?

#### Kevin Buzzard (Apr 06 2020 at 09:38):

function expected at
f
term has type
A ⟶ R

#### orlando (Apr 06 2020 at 09:38):

ok but it's not the problem

yes Kevin !

#### 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)

#### Scott Morrison (Apr 06 2020 at 09:38):

(Nevertheless, go edit the MWE now!)

#### Kevin Buzzard (Apr 06 2020 at 09:39):

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

#### 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

#### Johan Commelin (Apr 06 2020 at 09:39):

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

No...

#### 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

#### 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)

#### Scott Morrison (Apr 06 2020 at 09:41):

do the coercion on the other side?

#### 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.

#### 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)

#### 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.

#### Kenny Lau (Apr 06 2020 at 09:43):

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

Why?

#### Kenny Lau (Apr 06 2020 at 09:43):

because Lean elaborates from left to right

#### Kenny Lau (Apr 06 2020 at 09:43):

if you specify the inner type then Lean has to backtrack

#### Kenny Lau (Apr 06 2020 at 09:44):

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

#### orlando (Apr 06 2020 at 09:47):

ohhhh that work !

#### Kevin Buzzard (Apr 06 2020 at 09:47):

I think all our suggestions work :-)

#### orlando (Apr 06 2020 at 09:50):

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

#### 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.

#### 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

#### orlando (Apr 06 2020 at 13:00):

it's not minimal :upside_down:

#### Kevin Buzzard (Apr 06 2020 at 13:01):

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

I edit Kevin !

#### Johan Commelin (Apr 06 2020 at 13:02):

What happens if you Ctrl-click on unop

#### 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

#### Kevin Buzzard (Apr 06 2020 at 13:03):

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

#### 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.

#### Reid Barton (Apr 06 2020 at 13:04):

IIRC, you want f.unop for a hom

#### Reid Barton (Apr 06 2020 at 13:04):

but I probably don't

#### Kevin Buzzard (Apr 06 2020 at 13:05):

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

#### 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

#### orlando (Apr 06 2020 at 13:07):

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

#### Johan Commelin (Apr 06 2020 at 13:07):

f.unop is hom.unop f

#### Johan Commelin (Apr 06 2020 at 13:07):

Or actually category_theory.category.hom.unop f

#### 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