## Stream: new members

### Topic: Help constructing a natural transformation

#### Vasily Ilin (May 20 2022 at 00:07):

I have state

K: Type u_1
_inst_1: comm_ring K
⊢ coyoneda.obj (opposite.op (Algebra.of K K[X])) ⟶ forget (Algebra K)


in my proof. What should my next line be? I tried

hom :=
{ app := sorry,
naturality' := sorry,
},


but getting invalid 'begin-end' expression, ',' expected.
Here is the full code:

-- https://leanprover-community.github.io/mathlib_docs/category_theory/functor/hom.html
-- THE PLAN IS TO DEFINE AN AFFINE GROUP SCHEME AS A REPRESENTABLE FUNCTOR FROM K-ALGEBRAS TO GROUPS, AND PROVE THAT G_a := Hom(K[X], _) IS AN AFFINE GROUP SCHEME

import category_theory.types
import algebra.category.Algebra.basic
import algebra.category.Group.basic
import data.polynomial.basic
import data.polynomial.algebra_map
import category_theory.over
import tactic

open_locale polynomial
open polynomial
open category_theory

variables (K : Type*) [comm_ring K]
-- variables (K_alg : Type*) [category K_alg] [category_theory.under K] -- category of commutative K-algebras. But how to use it...

class affine_scheme :=
(scheme : Algebra K ⥤ Type*)
(corepresentable : scheme.corepresentable)

class affine_group_scheme :=
(scheme : Algebra K ⥤ Group)
(corepresentable : (scheme ⋙ forget Group).corepresentable)

-- DEFINING G_a
instance G_a : affine_scheme K :=
{
scheme := forget (Algebra K),
corepresentable := begin
refine {has_corepresentation := _},
refine ⟨opposite.op (Algebra.of K K[X]), _⟩, -- ∃ (f : coyoneda.obj (opposite.op (Algebra.of K K[X])) ⟶ forget (Algebra K)), is_iso f
refine exists.intro _ _,
hom :=
{ app := sorry,
naturality' := sorry,
},
-- need to contruct a natural tranformation Hom(K[X], _) ⟶ forget (Algebra K)
-- see for an example of defining a natural transformation https://leanprover-community.github.io/mathlib_docs/category_theory/yoneda.html#category_theory.yoneda_lemma
end,
}


#### Adam Topaz (May 20 2022 at 00:15):

I would avoid constructing the corepresentable term in tactic mode.

#### Adam Topaz (May 20 2022 at 00:19):

Also, I think you're misunderstanding what typeclasses are for. Certainly defining G_a : affine_scheme K makes no sense if you want $\mathbb{G_a}$.

#### Adam Topaz (May 20 2022 at 00:25):

But if you ignore those issues, here is something to get you started

instance G_a : affine_scheme K :=
{
scheme := forget (Algebra K),
corepresentable := begin
refine {has_corepresentation := _},
refine ⟨opposite.op (Algebra.of K K[X]), _⟩, -- ∃ (f : coyoneda.obj (opposite.op (Algebra.of K K[X])) ⟶ forget (Algebra K)), is_iso f
refine exists.intro _ _,
refine ⟨_,_⟩,
{ intros A, dsimp, intros f,
exact f X },
{ tidy },
{ apply_with nat_iso.is_iso_of_is_iso_app { instances := ff },
intros A, rw is_iso_iff_bijective,
sorry
}
end,
}


#### Violeta Hernández (May 20 2022 at 00:28):

The solution here is to make G_a a def instead of an instance

#### Violeta Hernández (May 20 2022 at 00:30):

An instance is some theorem or construction that you want to always make available on some type. For instance, there is an instance field ℝ that builds a field structure on ℝ, which you have available every time some theorem calls for a field.

#### Violeta Hernández (May 20 2022 at 00:30):

Here, you just want to build some specific object, nothing canonical. So you should have a def instead.

#### Reid Barton (May 20 2022 at 02:26):

And affine_scheme and affine_group_scheme should be structures

#### Junyan Xu (May 20 2022 at 03:14):

Note that we have docs#algebraic_geometry.is_affine

Last updated: Dec 20 2023 at 11:08 UTC