Help constructing a natural transformation

Stream: new members

[Vasily Ilin]

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]

I would avoid constructing the corepresentable term in tactic mode.

[Adam Topaz]

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]

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]

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

[Violeta Hernández]

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]

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

[Reid Barton]

And affine_scheme and affine_group_scheme should be structures

[Junyan Xu]

Note that we have docs#algebraic_geometry.is_affine