category over and under

Stream: maths

[orlando]

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]

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 ?

[Kenny Lau]

f a

[orlando]

it's doesn't work !!!

[Kenny Lau]

include all the imports

[Kenny Lau]

the W in MWE is important too

[orlando]

Sorry i don't understand ? What is MWE ?

[Kenny Lau]

minimal working example

[Kenny Lau]

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]

(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]

(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]

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]

missing close parenthesis on the last line?

[Kevin Buzzard]

function expected at
  f
term has type
  A ⟶ R

[orlando]

ok but it's not the problem

[orlando]

yes Kevin !

[Scott Morrison]

(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]

(Nevertheless, go edit the MWE now!)

[Kevin Buzzard]

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

[Kevin Buzzard]

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

works

[Johan Commelin]

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

[Scott Morrison]

No...

[Kenny Lau]

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]

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

[Scott Morrison]

do the coercion on the other side?

[Scott Morrison]

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]

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]

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]

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

[Kevin Buzzard]

Why?

[Kenny Lau]

because Lean elaborates from left to right

[Kenny Lau]

if you specify the inner type then Lean has to backtrack

[Kenny Lau]

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

[orlando]

ohhhh that work !

[Kevin Buzzard]

I think all our suggestions work :-)

[orlando]

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

[Kevin Buzzard]

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]

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]

it's not minimal :upside_down:

[Kevin Buzzard]

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

[orlando]

I edit Kevin !

[Johan Commelin]

What happens if you Ctrl-click on unop

[Johan Commelin]

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

[Kevin Buzzard]

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

[Reid Barton]

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

[Reid Barton]

IIRC, you want f.unop for a hom

[Reid Barton]

but I probably don't

[Kevin Buzzard]

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

[Reid Barton]

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]

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

[Johan Commelin]

f.unop is hom.unop f

[Johan Commelin]

Or actually category_theory.category.hom.unop f

[orlando]

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: