OAI/GroupTheory/FiniteLattice/CanonicalQuotient.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteLattice.CommonCore.preimageMap line 11

   Source documentation

   Restrict alpha to Q and identify its image J with T.

   def preimageMap (alpha : A →* H) (Q : Subgroup A) (J : Subgroup H)
       (himage : Q.map alpha = J) (e : T ≃* J) : Q →* T where
   …

2. theorem OAI.FiniteLattice.CommonCore.preimageMap_surjective line 27
3. theorem OAI.FiniteLattice.CommonCore.preimageMap_ker_iff line 42

   Source documentation

   The kernel of the transported map consists of the elements killed by alpha.

   theorem preimageMap_ker_iff (alpha : A →* H) (Q : Subgroup A)
       (J : Subgroup H) (himage : Q.map alpha = J) (e : T ≃* J) (q : Q) :
       q ∈ (preimageMap alpha Q J himage e).ker ↔ alpha q = 1 := by
   …

   Mentions: OAI.FiniteLattice.CommonCore.preimageMap

4. def OAI.FiniteLattice.CommonCore.canonicalTheta line 59

   Source documentation

   The first isomorphism theorem identifies the quotient of Q by the kernel with T.

   noncomputable def canonicalTheta (alpha : A →* H) (Q : Subgroup A)
       (J : Subgroup H) (himage : Q.map alpha = J) (e : T ≃* J) :
       (Q ⧸ (preimageMap alpha Q J himage e).ker) ≃* T :=
   …

   Mentions: OAI.FiniteLattice.CommonCore.preimageMap

5. theorem OAI.FiniteLattice.CommonCore.canonicalTheta_mk line 65